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

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

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:

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

Hope this helps,

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.