Skip to content
Snippets Groups Projects
Commit 12e81733 authored by loki der quaeler's avatar loki der quaeler
Browse files

Changelog updates

. Adding verbiage concerning no-monolith-creation, help usage, and the TraceExplorer functionality.
parent 5a2c4640
No related branches found
No related tags found
No related merge requests found
......@@ -9,19 +9,22 @@ The high level changelog is available at http://research.microsoft.com/en-us/um/
* More powerful TLC module overrides that can programmatically manipulate a successor state. bb64cfd921c2e8846f47a5818d85cd0e8f2aa2c5
* Write snapshots of state graph in dot/gv format after every new state. 305f38b1b7f68a0f4885615e7a148c3bf83aad95
* A number of additions pertaining to working with trace expressions have been added to the command line tool `tlc2.TLC` and a new peer command line tool `tlc2.TraceExplorer` - see [GitHub Issue 393](https://github.com/tlaplus/tlaplus/issues/393) for an overview and background. Salient points include:
* Running TLC with both the `-tool` and `-generateSpecTE` flags will, in the event that the model check encounters errors, generate a `SpecTE.tla` and `SpecTE.cfg` file pair that captures
* Running TLC with both the `-generateSpecTE` flag will enable 'tool mode' output and, in the event that the model check encounters errors, generate a `SpecTE.tla` and `SpecTE.cfg` file pair that captures
the state trace reconstruction in an Init-Next relation spec.
* This `SpecTE.tla` will be a monolithic file, prefaced by the tool output, followed a the `SpecTE` MODULE definition which includes all extended non-StandardModule TLA code as well.
* TraceExplorer exposes three capabilities:
* This `SpecTE.tla` will, by default, be a monolithic file, prefaced by the tool output, followed a the `SpecTE` MODULE definition which includes all extended non-StandardModule TLA code as well.
* To prevent the monolith inclusion of dependent TLA code, specify `-nomonolith`
* Running TLC with `-h` now displays a usage page reminiscent of a standard man page.
* TraceExplorer exposes four capabilities:
* running the TraceExplorer with no spec name puts the TraceExplorer into a mode to receive input via stdin (e.g in order to pipe tool-mode output from TLC)
* pretty-printing: given an existing tool-mode output from a previous model check run (or piping in such output), pretty-printing will display an output stack to the terminal in basically the same format as one would see in the Toolbox's Error Viewer
* SpecTE generation: given an existing tool-mode output from a previous model check run (or piping in such output), create a `SpecTE.tla` and `SpecTE.cfg` file pair
* SpecTE generation: given an existing tool-mode output from a previous model check run (or piping in such output), create a `SpecTE.tla` and `SpecTE.cfg` file pair - this **will not** be a monolithic version.
* Expression exploration: given an existing tool-mode output from a previous model check run (or piping in such output), and file of expressions, one per line:
* create a `SpecTE.tla` and `SpecTE.cfg` file pair if one doesn't exist
* then create a `TE.tla` and `TE.cfg` file pair which extends SpecTE and contains appropriate conjunctions featuring the expressions
* then run model checking on this TE spec, both creating a `TE.out` and dumping the tool-mode output to stdout
* then do a courtesy pretty-print of the output. Pretty-printing in this scenario will ANSI-bold the expressions and their evaluated values
* running `tlc2.TraceExplorer` with no arguments will display helpful usage verbiage
* Single expression exploration: as a sort of REPL-adjacent, any single TLA+ expression can be evaluated.
* running `tlc2.TraceExplorer` with no arguments, or `-h` will display helpful usage verbiage
#### Toolbox
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Please register or to comment