(************************************************************ * IMITATOR MODEL * * Small problem to cook noodles * * 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!] * Source : "SITH" course final examination at Institut Galilée, Université Paris 13 (2013-2014) * Author : Étienne André * Modeling : Étienne André * Input by : Étienne André * * Created : 2014/03/21 * Last modified : 2015/07/30 * * IMITATOR version: 2.7.1 ************************************************************) var xPot, xTimer : clock; dPot, dTimer : parameter; (************************************************************) automaton system (************************************************************) synclabs: startTimer, ring, boilover, miam; initially heating; loc heating: while xPot <= dPot wait {} when True do {xTimer' = 0} sync startTimer goto ticking; when xPot = dPot sync boilover goto catastrophe; loc ticking: while xPot <= dPot & xTimer <= dTimer wait {} when xTimer = dTimer sync ring goto cooked; when xPot = dPot sync boilover goto catastrophe; loc cooked: while xPot <= dPot wait {} when xPot = dPot sync miam goto eating; loc eating: while True wait {} loc catastrophe: while True wait {} end (* system *) (************************************************************) (* Initial state *) (************************************************************) init := (*------------------------------------------------------------*) (* INITIAL LOCATION *) (*------------------------------------------------------------*) & loc[system] = heating (*------------------------------------------------------------*) (* INITIAL CLOCKS *) (*------------------------------------------------------------*) & xPot = 0 & xTimer = 0 (*------------------------------------------------------------*) (* PARAMETER CONSTRAINTS *) (*------------------------------------------------------------*) & dPot >= 0 & dTimer >= 0 ; (************************************************************) (* Property specification *) (************************************************************) property := unreachable loc[system] = catastrophe; (************************************************************) (* The end *) (************************************************************) end