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

*From*: Stephan Merz <stephan.merz@xxxxxxxxx>*Date*: Sat, 23 Feb 2019 08:57:05 +0100*References*: <d9cca9af-92e6-498c-a509-22135e553611@googlegroups.com>

Hello Tim, and welcome to the TLA+ Google group!
--
Could you elaborate on what you understand by "safety"? In TLA+ and similar specification formalisms, a safety property is a set of behaviors such that "nothing bad ever happens" [1,2], but I believe that you have something different in mind.
The TLA+ tools can be called from the command line [3], but TLA+ is not meant to be executable. (The model checker TLC can be seen as providing an interpreter for a subset of TLA+.)
TLA+ is based on logic and contains all the logical expressions used in the video lectures, so I am not sure I understand the question.
The temporal operators of TLA+ are deliberately restricted so that all temporal formulas are invariant under stuttering [4,5]. In particular, this excludes unconstrained use of LTL's next-time operator. Binary connectives such as "until" or "unless" are not part of TLA+ but can in fact be defined using quantification over state variables (beware: this form of quantification is not supported by TLC), and it can be shown that the temporal logic of TLA+ is more expressive than the next-free fragment of LTL. However, the philosophy of TLA+ is to write state-machine specifications of systems, and for these "always", "eventually", and priming (the next-state operator applied to state variables and, by extension, to state formulas) is enough. Hope this helps, Stephan [2] Bowen Alpern, Fred B. Schneider: Defining Liveness. Inf. Process. Lett. 21(4): 181-185 (1985). [5] Doron A. Peled, Thomas Wilke: Stutter-Invariant Temporal Properties are Expressible Without the Next-Time Operator. Inf. Process. Lett. 63(5): 243-246 (1997). 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+unsubscribe@xxxxxxxxxxxxxxxx. To post to this group, send email to tlaplus@xxxxxxxxxxxxxxxx. Visit this group at https://groups.google.com/group/tlaplus. For more options, visit https://groups.google.com/d/optout. |

**References**:**[tlaplus] New To Group***From:*tobrien

- Prev by Date:
**Re: [tlaplus] Re: add fairness properties to a specification with PlusCal INSTANCEs** - Next by Date:
**[tlaplus] How to test a process eventually succeeds after indefinite number of retries?** - Previous by thread:
**[tlaplus] New To Group** - Next by thread:
**[tlaplus] How to test a process eventually succeeds after indefinite number of retries?** - Index(es):