(************************************************************
 *                      IMITATOR MODEL                      
 *
 * Coffee machine
 *
 * 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")
 * Source          : Own work
 * Author          : Étienne André
 * Input by        : Étienne André, Laure Petrucci
 *
 * Created         : 2011/01/21
 * Last modified   : 2020/11/23
 *
 * IMITATOR version: 3.0
 ************************************************************)

var

(* Clocks *)
 	x, y
		: clock;

(* Parameters *)
	p1, p2, p3
		: parameter;



(************************************************************)
  automaton machine
(************************************************************)


(* enter your automaton here *)

end (* machine *)

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

init :=
	(*------------------------------------------------------------
	   INITIAL LOCATION
	  ------------------------------------------------------------*)
	& loc[machine] = idle

	(*------------------------------------------------------------
	   INITIAL CLOCKS
	  ------------------------------------------------------------*)
	& x = 0
	& y = 0

	(*------------------------------------------------------------
	   INITIAL DISCRETE
	  ------------------------------------------------------------*)

	(*------------------------------------------------------------
	   PARAMETER CONSTRAINTS
	  ------------------------------------------------------------*)
	& p1 >= 0
	& p2 >= 0
	& p3 >= 0
;

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