Do Constraints Confuse Properties?

[sbublitz24]

Hello to all,

receiving a success message from TLC for a spec I wrote was confusing.

I was sure a property was hurt, so no success was expected.

The idea is to have a property fulfilled in every behaviour and

than to cut off the behaviour with a constraint before the property becomes true.

Here is a small spec and the corresponding config illustrating this.

TLC reports success when run in the VSCode TLA+ extension.

Is there something I overlooked?

Any explanation is welcome,

Siegfried

Gesendet mit Proton Mail: Ein sicherer E-Mail-Dienst.