protocol.v 729 Bytes
Newer Older
Zhen Zhang's avatar
Zhen Zhang committed
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31
From iris.algebra Require Export sts.
From iris.program_logic Require Import ghost_ownership.
From iris.prelude Require Export gmap.

Inductive state :=
  | Init
  | Req
  | Exec
  | Resp
  | Ack.

Inductive token := White | Black | Lock.

Global Instance stateT_inhabited: Inhabited state := populate Init.

Inductive prim_step : relation state :=
  | Initialize: prim_step Init Req
  | Execute: prim_step Req Exec
  | Respond: prim_step Exec Resp
  | Acknowledge: prim_step Resp Ack.

Definition tok (s : state) : set token :=
  match s with
  | Init | Ack  => {[ Black; White ]}
  | Req  | Resp => {[ White ]}
  | Exec        => {[ Lock ]}
  end.

Global Arguments tok !_ /.

Canonical Structure sts := sts.STS prim_step tok.