File size: 552 Bytes
5befefa | 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 | import SovereignApollo.State
inductive CommsState where
| Acquire | Lock | Data | Drop
deriving DecidableEq, Repr
def commsTransition : CommsState → CommsState → Prop
| .Acquire, .Lock => True
| .Lock, .Data => True
| .Data, .Drop => True
| .Drop, .Acquire => True
| s, t => s = t -- stutter allowed
theorem comms_no_skip_acquire_to_data : ¬ commsTransition .Acquire .Data := by
simp [commsTransition]
theorem comms_reflexive (s : CommsState) : commsTransition s s := by
cases s <;> simp [commsTransition]
|