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

*From*: Stephan Merz <stepha...@xxxxxxxxx>*Date*: Wed, 9 Nov 2016 08:42:51 +0100*References*: <b7fdd1df-31e7-46f4-974e-7056aee9b83f@googlegroups.com>

Hello,
First, note that this formula is quite certainly not what you intend to verify. It is true of a behavior if eventually the variable hr changes value and its value in the first state is different from one. (An implication is true if the formula on its left-hand side is false.)
Well, TLC's error message is pretty explicit here. As explained in Specifying Systems (chapter 14.2.4), TLC checks only a subset of temporal formulas, and <><<A>>_v is not part of that subset. TLC can check that each of the following formulas holds of the HourClock specification (with fairness): <>(hr = 2) []<><< hr=1 /\ hr' = 2 >>_hr <>[][ hr=1 => hr' = 2 ]_hr Hope this helps, Stephan |

**Follow-Ups**:**Re: [tlaplus] Eventual action***From:*vit . . .

**References**:**Eventual action***From:*vit . . .

- Prev by Date:
**Re: Vim plugin for TLA+** - Next by Date:
**Re: [tlaplus] Eventual action** - Previous by thread:
**Eventual action** - Next by thread:
**Re: [tlaplus] Eventual action** - Index(es):