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

*From*: Stephan Merz <stephan.merz@xxxxxxxxx>*Date*: Wed, 4 Oct 2023 09:20:02 +0200*References*: <81a73f7d-ab60-4d68-8dd1-dbe1620816fcn@googlegroups.com> <89CE3139-C47F-4421-BF15-4D078251545E@gmail.com> <CABW84Kwrcahcx7UVQMVcfE-eOSZmznpmo00ejFxnZvX=_Ct60w@mail.gmail.com>

Hi Jones, TLA+ formulas describe behaviors in terms of properties of states, which are assignments of values to variables. TLA+ is "extensional" in the sense that nothing but those values (including their changes during state transitions) are observable. Your state machine where I == v \in {0,1} N == v' \in {0,1} Spec == I /\ [][N]_v allows runs in which v changes value only finitely often, in other words, v has some fixed value forever after a finite prefix. From what you write, it looks like you have an "intensional" view of your specification where you record when action N takes place even if its occurrence is not visible in the value of v, and you want to require N to happen infinitely often. This leads you to suggest writing LiveSpec == Spec /\ []<>N [1] TLA+ doesn't adopt this view: you would have to make occurrences of N visible, perhaps by introducing another variable such as I == v \in {0,1} /\ tick = FALSE N == v' \in {0,1} /\ tick' = ~ tick Spec == I /\ [][N]_<<v,tick>> LiveSpec == Spec /\ []<><<N>>_<<v, tick>> A core design principle of TLA+ is to ensure that all temporal formulas are insensitive to finite stuttering, and requiring actions to be "guarded" in the forms [][A]_v and <><<A>>_v is a sufficient (but not necessary) condition to ensure this. For example, consider the (non-TLA+) formula <>(x' ~= x+1): this formula is false for a behavior where x = 0, 1, 2, 3, ... but true for a behavior where x = 0, 0, 1, 2, 3, ..., so inserting a stuttering step affects the meaning of the formula. Best, Stephan [1] Incidentally, note that in this example, Spec and LiveSpec would actually be equivalent, assuming LiveSpec were a legal TLA+ formula.
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/8E9DE382-49C2-4F34-8467-F3461B3BE487%40gmail.com. |

**Follow-Ups**:**Re: [tlaplus] Fairness conditions and <<A>>_v***From:*Jones Martins

**References**:**[tlaplus] Fairness conditions and <<A>>_v***From:*Jones Martins

**Re: [tlaplus] Fairness conditions and <<A>>_v***From:*Stephan Merz

**Re: [tlaplus] Fairness conditions and <<A>>_v***From:*Jones Martins

- Prev by Date:
**Re: [tlaplus] hierarchical finite state machine - liveness** - Next by Date:
**[tlaplus] Re: TLA+ project meetings** - Previous by thread:
**Re: [tlaplus] Fairness conditions and <<A>>_v** - Next by thread:
**Re: [tlaplus] Fairness conditions and <<A>>_v** - Index(es):