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

// there is at least one problems in this specification:
// After coinElse, the controller may go into the BROKEN state after returning the coin; and there it will loop. 
//      Note: The behavior for the interaction returnChange is non-deterministic.
// This is shown by TEST1 which checks whether a given interaction sequence can be realized: 
//    there are two possible execution paths in the coffee machine: one is correct (leading to the STOP) and one deadlocks (see drawing).
// This is also shown by the progress check on USERVIEW.

CONTROLLER = (coin[5] -> PAIDFIVE | coin[10] -> PAIDTEN
             | coinElse -> returnChange -> BROKEN | coinElse -> returnChange -> CONTROLLER),
BROKEN = ({coin[5], coin[10], coinElse} -> returnChange -> BROKEN), 

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 : may loose a "coffeeOK" message
// PREPARECOFFEE = (coffeeOK -> HARDWARE | looseMessage -> HARDWARE).

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


// ||COFFEEMACHINE = (CONTROLLER || HARDWARE).

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

||USERVIEW =  (CONTROLLER || HARDWARE) @ UserAlphabet.

TESTCASE1 = (coinElse -> returnChange -> coin[5] -> tea -> cupOfTea -> STOP) + UserAlphabet.
||TEST1 = (USERVIEW || TESTCASE1).

property SAFENESS = (tea -> cupOfTea -> SAFENESS | coffee -> cupOfCoffee -> SAFENESS).
||SAFETYCHECK = (USERVIEW || SAFENESS).

progress SOME = {tea}