Skip to content
Permalink
Browse files

Add markdown variant of execution statistics dialog.

The [TLA+ vscode extension](https://github.com/alygin/vscode-tlaplus)
will e.g. link to this file.

[Feature][TLC]
  • Loading branch information
lemmy committed Dec 1, 2019
1 parent e25ead4 commit 93eb3be081f5b041981becb870f17106f4747768
@@ -141,6 +141,7 @@ protected Control createCustomArea(Composite parent) {
c.setLayout(new GridLayout());
c.setLayoutData(new GridData(SWT.FILL, SWT.FILL, true, true));

//NOTE: Take care of ExecutionStatisticsCollector.md when updating!!!
final String txt = String.format("%s"
+ "* Total number of cores and cores assigned to TLC\n"
+ "* Heap and off-heap memory allocated to TLC\n"
@@ -0,0 +1,14 @@
You can help make the TLA+ tools better by allowing TLC to collect execution statistics. Execution statistics are made [publicly available](https://exec-stats.tlapl.us) on the web and contain the following information:

* Total number of cores and cores assigned to TLC
* Heap and off-heap memory allocated to TLC
* TLC version (git commit SHA)
* If breadth-first search, depth-first search or simulation mode is active
* TLC implemenation for the sets of seen and unseen states
* If TLC has been launched from an IDE
* Name, version, and architecture of the OS
* Vendor, version, and architecture of JVM
* The current date and time
* An installation ID which allows to group execution statistic (optionally)

Execution statistics do not contain personal information. You can opt-out any time.

0 comments on commit 93eb3be

Please sign in to comment.
You can’t perform that action at this time.