(*** WARNING! This IMITATOR model was automatically generated by fischer-novar-gen.py ***)

var
	x1, x2, x3, x4
	: 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 process4
	synclabs: Start4, SetX4, Enter4, SetX04;

	loc idle4: invariant True
		when True sync Start4 do {x4 := 0} goto trying4;

	loc trying4: invariant True
		when x4 < delta sync SetX4 do {x4 := 0} goto waiting4;

	loc waiting4: invariant True
		when x4 > Delta sync Enter4 do {nb := nb + 1} goto critical4;

	loc critical4: invariant True
		when True sync SetX04 do {nb := nb - 1} goto idle4;

end

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

	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 Start4 do {} goto Val0;
	when True sync SetX1 do {} goto Val1;
	when True sync SetX2 do {} goto Val2;
	when True sync SetX3 do {} goto Val3;
	when True sync SetX4 do {} goto Val4;

	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;
	when True sync SetX4 do {} goto Val4;

	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;
	when True sync SetX4 do {} goto Val4;

	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;
	when True sync SetX4 do {} goto Val4;

	loc Val4: invariant True
	when True sync Enter4 do {} goto Val4;
	when True sync SetX04 do {} goto Val0;
	when True sync SetX1 do {} goto Val1;
	when True sync SetX2 do {} goto Val2;
	when True sync SetX3 do {} goto Val3;
	when True sync SetX4 do {} goto Val4;
end

automaton observer

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

	loc obs_BAD: invariant True wait {}
end (* observer *)


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

property := unreachable loc[observer] = obs_BAD;

end