----------------------------- 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
=============================================================================