Advanced options

Status checking

The Toolbox remembers the coloring of proof steps. It can be very useful when re-opening a module to know quicky what has been already proved and what has not. However, the color used by the Toolbox to highlight a proof step reflects the step's proof status the last time TLAPS checked the proof. This status may be obsolete if you have edited the proof since then. You can check the current status of a proof step (and of all its substeps) by clicking and then right-clicking on the step (or use the ctrl+G,ctrl+T / cmd-G,cmd-T shortcut), as shown in the following screenshot:

Proving an obligation can take time, but checking its status is pretty fast. (It is not instantaneous because the obligations still have to be computed.) It's a good idea to check the proof status of the complete theorem from time to time, since changing some step could change a later proof obligation, making its previous status no longer meaningful. You can edit your file while the Toolbox is checking proof statuses. (The file is read-only while a proof is in progress.) You can instruct TLAPS to check the status of (or to prove) all theorems in the file by giving the usual command when the cursor is outside any theorem or its proof.

Prover options

If you don't use tactics, the default behaviour of TLAPS is to send obligations to Z3, then to Zenon, then to Isabelle, stopping when one of them succeeds. You can change this behavior, by clicking on "Launch Prover" when right-clicking on a proof-step:

As you can see, you can either ask TLAPS not to prove obligations (that's similar to status checking), or ask TLAPS to make Isabelle check proofs provided by Zenon.

You can also ask TLAPS to forget previous results about obligations of a particular proof-step or the entire module.

Finally, you can specify command-line options that will be added to the ones normally used by the Toolbox when it launches tlapm. The most useful options are the following:

• --threads n : change the maximum number of back-end provers that are launched in parallel. The default is the number of CPU cores on your machine.
• --method list : change the default list of back-end provers for BY and OBVIOUS steps. The argument is a comma-separated list of methods. The following methods are available:

  name	method
  zenon	Zenon
  auto	Isabelle with tactic auto
  blast	Isabelle with tactic blast
  force	Isabelle with tactic force
  smt	baseline SMT solver (by default Z3)
  z3	Z3
  cvc4	CVC4

• --solver line : change the baseline SMT solver. See Tactics for instructions on using this option.
• --fast-isabelle : on Windows, invoke Isabelle via a short-cut that saves a few seconds from Isabelle's start-up time. On other architectures, this option does nothing.
• --stretch f : multiply all timeouts by a factor of f. This is particularly useful when using a slower machine to re-check proofs made on a faster machine.