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

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

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.


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.