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

*From*: Markus Kuppe <tlaplus-google-group@xxxxxxxxxxx>*Date*: Sat, 30 Mar 2019 09:00:51 -0700*References*: <83437afa-a9b8-4966-8938-806d68fe7f57@googlegroups.com> <ED45F0CB-DFF4-4710-A6FE-27190E4D10A3@gmail.com> <e69d85f0-3fe8-f0ab-f7cf-f44c97375483@lemmster.de> <33a2e968-7a5d-4269-a074-fd6da1f1dc79@googlegroups.com> <c6e1379b-d29b-c7ad-edea-307cc49b84df@lemmster.de> <14372a00-0db7-40f2-b917-80a13710262a@www.fastmail.com> <e97797dd-81f2-a751-3c3a-6f969ae8d758@lemmster.de>

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.

**References**:**[tlaplus] Why does adding a new step collapse my model to a single state?***From:*Xavier Shay

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

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

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

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

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

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

- Prev by Date:
**Re: [tlaplus] When TLC error trace send with stuttering - what does this mean?** - Next by Date:
**Re: [tlaplus] Understand symmetric set** - Previous by thread:
**Re: [tlaplus] Why does adding a new step collapse my model to a single state?** - Next by thread:
**[tlaplus] When TLC error trace send with stuttering - what does this mean?** - Index(es):