using:tlc:config_file

This page is read only. You can view the source, but not change it. Ask your administrator if you think this is wrong.
====== 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.

At the bare minimum a ''%%SPECIFICATION%%'' should be provided.


===== Supported Sections =====

==== SPECIFICATION ====

The name of the predicate that usually has the form of: ''%%Init /\ [][Next]_vars /\backslash%%''.

Usually per convention it’s called ''%%Spec%%''.

<code>
SPECIFICATION
    Spec
</code>

==== Constants or Constant (they’re aliases) ====

You can use it to specify the constant used in the model.

<code>
CONSTANTS
    Processes = {1,2,3}
</code>

Equivalent to:

<code>
CONSTANT
    Processes = {1,2,3}
</code>

==== INVARIANT or INVARIANTS (they’re aliases) ====

Invariants that you want to verify.

<code>
INVARIANT
    TypeOk \* Always verify your types!
</code>

==== PROPERTIES or PROPERTY (they’re aliases) ====

Temporal properties you want to verify.

<code>
PROPERTIES
    Termination
</code>

==== CONSTRAINT or CONSTRAINTS (they’re aliases) ====

Used to restrict the state space to be explored. Helps restricting unbounded models.

==== SYMMETRY ====

Helps reducing the state space to explore by removing symmetric states. You can’t check liveness properties when symmetry is used. See: https:%%//%%federicoponzi.github.io/tlaplus-wiki/codebase/wishlist.html#liveness-checking-under-symmetry-difficulty-high-skills-java-tla

==== VIEW ====

==== CHECK_DEADLOCK ====

==== POSTCONDITION ====

==== ALIAS ====

==== INIT ====

==== NEXT ====

===== A copy-pastable example: =====

<code>
SPECIFICATION Spec

CONSTANTS
    Nodes = 3

INVARIANT
    TypeOK

PROPERTIES
    Termination

\* Check presence of deadlocks. This is true by default.
CHECK_DEADLOCK 
    FALSE
</code>

===== Resources =====

Check the EBNF and more info on the apalache documentation [[https://apalache.informal.systems/docs/apalache/tlc-config.html|here]].