(*******************************************************************************
 *                                IMITATOR MODEL                               
 * 
 * Title            : coffeeDrinker_toolpaper
 * Description      : Coffee vending machine; a single button is used to wake the machine up, and to add sugar. Then a cup, and coffee are delivered after a (parametric) time.
 * Correctness      : Many possibilities (e.g., "it is possible to get a coffee")
 * Scalable         : no
 * Generated        : no
 * Categories       : Education ; Toy
 * Source           : Own work
 * bibkey           : 
 * Author           : Étienne André
 * Modeling         : Étienne André
 * Input by         : Étienne André
 * License          : Creative Commons Attribution-ShareAlike 4.0 International (CC BY-SA 4.0)
 * 
 * Created          : 2011/01/21
 * Last modified    : 2021/07/09
 * Model version    : 
 * 
 * IMITATOR version : 3.1
 ******************************************************************************)




var

(* Clocks *)
 	x, y1, y2
		: clock;


(* Parameters *)
	(* time during which one can add sugar *)
	p_add_sugar,
	
	(* time needed to prepare the coffee from the first button pressure *)
	p_coffee,

	
	(* interval of time between 2 consecutive pressures by the user *)
 	p_button (*= 2*),
 	
 	
	(* interval of work without need for coffee *)
	p_work_min = 3600, p_work_max = 7200,
	
	(* time after which the drinker gets mad *)
	p_patience_max = 15,
	
	(* Parametric time before one can get a coffee *)
	p_max = 0,
	
	
	(* First parameter valuation (non-parametric model) *)
(*	p_button = 1,
	p_add_sugar = 4,
	p_coffee = 7 *)
	
	(* Second parameter valuation (non-parametric model) *)
(*	p_button = 2,
	p_add_sugar = 6,
	p_coffee = 8 *)
	
	(* Third parameter valuation (non-parametric model) *)
(*	p_button = 1,
	p_add_sugar = 7,
	p_coffee = 12,
	p_max = 20,*)
	
		: parameter;

	
(* Discrete variables *)
	nb_sugar
		: int;

(* Constants *)
	MAX_SUGAR = 3
		: int;


(************************************************************)
  automaton machine
(************************************************************)
synclabs: press, cup, coffee, sleep;

loc idle: invariant True
	when True sync press do {x := 0} goto add_sugar;

loc add_sugar: invariant x <= p_add_sugar
(* 	when x1 < p_button sync press goto add_sugar; *)
	when True sync press goto add_sugar;
	when x = p_add_sugar sync cup do {x := 0} goto preparing_coffee;

loc preparing_coffee: invariant x <= p_coffee
(* 	when x2 = p_coffee sync coffee goto idle; *)
(* 	when True sync press goto preparing_coffee; *)
	when x = p_coffee sync coffee do {x := 0} goto cdone;

loc cdone: invariant x <= 10
	when True sync press do {x := 0} goto add_sugar;
	when x = 10 sync sleep goto idle;

end (* machine *)


(************************************************************)
  automaton researcher
(************************************************************)
synclabs: press, coffee;

loc researching: invariant y1 <= p_work_max
	when y1 >= p_work_min sync press do {y1 := 0, y2 := 0, nb_sugar := 0} goto add_sugar;

loc add_sugar: invariant y2 <= p_patience_max & y1 <= p_button & nb_sugar <= MAX_SUGAR - 1
	when y1 = p_button & nb_sugar < MAX_SUGAR - 1 sync press do {y1 := 0, nb_sugar := nb_sugar + 1} goto add_sugar;
	when y1 = p_button & nb_sugar = MAX_SUGAR - 1 sync press do {nb_sugar := nb_sugar + 1} goto wait_coffee;
	when y2 = p_patience_max goto mad;
	when True sync coffee goto mad;

loc wait_coffee: invariant y2 <= p_patience_max
	when y2 < p_patience_max sync coffee do {y1 := 0, y2 := 0} goto researching;
	when y2 = p_patience_max goto mad;

loc mad: invariant True
	(* Self-loop to avoid deadlocks when the researcher is already mad *)
	when True sync coffee goto mad;

end (* researcher *)


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

init := {
	
    discrete =
		(*------------------------------------------------------------*)
		(* Initial location *)
		(*------------------------------------------------------------*)
		loc[machine]		:= idle,
		loc[researcher]		:= researching,

		(*------------------------------------------------------------*)
		(* Initial discrete variables assignments *)
		(*------------------------------------------------------------*)
		nb_sugar := 0,

    ;

    continuous =        
		(*------------------------------------------------------------*)
		(* Initial clock constraints *)
		(*------------------------------------------------------------*)
		& x = 0

		(*------------------------------------------------------------*)
		(* Parameter constraints *)
		(*------------------------------------------------------------*)
		& y1 >= 0 & y1 <= p_work_max (* working since some time *)
		& y2 >= 0 (* arbitrary *)
		& p_button > 0
		& p_add_sugar > 0
		& p_coffee > 0
	(* 	& p_press >= 0 *)
		& p_work_min >= 0
		& p_work_min <= p_work_max
		& p_patience_max >= 0
		
		& p_max >= 0
	;
}



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