Parameters for fine tuning

The parameters for fine tuning can be passed to the checker in a properties file. Its name is given with the command-line option --tuning-options-file=my.properties. This file supports variable substitution, e.g., ${x} is replaced with the value of x, if it was previously declared.

Alternatively, you can pass the tuning options right in the command-line by passing the option --tuning-options that has the following format:

```
--tuning-options=key1=val1
--tuning-options=key1=val1:key2=val2
...
```

The following options are supported:

Randomization

smt.randomSeed=<int> passes the random seed to z3 (via z3's parameters sat.random_seed and smt.random_seed).

Timeouts

search.smt.timeout=<seconds> defines the timeout to the SMT solver in seconds. The default value is 0, which stands for the unbounded timeout. For instance, the timeout is used in the following cases: checking if a transition is enabled, checking an invariant, checking for deadlocks. If the solver times out, it reports 'UNKNOWN', and the model checker reports a runtime error.

Invariant mode

search.invariant.mode=(before|after) defines the moment when the invariant is checked. In the after mode, all transitions are first translated, one of them is picked non-deterministically and then the invariant is checked. Although this mode reduces the number of SMT queries, it usually requires more memory than the before mode. In the before mode, the invariant is checked for every enabled transition independently. The before mode may drastically reduce memory consumption, but it may take longer than the after mode, provided that Apalache has enough memory. The default mode is before.

Guided search

Preliminaries

In the following, step 0 corresponds to the initialization with Init, step 1 is the first step with Next, etc.

Transition filter

search.transitionFilter=<regex>. Restrict the choice of symbolic transitions at every step with a regular expression. The regular expression should recognize words of the form s->t, where s is a step number and t is a transition number.

For instance, search.transitionFilter=(0->0|1->5|2->(2|3)|[3-9]->.*|[1-9][0-9]+->.*) requires to start with the 0th transition, continue with the 5th transition, then execute either the 2nd or the 3rd transition and after that execute arbitrary transitions until the length.

Note that there is no direct correspondence between the transition numbers and the actions in the TLA+ spec. To find the numbers, run Apalache with --write-intermediate=true and check the transition numbers in _apalache-out/<MySpec>.tla/*/intermediate/XX_OutTransitionFinderPass.tla: the 0th transition is called Next_si_0000, the 1st transition is called Next_si_0001, etc.

Invariant filter

search.invariantFilter=<regex>. Check the invariant only at the steps that satisfy the regular expression. The regular expression should recognize words of the form s->ki, where s is a step number, k is an invariant kind ("state" or "action"), and i is an invariant number.

For instance, search.invariantFilter=10->.*|15->state0|20->action1 tells the model checker to check

  • all invariants only after exactly 10 steps have been made,
  • the first state invariant only after exactly 15 steps, and
  • the second action invariant after exactly 20 steps.

Trace invariants are checked regardless of this filter.

Note that there is no direct correspondence between invariant numbers and the operators in a TLA+ spec. Rather, the numbers refer to verification conditions (i.e., broken up parts of a TLA+ invariant operator). To find these numbers, run Apalache with --write-intermediate=true and check the invariant numbers in _apalache-out/<MySpec>.tla/*/intermediate/XX_OutVCGen.tla. The 0th state invariant is called VCInv_si_0, the 1st state invariant is called VCInv_si_1, and so on. For action invariants, the declarations are named VCActionInv_si_0, VCActionInv_si_1 etc.

This option is useful, e.g., for checking consensus algorithms, where the decision cannot be revoked. So instead of checking the invariant after each step, we can do that after the algorithm has made a good number of steps. You can also use this option to check different parts of an invariant on different machines to speed up turnaround time.

Translation to SMT

Short circuiting

rewriter.shortCircuit=(false|true). When rewriter.shortCircuit=true, A \/ B and A /\ B are translated to SMT as if-then-else expressions, e.g., (ite A true B). Otherwise, disjunctions and conjunctions are directly translated to (or ...) and (and ...) respectively. By default, rewriter.shortCircuit=false.