13 lines
537 B
Text
13 lines
537 B
Text
----------------------------- MODULE Controls -----------------------------
|
|
EXTENDS Keep
|
|
|
|
\* Bounded append-only controls partition all traces; fair actions never change inputs.
|
|
CONSTANTS First, Last
|
|
ASSUME First \in GoalStates /\ Last \in GoalStates
|
|
Control == <<First, Last>>
|
|
|
|
Prefix == Len(inputs') <= Len(Control) /\
|
|
\A i \in 1..Len(inputs') : inputs'[i] = Control[i]
|
|
PartNext == Next /\ Prefix
|
|
PartSpec == Init /\ [][PartNext]_vars /\ Fairness
|
|
=============================================================================
|