/** Coffee Machine example
 *  This specification is similar to the specification in the file 
 *       coffeeMachine-withProgressProblem.lts    */ 

CONTROLLER = (coin[5] -> PAIDFIVE | coin[10] -> PAIDTEN
             | coinElse -> returnChange -> CONTROLLER),
PAIDFIVE = (tea -> MAKETEA | coffee -> returnChange -> CONTROLLER),
PAIDTEN = (tea -> returnCoin[5] -> MAKETEA | coffee -> MAKECOFFEE),
MAKETEA = (fillWater -> waterOK -> heatWater -> warm -> cupOfTea -> CONTROLLER),
MAKECOFFEE = (fillWater -> waterOK -> fillCoffee -> heatWater -> warm -> coffeeOK -> cupOfCoffee -> CONTROLLER).

HARDWARE = (fillWater -> waterOK -> HARDWARE | heatWater -> warm -> HARDWARE | fillCoffee -> PREPARECOFFEE),
PREPARECOFFEE = (coffeeOK -> HARDWARE). 

||COFFEE_MACHINE =  (CONTROLLER || HARDWARE) .