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

[Markus Kuppe <tlaplus-google-group@xxxxxxxxxxx>]

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

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