(************************************************************ * 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 : 2020/08/13 * Last modified : 2020/08/13 * * IMITATOR version: 3 ************************************************************) property := #synth EF(loc[machine] = cdone);