[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
Re: [tlaplus] TLAPS project status
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>.
>