Re: [tlaplus] New To Group

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,

Stephan

[1] http://lamport.azurewebsites.net/pubs/pubs.html#proving

[2] Bowen Alpern, Fred B. Schneider: Defining Liveness. Inf. Process. Lett. 21(4): 181-185 (1985).

[3] http://lamport.azurewebsites.net/tla/standalone-tools.html

[4] https://members.loria.fr/SMerz/papers/tla+logic2008.html

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