-- Kai's two-phase-commit example.
-- One coordinator, two agents.
-- Use actions rather than shared variables, to handle arbitrary crashing.

type LiftedBool = {Bottom, False1, True1}

-- Environment state.
votes    : LiftedBool[3]
decision : LiftedBool
commit   : LiftedBool[3]
crash    : Bool[3]

-- Agents can fail to even start.
init_cond = (votes[0] == Bottom /\ votes[1] == Bottom /\ votes[2] == Bottom)
	 /\ decision == Bottom
	 /\ (commit[0] == Bottom /\ commit[1] == Bottom /\ commit[2] == Bottom)

agent M "tpc_coord"    ( votes )
agent A "tpc_protocol" ( decision )
agent B "tpc_protocol" ( decision )

transitions
begin
  -- Any agent can crash at any time.
  if True -> crash[0] := True
  [] True -> skip
  fi;
  if True -> crash[1] := True
  [] True -> skip
  fi;
  if True -> crash[2] := True
  [] True -> skip
  fi;

  -- Consider an agent's vote, provided they haven't crashed.
  if neg crash[1] ->
    if A.VoteToCommit -> votes[1] := True1
    [] A.VoteToAbort  -> votes[1] := False1
    fi
  fi;
  if neg crash[2] ->
    if B.VoteToCommit -> votes[2] := True1
    [] B.VoteToAbort  -> votes[2] := False1
    fi
  fi;

  -- Update the broadcast, provided the coordinator hasn't crashed.
  if neg crash[0] ->
    if M.BroadcastCommit -> decision := True1
    [] M.BroadcastAbort  -> decision := False1
    fi
  fi;

  -- Consider an agent's commit decision, provided they haven't crashed.
  if neg crash[0] ->
    if M.Commit -> commit[0] := True1
    [] M.Abort  -> commit[0] := False1
    fi
  fi;
  if neg crash[1] ->
    if A.Commit -> commit[1] := True1
    [] A.Abort  -> commit[1] := False1
    fi
  fi;
  if neg crash[2] ->
    if B.Commit -> commit[2] := True1
    [] B.Abort  -> commit[2] := False1
    fi
  fi
end

-- After the first phase, Agent 1 knows whether everyone wants to commit.
spec_obs_ctl = AX (neg (crash[0] \/ crash[1] \/ crash[2])
             /\ (M.vote /\ A.vote /\ B.vote))
	       => Knows M (M.vote /\ A.vote /\ B.vote)
		  
-- After the second phase, everyone either crashed, committed, or aborted.
spec_obs_ctl = AX AX AX
   ((crash[0] \/ (commit[0] /= Bottom /\ (decision == True1 <=> commit[0] == True1)))
 /\ (crash[1] \/ (commit[1] /= Bottom /\ (decision == True1 <=> commit[1] == True1)))
 /\ (crash[2] \/ (commit[2] /= Bottom /\ (decision == True1 <=> commit[2] == True1))))

-- Phrase the overall spec as a knowledge formula.
spec_obs_ctl = AX AX AX
	      (commit[0] == True1 => Knows M (M.vote /\ A.vote /\ B.vote))
           /\ (commit[1] == True1 => Knows A (M.vote /\ A.vote /\ B.vote))
           /\ (commit[2] == True1 => Knows B (M.vote /\ A.vote /\ B.vote))

-- If the coordinator crashes, no-one commits, unless the decision has
-- already been made before the crash.
-- So, decision == Bottom is interpreted to mean "abort".
spec_obs_ctl = AG
  crash[0] =>
    (decision == Bottom
      /\ commit[0] /= True1 /\ commit[1] /= True1 /\ commit[2] /= True1)
  \/ decision == True1

-- Coordinator's protocol.
protocol "tpc_coord"
	     (
	      votes : observable LiftedBool[3]
	     )
vote : observable Bool

begin
  -- Collect the votes.
  skip;
  if vote /\ votes[1] == True1 /\ votes[2] == True1
  then
    begin
      << BroadcastCommit >>;
      << Commit >>
    end
  else
    begin
      << BroadcastAbort >>;
      << Abort >>
    end
end

-- Non-coordinator's protocol. (Kai's "optimised" version)
-- Agents can abort straight away, if they want to.
protocol "tpc_protocol"
	     (
	      decision : observable LiftedBool
	     )
vote : observable Bool

begin
  if vote
  then
    begin
      << VoteToCommit >>;
      skip; -- Wait for broadcast from Agent 1.
      if decision == True1
        then << Commit >>
        else << Abort >>
    end
  else
    begin
      << VoteToAbort >>;
      << Abort >>
    end
end