Latest release of TLA Proof System

[harolda...@gmail.com]

Hello,

I am interested in TLA Proof System. As far as I know temporal reasoning is not supported in the TLAPS at the moment. Maybe I am working with old version of TLAPS, which is 1.4.3 (June 2015).

Version history says:

TLAPS version 1.4.3 (June 2015)
TLAPS version 1.3.2 (May 2014)
TLAPS version 1.3.0 (March 2014)
TLAPS version 1.2.1 (September 2013)
TLAPS version 1.1.1 (November 2012)
TLAPS version 1.0 (January 2012)
TLAPS version 0.9 (October 2010)

Is "TLAPS version 1.4.3 (June 2015)" the latest version of TLAPS ?

Does somebody know when the new version of TLAPS will be released ?

Kind Regards,
Harold

[Stephan Merz]

Hello Harold,

it looks like you are running the most recent public version of TLAPS. We are preparing a bug fix release that should have appeared at the end of last year but unfortunately has been held up by a few technical issues. Also, work has started on supporting ENABLED as a first step towards reasoning about more general liveness properties, but I don't know when we'll be ready to release that.

Best regards,
Stephan

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

[Haroldas Giedra]

Thank you very much, Stephan. At the moment I am working with propositional temporal logic. I tried to verify some proofs with temporal reasoning and it seem it worked out.  

Kind Regards,

Harold  

You received this message because you are subscribed to a topic in the Google Groups "tlaplus" group.
To unsubscribe from this topic, visit https://groups.google.com/d/topic/tlaplus/3xgMOS6Okgc/unsubscribe.
To unsubscribe from this group and all its topics, send an email to tlaplus+u...@googlegroups.com.

[Stephan Merz]

Glad to hear that – propositional temporal reasoning is indeed supported by the current version through the PTL backend.

Stephan

> To unsubscribe from this group and stop receiving emails from it, send an email to tlaplus+unsubscribe@googlegroups.com.

> To post to this group, send email to tla...@googlegroups.com.
> Visit this group at https://groups.google.com/group/tlaplus.
> For more options, visit https://groups.google.com/d/optout.

--
You received this message because you are subscribed to a topic in the Google Groups "tlaplus" group.
To unsubscribe from this topic, visit https://groups.google.com/d/topic/tlaplus/3xgMOS6Okgc/unsubscribe.

To unsubscribe from this group and all its topics, send an email to tlaplus+unsubscribe@googlegroups.com.