The TLA Toolbox is an IDE (integrated development environment) for the TLA+ tools.
You can use it to:
Create and edit your specs, with the locations of parsing errors marked in the modules.
Run the PlusCal translator, with the locations of translation errors marked in the PlusCal code.
View the pretty-printed versions of your modules.
Run the TLC model checker. You do this by creating one or more models, which specify the
information TLC needs to check the spec: what the spec is, what properties to check, the values
to substitute for constant parameters, etc. Among the features the Toolbox provides is an error
trace viewer and explorer that allows you to:
Explore a structured view of the states.
See exactly what parts of the state are changed in each step.
Evaluate arbitrary state and action formulas at each step in the trace.
Run TLAPS, the TLA+ proof system.
Details for tlaplus
License
MIT
Last updated
17 May 2017 - latest/stable
17 May 2017 - latest/candidate
This snap hasn't been updated in a while. It might be unmaintained and have stability or security issues.
(Ownership verified)
The publisher has verified that they own this domain.
It does not guarantee the Snap is an official upload
from the upstream project.
Snaps are applications packaged with all their dependencies to run on all popular Linux distributions from a single build. They update automatically and roll back gracefully.
Snaps are discoverable and installable from the Snap Store, an app store with an audience of millions.
Enable snapd
Snap can be installed on elementary OS from the command line. Open Terminal from the Applications launcher and type the following:
sudo apt update
sudo apt install snapd
Either log out and back in again, or restart your system, to ensure snap’s paths are updated correctly.
Install tlaplus
To install tlaplus, simply use the following command: