Hello everyone.
What do you think, is a violation of the temporal property a normal behavior or not?
Because from my point of view, it shouldn't be any violation.
So this is a very simple example:
EXTENDS Integers
VARIABLES step, state
vars == <<step, state>>
TypeOK ==
state \in {"created", "inProgress", "completed"}
Init ==
/\ step = 1
/\ state = "created"
InProgress ==
/\ state = "created"
/\ step' = step + 1
/\ state' = "inProgress"
Completed ==
/\ state = "inProgress"
/\ step' = step + 1
/\ state' = "completed"
Next ==
\/ InProgress
\/ Completed
Spec == Init /\ [][Next]_vars
TemporalProperty ==
[]<><<state = "completed">>_vars
I am trying to check the temporal property "TemporalProperty" and it fails on the last step:
/\ state = "completed"
/\ step = 3
Stuttering State(num = 4)
If we look at the temporal property _expression_:
[]<><<state = "completed">>_vars
It says: "should always eventually happen, state = "completed" or vars should be changed".
So on the last step (and all the next steps) state = "completed" and this satisfies the temporal property.
Why does the stuttering error appear?
Thanks for your attention.
--
Bye.
Best regards, Rostislav Nikitin.