(************************************************************
 *                      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   : 2017/06/29
 *
 * IMITATOR version: 2.9.1
 ************************************************************)

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
(************************************************************)

(* enter your automaton here *)



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

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

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

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



(************************************************************)
(* Property specification *)
(************************************************************)

property := unreachable loc[machine] = cdone;


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