You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
TLC does not handle variable-level expressions in liveness properties such as Live below:
----MODULE PCal ----CONSTANTProducerASSUME(IsFiniteSet(Producer))...variable P \in SUBSET Producer;define{
Live ==\Ap\inP: []<>(SomeAction(p)_vars)
}process (p\inP){...}\* TLA+ translationCONSTANTProducer...VARIABLE P
...Init==P\inSUBSETProducer...Live == \Ap\inP:[]<>(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.
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:
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).
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"]INTLCCheck(Config,Args,"/path/to/spec.tla")
Could you reserve a keyword in the TLC configuration format, e.g., CINIT or CONSTINIT, so we could use a TLC config as the primary configuration format for Apalache too?
lemmy
changed the title
Better Toolbox support for model checking different CONSTANT values
Support for model checking different CONSTANT values
Jul 23, 2021
Problem
TLC does not handle variable-level expressions in liveness properties such as
Live
below: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 ifP
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
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 specL
introduces "constant variables" to check various subsets ofH
's constants;H
's properties will likely be violated:Related: Apalache's constant initializer is similar. See also informalsystems/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. TheIOExec
would become:whereas
TLCCheck
is defined as:The text was updated successfully, but these errors were encountered: