TLX.TLC
(TLX v0.5.2)
Copy Markdown
Invokes TLC model checker as a Java subprocess using -tool mode
for structured, machine-parseable output.
Summary
Functions
Run TLC on a .tla file with a .cfg configuration.
Parse tool-mode output into a list of {code, level, body} tuples.
Parse TLC -tool mode output into structured results.
Functions
Run TLC on a .tla file with a .cfg configuration.
Returns {:ok, output} on success or {:error, reason, output} on failure.
Options:
:tla2tools— path to tla2tools.jar (default: auto-detect):workers— number of TLC worker threads (default: "auto"):deadlock— iffalse, suppress deadlock checking (default: true)
Parse tool-mode output into a list of {code, level, body} tuples.
Parse TLC -tool mode output into structured results.
Tool mode wraps each message in:
@!@!@STARTMSG <code>:<level> @!@!@
<body>
@!@!@ENDMSG <code> @!@!@