(*******************************************************************************
 *                                IMITATOR MODEL                               
 * 
 * Title            : coffeeDrinker_unbounded
 * 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      : The scientist never gets mad
 * 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 *)
 	x1, x2, y1, y2
		: clock;

(* Parameters *)
	(* time during which the button cannot be pressed after a pressure *)
(* 	p_block_button, *)
	(* 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 work without need for coffee *)
	p_work_min,
	p_work_max,
	(* Minimal interval of time between 2 consecutive pressures by the user *)
	p_press_min,
	(* time after which the drinker gets mad *)
	p_patience_max,
		: parameter;

(* Discrete variables *)
	nb_sugar
		: int;

(* Constants *)
(*	MAX_SUGAR = 2
		: int;
*)

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

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

loc add_sugar: invariant x2 <= p_add_sugar & x2 <= p_coffee
	when (*x1 >= p_block_button*)True sync press do {x1 := 0} goto add_sugar;
	when x2 = p_add_sugar sync cup do {} goto preparing_coffee;

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

loc cdone: invariant x1 <= 10
	when True sync press do {x1 := 0, x2 := 0} goto add_sugar;
	when x1 = 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;

(*** TODO: an improvement would be to first nonderministically chose the number of sugars to add, and then to indeed add it (and get mad if it is impossible to get a coffee with this number); otherwise, the scientist may not get the desired number of sugards depending on the relationship between p_press_min and p_add_sugar ***)
loc add_sugar: invariant y2 <= p_patience_max
	(* Can always add more sugar *)
	when y1 >= p_press_min sync press do {y1 := 0, nb_sugar := nb_sugar + 1} goto add_sugar;
	(* Can also non-deterministically stop adding sugar and wait for coffee *)
	when True goto wait_coffee;
	when y2 = p_patience_max 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

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 *)
		(*------------------------------------------------------------*)
		& x1 = 0
		& x2 = 0

		(*------------------------------------------------------------*)
		(* Parameter constraints *)
		(*------------------------------------------------------------*)
		& y1 >= 0 & y1 <= p_work_max
	(* 	& p_block_button >= 0 *)
		& p_add_sugar >= 0
		& p_coffee >= 0
		& p_press_min >= 0
		& p_work_min >= 0
		& p_work_min <= p_work_max
		& p_patience_max >= 0	;
}
;


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