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

["Xavier Shay" <hello@xxxxxxxxxxxxxx>]

On Sat, Mar 30, 2019, at 10:56 AM, Markus Kuppe wrote:
> On 29.03.19 14:32, Xavier Shay wrote:
> > This got me thinking what could be different between our environments,
> > and led me to a discovery:
> > 
> > This "collapsing" only happens when either (or both) VoidRedundantAuths
> > or EventualCapture are added to the model as a temporal property to
> > check. (I also have DistinctIds and NoDoubleCapture as invariants, they
> > do not cause the issue.) I am suspicious of the `Success ~>` pattern I
> > have used in those, it feels a bit weird, but am not sure why yet.
> > 
> > I'm using toolbox on Ubuntu 18.10. Here is a link to a zip of my
> > payments.toolbox
> > folder: https://drive.google.com/file/d/1qASlY0euOqg7VCd2QFKD68y86ieLICwf/view?usp=sharing
> > 
> > Thank you both for taking the time to assist!
> 
> Hi Xavier,
> 
> can you share a screenshot of the Result Page when it only displays a
> single state?  All MC.out files in the zip file - created by TLC running
> in the Toolbox - show more than one distinct state.
Attached two files - one showing the "single state", another ostensibly working - showing what I get with no properties checked.

Is this what you were asking for? I can make a video later today of me actually running the model, in case there's something wrong I'm doing there. (I'm just pressing F11 though.)

Xavier

> 
> Thanks
> Markus
> 
> -- 
> You received this message because you are subscribed to a topic in the 
> Google Groups "tlaplus" group.
> To unsubscribe from this topic, visit 
> https://groups.google.com/d/topic/tlaplus/VaH-MNxtcBQ/unsubscribe.
> To unsubscribe from this group and all its topics, 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.
>

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

Attachment: model-checking-results-with-temporal-property.png
Description: PNG image

Attachment: model-results-no-properties-or-invariants.png
Description: PNG image