(*******************************************************************************
 *                                IMITATOR MODEL                               
 * 
 * Title            : FischerPS08-3
 * Description      : 
 * Correctness      : 
 * Scalable         : yes
 * Generated        : yes
 * Categories       : Academic ; Protocol ; RTS
 * Source           : Wojciech Penczek, Maciej Szreter. SAT-based Unbounded Model Checking of Timed Automata. Fundam. Inform. 85(1-4): 425-440 (2008)
 * bibkey           : PS08
 * Author           : Wojciech Penczek and Maciej Szreter
 * Modeling         : Wojciech Penczek and Maciej Szreter
 * Input by         : Étienne André
 * License          : 
 * 
 * Created          : 
 * Last modified    : 
 * Model version    : 
 * 
 * IMITATOR version : 3
 ******************************************************************************)




var
	x1, x2, x3
	: clock;

	nb
	: discrete;

	delta, Delta
	: parameter;

automaton process1
	synclabs: Start1, SetX1, Enter1, SetX01;

	loc idle1: invariant True
		when True sync Start1 do {x1 := 0} goto trying1;

	loc trying1: invariant True
		when x1 < delta sync SetX1 do {x1 := 0} goto waiting1;

	loc waiting1: invariant True
		when x1 > Delta sync Enter1 do {nb := nb + 1} goto critical1;

	loc critical1: invariant True
		when True sync SetX01 do {nb := nb - 1} goto idle1;

end

automaton process2
	synclabs: Start2, SetX2, Enter2, SetX02;

	loc idle2: invariant True
		when True sync Start2 do {x2 := 0} goto trying2;

	loc trying2: invariant True
		when x2 < delta sync SetX2 do {x2 := 0} goto waiting2;

	loc waiting2: invariant True
		when x2 > Delta sync Enter2 do {nb := nb + 1} goto critical2;

	loc critical2: invariant True
		when True sync SetX02 do {nb := nb - 1} goto idle2;

end

automaton process3
	synclabs: Start3, SetX3, Enter3, SetX03;

	loc idle3: invariant True
		when True sync Start3 do {x3 := 0} goto trying3;

	loc trying3: invariant True
		when x3 < delta sync SetX3 do {x3 := 0} goto waiting3;

	loc waiting3: invariant True
		when x3 > Delta sync Enter3 do {nb := nb + 1} goto critical3;

	loc critical3: invariant True
		when True sync SetX03 do {nb := nb - 1} goto idle3;

end

automaton variable
	synclabs:
	Start1, SetX1, Enter1, SetX01, Start2, SetX2, Enter2, SetX02, Start3, SetX3, Enter3, SetX03;

	loc Val0: invariant True
	when True sync Start1 do {} goto Val0;
	when True sync Start2 do {} goto Val0;
	when True sync Start3 do {} goto Val0;
	when True sync SetX1 do {} goto Val1;
	when True sync SetX2 do {} goto Val2;
	when True sync SetX3 do {} goto Val3;

	loc Val1: invariant True
	when True sync Enter1 do {} goto Val1;
	when True sync SetX01 do {} goto Val0;
	when True sync SetX1 do {} goto Val1;
	when True sync SetX2 do {} goto Val2;
	when True sync SetX3 do {} goto Val3;

	loc Val2: invariant True
	when True sync Enter2 do {} goto Val2;
	when True sync SetX02 do {} goto Val0;
	when True sync SetX1 do {} goto Val1;
	when True sync SetX2 do {} goto Val2;
	when True sync SetX3 do {} goto Val3;

	loc Val3: invariant True
	when True sync Enter3 do {} goto Val3;
	when True sync SetX03 do {} goto Val0;
	when True sync SetX1 do {} goto Val1;
	when True sync SetX2 do {} goto Val2;
	when True sync SetX3 do {} goto Val3;
end

automaton observer

	loc obs_OK: invariant True
		(* Change '2' with any number of processes in CS *)
		when nb = 2 do {} goto obs_BAD;

	loc obs_BAD: invariant True
end (* observer *)


	init := True
	& loc[process1] = idle1
	& loc[process2] = idle2
	& loc[process3] = idle3
	& loc[variable] = Val0
	& loc[observer] = obs_OK
	& x1 = 0
	& x2 = 0
	& x3 = 0
	& nb = 0
	& Delta >= 0
	& delta >= 0;

end