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

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