Translating

[ns]

Apologies if I'm rehashing a subject that has been thoroughly hashed, but I am looking at translating some LTL formulas into TLA+. In particular the formulas are assertions to a model checker and may contain the X operator. So you may see something like [] (x>0 --> X x=1) along with some fairness assumption about the model. Now as it stands it won't translate to TLA+, but if I insist on it saying 

    [] ((x>0 /\ x=K)--> X (x=1 \/ x=K)) 

ie ensuring a stutter step is always allowed, is it correct to translate this as 

    [] [IF x>0 THEN x'=1 \/ x'=x]_<<x>>   ?

Thanks!

[Leslie Lamport]

Close.  Just replace  IF A THEN B  by  A => B .  (Implication is written => rather than -> in TLA+.)
However, the x'=x is redundant because [A]_<<x>>  means  A \/ (x'=x).

[ns]

Yes I'm sorry I knew that, I'm embarrassed to see that I wrote that. I need to check what I write before hitting "Post" from now on! But thank you for the correction and the confirmation of my understanding