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

*From*: ns <nedsri1988@xxxxxxxxx>*Date*: Wed, 31 Aug 2022 10:55:39 -0700 (PDT)*References*: <402fb7ef-74b1-46c5-a930-f0a2b5df4094n@googlegroups.com> <3373d8fd-341e-43ed-9031-d7952fad788dn@googlegroups.com>

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

On Tuesday, August 30, 2022 at 10:31:36 PM UTC-7 Leslie Lamport wrote:

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).On Tuesday, August 30, 2022 at 8:56:48 PM UTC-7 ns wrote: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!

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 view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/69c869a6-694c-4821-b82a-a2456452c1aen%40googlegroups.com.

**References**:**[tlaplus] Re: Translating***From:*Leslie Lamport

- Prev by Date:
**[tlaplus] Re: Translating** - Next by Date:
**[tlaplus] Specifying Systems- BoundedFIFO error- Figure 4.2** - Previous by thread:
**[tlaplus] Re: Translating** - Next by thread:
**[tlaplus] Specifying Systems- BoundedFIFO error- Figure 4.2** - Index(es):