http://docs.tlapl.us/ 2026-04-30T08:29:31+00:00 http://docs.tlapl.us/ http://docs.tlapl.us/_media/logo.png text/html 2024-09-28T23:04:25+00:00 Anonymous (anonymous@undisclosed.example.com) http://docs.tlapl.us/using:tlc:config_file?rev=1727564665&do=diff Config files The config files are used for TLC model checking. The possible contents of the config file itself are presented below. The config file has .cfg extension, and usually has the same name of your spec (.tla file). TODO: values supported in config files. Typed model values. text/html 2024-09-28T15:58:38+00:00 Anonymous (anonymous@undisclosed.example.com) http://docs.tlapl.us/using:tlc:liveness?rev=1727539118&do=diff Liveness checks if TLC is configured to check three temporal formulas A,B,C; TLC does not check if A, B or C are identical formulas. If TLC is set to check A, A, A (it will still create three OrderOfSolutions). It is up to the user to prevent this. text/html 2024-09-28T23:03:23+00:00 Anonymous (anonymous@undisclosed.example.com) http://docs.tlapl.us/using:tlc:start?rev=1727564603&do=diff TLC Model Checker TLC is an explicit state model checker originally written by Yu et al. [1999] to verify TLA+ specifications. TLC can check a subset of TLA+ that is commonly needed to describe real-world systems, most notably finite systems. To run it, you will need Java runtime environment version 11. text/html 2024-09-28T15:58:37+00:00 Anonymous (anonymous@undisclosed.example.com) http://docs.tlapl.us/using:tlc:trace_validation?rev=1727539117&do=diff Trace Validation This is a comment from Markus Kuppe from Github. Trace Validation (TV) essentially adopts this approach by mapping recorded implementation states to TLA+ specification states. This method is practical as it derives implementation states directly from the execution of the implementation, avoiding the complexities of symbolic interpretation of the source code. However, TV is not exhaustive. It verifies that only a certain subset of all potential system executions aligns with the…