(************************************************************
 *                      IMITATOR MODEL                      
 *
 * Coffee vending machine with drinker. Version for an IMITATOR tool paper.
 *
 * 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.
	Drinker: [ongoing work]
 * Correctness     : Many possibilities (e.g., "it is possible to get a coffee")
 * Source          : Own work
 * Author          : Étienne André
 * Input by        : Étienne André
 *
 * Created         : 2015/10/17
 * Last modified   : 2020/08/13
 *
 * IMITATOR version: 3
 ************************************************************)


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

(* First property: the researcher never gets mad *)
property := #synth AGnot(loc[researcher] = mad);