(*******************************************************************************
 *                                IMITATOR MODEL                               
 * 
 * Title            : Pipeline_KP12_3_2
 * 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.
 * Correctness      : φ2 = ConsWaiting ∧ ProdReady ∧ xtotal ≥ 5
 * Scalable         : yes
 * Generated        : 
 * Categories       : Academic ; ProdCons
 * Source           : SMT-based Parameter Synthesis for L/U Automata, Michał Knapik and Wojciech Penczek
 * bibkey           : KP12
 * Author           : Michał Knapik and Wojciech Penczek
 * Modeling         : Michał Knapik and Wojciech Penczek
 * Input by         : Étienne André
 * License          : 
 * 
 * Created          : 2018/08/20
 * Last modified    : 2020/08/18
 * Model version    : 
 * 
 * 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, *) (*False*)
(* 	a = 0, b = 1, c = 1, d = 3, e = 0, f = 0, *) (*False*)
(* 	a = 1, b = 1, c = 0, d = 1, e = 0, f = 0, *) (*True*)
(* 	a = 0, b = 3, c = 1, d = 7, e = 1, f = 1, *) (*False*)
(* 	a = 1, b = 2, c = 2, d = 6, e = 0, f = 0, *) (*False*)
(*  	a = 2, b = 2, c = 0, d = 1, e = 0, f = 1,  (*False*) *)
(* 	a = 1, b = 1, c = 1, d = 4, e = 0, f = 0, *) (*True*)
(* 	a = 1, b = 1, c = 1, d = 3, e = 0, f = 0, *) (*False*)
(* 	a = 3, b = 3, c = 0, d = 2, e = 0, f = 1, *) (*True*)
(* 	a = 0, b = 2, c = 0, d = 4, e = 1, f = 1, *) (*False*)
		: 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, 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 send;

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

end (* Node1 *)


(************************************************************)
  automaton Node2
(************************************************************)
synclabs: Node2Process1, Node2Process2, 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 send;

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

end (* Node2 *)


(************************************************************)
  automaton Node3
(************************************************************)
synclabs: Node3Process1, Node3Process2, 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 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