(************************************************************
 *                      IMITATOR MODEL                      
 *
 * Coffee machine
 *
 * 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")
 * Source          : Own work
 * Author          : Étienne André
 * Input by        : Étienne André
 *
 * Created         : 2011/01/21
 * Last modified   : 2020/08/13
 *
 * 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