(************************************************************
 *                      IMITATOR MODEL                      
 *
 * Empty template of a case study
 *
 * Description     : Packaging system
 * Correctness     : Risk unreachable (??)
 * Source          : https://github.com/astefano/efsmt_coverts/tree/master/imitator_examples/Imitator/packaging
 * Author          : Lacramioara Astefanoaei
 * Modeling        : Lacramioara Astefanoaei
 * Input by        : Lacramioara Astefanoaei / Étienne André
 * License         : Creative Commons Attribution-ShareAlike 4.0 International (CC BY-SA 4.0)
 *
 * Created         : 2017/01/18
 * Last modified   : 2020/08/13
 *
 * IMITATOR version: 3
 ************************************************************)

var

(* Clocks *)
 	x,y 
		: clock;

(* Parameters *)
	a, b: parameter;



(************************************************************)
  automaton FFS
(************************************************************)
synclabs: fillm, shipm, resumem, errpm;

loc f0: invariant True
	when True sync fillm do {x := 0} goto f1;

loc f1: invariant x <= 2
	when True sync errpm do {x := 0} goto f2;
	when x <= 1 sync shipm do {x := 0} goto f0;

loc f2: invariant x <= b
	when x >= a sync resumem do {x := 0} goto f1;

end


(************************************************************)
automaton Monitor
(************************************************************)
synclabs: packm, fillm, shipm, errpm, resolvem, resumem;

loc m0: invariant True
	when True sync fillm do {} goto m1;
	when True sync packm do {} goto m0;

loc m1: invariant True
	when True sync errpm do {} goto m2;
	when True sync packm do {} goto m1;
	when True sync shipm do {} goto m0;

loc m2: invariant True
	when True sync resumem do {} goto m3;
	when True sync resolvem do {} goto m1;

loc m3: invariant True
	when True sync resolvem do {} goto m1;
	when True sync shipm do {} goto risk;

loc risk: invariant True
(*	when True sync resolvem do {} goto risk;
	when True sync shipm do {} goto risk;
	when True sync fillm do {} goto risk;
	when True sync resumem do {} goto risk;	
	when True sync packm do {} goto risk;
	when True sync errpm do {} goto risk;*)

end


(************************************************************)
automaton Packaging
(************************************************************)

synclabs: packm, resolvem, errpm;

loc p0: invariant y <= 5
	when True sync packm do {y := 0} goto p0;
	when True sync errpm do {y := 0} goto p1;

loc p1: invariant y <= 50
	when y >= 10 sync resolvem do {y := 0} goto p0;

end


(************************************************************)
(* Original synchronization model *)
(************************************************************)
(*ship , shipm

pack , packm

resume , resumem

fill , fillm

err , errp, errm

pack , packm

resolve , resolvem*)


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

init :=
	(*------------------------------------------------------------*)
	(* Initial location *)
	(*------------------------------------------------------------*)
	& loc[FFS] = f0
	& loc[Monitor] = m0
	& loc[Packaging] = p0

	(*------------------------------------------------------------*)
	(* Initial clock constraints *)
	(*------------------------------------------------------------*)
	& x = 0
	& y = 0 (*** NOTE: in the original model, y=0 was ommitted; error?? ***)

	(*------------------------------------------------------------*)
	(* Parameter constraints *)
	(*------------------------------------------------------------*)
	& a >= 0
	& b >= 0
;

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