diff --git a/general/docs/changelogs/ch1_6_1.md b/general/docs/changelogs/ch1_6_1.md index 60d0be14d7292f2fa592abb57f0349450c4ea04f..e629d5af916bfed0c50db03987947bbb0f893adb 100644 --- a/general/docs/changelogs/ch1_6_1.md +++ b/general/docs/changelogs/ch1_6_1.md @@ -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