atmproc /* as inputs */ SIGNAL insertcard, insertcode(integer), cancelop, credit, debit, credita(integer), OKcancel, numberbanknotes(integer), a10,a20,a50,a100; /* as outputs */ SIGNAL bknote10,bknote20,bknote50,bknote100, cancelopquestion, creditreceipt, creditamount, debitamount, debitreceipt, errorcode, OKop, returncard, retaincard; cardchan [bknote10,bknote20,bknote50,bknote100, cancelopquestion, creditreceipt, creditamount, debitamount, debitreceipt, errorcode, returncard, OKop, retaincard] [insertcard, insertcode, cancelop, credit, debit, credita, OKcancel, numberbanknotes, a10,a20,a50,a100]