Hello,
> Note that this implication is evaluated in the initial state of a behavior because it is not in the scope of a temporal operator. Since Counter is initialized to 0, the formula is simply equivalent to
>
> WF_Counter(Next)
>
> But perhaps you meant to assert that the counter should eventually be incremented in states where the counter value is less than 100. This is expressed by the fairness condition
>
> WF_Counter(Counter < 100 /\ Next)
Thank you, for the explanation! That was what I actually wanted to express.
After changing this line, everything works as I expect.
Btw, when checking which version of TLC I have, I found that the toolbox reports inconsistent information:
Help -> About shows
> This is Version 1.8.0 of Day Month Year and includes:
> - SANY Version 2.2 of 20 April 2020
> - TLC Version 2.15 of 20 April 2020
While TLC Model Checker -> TLC Console shows in the first line
> TLC2 Version 2.18 of Day Month 20?? (rev: ca5ad64)
I'm running the latest release of the toolbox from Github (
https://github.com/tlaplus/tlaplus/releases#latest-tla-files).
Matthias