crash.cub

(* ********************************************************************************* *
 * T. D. Chandra and S. Toueg.
 * Time and message efficient reliable broadcasts.
 * In Proceedings of the 4th international workshop on Distributed algorithms,
 * pages 289-303, New York, NY, USA, 1991.
 * 
 *
 * Protocol 1, CRASH FAILURES
 * 
 * 1st round..................................transitions 1,2
 * 1st --> 2nd round..........................transitions 3,4
 * 2nd round..................................transitions 5,6
 * 2nd --> 3rd round..........................transition  7
 * 3rd round..................................transitions 8,9
 * 3rd --> 4th round..........................transition  10
 * 4th round (coordinator election)...........transition  11
 * coord election after coord crash...........transition  12
 * decided processes..........................transition  13
 *
 * ********************************************************************************* *)
 
(*

	(* Round of the execution *)
	global nat round [nat]
	(* estimate of the processes (true = m; false = undefined) *)
	local bool estimate [nat]
	(* state of the processes (true = decided; false = undecided) *)
	local bool state [nat]
	(* who's the coordinator *)
	local bool coord [nat]
	(* who has already been coordinator *)
	local bool aCoord [nat]
	(* processes that has done the operations of the round *)
	local bool done [nat]
	(* someone sent a request? *)
	global bool request [nat]
	(* decision value of the processes (as estimate)*)
	local bool decisionValue [nat]

*)

var Round : int
var Request : bool

array Estimate[proc] : bool
array State[proc] : bool 
array Coord[proc] : bool
array ACoord[proc] : bool 
array Done[proc] : bool
array DecisionValue[proc] : bool

(* initial configuration *)
init (x) {
  Round = 1 && State[x] = False && Coord[x] = False &&
  ACoord[x] = False && Done[x] = False && Request = False
}

(* unsafe configuration (agreement) *)
unsafe (x y) {
  State[x] = True && State[y] = True && 
  DecisionValue[x] <> DecisionValue[y]
}

(* 1) An undecided process sends a request message to the coordinator *)
transition t1 (x y)
requires { Round = 1 && Done[x] = False && State[x] = False && Coord[y] = True }
{ 
  Request := True; 
  Done[j] := case 
              | j = x : True 
	      | _ : Done[j] 
}

(* 2) If the coordinator is not decided sends a request to himself *)
transition t2 (x)
requires { Round = 1 && Coord[x] = True && Done[x] = False && State[x] = False }
{ 
  Request := True;
  Done[j] := case 
  	      | j = x : True 
	      | _ : Done[j] 
}

(* 3) If the coordinator received at least one request the system goes in round 2 *)
transition t3 (x)
requires { Round = 1 && Request = True && Coord[x] = True && Done[x] = True &&
	   forall_other j. Done[j] = True }
{ 
  Round := 2;
  Done[j] := case 
  	      | _ : False 
}


(* 4) If the coordinator didn't received any request is dismissed *)
transition t4(x)
requires { Round = 1 && Request = False && Coord[x] = True && Done[x] = True &&
	   forall_other j. Done[j] = True }
{ 
  Coord[j] := case 
  	       | j = x : False 
	       | _ : Coord[j] ;
  ACoord[j] := case 
  	        | j = x : True 
		| _ : ACoord[j] 
}

(* 5) The coordinator sends his estimate to an undecided process *)
transition t5(x y)
requires { Round = 2 && Done[x] = False && State[x] = False && Coord[y] = True }
{ 
  Estimate[j] := case 
  	      	  | j = x : Estimate[y] 
		  | _ : Estimate[j] ;
  Done[j] := case 
  	      | j = x : True 
	      | _ : Done[j] 
}

(* 6) The undecided coordinator does nothing in this round *)
transition t6(x)
requires { Round = 2 && State[x] = False && Done[x] = False && Coord[x] = True }
{ 
  Done[j] := case 
  	      | j = x : True 
	      | _ : Done[j] 
}

(* 7) Round 2 completed. System goes to round 3 *)
transition t7(x)
requires { Round = 2 && Done[x] = True && Coord[x] = True && 
	   forall_other j. Done[j] = True }
{ 
  Round := 3;
  Done[j] := case | _ : False 
}


(* 8) Coordinator sends a 'decide' message to an undecided process *)
transition t8 (x y)
requires { Round = 3 && Done[x] = False && State[x] = False && Coord[y] = True }
{ 
  State[j] := case 
  	       | j = x : True 
	       | _ : State[j] ;
  Done[j] := case 
  	       | j = x : True 
	       | _ : Done[j] ;
  DecisionValue[j] := case 
  		       | j = x : Estimate[x] 
		       | _ : DecisionValue[j] 
}

(* 9) If the coordinator is undecided takes a decision. *)
transition t9(x)
requires { Round = 3 && Done[x] = False && State[x] = False && Coord[x] = True }
{ 
  State[j] := case 
  	       | j = x : True 
	       | _ : State[j] ;
  Done[j] := case 
  	       | j = x : True 
	       | _ : Done[j] ;
  DecisionValue[j] := case 
  		       | j = x : Estimate[x] 
		       | _ : DecisionValue[j] 
}


(* 10) Round 3 completed. System goes to round 4 *)
transition t10(x)
requires { Round = 3 && Done[x] = True && Coord[x] = True && 
	  forall_other j. Done[j] = True }
{ 
  Round := 4 ;
  Done[j] := case | _ : False 
}

(* 11) The coordinator in office is dismissed, a new process is elected as coordinator.
       The system restarts from round 1 *)
transition t11 (x y)
requires { Round = 4 && Coord[x] = True && Coord[y] = False && 
	  ACoord[y] = False }
{ 
  Round := 1 ; 
  Request := False ;
  ACoord[j] := case 
  	        | j = x : True 
		| _ : ACoord[j] ;
  Done[j] := case | _ : False ;
  Coord[j] := case 
  	       | j = x : False 
	       | j = y : True 
	       | _ : Coord[j] 
}

(* 12) If there's no coordinator (maybe the coordinator in office crashed)
       a new one is elected and the system restarts from round 1 *)
transition t12 (x)
requires { Coord[x] = False && ACoord[x] = False &&	
	  forall_other j. Coord[j] = False }
{ 
  Round := 1 ; 
  Request := False ;
  Coord[j] := case 
  	       | j = x : True 
	       | _ : Coord[j] ;
  Done[j] := case | _ : False 
}


(* 13) Decided processes follow undecided ones doing nothing *)
transition t13 (x)
requires { State[x] = True && Done[x] = False }
{ 
  Done[j] := case 
  	      | j = x : True 
	      | _ : Done[j] 
}