---
source: libtlafmt/tests/format.rs
expression: output
input_file: libtlafmt/tests/corpus/TLAPS.tla
---
--------------------------------- MODULE TLAPS ---------------------------------
(* Backend pragmas. *)
(***************************************************************************)
(* Each of these pragmas can be cited with a BY or a USE. The pragma that *)
(* is added to the context of an obligation most recently is the one whose *)
(* effects are triggered. *)
(***************************************************************************)
(***************************************************************************)
(* The following pragmas should be used only as a last resource. They are *)
(* dependent upon the particular backend provers, and are unlikely to have *)
(* any effect if the set of backend provers changes. Moreover, they are *)
(* meaningless to a reader of the proof. *)
(***************************************************************************)
(**************************************************************************)
(* Backend pragma: use the SMT solver for arithmetic. *)
(* *)
(* This method exists under this name for historical reasons. *)
(**************************************************************************)
SimpleArithmetic == TRUE (*{ by (prover:"smt3") }*)
(**************************************************************************)
(* Backend pragma: SMT solver *)
(* *)
(* This method translates the proof obligation to SMTLIB2. The supported *)
(* fragment includes first-order logic, set theory, functions and *)
(* records. *)
(* SMT calls the smt-solver with the default timeout of 5 seconds *)
(* while SMTT(n) calls the smt-solver with a timeout of n seconds. *)
(**************************************************************************)
SMT == TRUE (*{ by (prover:"smt3") }*)
SMTT(X) == TRUE (*{ by (prover:"smt3"; timeout:@) }*)
(**************************************************************************)
(* Backend pragma: CVC3 SMT solver *)
(* *)
(* CVC3 is used by default but you can also explicitly call it. *)
(**************************************************************************)
CVC3 == TRUE (*{ by (prover: "cvc33") }*)
CVC3T(X) == TRUE (*{ by (prover:"cvc33"; timeout:@) }*)
(**************************************************************************)
(* Backend pragma: Yices SMT solver *)
(* *)
(* This method translates the proof obligation to Yices native language. *)
(**************************************************************************)
Yices == TRUE (*{ by (prover: "yices3") }*)
YicesT(X) == TRUE (*{ by (prover:"yices3"; timeout:@) }*)
(**************************************************************************)
(* Backend pragma: veriT SMT solver *)
(* *)
(* This method translates the proof obligation to SMTLIB2 and calls veriT.*)
(**************************************************************************)
veriT == TRUE (*{ by (prover: "verit") }*)
veriTT(X) == TRUE (*{ by (prover:"verit"; timeout:@) }*)
(**************************************************************************)
(* Backend pragma: Z3 SMT solver *)
(* *)
(* This method translates the proof obligation to SMTLIB2 and calls Z3. *)
(**************************************************************************)
Z3 == TRUE (*{ by (prover: "z33") }*)
Z3T(X) == TRUE (*{ by (prover:"z33"; timeout:@) }*)
(**************************************************************************)
(* Backend pragma: SPASS superposition prover *)
(* *)
(* This method translates the proof obligation to the DFG format language *)
(* supported by the ATP SPASS. The translation is based on the SMT one. *)
(**************************************************************************)
Spass == TRUE (*{ by (prover: "spass") }*)
SpassT(X) == TRUE (*{ by (prover:"spass"; timeout:@) }*)
(**************************************************************************)
(* Backend pragma: The PTL propositional linear time temporal logic *)
(* prover. It currently is the LS4 backend. *)
(* *)
(* This method translates the negetation of the proof obligation to *)
(* Seperated Normal Form (TRP++ format) and checks for unsatisfiability *)
(**************************************************************************)
LS4 == TRUE (*{ by (prover: "ls4") }*)
PTL == TRUE (*{ by (prover: "ls4") }*)
(**************************************************************************)
(* Backend pragma: Zenon with different timeouts (default is 10 seconds) *)
(* *)
(**************************************************************************)
Zenon == TRUE (*{ by (prover:"zenon") }*)
ZenonT(X) == TRUE (*{ by (prover:"zenon"; timeout:@) }*)
(********************************************************************)
(* Backend pragma: Isabelle with different timeouts and tactics *)
(* (default is 30 seconds/auto) *)
(********************************************************************)
Isa == TRUE (*{ by (prover:"isabelle") }*)
IsaT(X) == TRUE (*{ by (prover:"isabelle"; timeout:@) }*)
IsaM(X) == TRUE (*{ by (prover:"isabelle"; tactic:@) }*)
IsaMT(X, Y) == TRUE (*{ by (prover:"isabelle"; tactic:@; timeout:@) }*)
(***************************************************************************)
(* The following theorem expresses the (useful implication of the) law of *)
(* set extensionality, which can be written as *)
(* *)
(* THEOREM \A S, T : (S = T) <=> (\A x : (x \in S) <=> (x \in T)) *)
(* *)
(* Theorem SetExtensionality is sometimes required by the SMT backend for *)
(* reasoning about sets. It is usually counterproductive to include *)
(* theorem SetExtensionality in a BY clause for the Zenon or Isabelle *)
(* backends. Instead, use the pragma IsaWithSetExtensionality to instruct *)
(* the Isabelle backend to use the rule of set extensionality. *)
(***************************************************************************)
IsaWithSetExtensionality == TRUE
(*{ by (prover:"isabelle"; tactic:"(auto intro: setEqualI)")}*)
THEOREM SetExtensionality == \A S,T : (\A x : x \in S <=> x \in T) => S = T
OBVIOUS
(***************************************************************************)
(* The following theorem is needed to deduce NotInSetS \notin SetS from *)
(* the definition *)
(* *)
(* NotInSetS == CHOOSE v : v \notin SetS *)
(***************************************************************************)
THEOREM NoSetContainsEverything == \A S : \E x : x \notin S
OBVIOUS (*{by (isabelle "(auto intro: inIrrefl)")}*)
--------------------------------------------------------------------------------
(********************************************************************)
(********************************************************************)
(********************************************************************)
(********************************************************************)
(* Old versions of Zenon and Isabelle pragmas below *)
(* (kept for compatibility) *)
(********************************************************************)
(**************************************************************************)
(* Backend pragma: Zenon with different timeouts (default is 10 seconds) *)
(* *)
(**************************************************************************)
SlowZenon == TRUE (*{ by (prover:"zenon"; timeout:20) }*)
SlowerZenon == TRUE (*{ by (prover:"zenon"; timeout:40) }*)
VerySlowZenon == TRUE (*{ by (prover:"zenon"; timeout:80) }*)
SlowestZenon == TRUE (*{ by (prover:"zenon"; timeout:160) }*)
(********************************************************************)
(* Backend pragma: Isabelle's automatic search ("auto") *)
(* *)
(* This pragma bypasses Zenon. It is useful in situations involving *)
(* essentially simplification and equational reasoning. *)
(* Default imeout for all isabelle tactics is 30 seconds. *)
(********************************************************************)
Auto == TRUE (*{ by (prover:"isabelle"; tactic:"auto") }*)
SlowAuto == TRUE (*{ by (prover:"isabelle"; tactic:"auto"; timeout:120) }*)
SlowerAuto == TRUE (*{ by (prover:"isabelle"; tactic:"auto"; timeout:480) }*)
SlowestAuto == TRUE (*{ by (prover:"isabelle"; tactic:"auto"; timeout:960) }*)
(********************************************************************)
(* Backend pragma: Isabelle's "force" tactic *)
(* *)
(* This pragma bypasses Zenon. It is useful in situations involving *)
(* quantifier reasoning. *)
(********************************************************************)
Force == TRUE (*{ by (prover:"isabelle"; tactic:"force") }*)
SlowForce == TRUE (*{ by (prover:"isabelle"; tactic:"force"; timeout:120) }*)
SlowerForce == TRUE (*{ by (prover:"isabelle"; tactic:"force"; timeout:480) }*)
SlowestForce == TRUE (*{ by (prover:"isabelle"; tactic:"force"; timeout:960) }*)
(***********************************************************************)
(* Backend pragma: Isabelle's "simplification" tactics *)
(* *)
(* These tactics simplify the goal before running one of the automated *)
(* tactics. They are often necessary for obligations involving record *)
(* or tuple projections. Use the SimplfyAndSolve tactic unless you're *)
(* sure you can get away with just Simplification *)
(***********************************************************************)
SimplifyAndSolve == TRUE
(*{ by (prover:"isabelle"; tactic:"clarsimp auto?") }*)
SlowSimplifyAndSolve == TRUE
(*{ by (prover:"isabelle"; tactic:"clarsimp auto?"; timeout:120) }*)
SlowerSimplifyAndSolve == TRUE
(*{ by (prover:"isabelle"; tactic:"clarsimp auto?"; timeout:480) }*)
SlowestSimplifyAndSolve == TRUE
(*{ by (prover:"isabelle"; tactic:"clarsimp auto?"; timeout:960) }*)
Simplification == TRUE (*{ by (prover:"isabelle"; tactic:"clarsimp") }*)
SlowSimplification == TRUE
(*{ by (prover:"isabelle"; tactic:"clarsimp"; timeout:120) }*)
SlowerSimplification == TRUE
(*{ by (prover:"isabelle"; tactic:"clarsimp"; timeout:480) }*)
SlowestSimplification == TRUE
(*{ by (prover:"isabelle"; tactic:"clarsimp"; timeout:960) }*)
(**************************************************************************)
(* Backend pragma: Isabelle's tableau prover ("blast") *)
(* *)
(* This pragma bypasses Zenon and uses Isabelle's built-in theorem *)
(* prover, Blast. It is almost never better than Zenon by itself, but *)
(* becomes very useful in combination with the Auto pragma above. The *)
(* AutoBlast pragma first attempts Auto and then uses Blast to prove what *)
(* Auto could not prove. (There is currently no way to use Zenon on the *)
(* results left over from Auto.) *)
(**************************************************************************)
Blast == TRUE (*{ by (prover:"isabelle"; tactic:"blast") }*)
SlowBlast == TRUE (*{ by (prover:"isabelle"; tactic:"blast"; timeout:120) }*)
SlowerBlast == TRUE (*{ by (prover:"isabelle"; tactic:"blast"; timeout:480) }*)
SlowestBlast == TRUE (*{ by (prover:"isabelle"; tactic:"blast"; timeout:960) }*)
AutoBlast == TRUE (*{ by (prover:"isabelle"; tactic:"auto, blast") }*)
(**************************************************************************)
(* Backend pragmas: multi-back-ends *)
(* *)
(* These pragmas just run a bunch of back-ends one after the other in the *)
(* hope that one will succeed. This saves time and effort for the user at *)
(* the expense of computation time. *)
(**************************************************************************)
(* CVC3 goes first because it's bundled with TLAPS, then the other SMT
solvers are unlikely to succeed if CVC3 fails, so we run zenon and
Isabelle before them. *)
AllProvers == TRUE (*{
by (prover:"cvc33")
by (prover:"zenon")
by (prover:"isabelle"; tactic:"auto")
by (prover:"spass")
by (prover:"smt3")
by (prover:"yices3")
by (prover:"verit")
by (prover:"z33")
by (prover:"isabelle"; tactic:"force")
by (prover:"isabelle"; tactic:"(auto intro: setEqualI)")
by (prover:"isabelle"; tactic:"clarsimp auto?")
by (prover:"isabelle"; tactic:"clarsimp")
by (prover:"isabelle"; tactic:"auto, blast")
}*)
AllProversT(X) == TRUE (*{
by (prover:"cvc33"; timeout:@)
by (prover:"zenon"; timeout:@)
by (prover:"isabelle"; tactic:"auto"; timeout:@)
by (prover:"spass"; timeout:@)
by (prover:"smt3"; timeout:@)
by (prover:"yices3"; timeout:@)
by (prover:"verit"; timeout:@)
by (prover:"z33"; timeout:@)
by (prover:"isabelle"; tactic:"force"; timeout:@)
by (prover:"isabelle"; tactic:"(auto intro: setEqualI)"; timeout:@)
by (prover:"isabelle"; tactic:"clarsimp auto?"; timeout:@)
by (prover:"isabelle"; tactic:"clarsimp"; timeout:@)
by (prover:"isabelle"; tactic:"auto, blast"; timeout:@)
}*)
AllSMT == TRUE (*{
by (prover:"cvc33")
by (prover:"smt3")
by (prover:"yices3")
by (prover:"verit")
by (prover:"z33")
}*)
AllSMTT(X) == TRUE (*{
by (prover:"cvc33"; timeout:@)
by (prover:"smt3"; timeout:@)
by (prover:"yices3"; timeout:@)
by (prover:"verit"; timeout:@)
by (prover:"z33"; timeout:@)
}*)
AllIsa == TRUE (*{
by (prover:"isabelle"; tactic:"auto")
by (prover:"isabelle"; tactic:"force")
by (prover:"isabelle"; tactic:"(auto intro: setEqualI)")
by (prover:"isabelle"; tactic:"clarsimp auto?")
by (prover:"isabelle"; tactic:"clarsimp")
by (prover:"isabelle"; tactic:"auto, blast")
}*)
AllIsaT(X) == TRUE (*{
by (prover:"isabelle"; tactic:"auto"; timeout:@)
by (prover:"isabelle"; tactic:"force"; timeout:@)
by (prover:"isabelle"; tactic:"(auto intro: setEqualI)"; timeout:@)
by (prover:"isabelle"; tactic:"clarsimp auto?"; timeout:@)
by (prover:"isabelle"; tactic:"clarsimp"; timeout:@)
by (prover:"isabelle"; tactic:"auto, blast"; timeout:@)
}*)
--------------------------------------------------------------------------------
(***************************************************************************)
(* TEMPORAL LOGIC *)
(* *)
(* The following rules are intended to be used when TLAPS handles temporal *)
(* logic. They will not work now. Moreover when temporal reasoning is *)
(* implemented, these rules may be changed or omitted, and additional *)
(* rules will probably be added. However, they are included mainly so *)
(* their names will be defined, preventing the use of identifiers that are *)
(* likely to produce name clashes with future versions of this module. *)
(***************************************************************************)
(***************************************************************************)
(* The following proof rules (and their names) are from the paper "The *)
(* Temporal Logic of Actions". *)
(***************************************************************************)
THEOREM RuleTLA1 == ASSUME STATE P, STATE f,
P /\ (f' = f) => P'
PROVE []P <=> P /\ [][P => P']_f
THEOREM RuleTLA2 == ASSUME STATE P, STATE Q, STATE f, STATE g,
ACTION A, ACTION B,
P /\ [A]_f => Q /\ [B]_g
PROVE []P /\ [][A]_f => []Q /\ [][B]_g
THEOREM RuleINV1 == ASSUME STATE I, STATE F, ACTION N,
I /\ [N]_F => I'
PROVE I /\ [][N]_F => []I
THEOREM RuleINV2 == ASSUME STATE I, STATE f, ACTION N
PROVE []I => ([][N]_f <=> [][N /\ I /\ I']_f)
THEOREM RuleWF1 == ASSUME STATE P, STATE Q, STATE f, ACTION N, ACTION A,
P /\ [N]_f => (P' \/ Q'),
P /\ <<N /\ A>>_f => Q',
P => ENABLED <<A>>_f
PROVE [][N]_f /\ WF_f(A) => (P ~> Q)
THEOREM RuleSF1 == ASSUME STATE P, STATE Q, STATE f,
ACTION N, ACTION A, TEMPORAL F,
P /\ [N]_f => (P' \/ Q'),
P /\ <<N /\ A>>_f => Q',
[]P /\ [][N]_f /\ []F => <> ENABLED <<A>>_f
PROVE [][N]_f /\ SF_f(A) /\ []F => (P ~> Q)
(***************************************************************************)
(* The rules WF2 and SF2 in "The Temporal Logic of Actions" are obtained *)
(* from the following two rules by the following substitutions: `. *)
(* *)
(* ___ ___ _______________ *)
(* M <- M , g <- g , EM <- ENABLED <<M>>_g .' *)
(***************************************************************************)
THEOREM RuleWF2 == ASSUME STATE P, STATE f, STATE g, STATE EM,
ACTION A, ACTION B, ACTION N, ACTION M,
TEMPORAL F,
<<N /\ B>>_f => <<M>>_g,
P /\ P' /\ <<N /\ A>>_f /\ EM => B,
P /\ EM => ENABLED A,
[][N /\ ~B]_f /\ WF_f(A) /\ []F /\ <>[]EM => <>[]P
PROVE [][N]_f /\ WF_f(A) /\ []F => []<><<M>>_g \/ []<>(~EM)
THEOREM RuleSF2 == ASSUME STATE P, STATE f, STATE g, STATE EM,
ACTION A, ACTION B, ACTION N, ACTION M,
TEMPORAL F,
<<N /\ B>>_f => <<M>>_g,
P /\ P' /\ <<N /\ A>>_f /\ EM => B,
P /\ EM => ENABLED A,
[][N /\ ~B]_f /\ SF_f(A) /\ []F /\ []<>EM => <>[]P
PROVE [][N]_f /\ SF_f(A) /\ []F => []<><<M>>_g \/ <>[](~EM)
(***************************************************************************)
(* The following rule is a special case of the general temporal logic *)
(* proof rule STL4 from the paper "The Temporal Logic of Actions". The *)
(* general rule is for arbitrary temporal formulas F and G, but it cannot *)
(* yet be handled by TLAPS. *)
(***************************************************************************)
THEOREM RuleInvImplication ==
ASSUME STATE F, STATE G,
F => G
PROVE []F => []G
PROOF OMITTED
(***************************************************************************)
(* The following rule is a special case of rule TLA2 from the paper "The *)
(* Temporal Logic of Actions". *)
(***************************************************************************)
THEOREM RuleStepSimulation ==
ASSUME STATE I, STATE f, STATE g,
ACTION M, ACTION N,
I /\ I' /\ [M]_f => [N]_g
PROVE []I /\ [][M]_f => [][N]_g
PROOF OMITTED
(***************************************************************************)
(* The following may be used to invoke a decision procedure for *)
(* propositional temporal logic. *)
(***************************************************************************)
PropositionalTemporalLogic == TRUE
================================================================================