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