// ************************************************************************** //
//                                                                            //
//    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);
    }
}