$\backslash$The Account component is state$-$based and supports three types of transactions: withdrawal, deposit, and balance inquiry. Before any account transactions can be performed on the account, operation login$()$ must be issued followed by pin$()$ operation. The pin$()$ operation must contain the valid pin # $($parameter x$)$ that must be the same as the pin # provided in the open$()$ operation $($parameter y$).$ It is allowed a maximum of $3$ attempts to "provide" an invalid pin. The account requires a minimum balance of $$100.$ If a balance is below the minimum balance in the account, a $$10$ fee is imposed on each transaction $($withdraw$,$ deposit$).$ The detailed behavior of the Account component is specified using EFSM. The EFSM of Figure $1$ shows the detailed behavior of the Account component.