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

Changelog updates

. Updating nomnolith sub-option.
parent 845f9aa0
No related branches found
No related tags found
No related merge requests found
......@@ -12,7 +12,7 @@ The high level changelog is available at http://research.microsoft.com/en-us/um/
* 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, 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`
* To prevent the monolith inclusion of dependent TLA code, specify `nomonolith` after the `-generateSpecTE`
* 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)
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Please register or to comment