(************************************************************
 *                      IMITATOR MODEL                      
 *
 * Fischer protocol for mutual exclusion (parametric timed version)
 *
 * 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)
 * Source          : Model described in "Parametric Real-Time Reasoning" (fig. 2) Alur, Henzinger, Vardi (STOC 1993)
 * Author          : Alur, Henzinger, Vardi
 * Modeling        : Alur, Henzinger, Vardi
 * Input by        : Etienne Andre
 *
 * Created         : 2011/11/25
 * Last modified   : 2018/11/13
 *
 * IMITATOR version: 2.10.4
 ************************************************************)


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
	----------------------

;


(************************************************************)
(* Property specification *)
(************************************************************)
property := unreachable loc[P1] = P1_4 & loc[P2] = P2_4;


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