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

var
	x1, x2
	: 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 variable
	synclabs:
	Start1, SetX1, Enter1, SetX01, Start2, SetX2, Enter2, SetX02;

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

	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;

	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;
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[variable] = Val0
	& loc[observer] = obs_OK
	& x1 = 0
	& x2 = 0
	& nb = 0
	& Delta >= 0
	& delta >= 0;

property := unreachable loc[observer] = obs_BAD;

end