(************************************************************ * 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 : 2018/11/13 * * IMITATOR version: 2.10.4 ************************************************************) 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 (************************************************************) synclabs: press, cup, coffee, sleep; loc idle: invariant True when True sync press do {x := 0, y := 0} goto add_sugar; loc add_sugar: invariant y <= p2 when x >= p1 sync press do {x := 0} goto add_sugar; when y = p2 sync cup do {} goto preparing_coffee; loc preparing_coffee: invariant y <= p3 (* when y = p3 sync coffee goto idle; *) when y = p3 sync coffee do {x := 0} goto cdone; loc cdone: invariant x <= 10 when True sync press do {x := 0, y := 0} goto add_sugar; when x = 10 sync sleep goto idle; end (* machine *) (************************************************************) (* 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