Problem

TLC does not handle variable-level expressions in liveness properties such as Live below:

---- MODULE PCal ----
CONSTANT Producer
ASSUME(IsFiniteSet(Producer))
...
variable P \in SUBSET Producer;
define {
   Live == \A p \in P: []<>(SomeAction(p)_vars)
}
process (p \in P) {
   ...
}

\* TLA+ translation

CONSTANT Producer
...

VARIABLE P
...

Init == P \in SUBSET Producer
...

Live == \A p \in P: []<>(SomeAction(p)_vars)
====

At startup, TLC eagerly processes the liveness properties and creates the tableau for the liveness formulas. For example, the universal quantifier above leads to a conjunct for each element of P. Obviously, this doesn't work if P is a variable whose value is unknown at startup.

In the (special) case above, the conjuncts could potentially be amended with conditionals that are evaluated when the value of the variable P is known. However, P could have any value, and, thus, we would have to handle new runtime errors in addition to paying a performance penalty.

In the Wild

• Polish and extend tutorial lemmy/BlockingQueue#5 (comment) (Better tooling can be considered to be the root cause of this issue)
• The various script in the artifact of the RenamingProof are an example where this feature would be useful. However, this feature is probably best implemented at the TLC level to address the CLI use case.

Workaround A:

LL: "The ideal way would be for the user to specify in TLC's cfg file that a constant Succ be turned into a variable initialized to an arbitrary element of S, where S is an identifier defined to equal a constant. Implementing that is not trivial."

An approach would be to switch from EXTEND in the MC.tla file to INSTANCE with a re-definition of the CONSTANTS. TLC would then have to traverse the semantic graph to patch the const node with a variable node. Level-checking, especially related to liveness, might not like this idea. It is unclear how this would work with symmetry sets. The second workaround below doesn't have this kind of problem.

Assuming a plain, high-level spec H, it is impractical to check refinement if a lower-level spec L introduces "constant variables" to check various subsets of H's constants; H's properties will likely be violated:

---- MODULE H ----
CONSTANT C
...
====

---- MODULE L ----
CONSTANT C
VARIALBES c

Init ==
  c \in SUBSET C

H = INSTANCE H

THEOREM Spec => H!Spec
====

Related: Apalache's constant initializer is similar. See also apalache-mc/apalache#79

Workaround B:

Run TLC multiple times/once for each configuration:

LL: "I was doing something by hand that should be mechanized. I'm writing a spec of an algorithm in which Succ is a CONSTANT parameter. I wanted to test the algorithm for all values of Succ in some set S. The only way to do that is to make Succ a variable that is left unchanged by the next-state relation. It would be nice if I didn't have to do that manually. It seems like too much work to do it properly. But I wonder if there is some kludgy way to tell the Toolbox to create a new file with the necessary transformation that will work most of the time."

The kludge proposed by LL above would require running multiple instances of TLC in parallel, which makes #378 a prerequisite. This idea has essentially been implemented at the TLC and not the Toolbox level with #577 (comment) and #577 (comment).

TODO:

lemmy/BlockingQueue@f3075bf shows how sets of constant values can be checked.

Eventually, a more high-level operator TLCExt!TLCCheck should be defined (implemented by a Java module override) that runs TLC in the current JVM. The IOExec would become:

LET Args=="-workers auto -noTE"
    Config== [Invariants|->{"Inv1", "Inv2"}, Constants|-> [Data|->Data, N|->42], Spec |-> "Spec"] 
IN TLCCheck(Config, Args, "/path/to/spec.tla")

whereas TLCCheck is defined as:

TLCCheck(Config, Args, Spec) ==
   [Trace |-> TRACE, Statistics |-> TLCGet("stats"), Config |-> TLCGet("config"), ...]