/** Coffee Machine example
 *  
 *  inspired by the Coffee Machine example in the Telelogic TAU Tutorial
 *  
 *  Gregor v. Bochmann, December 2008 */

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 -> coffeeOK -> heatWater -> warm -> cupOfCoffee -> CONTROLLER).

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

// faulty hardware (1): may loose a "coffeeOK" message
// PREPARECOFFEE = (coffeeOK -> HARDWARE | looseMessage -> HARDWARE).

// faulty hardware (2): when adding coffee, may repeat a loop an arbitrary number of times 
//     before providing the "coffeeOK" message
// PREPARECOFFEE = (coffeeOK -> HARDWARE | tryToFix -> LOOP), LOOP = (tryToFix -> LOOP | coffeeOK -> HARDWARE).

// faulty hardware (3): when adding coffee, may get into a loop where it stays forever
// PREPARECOFFEE = (coffeeOK -> HARDWARE | tryToFix -> LOOP), LOOP = (tryToFix -> LOOP).

set User_interface = {coin[5], coin[10], coinElse, tea, coffee, returnChange, returnCoin[5], cupOfTea, cupOfCoffee}

||DETAILEDVIEW =  (CONTROLLER || HARDWARE). 


||USERVIEW =  (CONTROLLER || HARDWARE) @ User_interface. // only the interactions of the user interface are visible


property SAFENESS = (tea -> cupOfTea -> SAFENESS).
// this property involves only the alphabet {tea, cupOfTea} and it defines a certain 
//     order of execution of these interactions (ignoring all other interactions). 
//     This means that after a tea interaction there must be a cupOfTea interaction, 
//           and not an other interaction of the alphabet, such as another tea interaction. 
||CHECK1 = (DETAILEDVIEW || SAFENESS).


progress SOME = {tea}
||CHECK2 = (DETAILEDVIEW || SOME).

assert SS = ( {coin[10]} -> <> {cupOfCoffeeee} ) // formula in Linear Temporal Logic