Hi,I would also like to point out to the Practical hints section of the TLAPS website: https://tla.msr-inria.inria.fr/tlaps/content/ Documentation/Tutorial/ Practical_hints.html Also, default SMT solver for TLAPS is CVC3. In some cases I have seen that CVC3 is unable to prove certain arithmetic formulae which seem completely trivial to me. For example the following:Ballots == Nat<5>1. PICK m \in msgs: Phase1b(a)!(m) ...<5>5. (\A b \in Ballots, s \in Slots, v \in Values: b > X(s) => Y(b,s,v))' ...
<5>6. \A s \in Slots: X(s) \in Ballots \cup {-1} ...
<5>7. (\A b \in Ballots, s \in Slots, v \in Values: b \in X(s)+1..m1.bal-1 => Y(b,s,v))'
BY <5>5, <5>6, <5>1, Z3CVC3 cannot check the proof of <5>7 in the default timeout but Z3 checks it instantaneously.Lesson being that if faced with an arithmetic proof which is not going through, try Z3 before writing a much longer proof (I initially did that for <5>7, I believe it was around 40 lines long).Hope this helps too,SakshamOn Mon, Aug 19, 2019 at 3:18 AM Stephan Merz <steph...@xxxxxxxxx> wrote:Hello,--the default strategy of TLAPS is to try first the SMT backend, then Zenon, then Isabelle (with the "auto" tactic). As long as your proof obligation is proved, you don't need to worry which backend succeeded. You can find out by looking at the proof console and then document this by adding "BY Zenon" etc. so that you don't have to wait for the other backends to timeout.Generally, SMT helps with obligations involving arithmetic and basic reasoning about sets and functions. Its main weakness is reasoning about formulas with quantifiers (explicitly present in the proof obligation or generated from the encoding of set theory). Zenon is usually more successful for obligations involving first-order logic (quantifiers) and set theory, but it doesn't know anything about arithmetic. Isabelle occasionally proves one-off goals that SMT or Zenon don't catch but is mainly useful for goals involving schematic variables (technically, second-order unification) such as induction proofs. Isabelle contains other proof methods than "auto" that can be invoked as IsaM("blast") or IsaM("force") but knowledge about the inner workings of the backend is necessary to be able to use them effectively.Reasoning about sequences, finite sets and cardinality, bags, and recursive function definitions is currently not (or hardly) supported by the automated backends. You need to explicitly invoke theorems from library modules (including SequenceTheorems.tla, FiniteSetTheorems.tla, NaturalsInduction.tla, WellFoundedInduction.tla). You may want to look at the versions of these modules with proofs to get a feel for how to conduct proofs about these structures. Suggestions for useful lemmas that should be included in the library are always welcome.And we should certainly produce a tutorial for using TLAPS ...Hope this helps,StephanOn 14 Aug 2019, at 05:28, Hengfeng Wei <hengx...@xxxxxxxxx> wrote:Dear All,I am learning TLAPS proofs by following the "official" examples released with TLAPS.I notice that sometimes we need to explicitly specify the backend provers,like "BY IsaM("force")", "BY Z3", "BY SMT", and so on.But, I have no idea which one/ones to choose (and in which situations).What are the strengths/weaknesses of these backend provers?Are there any instructions on when and how to explicitly specify some (which?) backend provers?Best regards,hengxin--
You received this message because you are subscribed to the Google Groups "tlaplus" group.
To unsubscribe from this group and stop receiving emails from it, send an email to tla...@googlegroups.com .
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/e90c0e0f-206a- .4f9f-aa60-fb9899240aba% 40googlegroups.com
You received this message because you are subscribed to the Google Groups "tlaplus" group.
To unsubscribe from this group and stop receiving emails from it, send an email to tla...@googlegroups.com .
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/637DCE0D-4C72- .497A-A340-4AE96D23BF27% 40gmail.com