Re: [tlaplus] Invariant TCTypeOK is violated in a simple spec

Hello,

the model checker shows you a counter-example to the invariant TCTypeOK where i reaches value 20, and how should it be otherwise?

An invariant has to be true in all states that your specification can reach. Since all your actions increment i, it can grow beyond any bound. The predicate

i \in Nat \ {0,1}

is an invariant of your specification (but since your model has an infinite state space, TLC will not be able to verify it exhaustively).

Regards,

Stephan

On 22 Mar 2019, at 15:57, Adi <adi4info@xxxxxxxxx> wrote:

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.

--
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.