70 lines
1.8 KiB
Text
70 lines
1.8 KiB
Text
---- MODULE StateChart ----
|
|
EXTENDS TLC \* For @@: function left-merge
|
|
|
|
(*
|
|
Interesting to note: although the parent states LoggedIn and Reports are never listed
|
|
in the behavior traces, they enable unlisted transitions like Main|Settings|Report(1,2) -> LogOut,
|
|
all created by the single Trans("LogIn", "LogOut") line.
|
|
*)
|
|
VARIABLE state
|
|
|
|
States == {
|
|
"LogOut",
|
|
"LogIn",
|
|
"Main",
|
|
"Settings",
|
|
"Reports",
|
|
"Report1",
|
|
"Report2"
|
|
}
|
|
|
|
\* Associate child states
|
|
TopDown == SortSeq @@ [ LogIn |-> {"Main", "Settings", "Reports"},
|
|
Reports |-> {"Report1", "Report2"}
|
|
] @@ [s \in States |-> {}]
|
|
|
|
\* Associate parent states
|
|
BottomUp == [ Report1 |-> "Reports",
|
|
Report2 |-> "Reports",
|
|
Reports |-> "LogIn",
|
|
Main |-> "LogIn",
|
|
Settings |-> "LogIn" ]
|
|
|
|
\* Ensure no double parents in TopDown: the intersection of their children set is empty if they are different
|
|
ASSUME \A s1, s2 \in States: s1 # s2 => TopDown[s1] \cap TopDown[s2] = {}
|
|
|
|
RECURSIVE InTD(_, _)
|
|
InTD(s, p) ==
|
|
\/ s = p
|
|
\/ \E c \in TopDown[p]: InTD(s, c)
|
|
|
|
RECURSIVE InBU(_, _)
|
|
InBU(s, p) ==
|
|
\/ s = p
|
|
\/ \E c \in DOMAIN BottomUp:
|
|
/\ p = BottomUp[c]
|
|
/\ InBU(s, c)
|
|
|
|
\* Check that InTD and InBU are identical
|
|
ASSUME \A s1, s2 \in States: InTD(s1, s2) <=> InBU(s1, s2)
|
|
|
|
Trans(from, to) ==
|
|
/\ InTD(state, from)
|
|
/\ state' = to
|
|
|
|
Init == state = "LogOut"
|
|
|
|
Next ==
|
|
\/ Trans("LogOut", "Main")
|
|
\/ Trans("Main", "Settings")
|
|
\/ Trans("Settings", "Main")
|
|
\/ Trans("LogIn", "LogOut")
|
|
\/ Trans("LogIn", "Report1")
|
|
\/ Trans("Report1", "Report2")
|
|
\/ Trans("Report2", "Report1")
|
|
\/ Trans("Reports", "Main")
|
|
|
|
Spec == Init /\ [][Next]_state
|
|
|
|
AlwaysInLeaf == TopDown[state] = {}
|
|
====
|