two_phase_commit.pml

mtype = { Ready, NotReady, Commit, Abort }
chan from_arbiter[4] = [1] of { mtype };
chan from_worker[4] = [1] of { mtype };

active proctype Arbiter() {
  assert (_pid == 0);
  mtype v1, v2, v3;
  from_arbiter[1]!Ready;
  from_arbiter[2]!Ready;
  from_arbiter[3]!Ready;
  from_worker[1]?v1;
  from_worker[2]?v2;
  from_worker[3]?v3;
  if
  :: v1 == NotReady || v2 == NotReady || v3 == NotReady ->
     from_arbiter[1]!Abort;
     from_arbiter[2]!Abort;
     from_arbiter[3]!Abort;
  :: else
     from_arbiter[1]!Commit;
     from_arbiter[2]!Commit;
     from_arbiter[3]!Commit;
  fi
}

active [3] proctype Worker() {
  assert (1 <= _pid && _pid <= 4);
  mtype v;
  from_arbiter[_pid]?v;
  assert (v == Ready);
  if
  :: true ->
     from_worker[_pid]!NotReady;
     from_arbiter[_pid]?v;
     assert (v == Abort)
  :: true ->
     from_worker[_pid]!Ready;
     from_arbiter[_pid]?v;
     assert (v == Abort || v == Commit)
  fi
}