(*******************************************************************************
 *                                IMITATOR MODEL                               
 * 
 * Title            : NoodlesCooking
 * Description      : Toy example to cook noodles
 * Correctness      : The water must not boil over [in fact, no parameter valuation can prevent this, because the timer is not necessarily set from the beginning!]
 * Scalable         : 
 * Generated        : 
 * Categories       : Education ; Toy
 * Source           : "SITH" course final examination at Institut Galilée, Université Paris 13 (2013-2014)
 * bibkey           : 
 * Author           : Étienne André
 * Modeling         : Étienne André
 * Input by         : Étienne André
 * License          : 
 * 
 * Created          : 2014/03/21
 * Last modified    : 2020/08/13
 * Model version    : 
 * 
 * IMITATOR version : 3
 ******************************************************************************)




var 	xPot, xTimer
		: clock;
		
	dPot, dTimer
		: parameter;



(************************************************************)
  automaton system
(************************************************************)
synclabs: startTimer, ring, boilover, miam;

loc heating: invariant xPot <= dPot
	when True do {xTimer := 0} sync startTimer goto ticking;
	when xPot = dPot sync boilover goto catastrophe;

loc ticking: invariant xPot <= dPot & xTimer <= dTimer
	when xTimer = dTimer sync ring goto cooked;
	when xPot = dPot sync boilover goto catastrophe;

loc cooked: invariant xPot <= dPot
	when xPot = dPot sync miam goto eating;

loc eating: invariant True

loc catastrophe: invariant True
end (* system *)



(************************************************************)
(* Initial state *)
(************************************************************)
init :=
	(*------------------------------------------------------------*)
	(*   INITIAL LOCATION *)
	(*------------------------------------------------------------*)
	& loc[system] = heating

	(*------------------------------------------------------------*)
	(*   INITIAL CLOCKS *)
	(*------------------------------------------------------------*)
	& xPot = 0
	& xTimer = 0
	
	(*------------------------------------------------------------*)
	(*   PARAMETER CONSTRAINTS *)
	(*------------------------------------------------------------*)
	& dPot >= 0
	& dTimer >= 0
;


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