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

[tlaplus] Invariant TCTypeOK is violated in a simple spec

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,

---------------------------- MODULE Counter ----------------------------
EXTENDS Naturals, TLC, Integers

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.