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