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

*From*: Adi <adi4info@xxxxxxxxx>*Date*: Sat, 23 Mar 2019 05:16:02 -0700 (PDT)*References*: <eb2f2815-b121-49c8-bb9d-82829eeb6c47@googlegroups.com> <c3c8f81d-dcb8-40df-81d7-f9b9c3a2e723@googlegroups.com> <72AC0ECD-BD68-4966-8013-6988C92CE54F@gmail.com>

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

On Saturday, March 23, 2019 at 12:58:48 PM UTC+5:30, Stephan Merz wrote:

-- On Saturday, March 23, 2019 at 12:58:48 PM UTC+5:30, Stephan Merz wrote:

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.StephanOn 23 Mar 2019, at 06:09, Adi <adi4...@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+u...@googlegroups.com .

To post to this group, send email to tla...@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.

**References**:

- Prev by Date:
**Re: [tlaplus] Re: Invariant TCTypeOK is violated in a simple spec** - Next by Date:
**Re: [tlaplus] Re: Invariant TCTypeOK is violated in a simple spec** - Previous by thread:
**Re: [tlaplus] Re: Invariant TCTypeOK is violated in a simple spec** - Next by thread:
**Re: [tlaplus] Re: Invariant TCTypeOK is violated in a simple spec** - Index(es):