(*******************************************************************************
 *                                IMITATOR MODEL                               
 * 
 * Title            : FischerPS08-2
 * 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    : 2024/01/16
 * Model version    : 
 * 
 * IMITATOR version : 3.4
 ******************************************************************************)




var
	x1, x2
	: clock;

	nb
	: discrete;

	delta, Delta
	: parameter;

automaton process1
	actions: 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
	actions: 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
	actions:
	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
		(* Change '2' with any number of processes in CS *)
		when nb = 2 do {} goto obs_BAD;

	loc obs_BAD: invariant True
end (* observer *)


init := {
	discrete =
		loc[process1] := idle1,
		loc[process2] := idle2,
		loc[variable] := Val0,
		loc[observer] := obs_OK,

		nb := 0,
	;

	continuous =
		& x1 = 0
		& x2 = 0
		& Delta >= 0
		& delta >= 0
	;
}

end