Invariant TCTypeOK is violated in a simple spec

[Adi]

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

=============================================================================

[Hillel Wayne]

Try i <= 20 instead of i < 20.

--
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+u...@googlegroups.com.
To post to this group, send email to tla...@googlegroups.com.
Visit this group at https://groups.google.com/group/tlaplus.
For more options, visit https://groups.google.com/d/optout.

[Stephan Merz]

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

[Adi]

Thanks guys !!!

I modified the spec and now not getting error.

Actually I was confused by the error trace which showed red highlight on variable i when in states 3,4,5...etc. which led me to think that the invariant is violated at those steps also. I now feel that this is complete error trace leading to i == 21 which actually violated the invariant, not the steps in between.

Modified spec with no error:

---------------------------- MODULE RingCounter ----------------------------

EXTENDS Naturals, TLC, Integers
VARIABLES i

TCTypeOK == 

/\ i> 0
/\ i <= 20


Init == i \in (2..20)


Wrap ==
IF i > 19 THEN i' = 1 ELSE  i' = i + 1

FirstHalf ==
/\ i<10

/\ Wrap


Mid ==
/\ i=10
/\ Wrap

SecondHalf ==
/\ i>10

/\ Wrap



Next ==  FirstHalf \/ SecondHalf  \/ Mid \/ Wrap

=============================================================================

[Stephan Merz]

The red highlight in traces displayed in the Toolbox simply indicates which variables changed during the corresponding step. Since your spec has only a single variable, this is not very informative in your case.

Stephan 

On 23 Mar 2019, at 06:09, Adi <adi4...@gmail.com> wrote:

Thanks guys !!!

I modified the spec and now not getting error.

Actually I was confused by the error trace which showed red highlight on variable i when in states 3,4,5...etc. which led me to think that the invariant is violated at those steps also. I now feel that this is complete error trace leading to i == 21 which actually violated the invariant, not the steps in between.

--
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+u...@googlegroups.com.
To post to this group, send email to tla...@googlegroups.com.
Visit this group at https://groups.google.com/group/tlaplus.
For more options, visit https://groups.google.com/d/optout.

[Adi]

Oh Ok !!! Got it  !! Thanks !!

[Markus Kuppe]

On 22.03.19 22:09, Adi wrote:
> Actually I was confused by the error trace which showed red highlight on
> variable i when in states 3,4,5...etc. which led me to think that the
> invariant is violated at those steps also. I now feel that this is
> complete error trace leading to i == 21 which actually violated the
> invariant, not the steps in between.

The error trace explorer comes with detailed documentation:
http://nightly.tlapl.us/doc/model/executing-tlc.html#model

The same documentation is also available from the built-in Toolbox help.

Hope this helps,
Markus

[Adi]

Thanks Markus .....Will check that out !!