(*******************************************************************************
 *                                IMITATOR MODEL                               
 * 
 * Title            : coffee
 * Description      : Coffee machine (no coin, coffee is free!); 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         : 
 * Generated        : 
 * Categories       : Education ; Toy
 * Source           : Own work
 * bibkey           : 
 * Author           : Étienne André
 * Modeling         : 
 * Input by         : Étienne André
 * License          : 
 * 
 * Created          : 2011/01/21
 * Last modified    : 2020/08/13
 * Model version    : 
 * 
 * IMITATOR version : 3
 ******************************************************************************)




var

(* Clocks *)
 	x, y
		: clock;

(* Parameters *)
	p1, (* The minimum time between two consecutive requests for sugar *)
	p2, (* The time during which one can request sugar *)
	p3, (* The total time necessary to prepare coffee *)
		: parameter;



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

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

loc add_sugar: invariant y <= p2
	when x >= p1 sync press do {x := 0} goto add_sugar;
	when y = p2 sync cup do {} goto preparing_coffee;

loc preparing_coffee: invariant y <= p3
(* 	when y = p3 sync coffee goto idle; *)
	when y = p3 sync coffee do {x := 0} goto cdone;

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

end (* machine *)



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

init :=
	(*------------------------------------------------------------*)
	(* Initial location *)
	(*------------------------------------------------------------*)
	& loc[machine] = idle

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

	(*------------------------------------------------------------*)
	(* Parameter constraints *)
	(*------------------------------------------------------------*)
	& p1 >= 0
	& p2 >= 0
	& p3 >= 0
;



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