(************************************************************
 *                      IMITATOR MODEL                      
 *
 * Fischer's mutual exclusion protocol
 *
 * Description     : Fischer's mutual exclusion protocol with 2 processes
 * Correctness     : The mutual exclusion is ensured
 * Source          : ?
 * Author          : ?
 * Modeling        : Romain Soulat
 * Input by        : Romain Soulat, Étienne André
 * License         : Creative Commons Attribution-ShareAlike 4.0 International (CC BY-SA 4.0)
 *
 * Created         : < 2012/02/14
 * Last modified   : 2020/08/14
 *
 * IMITATOR version: 3
 ************************************************************)
 
var 
(* Clocks *)
	x1, (* P1's clock *)
	x2  (* P2's clock *)
		:clock;
	

(* Discrete *)
	k
		: discrete;

(* Parameters *)
	a,
	b
		: parameter;



(************************************************************)
automaton proc1
(************************************************************)
synclabs : tau,start1,set1,enter1,abort1,release1;


loc idle: invariant True
	when k=0 sync start1 do {x1 := 0} goto start;
	when True sync tau goto idle;
	
loc start: invariant x1<=a
	when True sync set1 do {k := 1, x1 := 0} goto check;
	when True sync tau goto start;

loc check: invariant True
	when k=1 & x1>=b sync enter1 goto CS;
	when k<1 & x1>=b sync abort1 goto idle;
	when k>1 & x1>=b sync abort1 goto idle;
	when True sync tau goto check;

loc CS: invariant True
	when True sync release1 do {k := 0} goto idle;
	when True sync tau goto CS;
end

(************************************************************)
automaton proc2
(************************************************************)
synclabs : tau,start2,set2,enter2,abort2,release2;


loc idle: invariant True
	when k=0 sync start2 do {x2 := 0} goto start;
	when True sync tau goto idle;
	
loc start: invariant x2<=a
	when True sync set2 do {k := 2, x2 := 0} goto check;
	when True sync tau goto start;

loc check: invariant True
	when k=2 & x2>=b sync enter2 goto CS;
	when k<2 & x2>=b sync abort2 goto idle;
	when k>2 & x2>=b sync abort2 goto idle;
	when True sync tau goto check;

loc CS: invariant True
	when True sync release2 do {k := 0} goto idle;
	when True sync tau goto CS;
end

(************************************************************)
automaton arbitrer
(************************************************************)
synclabs : set1,release1,
           set2,release2,
	   tau;
	   

loc loc_arbitrer: invariant True
	when True sync set1 goto loc_arbitrer;
	when True sync release1 goto loc_arbitrer;
	when True sync set2 goto loc_arbitrer;
	when True sync release2 goto loc_arbitrer;
	when True sync tau goto loc_arbitrer;
end



(************************************************************)
(* Initial state *)
(************************************************************)

init :=
	(*------------------------------------------------------------*)
	(* Initial location *)
	(*------------------------------------------------------------*)
	& loc[proc1] = idle
	& loc[proc2] = idle
	& loc[arbitrer] = loc_arbitrer

	(*------------------------------------------------------------*)
	(* Initial discrete assignments *)
	(*------------------------------------------------------------*)
	& k=0

	(*------------------------------------------------------------*)
	(* Initial clock constraints *)
	(*------------------------------------------------------------*)
	& x1 = 0
	& x2 = 0

	(*------------------------------------------------------------*)
	(* Parameter constraints *)
	(*------------------------------------------------------------*)
	& a >= 0
	& b >= 0
;


(************************************************************)
(* The end *)
(************************************************************)
end