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 -- 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/ae245354-5aec-d53b-b291-d16d3e299031%40kit.edu.
Attachment:
smime.p7s
Description: S/MIME Cryptographic Signature