(************************************************************ * IMITATOR MODEL * * Coffee vending machine with drinker. Version for an IMITATOR tool paper. * * 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. Drinker: [ongoing work] * Correctness : Many possibilities (e.g., "it is possible to get a coffee") * Source : Own work * Author : Étienne André * Input by : Étienne André * * Created : 2020/08/13 * Last modified : 2020/08/13 * * IMITATOR version: 3 ************************************************************) (************************************************************) (* Property specification *) (************************************************************) (* Second property: the researcher never gets mad AND is ensured to have 3 doses of sugar *) property := #synth AGnot ( loc[researcher] = mad or loc[machine] = cdone & nb_sugar < 3); (* projectresult((*p_patience_max, p_press,*) p_coffee); *)