Re: [tlaplus] Why does adding a new step collapse my model to a single state?

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

On 29.03.19 19:22, Markus Kuppe wrote:
> this looks strange, especially since it takes TLC 28 seconds to generate
> a single distinct state.  What output does the TLC console show (TLC
> model checker > TLC console)?  Lets take this discussion off-list though
> to not further spam the group.

For the record:  Xavier and I traced the issue down to a bug in one of
the recent nightly Toolbox builds.  The bug has already been fixed [2]
in the newest builds though.  For those affected, an upgrade to the
newest Toolbox build solves the issue.

Thanks
Markus

[1] https://github.com/tlaplus/tlaplus/issues/236#issuecomment-475064081
[2]
https://github.com/tlaplus/tlaplus/commit/00df10c877494b16165da3bda12d20b2f1a20eb3

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