CODEWITHSUNDEEP
tla+
Jakub M.
Jakub M.

Reputation: 33817

Check that system passes all the states

A variable state stands for state of a system, for instance state \in {"ready", "prepare", "do", "cleanup", "done"}. How to express condition that state should eventually pass all the five states (in any order)?

Working example (accepted answer):

EXTENDS Naturals
VARIABLE n
Init == n = 1
Next == IF n < 3 THEN n' = n + 1 ELSE n' = n
Spec == Init /\ [][Next]_<<n>> /\ WF_<<n>>(Next)
Check == \A s \in {1,2,3}: <>(s = n)    \* This goes: Model Overview >
                                        \* > "What to check?" > Properties

Upvotes: 3

Views: 73

Answers (1)

Hovercouch
Hovercouch

Reputation: 2314

Given States = {"ready", "prepare", "do", "cleanup", "done"}, you can check that it reaches some given state with

<>(state = "ready")

And you can check that it reaches all states with

\A s \in States: <>(state = s)

Upvotes: 2

Related Questions