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

Re: [tlaplus] TLAPS project status



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> 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: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> 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> 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 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 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 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.
>>> To post to this group, send email to tla...@xxxxxxxxxxxxxxxx.
>>> Visit this group at http://groups.google.com/group/tlaplus.
>>> For more options, visit 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.
>> To post to this group, send email to tla...@xxxxxxxxxxxxxxxx.
>> Visit this group at http://groups.google.com/group/tlaplus.
>> For more options, visit 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.
To post to this group, send email to tla...@xxxxxxxxxxxxxxxx.
Visit this group at http://groups.google.com/group/tlaplus.
For more options, visit 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.
To post to this group, send email to tla...@xxxxxxxxxxxxxxxx.
Visit this group at http://groups.google.com/group/tlaplus.
For more options, visit https://groups.google.com/d/optout.