(******************************************************************************* * IMITATOR MODEL * * Title : coffeeDrinker * 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. * Correctness : The scientist never gets mad * Scalable : no * Generated : no * Categories : Education ; Toy * Source : Own work * bibkey : * Author : Étienne André * Modeling : Étienne André * Input by : Étienne André * License : Creative Commons Attribution-ShareAlike 4.0 International (CC BY-SA 4.0) * * Created : 2011/01/21 * Last modified : 2021/07/09 * Model version : * * IMITATOR version : 3.1 ******************************************************************************) var (* Clocks *) x1, x2, y1, y2 : clock; (* Parameters *) (* time during which the button cannot be pressed after a pressure *) (* p_block_button, *) (* time during which one can add sugar *) p_add_sugar, (* time needed to prepare the coffee from the first button pressure *) p_coffee, (* interval of work without need for coffee *) p_work_min, p_work_max, (* Minimum interval of time between 2 consecutive pressures by the user *) p_press_min, (* time after which the drinker gets mad *) p_patience_max, : parameter; (* Discrete variables *) nb_sugar : int; (* Constants *) MAX_SUGAR = 3, : int; (************************************************************) automaton machine (************************************************************) synclabs: press, cup, coffee, sleep; loc idle: invariant True when True sync press do {x1 := 0, x2 := 0} goto add_sugar; loc add_sugar: invariant x2 <= p_add_sugar & x2 <= p_coffee when (*x1 >= p_block_button*)True sync press do {x1 := 0} goto add_sugar; when x2 = p_add_sugar sync cup do {} goto preparing_coffee; loc preparing_coffee: invariant x2 <= p_coffee (* when x2 = p_coffee sync coffee goto idle; *) when True sync press goto preparing_coffee; when x2 = p_coffee sync coffee do {x1 := 0} goto cdone; loc cdone: invariant x1 <= 10 when True sync press do {x1 := 0, x2 := 0} goto add_sugar; when x1 = 10 sync sleep goto idle; end (* machine *) (************************************************************) automaton researcher (************************************************************) synclabs: press, coffee; loc researching: invariant y1 <= p_work_max when y1 >= p_work_min sync press do {y1 := 0, y2 := 0, nb_sugar := 0} goto add_sugar; (*** TODO: an improvement would be to first nonderministically chose the number of sugars to add, and then to indeed add it (and get mad if it is impossible to get a coffee with this number); otherwise, the scientist may not get the desired number of sugards depending on the relationship between p_press_min and p_add_sugar ***) loc add_sugar: invariant y2 <= p_patience_max & nb_sugar <= MAX_SUGAR when y1 >= p_press_min & nb_sugar < MAX_SUGAR - 1 sync press do {y1 := 0, nb_sugar := nb_sugar + 1} goto add_sugar; when y1 >= p_press_min & nb_sugar = MAX_SUGAR - 1 sync press do {y1 := 0, nb_sugar := nb_sugar + 1} goto wait_coffee; (* Can also non-deterministically stop adding sugar and wait for coffee *) when True goto wait_coffee; when y2 = p_patience_max goto mad; loc wait_coffee: invariant y2 <= p_patience_max when y2 < p_patience_max sync coffee do {y1 := 0, y2 := 0} goto researching; when y2 = p_patience_max goto mad; loc mad: invariant True end (* researcher *) (************************************************************) (* Initial state *) (************************************************************) init := { discrete = (*------------------------------------------------------------*) (* Initial location *) (*------------------------------------------------------------*) loc[machine] := idle, loc[researcher] := researching, (*------------------------------------------------------------*) (* Initial discrete variables assignments *) (*------------------------------------------------------------*) nb_sugar := 0, ; continuous = (*------------------------------------------------------------*) (* Initial clock constraints *) (*------------------------------------------------------------*) & x1 = 0 & x2 = 0 (*------------------------------------------------------------*) (* Parameter constraints *) (*------------------------------------------------------------*) & y1 >= 0 & y1 <= p_work_max (* & p_block_button >= 0 *) & p_add_sugar >= 0 & p_coffee >= 0 & p_press_min >= 0 & p_work_min >= 0 & p_work_min <= p_work_max & p_patience_max >= 0 ; } (************************************************************) (* The end *) (************************************************************) end