[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

*From*: Jaak Ristioja <jaak.r...@xxxxxxxx>*Date*: Fri, 2 Oct 2015 13:44:26 +0300*References*: <560D2931.1070007@cyber.ee> <9642A567-6F5F-4C76-87F9-CB253C31C5ED@gmail.com> <CAFGa14GmuzZgb8YFVHwt7F2RFgP0LMAJz8evO9vKduwkO=rw4A@mail.gmail.com> <560E2155.5090500@cyber.ee> <CAFGa14E=wF=wtYaijvVr_73V5zgb=X60Q_YcV6bqB0NQALQcEg@mail.gmail.com> <E55F1FFF-D618-4FB8-8FBD-7172D0CA25AD@gmail.com>*User-agent*: curl/7.42.1

Thank you, your answers clarified this for me! Best regards, Jaak On 02.10.2015 09:54, Stephan Merz wrote: > Here is a concrete, though somewhat silly example of what (I believe) Tomer means. Note that steps <1>1 and the sub-step <2>3 of <1>2 cannot currently be proved: step <1>1 requires invoking a well-founded ordering and is therefore essentially non-propositional, and step <2>3 requires proving an ENABLED predicate. > > > VARIABLE a > Init == a \in Nat > Next == a'=a+1 > Spec == Init /\ [][Next]_a /\ WF_a(Next) > > LEMMA Spec => \A n \in Nat : <>[](a > n) > <1>0. Spec => [](a \in Nat) > <2>1. a \in Nat /\ [Next]_a => (a \in Nat)' > BY DEF Next > <2>. QED BY <2>1, PTL DEF Spec, Init > <1>. SUFFICES ASSUME NEW n \in Nat > PROVE Spec => <>[](a > n) > OBVIOUS > <1>1. Spec /\ [](a \in Nat) => <>(a = n) > OMITTED > <1>2. Spec => [](a=n => <>(a > n)) > <2>1. a=n /\ <<Next>>_a => (a>n)' > BY DEF Next > <2>2. a=n /\ UNCHANGED a => (a=n)' > OBVIOUS > <2>3. a=n => ENABLED <<Next>>_a > OMITTED > <2>. QED BY <2>1, <2>2, <2>3, PTL DEF Spec > <1>3. Spec /\ [](a \in Nat) => [](a>n => [](a>n)) > <2>1. a \in Nat /\ a>n /\ [Next]_a => (a \in Nat /\ a>n)' > BY DEF Next > <2>. QED BY <2>1, PTL DEF Spec > <1>. QED BY <1>0, <1>1, <1>2, <1>3, PTL > > Best, > Stephan > >> On 02 Oct 2015, at 08:24, Shaolintl . <shao...@xxxxxxxxx> wrote: >> >> Dear Jaak, >> >> A partial proof in TLA+ is a proof where some parts are omitted using the keywords: PROOF OMITTED when a sub-proof should have been given. >> If the statement not proved is relatively simple to trust (like maybe for fairness holding), then writing a partial proof might still increase confidence in the correctness of the property checked. >> >> And to clarify the meaning of "formulas are ptl valid". It means that the arbitrary formulas are instances of PTL valid formulas. >> >> Best regards, >> Tomer >> >> On 2 October 2015 at 08:16, Jaak Ristioja <jaak.r...@xxxxxxxx <mailto:jaak.r...@xxxxxxxx>> wrote: >> Dear Stephan and Tomer! >> >> Thank you for your answers (and a great tool)! >> >> What do you mean by partial liveness proofs? Can you give a simple example? >> >> >> Best regards, >> Jaak >> >> On 01.10.2015 18 <tel:01.10.2015%2018>:55, Shaolintl . wrote: >>> Dear Jaak, >>> >>> Just a small comment that the restricted support for ptl (propositional >>> temporal logic) doesn't mean it can handle ptl formulas only but that it >>> checks if formulas are ptl valid. You can use the prover to prove >>> arbitrary formulas if their validity depends on their ptl content only >>> using the syntax BY PTL. Some example are included in the examples >>> directory. >>> >>> This functionality suffices for proving safety properties but as Stephan >>> has mentioned, the lack of support for fairness and ENABLED means it >>> doesn't fully support liveness properties. Partial liveness proofs can >>> still be written. >>> >>> Best regards, >>> Tomer >>> On 1 Oct 2015 5:39 pm, "Stephan Merz" <Stepha...@xxxxxxxxx <mailto:Stepha...@xxxxxxxxx>> wrote: >>> >>>> Dear Jaak, >>>> >>>> thank you very much for your interest in the TLA+ prover. Temporal >>>> reasoning within TLAPS is currently still restricted to (essentially) >>>> propositional temporal logic. Supporting first-order temporal reasoning has >>>> been on our list for too long already, but requests like yours make it more >>>> pressing. >>>> >>>> Note that full liveness reasoning will also require support for reasoning >>>> about ENABLED predicates. We have plans on how to support this in the >>>> prover but we do not yet know how far they will take us in practice. I'm >>>> afraid that it will still take another year or two to get full support for >>>> liveness proofs. >>>> >>>> Our main implementation effort currently goes into a complete rewrite of >>>> the proof manager, including an integration with the SANY parser. >>>> >>>> Best regards, >>>> Stephan >>>> >>>> >>>>> On 01 Oct 2015, at 14:38, Jaak Ristioja <jaak.r...@xxxxxxxx <mailto:jaak.r...@xxxxxxxx>> wrote: >>>>> >>>>> Hello! >>>>> >>>>> As far as I can understand, the current version of TLAPS does not >>>>> perform temporal reasoning and hence can't be used to prove liveness >>>>> properties. Is support for temporal reasoning being developed? >>>>> >>>>> As one can currently observe from >>>>> https://tlaps.codeplex.com/SourceControl/list/changesets <https://tlaps.codeplex.com/SourceControl/list/changesets> TLAPS >>>>> development is not a completely open process, the only commits are >>>>> "version 1.2.1" and "push to version 1.4.3". What is the reason for this >>>>> and will it change in the future? >>>>> >>>>> I found https://tlaps.codeplex.com/SourceControl/latest#todo.txt <https://tlaps.codeplex.com/SourceControl/latest#todo.txt> but >>>>> what other means are there to track the status of TLAPS? >>>>> >>>>> >>>>> Best Regards, >>>>> Jaak Ristioja >>>>> Cybernetica AS >>>>> >>>>> >>>>> PS: http://www.msr-inria.fr/projects/tools-for-proofs/#downloads <http://www.msr-inria.fr/projects/tools-for-proofs/#downloads> still >>>>> states "The TLA+ proof system version 1.3.0 has been released!" >>>>> >>>>> -- >>>>> 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 tlaplus+u...@xxxxxxxxxxxxxxxx <mailto:tlaplus%2B...@xxxxxxxxxxxxxxxx>. >>>>> To post to this group, send email to tla...@xxxxxxxxxxxxxxxx <mailto:tla...@xxxxxxxxxxxxxxxx>. >>>>> Visit this group at http://groups.google.com/group/tlaplus <http://groups.google.com/group/tlaplus>. >>>>> For more options, visit https://groups.google.com/d/optout <https://groups.google.com/d/optout>. >>>>> <0x4FCA45E0.asc> >>>> >>>> -- >>>> 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 tlaplus+u...@xxxxxxxxxxxxxxxx <mailto:tlaplus%2B...@xxxxxxxxxxxxxxxx>. >>>> To post to this group, send email to tla...@xxxxxxxxxxxxxxxx <mailto:tla...@xxxxxxxxxxxxxxxx>. >>>> Visit this group at http://groups.google.com/group/tlaplus <http://groups.google.com/group/tlaplus>. >>>> For more options, visit https://groups.google.com/d/optout <https://groups.google.com/d/optout>. >>>> >>> >> >> -- >> 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 tlaplus+u...@xxxxxxxxxxxxxxxx <mailto:tlaplus%2B...@xxxxxxxxxxxxxxxx>. >> To post to this group, send email to tla...@xxxxxxxxxxxxxxxx <mailto:tla...@xxxxxxxxxxxxxxxx>. >> Visit this group at http://groups.google.com/group/tlaplus <http://groups.google.com/group/tlaplus>. >> For more options, visit https://groups.google.com/d/optout <https://groups.google.com/d/optout>. >> >> >> -- >> 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 tlaplus+u...@xxxxxxxxxxxxxxxx <mailto:tlaplus+u...@xxxxxxxxxxxxxxxx>. >> To post to this group, send email to tla...@xxxxxxxxxxxxxxxx <mailto:tla...@xxxxxxxxxxxxxxxx>. >> Visit this group at http://groups.google.com/group/tlaplus <http://groups.google.com/group/tlaplus>. >> For more options, visit https://groups.google.com/d/optout <https://groups.google.com/d/optout>. >

**References**:**TLAPS project status***From:*Jaak Ristioja

**Re: [tlaplus] TLAPS project status***From:*Stephan Merz

**Re: [tlaplus] TLAPS project status***From:*Shaolintl .

**Re: [tlaplus] TLAPS project status***From:*Jaak Ristioja

**Re: [tlaplus] TLAPS project status***From:*Shaolintl .

**Re: [tlaplus] TLAPS project status***From:*Stephan Merz

- Prev by Date:
**Re: [tlaplus] TLAPS project status** - Next by Date:
**Re: [tlaplus] Some distributed TLC errors not displayed in TLA+ Toolbox** - Previous by thread:
**Re: [tlaplus] TLAPS project status** - Next by thread:
**Re: [tlaplus] TLAPS project status** - Index(es):