// ************************************************************************** // // // // eses eses // // eses eses // // eses eseses esesese eses Embedded Systems Group // // ese ese ese ese ese // // ese eseseses eseseses ese Department of Computer Science // // eses eses ese eses // // eses eseses eseseses eses University of Kaiserslautern // // eses eses // // // // ************************************************************************** // module ATM(event ?cardInserted,?pinEntered,?sumEntered,?transactionOK, ?incorrectPin,?invalidCard,?withdraw,?checkBalance, !insertCard,!enterPin,!selectOption,!processTransaction, !releaseSum,!printReceipt,!ejectCard) { loop { emit (insertCard); await(cardInserted); weak abort { weak abort { emit (enterPin); await(pinEntered); emit (selectOption); await(withdraw or checkBalance); if(withdraw) { await(sumEntered); emit (processTransaction); await(transactionOK); emit (releaseSum); emit (printReceipt); } else if(checkBalance) { emit (processTransaction); await(transactionOK); emit (printReceipt); } } when(incorrectPin); } when(invalidCard); emit (ejectCard); } }