TLA+ Anonymized Execution Statistics

Apalache participates in the optional anonymized statistics programme along with TLA+ Toolbox, TLC (which is part of the Toolbox), and Visual Studio Code Plugin for TLA+.

The statistics collection is never enabled by default. You have to opt-in for the programme either in TLA+ Toolbox, or in Apalache. When statistics collection is enabled by the user, it is submitted to tlapl.us via the util.ExecutionStatisticsCollector, which is part of tla2tools.jar. Apalache accesses this class in at.forsyte.apalache.tla.Tool.

As explained in anonymized statistics programme, if you never create the file $HOME/.tlaplus/esc.txt, then the statistics is not submitted to tlapl.us. If you opt-in for the programme and later remove the file, then the statistics will not be submitted too.

Why do we ask you to help us

There are several reasons:

  • Although our project is open source, developing Apalache is our main job. We are grateful to Informal Systems for supporting us and to TU Wien, Vienna Science and Technology Fund, and Inria Nancy/LORIA, who supported us in the past. It is easier to convince our decision makers to continue the development, if we have clear feedback on how many people use and need Apalache.

  • We would like to know which features you are using most, so we can focus on them.

  • We would like to know which operating systems and Java versions need care and better be included in automated test suites.

How to opt-in and opt-out

To opt-in in the statistics collection, execute the following command:

./apalache-mc config --enable-stats=true

As a result of this command, a random identifier is written in $HOME/.tlaplus/esc.txt. This identifier is used by the execution statistics code.

To opt-out from the statistics collection, execute the following command:

./apalache-mc config --enable-stats=false

What exactly is submitted to tlapl.us

You can check the daily log at exec-stats.tlapl.us.

The following data is submitted for each run, if you have opted in:

  • Total number of CPU cores and cores assigned (the latter is 1 for now, but will change soon)
  • Java heap memory size (in Megabytes)
  • Apalache version (semantic version + build)
  • Command mode: parse, check, or typecheck
  • Name, version, and architecture of the OS
  • Vendor, version, and architecture of JVM
  • Timestamp + salt (a random number to make time less precise)
  • An installation ID that is stored in $HOME/.tlaplus/esc.txt