(******************************************************************************* * IMITATOR MODEL * * Title : coffee * 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") * Scalable : * Generated : * Categories : Education ; Toy * Source : Own work * bibkey : * Author : Étienne André * Modeling : * Input by : Étienne André * License : * * Created : 2011/01/21 * Last modified : 2020/08/13 * Model version : * * IMITATOR version : 3 ******************************************************************************) 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 ; (************************************************************) (* The end *) (************************************************************) end