(*******************************************************************************
 *                                IMITATOR MODEL                               
 * 
 * Title            : fischerHRSV02_2
 * Description      : Fischer's mutual exclusion protocol. Version with 2 processes.
 * Correctness      : No two processes in the mutual exclusion
 * Scalable         : in the number of processes
 * Generated        : no
 * Categories       : Academic ; Protocol ; RTS
 * Source           : From "Linear Parametric Model Checking of Timed Automata" Hune, Romijn, Stoelinga, Vaandrager, 2002
 * bibkey           : HRSV02
 * Author           : Hune, Romijn, Stoelinga, Vaandrager
 * Modeling         : Hune, Romijn, Stoelinga, Vaandrager
 * Input by         : Étienne André
 * License          : 
 * 
 * Created          : 2013/12/10
 * Last modified    : 2021/07/09
 * Model version    : 
 * 
 * IMITATOR version : 3.1
 ******************************************************************************)




var 
	
	x_1, (*P1's clock*)
	x_2, (*P2's clock*)
		:clock;
	

	lock
		: int;

	min_rw, max_rw,
	min_delay, max_delay,
		: parameter;


(************************************************************)
automaton process_1
(************************************************************)
synclabs: ;

loc start_1: invariant x_1 <= max_rw
	when lock <> 0 & x_1 > min_rw do {x_1 := 0} goto start_1;

	when lock = 0 & x_1 > min_rw do {x_1 := 0} goto set_1;

loc set_1: invariant x_1 <= max_rw
	(* Actually lock := i *)
	when x_1 > min_rw do {lock := 1, x_1 := 0} goto tryenter_1;

loc tryenter_1: invariant x_1 <= max_delay
	(* Actually lock = i *)
	when x_1 > min_delay & lock = 1 goto cs_1;
	(* Actually lock <> i *)
	when x_1 > min_delay & lock <> 1 do {x_1 := 0} goto start_1;

loc cs_1: invariant True
	when True do {x_1 := 0, lock := 0} goto start_1;

end (*process_1*)



(************************************************************)
automaton process_2
(************************************************************)
synclabs: ;

loc start_2: invariant x_2 <= max_rw
	when lock <> 0 & x_2 > min_rw do {x_2 := 0} goto start_2;

	when lock = 0 & x_2 > min_rw do {x_2 := 0} goto set_2;

loc set_2: invariant x_2 <= max_rw
	(* Actually lock := i *)
	when x_2 > min_rw do {lock := 2, x_2 := 0} goto tryenter_2;

loc tryenter_2: invariant x_2 <= max_delay
	(* Actually lock = i *)
	when x_2 > min_delay & lock = 2 goto cs_2;
	(* Actually lock <> i *)
	when x_2 > min_delay & lock <> 2 do {x_2 := 0} goto start_2;

loc cs_2: invariant True
	when True do {x_2 := 0, lock := 0} goto start_2;

end (*process_2*)



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

init := {
	
    discrete =
		(*------------------------------------------------------------*)
		(* Initial location *)
		(*------------------------------------------------------------*)
		loc[process_1] := start_1,
		loc[process_2] := start_2,

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

    ;

    continuous =        
		(*------------------------------------------------------------*)
		(* Initial clock constraints *)
		(*------------------------------------------------------------*)
		& x_1 = 0
		& x_2 = 0

		(*------------------------------------------------------------*)
		(* Parameter constraints *)
		(*------------------------------------------------------------*)
		& 0 <= min_rw
		& min_rw < max_rw
		& 0 <= min_delay
		& min_delay < max_delay
	;
}



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