(************************************************************
 *                      IMITATOR MODEL                      
 *
 * Producer/Consumer with n=3 processing nodes of length m=3
 *
 * Description     : The network presented in Figure 2 models the system consisting of the Producer feeding the Consumer with data sent through a sequence of nodes with additional processing capabilities. The model is scalable with respect to the number n of the processing nodes and the length m of each processing node and it contains three lower (a,c,e) and three upper (b,d,f) parameters. Note: the clocks were renamed (w.r.t. to [KP12]) for sake of simplicity.
	WARNING: the first of the valuations in [KP12] does not match the result of IMITATOR!
 * Correctness     : φ2 = ConsWaiting ∧ ProdReady ∧ xtotal ≥ 5
 * Source          : SMT-based Parameter Synthesis for L/U Automata, Michał Knapik and Wojciech Penczek
 * Author          : Michał Knapik and Wojciech Penczek
 * Modeling        : Michał Knapik and Wojciech Penczek
 * Input by        : Étienne André
 *
 * Created         : 2015/09/23
 * Last modified   : 2020/08/18
 *
 * IMITATOR version: 3
 ************************************************************)

var

(* Clocks *)
 	xprod, xnode1, xnode2, xnode3, xcons,
		xtotal,
		: clock;

(* Parameters *)
	a, b, c, d, e, f,
	(* Below are the valuations explicitly given in [KP12] *)
(* 	a = 0, b = 0, c = 0, d = 0, e = 0, f = 0, *)
(* 	a = 1, b = 1, c = 0, d = 1, e = 0, f = 1, *)
(* 	a = 2, b = 2, c = 0, d = 2, e = 0, f = 2, *)
(* 	a = 3, b = 3, c = 0, d = 3, e = 0, f = 3, *)
(* 	a = 4, b = 4, c = 0, d = 4, e = 0, f = 4, *)
(* 	a = 5, b = 5, c = 0, d = 5, e = 0, f = 5, *)
(* 	a = 6, b = 6, c = 0, d = 6, e = 0, f = 6, *)
(* 	a = 7, b = 7, c = 0, d = 7, e = 0, f = 7, *)
(* 	a = 8, b = 8, c = 0, d = 8, e = 0, f = 8, *)
(* 	a = 9, b = 9, c = 0, d = 9, e = 0, f = 9, *)
		: parameter;



(************************************************************)
  automaton Producer
(************************************************************)
synclabs: ProdReset, Feed2;

loc prodReady: invariant xprod <= d
	when xprod >= c sync Feed2 do {xprod := 0} goto prodWaiting;

loc prodWaiting: invariant xprod <= b
	when xprod >= a sync ProdReset do {xprod := 0} goto prodReady;

end (* Producer *)



(************************************************************)
  automaton Consumer
(************************************************************)
synclabs: ConsReset, Feed5;

loc consReady: invariant xcons <= d
	when xcons >= c sync Feed5 do {xcons := 0} goto consWaiting;

loc consWaiting: invariant xcons <= b
	when xcons >= a sync ConsReset do {xcons := 0} goto consReady;

end (* Consumer *)



(************************************************************)
  automaton Node1
(************************************************************)
synclabs: Node1Process1, Node1Process2, Node1Process3, Feed2, Feed3;

loc node1Ready: invariant xnode1 <= d
	when xnode1 >= c sync Feed2 do {xnode1 := 0} goto intermediate1;

loc intermediate1: invariant xnode1 <= f
	when xnode1 >= e sync Node1Process1 do {xnode1 := 0} goto intermediate2;

loc intermediate2: invariant xnode1 <= f
	when xnode1 >= e sync Node1Process2 do {xnode1 := 0} goto intermediate3;

loc intermediate3: invariant xnode1 <= f
	when xnode1 >= e sync Node1Process3 do {xnode1 := 0} goto send;

loc send: invariant xnode1 <= d
	when xnode1 >= c sync Feed3 do {xnode1 := 0} goto node1Ready;

end (* Node1 *)


(************************************************************)
  automaton Node2
(************************************************************)
synclabs: Node2Process1, Node2Process2, Node2Process3, Feed3, Feed4;

loc node2Ready: invariant xnode2 <= d
	when xnode2 >= c sync Feed3 do {xnode2 := 0} goto intermediate1;

loc intermediate1: invariant xnode2 <= f
	when xnode2 >= e sync Node2Process1 do {xnode2 := 0} goto intermediate2;

loc intermediate2: invariant xnode2 <= f
	when xnode2 >= e sync Node2Process2 do {xnode2 := 0} goto intermediate3;

loc intermediate3: invariant xnode2 <= f
	when xnode2 >= e sync Node2Process3 do {xnode2 := 0} goto send;

loc send: invariant xnode2 <= d
	when xnode2 >= c sync Feed4 do {xnode2 := 0} goto node2Ready;

end (* Node2 *)


(************************************************************)
  automaton Node3
(************************************************************)
synclabs: Node3Process1, Node3Process2, Node3Process3, Feed4, Feed5;

loc node3Ready: invariant xnode3 <= d
	when xnode3 >= c sync Feed4 do {xnode3 := 0} goto intermediate1;

loc intermediate1: invariant xnode3 <= f
	when xnode3 >= e sync Node3Process1 do {xnode3 := 0} goto intermediate2;

loc intermediate2: invariant xnode3 <= f
	when xnode3 >= e sync Node3Process2 do {xnode3 := 0} goto intermediate3;

loc intermediate3: invariant xnode3 <= f
	when xnode3 >= e sync Node3Process3 do {xnode3 := 0} goto send;

loc send: invariant xnode3 <= d
	when xnode3 >= c sync Feed5 do {xnode3 := 0} goto node3Ready;

end (* Node3 *)


(************************************************************)
  automaton observer
(************************************************************)

(*** NOTE: as of version 2.10, IMITATOR cannot use clocks in the property; therefore we use an observer to encode the x >= 5 part of the property ***)
loc waiting: invariant xtotal <= 5
	when xtotal = 5 goto finished;

loc finished: invariant True

end (* observer *)


(************************************************************)
(* Initial state *)
(************************************************************)

init :=
	(*------------------------------------------------------------*)
	(* Initial location *)
	(*------------------------------------------------------------*)
	& loc[Producer]	= prodReady
	& loc[Consumer]	= consReady
	& loc[Node1]	= node1Ready
	& loc[Node2]	= node2Ready
	& loc[Node3]	= node3Ready
	& loc[observer]	= waiting

	(*------------------------------------------------------------*)
	(* Initial clock constraints *)
	(*------------------------------------------------------------*)
	& xprod = 0
	& xnode1 = 0
	& xnode2 = 0
	& xnode3 = 0
	& xcons = 0
	& xtotal = 0

	(*------------------------------------------------------------*)
	(* Parameter constraints *)
	(*------------------------------------------------------------*)
	& a >= 0
	& b >= 0
	& c >= 0
	& d >= 0
	& e >= 0
	& f >= 0
;


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