Re: [tlaplus] TLAPS project status

[Jaak Ristioja <jaak.r...@xxxxxxxx>]

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.
>>
>