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 toz3
(viaz3
's parameterssat.random_seed
andsmt.random_seed
). -
Timeouts:
search.smt.timeout=<seconds>
defines the timeout to the SMT solver in seconds. The default value is0
, 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 theafter
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 thebefore
mode. In thebefore
mode, the invariant is checked for every enabled transition independently. Thebefore
mode may drastically reduce memory consumption, but it may take longer than theafter
mode, provided that Apalache has enough memory. The default mode isbefore
. -
Guided search:
search.transitionFilter=<regex>
. Restrict the choice of symbolic transitions at every step with a regular expression. The regular expression should recognize words over of the form 's->t', wheres
is a regular expression over step numbers andt
is a regular expression over transition numbers. 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 thelength.
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 calledNext_si_0000
, 1st transition is calledNext_si_0001
, etc. -
Invariant checking at certain steps:
search.invariantFilter=regex
. Check the invariant only at the steps that satisfy the regular expression. For instance,search.invariantFilter=10|15|20
tells the model checker to check the invariant only after exactly 10, 15, or 20 step were made. Step 0 corresponds to the initialization withInit
, step 1 is the first step withNext
, etc. This option is useful 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. -
Translation to SMT:
- Short circuiting:
rewriter.shortCircuit=(false|true)
. Whenrewriter.shortCircuit=true
,A \/ B
andA /\ 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
.
- Short circuiting: