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

Re: [tlaplus] New To Group

Hello Tim,

and welcome to the TLA+ Google group!

(1) I don't see any information on implementing safety with TLA+. Can anyone shed light on why this is the
    case and if TLA+ allows implementation of safety.

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.

(2) I would like to cal TLA+ from my application using command line or even better some api. Is there a guide on how to do this.

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

(3) I would like to use the logical expressions in Lamperts lectures not the TLA+ language.

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.

(4) does TLA+ have support for the full set of temporal operators O,<>,[ ], U (up until), W( true unless).

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,

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