peterson.csp

nametype t = 0..1

event P_begin, P_end
event Q_begin, Q_end

channel rd_flag0, wr_flag0 : t
channel rd_flag1, wr_flag1 : t
channel rd_turn, wr_turn : t

VAR(rd, wr, m) =
     rd!m -> VAR(rd, wr, m)
  [] wr?x -> VAR(rd, wr, x)

P = wr_flag0!1 -> wr_turn!1 -> P1
P1 = rd_flag1?flag1 -> rd_turn?turn ->
     if flag1 == 1 and turn == 1 then P1 else
     P_begin -> P_end -> wr_flag0!0 -> P

Q = wr_flag1!1 -> wr_turn!0 -> Q1
Q1 = rd_flag0?flag0 -> rd_turn?turn ->
     if flag0 == 1 and turn == 0 then Q1 else
     Q_begin -> Q_end -> wr_flag1!0 -> Q

VARS =   VAR(rd_flag0, wr_flag0, 0)
     ||| VAR(rd_flag1, wr_flag1, 0)
     ||| VAR(rd_turn, wr_turn, 0)

X = {| rd_flag0, wr_flag0, rd_flag1, wr_flag1, rd_turn, wr_turn |}

SYSTEM = ((P ||| Q) [|X|] VARS) \ X

SAFETY =
     P_begin -> P_end -> SAFETY
  [] Q_begin -> Q_end -> SAFETY

check SAFETY [T= SYSTEM