Hi All,
I'm a total beginner in TLA+ and I'm excited to learn this.
I began watching the TLA+ video lectures and toying with small specs on my own.
I'm facing a issue with model checking error. IN the below spec I expect no errors for values of i between 1 and 20. But model checker is giving error even when i = 3,4....20 giving out "Invariant TCTypeOK is violated."
Am I missing something obvious ?
Thanks in advance,
Adi
---------------------------- MODULE Counter ----------------------------
EXTENDS Naturals, TLC, Integers
VARIABLES i
TCTypeOK ==
/\ i> 1
/\ i < 20
Init == (i=2)
FirstHalf ==
/\ i<10
/\ i' = i+1
Mid ==
/\ i=10
/\ i' = i+1
SecondHalf ==
/\ i>10
/\ i' = i+1
Next == FirstHalf \/ SecondHalf \/ Mid
=============================================================================
--
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 post to this group, send email to tlaplus@xxxxxxxxxxxxxxxx.
Visit this group at https://groups.google.com/group/tlaplus.
For more options, visit https://groups.google.com/d/optout.