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

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



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 <adi4info@xxxxxxxxx> 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.

<Screen Shot 2019-03-23 at 10.34.11 AM.png>





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

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

On Friday, March 22, 2019 at 8:29:08 PM UTC+5:30, Adi 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.
<Screen Shot 2019-03-23 at 10.34.11 AM.png>

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