IDLE = (coin[5] -> PAIDFIVE | coin[10] -> PAIDTEN | coinElse -> returnChange -> IDLE),
PAIDFIVE = (tea -> MAKETEA | coffee -> returnChange -> IDLE),
PAIDTEN = (tea -> returnCoin[5] -> MAKETEA | coffee -> MAKECOFFEE),
MAKETEA = (cupOfTea -> IDLE),
MAKECOFFEE = (cupOfCoffee -> IDLE).

// check that cupOfTee is always obtained after pushing tea
property TeaSafeness = (tea -> cupOfTea -> TeaSafeness).
||Check1 = (IDLE || TeaSafeness).

// check that cupOfCoffe is never obtained after entering coin-5 
property CoffeeSafeness = (coin[10] -> C10 |  coin[5] -> cupOfTea -> CoffeeSafeness),
C10 = (cupOfTea -> CoffeeSafeness | cupOfCoffee -> CoffeeSafeness).
||Check2 = (IDLE || CoffeeSafeness).