(*******************************************************************************
 *                                IMITATOR MODEL                               
 * 
 * Title            : fischer_2
 * Description      : Fischer's mutual exclusion protocol with 2 processes
 * Correctness      : The mutual exclusion is ensured
 * Scalable         : 
 * Generated        : 
 * Categories       : Academic ; Protocol ; RTS
 * Source           : ?
 * bibkey           : 
 * 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    : 2021/07/09
 * Model version    : 
 * 
 * IMITATOR version : 3.1
 ******************************************************************************)



 
var 
(* Clocks *)
	x1, (* P1's clock *)
	x2  (* P2's clock *)
		:clock;
	

(* Discrete *)
	k
		: int;

(* 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 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 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 := {
	
    discrete =
		(*------------------------------------------------------------*)
		(* Initial location *)
		(*------------------------------------------------------------*)
		loc[proc1]		:= idle,
		loc[proc2]		:= idle,
		loc[arbitrer]	:= loc_arbitrer,

		(*------------------------------------------------------------*)
		(* Initial discrete variables assignments *)
		(*------------------------------------------------------------*)
		k := 0,

    ;

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

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


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