(*******************************************************************************
 *                                IMITATOR MODEL                               
 * 
 * Title            : FischerAHV93
 * Description      : Fischer protocol for mutual exclusion (parametric timed version). Modeled exactly as in [AHV93] although smarter modeling could have been done thanks to the IMITATOR syntax.
 * Correctness      : No two processes in the critical section (i.e., in P1_4 and P2_4 at the same time)
 * Scalable         : 
 * Generated        : 
 * Categories       : Academic ; Protocol ; RTS
 * Source           : Model described in "Parametric Real-Time Reasoning" (fig. 2) Alur, Henzinger, Vardi (STOC 1993)
 * bibkey           : AHV93
 * Author           : Alur, Henzinger, Vardi
 * Modeling         : Alur, Henzinger, Vardi
 * Input by         : Étienne André
 * License          : 
 * 
 * Created          : 2011/11/25
 * Last modified    : 2020/08/14
 * Model version    : 
 * 
 * IMITATOR version : 3
 ******************************************************************************)





var
 	x, x_prime
		: clock;

	a, b, c, d
			: parameter;


(************************************************************)
  automaton lock
(************************************************************)
synclabs: is_0, is_0_prime, is_1, is_1_prime, is_2, is_2_prime,
	set_0, set_0_prime, set_1, set_2_prime
;

loc lock0: invariant True
	when True sync is_0 goto lock0;
	when True sync is_0_prime goto lock0;
	when True sync set_1 goto lock1;
	when True sync set_2_prime goto lock2;

loc lock1: invariant True
	when True sync is_1 goto lock1;
	when True sync is_1_prime goto lock1;
	when True sync set_0 goto lock0;
	when True sync set_0_prime goto lock0;
	when True sync set_2_prime goto lock2;

loc lock2: invariant True
	when True sync is_2 goto lock2;
	when True sync is_2_prime goto lock2;
	when True sync set_1 goto lock1;
	when True sync set_0 goto lock0;
	when True sync set_0_prime goto lock0;

end (*lock*)



(************************************************************)
  automaton P1
(************************************************************)
synclabs: is_0, is_1, is_2, set_0, set_1;

loc P1_0: invariant True
	when True goto P1_0;
	when True goto P1_1;

loc P1_1: invariant True
	when True sync is_2 goto P1_1;
	when True sync is_0 do {x := 0} goto P1_2;

loc P1_2: invariant True
	when c < x & x < d sync set_1 do {x := 0} goto P1_3;

loc P1_3: invariant True
	when a < x & x < b sync is_2 goto P1_1;
	when a < x & x < b sync is_1 goto P1_4;

loc P1_4: invariant True
	when True goto P1_4;
	when True sync set_0 goto P1_0;

end (*P1*)



(************************************************************)
  automaton P2
(************************************************************)
synclabs: is_0_prime, is_1_prime, is_2_prime, set_0_prime, set_2_prime;

loc P2_0: invariant True
	when True goto P2_0;
	when True goto P2_1;

loc P2_1: invariant True
	when True sync is_1_prime goto P2_1;
	when True sync is_0_prime do {x_prime := 0} goto P2_2;

loc P2_2: invariant True
	when c < x_prime & x_prime < d sync set_2_prime do {x_prime := 0} goto P2_3;

loc P2_3: invariant True
	when a < x_prime & x_prime < b sync is_2_prime goto P2_1;
	when a < x_prime & x_prime < b sync is_1_prime goto P2_4;

loc P2_4: invariant True
	when True goto P2_4;
	when True sync set_0_prime goto P2_0;

end (*P2*)


(************************************************************)
(* Initial state *)
(************************************************************)
init :=
	(*----------------------
	-- Initial locations
	----------------------*)
	& loc[lock] = lock0
	& loc[P1]   = P1_0
	& loc[P2]   = P2_0
	
	(*----------------------
	-- Clocks
	----------------------*)

	(*----------------------
	-- Given constraints
	----------------------*)
	& a >= 0
	& b >= 0
	& c >= 0
	& d >= 0

	(*----------------------
	-- Instantiations
	----------------------*)

;


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