// File created by the EOFM to PRISM Translator with Error Generation
// Version Compiled On :Tue Sep 22 18:48:35 EDT 2020
// Translation Date: Tue Sep 22 18:49:17 EDT 2020
// Input File: C:\Users\mbolton\Dropbox\Projects\FMITF 2019-\EOFM Cases\ATM3\ATM.xml
// Output File: C:\Users\mbolton\Dropbox\Projects\FMITF 2019-\EOFM Cases\ATM3\ATM.pm

mdp

// Initial State and No Error
const int Initial = -1;
const int NoError = 0;
const int Error = 1;

// Constants from EOFM

// Constants for EOFM User Defined Types
const int actReady = 0;
const int actExecuting = 1;
const int actDone = 2;
const int Welcome = 0;
const int EnterPIN = 1;
const int Withdraw = 2;
const int OutputCash = 3;
const int OutputCard = 4;
const int IncorrectPIN = 0;
const int CorrectPIN = 1;
const int NoValue = 0;
const int IncorrectValue = 1;
const int CorrectValue = 2;


// Cognitive Function Modules
const double CPCSum = 4;
formula terminationCondition = (aGetCash = actDone);

const double P_OBS_Error = CPCSum > -9 ? pow(10.0, -2.0775 + 0.0055 * pow(CPCSum, 2) - 0.2458 * CPCSum + 0.284) : pow(10.0, -2.0775);
const double P_OBS_NoError = 1 - P_OBS_Error;
module observationFunction
	observation : [Initial..Error] init Initial;
	[EOFMTaskTransition] ( ! terminationCondition) -> 
		  P_OBS_NoError :
		  (observation' = NoError)
		+ P_OBS_Error :
		  (observation' = Error)
	;
endmodule

const double P_INT_Error = CPCSum > -9 ? pow(10.0, -1.3495 + 0.0041 * pow(CPCSum, 2) - 0.2046 * CPCSum + 0.2244) : pow(10.0, -1.3495);
const double P_INT_NoError = 1 - P_INT_Error;
module interpretationFunction
	interpretation : [Initial..Error] init Initial;
	[EOFMTaskTransition] ( ! terminationCondition) -> 
		  P_INT_NoError :
		  (interpretation' = NoError)
		+ P_INT_Error :
		  (interpretation' = Error)
	;
endmodule

const double P_PLAN_Error = 0;//CPCSum > -9 ? pow(10.0, -2 + 0.0052 * pow(CPCSum, 2) - 0.2828 * CPCSum + 0.4019) : pow(10.0, -2);
const double P_PLAN_NoError = 1 - P_PLAN_Error;
module planningFunction
	planning : [Initial..Error] init Initial;
	[EOFMTaskTransition] ( ! terminationCondition) -> 
		  P_PLAN_NoError :
		  (planning' = NoError)
		+ P_PLAN_Error :
		  (planning' = Error)
	;
endmodule

const double P_EXE_Error = CPCSum > -9 ? pow(10.0, -2.412 + 0.0065 * pow(CPCSum, 2) - 0.286 * CPCSum + 0.4079) : pow(10.0, -2.412);
const double P_EXE_NoError = 1 - P_EXE_Error;
module executionFunction
	execution : [Initial..Error] init Initial;
	[EOFMTaskTransition] ( ! terminationCondition) -> 
		  P_EXE_NoError :
		  (execution' = NoError)
		+ P_EXE_Error :
		  (execution' = Error)
	;
endmodule

module humanOperators
	submitted : bool init false;
	// Variables for pATMUser
	hEnterCard : bool init false;
	hTakeCash : bool init false;
	hTakeCard : bool init false;
	hEnterPIN : [IncorrectPIN..CorrectPIN] init CorrectPIN;
	hEnterCashVal : [NoValue..CorrectValue] init NoValue;
	hCancel : bool init false;
	lDesiredValue : [NoValue..CorrectValue] init CorrectValue;
	aGetCash : [actReady..actDone] init actReady;
	aInsertCard : [actReady..actDone] init actReady;
	hEnterCard_1 : [actReady..actDone] init actReady;
	aEnterPin : [actReady..actDone] init actReady;
	hEnterPIN_2 : [actReady..actDone] init actReady;
	aEnterCashValue : [actReady..actDone] init actReady;
	hEnterCashVal_3 : [actReady..actDone] init actReady;
	aRetreiveOutputs : [actReady..actDone] init actReady;
	aAquireCash : [actReady..actDone] init actReady;
	hTakeCash_4 : [actReady..actDone] init actReady;
	aRetreiveCard : [actReady..actDone] init actReady;
	hTakeCard_5 : [actReady..actDone] init actReady;


	// Normative transitions for aGetCash
	// aGetCash: Normative Ready -> Executing
	[EOFMTaskTransition] ((planning = NoError) & (((aGetCash = actReady))  &  (aGetCash != actExecuting & aInsertCard != actExecuting & hEnterCard_1 != actExecuting & aEnterPin != actExecuting & hEnterPIN_2 != actExecuting & aEnterCashValue != actExecuting & hEnterCashVal_3 != actExecuting & aRetreiveOutputs != actExecuting & aAquireCash != actExecuting & hTakeCash_4 != actExecuting & aRetreiveCard != actExecuting & hTakeCard_5 != actExecuting))) -> 
		  (aGetCash' = actExecuting)
	;
	// aGetCash: Normative Executing -> Done
	[EOFMTaskTransition] ((planning = NoError) & (((aGetCash = actExecuting) & aInsertCard = actDone & aEnterPin = actDone & aEnterCashValue = actDone & aRetreiveOutputs = actDone))) -> 
		  (aGetCash' = actDone)
	;
	// aGetCash:  Normative Done->Ready
	[EOFMTaskTransition] ((planning = NoError) & ((aGetCash = actDone))) -> 
		  (aGetCash' = actReady)
		& (aInsertCard' = actReady)
		& (hEnterCard_1' = actReady)
		& (aEnterPin' = actReady)
		& (hEnterPIN_2' = actReady)
		& (aEnterCashValue' = actReady)
		& (hEnterCashVal_3' = actReady)
		& (aRetreiveOutputs' = actReady)
		& (aAquireCash' = actReady)
		& (hTakeCash_4' = actReady)
		& (aRetreiveCard' = actReady)
		& (hTakeCard_5' = actReady)
	;

	// Erroneous transitions for aGetCash
	// aGetCash: Erroneous Ready->Done Omission
	[EOFMTaskTransition] ((aGetCash = actReady) & (planning = Error) & ((aGetCash = actReady))) -> 
		  (aGetCash' = actDone)
	;
	// aGetCash: Erroenous Ready->Ready Delay
	[EOFMTaskTransition] ((aGetCash = actReady) & (planning = Error) & ((aGetCash = actReady))) -> 
		  (aGetCash' = actReady)
	;
	// aGetCash: Erroneous Ready->Exeucting Intrusion
	[EOFMTaskTransition] ((aGetCash = actReady) & (((planning = Error) & ( ! ((aGetCash = actReady)))))) -> 
		  (aGetCash' = actExecuting)
	;
	// aGetCash: Erroneous Executing->Executing Delay
	[EOFMTaskTransition] ((aGetCash = actExecuting) & (((planning = Error)) & (((aGetCash = actExecuting) & aInsertCard = actDone & aEnterPin = actDone & aEnterCashValue = actDone & aRetreiveOutputs = actDone)))) -> 
		  (aGetCash' = actExecuting)
	;
	// aGetCash: Erroneous Executing->Executing with Reset (Restart)
	[EOFMTaskTransition] ((aGetCash = actExecuting) & ((planning = Error) & ( ! (((aGetCash = actExecuting) & aInsertCard = actDone & aEnterPin = actDone & aEnterCashValue = actDone & aRetreiveOutputs = actDone))) | (interpretation = Error))) -> 
		  (aGetCash' = actExecuting)
		& (aInsertCard' = actReady)
		& (hEnterCard_1' = actReady)
		& (aEnterPin' = actReady)
		& (hEnterPIN_2' = actReady)
		& (aEnterCashValue' = actReady)
		& (hEnterCashVal_3' = actReady)
		& (aRetreiveOutputs' = actReady)
		& (aAquireCash' = actReady)
		& (hTakeCash_4' = actReady)
		& (aRetreiveCard' = actReady)
		& (hTakeCard_5' = actReady)
	;
	// aGetCash: Erroneous Executing->Done Omission
	[EOFMTaskTransition] ((aGetCash = actExecuting) & ((planning = Error) & ( ! ((aGetCash = actExecuting) & aInsertCard = actDone & aEnterPin = actDone & aEnterCashValue = actDone & aRetreiveOutputs = actDone)))) -> 
		  (aGetCash' = actDone)
	;
	// aGetCash: Erroneous Done->Executing Intrusion
	[EOFMTaskTransition] ((aGetCash = actDone) & ((planning = Error))) -> 
		  (aGetCash' = actExecuting)
		& (aInsertCard' = actReady)
		& (hEnterCard_1' = actReady)
		& (aEnterPin' = actReady)
		& (hEnterPIN_2' = actReady)
		& (aEnterCashValue' = actReady)
		& (hEnterCashVal_3' = actReady)
		& (aRetreiveOutputs' = actReady)
		& (aAquireCash' = actReady)
		& (hTakeCash_4' = actReady)
		& (aRetreiveCard' = actReady)
		& (hTakeCard_5' = actReady)
	;

	// Normative transitions for aInsertCard
	// aInsertCard: Normative Ready -> Executing
	[EOFMTaskTransition] (((planning = NoError) & (interpretation = NoError)) & (((aInsertCard = actReady) & aGetCash = actExecuting)  &  (iInterfaceState = Welcome) &  !  (iInterfaceState != Welcome)  &  (aInsertCard != actExecuting & hEnterCard_1 != actExecuting))) -> 
		  (aInsertCard' = actExecuting)
	;
	// aInsertCard: Normative Executing -> Done
	[EOFMTaskTransition] (((planning = NoError) & (interpretation = NoError)) & (((aInsertCard = actExecuting) & hEnterCard_1 = actDone)  & (iInterfaceState != Welcome))) -> 
		  (aInsertCard' = actDone)
	;
	// aInsertCard: Normative Executing -> Executing with Reset
	[EOFMTaskTransition] (((planning = NoError) & (interpretation = NoError)) & (((aInsertCard = actReady) & aGetCash = actExecuting)  & (iInterfaceState != Welcome))) -> 
		  (aInsertCard' = actDone)
	;
	// aInsertCard:  Normative Executing -> Executing with Reset
	[EOFMTaskTransition] (((planning = NoError) & (interpretation = NoError)) & (((aInsertCard = actExecuting) & hEnterCard_1 = actDone)  &  (iInterfaceState = Welcome)  &   !  (iInterfaceState != Welcome))) -> 
		  (aInsertCard' = actExecuting)
		& (hEnterCard_1' = actReady)
	;

	// Erroneous transitions for aInsertCard
	// aInsertCard: Erroneous Ready->Done Omission
	[EOFMTaskTransition] ((aInsertCard = actReady) & ((planning = Error) | (interpretation = Error)) & ((aInsertCard = actReady) & aGetCash = actExecuting) &  ! (iInterfaceState != Welcome)) -> 
		  (aInsertCard' = actDone)
	;
	// aInsertCard: Erroenous Ready->Ready Delay
	[EOFMTaskTransition] ((aInsertCard = actReady) & ((planning = Error) | (interpretation = Error)) & ((aInsertCard = actReady) & aGetCash = actExecuting) & (iInterfaceState = Welcome) &  ! (iInterfaceState != Welcome)) -> 
		  (aInsertCard' = actReady)
	;
	// aInsertCard: Erroneous Ready->Exeucting Intrusion
	[EOFMTaskTransition] ((aInsertCard = actReady) & (((planning = Error) & ( ! ((aInsertCard = actReady) & aGetCash = actExecuting) |  ! (iInterfaceState = Welcome) | (iInterfaceState != Welcome))) | ((interpretation = Error) & ( ! (iInterfaceState = Welcome) | (iInterfaceState != Welcome))))) -> 
		  (aInsertCard' = actExecuting)
	;
	// aInsertCard: Erroneous Executing->Executing Delay
	[EOFMTaskTransition] ((aInsertCard = actExecuting) & (((planning = Error) | (interpretation = Error)) & (((aInsertCard = actExecuting) & hEnterCard_1 = actDone)) & ((iInterfaceState != Welcome) | (iInterfaceState = Welcome)))) -> 
		  (aInsertCard' = actExecuting)
	;
	// aInsertCard: Erroneous Executing->Executing with Reset (Restart)
	[EOFMTaskTransition] ((aInsertCard = actExecuting) & ((planning = Error) & ( ! (((aInsertCard = actExecuting) & hEnterCard_1 = actDone)) |  ! (iInterfaceState = Welcome) | (iInterfaceState != Welcome)) | (interpretation = Error) & ( ! (iInterfaceState = Welcome) | (iInterfaceState != Welcome)))) -> 
		  (aInsertCard' = actExecuting)
		& (hEnterCard_1' = actReady)
	;
	// aInsertCard: Erroneous Executing->Done Omission
	[EOFMTaskTransition] ((aInsertCard = actExecuting) & ((planning = Error) & ( ! ((aInsertCard = actExecuting) & hEnterCard_1 = actDone) |  ! (iInterfaceState != Welcome)) | ((interpretation = Error) &  ! (iInterfaceState != Welcome)))) -> 
		  (aInsertCard' = actDone)
	;
	// aInsertCard: Erroneous Done->Executing Intrusion
	[EOFMTaskTransition] ((aInsertCard = actDone) & ((planning = Error))) -> 
		  (aInsertCard' = actExecuting)
		& (hEnterCard_1' = actReady)
	;
	// aInsertCard: allows the actions to be reset normatively for activities that are done erroneously when the parent is ready
	[EOFMTaskTransition] ((aInsertCard = actDone) & (aGetCash = actReady)) -> 
		  (aInsertCard' = actReady)
		& (hEnterCard_1' = actReady)
	;

	// Normative transitions for hEnterCard_1
	// hEnterCard_1: Normative Ready->Executing
	[EOFMTaskTransition] ((execution = NoError) & (hEnterCard_1 = actReady) & (aInsertCard = actExecuting) & ready) -> 
		  (hEnterCard_1' = actExecuting)
		& (hEnterCard' = true)
		& (submitted' = true)
	;

	// Erroneous transitions for hEnterCard_1
	// hEnterCard_1: Erroenous Ready->Executing or Done->Executing sequence error / intrusion
	[EOFMTaskTransition] ((execution = Error) & (((hEnterCard_1 = actReady) &  ! (aInsertCard = actExecuting)) | (hEnterCard_1 = actDone)) & ready) -> 
		  (hEnterCard_1' = actExecuting)
		& (hEnterCard' = true)
		& (submitted' = true)
	;
	// hEnterCard_1: Erroenous Ready->Executing or Done->Executing doing the a wrong action in place of the right one
	[EOFMTaskTransition] ((execution = Error) & (hEnterCard_1 = actReady) & (aInsertCard = actExecuting) & ready) -> 
		  (hEnterCard_1' = actExecuting)
		& (hEnterPIN' = CorrectPIN)
		& (submitted' = true)
	;
	// hEnterCard_1: Erroenous Ready->Executing or Done->Executing doing the a wrong action in place of the right one
	[EOFMTaskTransition] ((execution = Error) & (hEnterCard_1 = actReady) & (aInsertCard = actExecuting) & ready) -> 
		  (hEnterCard_1' = actExecuting)
		& (hTakeCard' = true)
		& (submitted' = true)
	;
	// hEnterCard_1: Erroenous Ready->Executing or Done->Executing doing the a wrong action in place of the right one
	[EOFMTaskTransition] ((execution = Error) & (hEnterCard_1 = actReady) & (aInsertCard = actExecuting) & ready) -> 
		  (hEnterCard_1' = actExecuting)
		& (hEnterCashVal' = lDesiredValue)
		& (submitted' = true)
	;
	// hEnterCard_1: Erroenous Ready->Executing or Done->Executing doing the a wrong action in place of the right one
	[EOFMTaskTransition] ((execution = Error) & (hEnterCard_1 = actReady) & (aInsertCard = actExecuting) & ready) -> 
		  (hEnterCard_1' = actExecuting)
		& (hTakeCash' = true)
		& (submitted' = true)
	;
	// hEnterCard_1: Erroenous Ready->Done Omission
	[EOFMTaskTransition] ((execution = Error) & (hEnterCard_1 = actReady) & (aInsertCard = actExecuting) & ready) -> 
		  (hEnterCard_1' = actDone)
	;
	// hEnterCard_1: Erroenous Ready->Ready Delay
	[EOFMTaskTransition] ((execution = Error) & (hEnterCard_1 = actReady) & (aInsertCard = actExecuting) & ready) -> 
		  (hEnterCard_1' = actReady)
		& (submitted' = true)
	;
	// hEnterCard_1: Done->Ready  allows the actions to be reset normatively for activities that are done erroneously when the parent is ready
	[EOFMTaskTransition] ((hEnterCard_1 = actDone) & (aInsertCard = actReady)) -> 
		  (hEnterCard_1' = actReady)
	;

	// Normative transitions for aEnterPin
	// aEnterPin: Normative Ready -> Executing
	[EOFMTaskTransition] (((planning = NoError) & (interpretation = NoError)) & (((aEnterPin = actReady) & aGetCash = actExecuting & aInsertCard = actDone)  &  (iInterfaceState = EnterPIN) &  !  (iInterfaceState != EnterPIN)  &  (aEnterPin != actExecuting & hEnterPIN_2 != actExecuting))) -> 
		  (aEnterPin' = actExecuting)
	;
	// aEnterPin: Normative Executing -> Done
	[EOFMTaskTransition] (((planning = NoError) & (interpretation = NoError)) & (((aEnterPin = actExecuting) & hEnterPIN_2 = actDone)  & (iInterfaceState != EnterPIN))) -> 
		  (aEnterPin' = actDone)
	;
	// aEnterPin: Normative Executing -> Executing with Reset
	[EOFMTaskTransition] (((planning = NoError) & (interpretation = NoError)) & (((aEnterPin = actReady) & aGetCash = actExecuting & aInsertCard = actDone)  & (iInterfaceState != EnterPIN))) -> 
		  (aEnterPin' = actDone)
	;
	// aEnterPin:  Normative Executing -> Executing with Reset
	[EOFMTaskTransition] (((planning = NoError) & (interpretation = NoError)) & (((aEnterPin = actExecuting) & hEnterPIN_2 = actDone)  &  (iInterfaceState = EnterPIN)  &   !  (iInterfaceState != EnterPIN))) -> 
		  (aEnterPin' = actExecuting)
		& (hEnterPIN_2' = actReady)
	;

	// Erroneous transitions for aEnterPin
	// aEnterPin: Erroneous Ready->Done Omission
	[EOFMTaskTransition] ((aEnterPin = actReady) & ((planning = Error) | (interpretation = Error)) & ((aEnterPin = actReady) & aGetCash = actExecuting & aInsertCard = actDone) &  ! (iInterfaceState != EnterPIN)) -> 
		  (aEnterPin' = actDone)
	;
	// aEnterPin: Erroenous Ready->Ready Delay
	[EOFMTaskTransition] ((aEnterPin = actReady) & ((planning = Error) | (interpretation = Error)) & ((aEnterPin = actReady) & aGetCash = actExecuting & aInsertCard = actDone) & (iInterfaceState = EnterPIN) &  ! (iInterfaceState != EnterPIN)) -> 
		  (aEnterPin' = actReady)
	;
	// aEnterPin: Erroneous Ready->Exeucting Intrusion
	[EOFMTaskTransition] ((aEnterPin = actReady) & (((planning = Error) & ( ! ((aEnterPin = actReady) & aGetCash = actExecuting & aInsertCard = actDone) |  ! (iInterfaceState = EnterPIN) | (iInterfaceState != EnterPIN))) | ((interpretation = Error) & ( ! (iInterfaceState = EnterPIN) | (iInterfaceState != EnterPIN))))) -> 
		  (aEnterPin' = actExecuting)
	;
	// aEnterPin: Erroneous Executing->Executing Delay
	[EOFMTaskTransition] ((aEnterPin = actExecuting) & (((planning = Error) | (interpretation = Error)) & (((aEnterPin = actExecuting) & hEnterPIN_2 = actDone)) & ((iInterfaceState != EnterPIN) | (iInterfaceState = EnterPIN)))) -> 
		  (aEnterPin' = actExecuting)
	;
	// aEnterPin: Erroneous Executing->Executing with Reset (Restart)
	[EOFMTaskTransition] ((aEnterPin = actExecuting) & ((planning = Error) & ( ! (((aEnterPin = actExecuting) & hEnterPIN_2 = actDone)) |  ! (iInterfaceState = EnterPIN) | (iInterfaceState != EnterPIN)) | (interpretation = Error) & ( ! (iInterfaceState = EnterPIN) | (iInterfaceState != EnterPIN)))) -> 
		  (aEnterPin' = actExecuting)
		& (hEnterPIN_2' = actReady)
	;
	// aEnterPin: Erroneous Executing->Done Omission
	[EOFMTaskTransition] ((aEnterPin = actExecuting) & ((planning = Error) & ( ! ((aEnterPin = actExecuting) & hEnterPIN_2 = actDone) |  ! (iInterfaceState != EnterPIN)) | ((interpretation = Error) &  ! (iInterfaceState != EnterPIN)))) -> 
		  (aEnterPin' = actDone)
	;
	// aEnterPin: Erroneous Done->Executing Intrusion
	[EOFMTaskTransition] ((aEnterPin = actDone) & ((planning = Error))) -> 
		  (aEnterPin' = actExecuting)
		& (hEnterPIN_2' = actReady)
	;
	// aEnterPin: allows the actions to be reset normatively for activities that are done erroneously when the parent is ready
	[EOFMTaskTransition] ((aEnterPin = actDone) & (aGetCash = actReady)) -> 
		  (aEnterPin' = actReady)
		& (hEnterPIN_2' = actReady)
	;

	// Normative transitions for hEnterPIN_2
	// hEnterPIN_2: Normative Ready->Executing
	[EOFMTaskTransition] ((execution = NoError) & (hEnterPIN_2 = actReady) & (aEnterPin = actExecuting) & ready) -> 
		  (hEnterPIN_2' = actExecuting)
		& (hEnterPIN' = CorrectPIN)
		& (submitted' = true)
	;

	// Erroneous transitions for hEnterPIN_2
	// hEnterPIN_2: Erroenous Ready->Executing or Done->Executing sequence error / intrusion
	[EOFMTaskTransition] ((execution = Error) & (((hEnterPIN_2 = actReady) &  ! (aEnterPin = actExecuting)) | (hEnterPIN_2 = actDone)) & ready) -> 
		  (hEnterPIN_2' = actExecuting)
		& (hEnterPIN' = CorrectPIN)
		& (submitted' = true)
	;
	// hEnterPIN_2: Erroenous Ready->Executing or Done->Executing doing the a wrong action in place of the right one
	[EOFMTaskTransition] ((execution = Error) & (hEnterPIN_2 = actReady) & (aEnterPin = actExecuting) & ready) -> 
		  (hEnterPIN_2' = actExecuting)
		& (hTakeCard' = true)
		& (submitted' = true)
	;
	// hEnterPIN_2: Erroenous Ready->Executing or Done->Executing doing the a wrong action in place of the right one
	[EOFMTaskTransition] ((execution = Error) & (hEnterPIN_2 = actReady) & (aEnterPin = actExecuting) & ready) -> 
		  (hEnterPIN_2' = actExecuting)
		& (hEnterCashVal' = lDesiredValue)
		& (submitted' = true)
	;
	// hEnterPIN_2: Erroenous Ready->Executing or Done->Executing doing the a wrong action in place of the right one
	[EOFMTaskTransition] ((execution = Error) & (hEnterPIN_2 = actReady) & (aEnterPin = actExecuting) & ready) -> 
		  (hEnterPIN_2' = actExecuting)
		& (hTakeCash' = true)
		& (submitted' = true)
	;
	// hEnterPIN_2: Erroenous Ready->Executing or Done->Executing doing the a wrong action in place of the right one
	[EOFMTaskTransition] ((execution = Error) & (hEnterPIN_2 = actReady) & (aEnterPin = actExecuting) & ready) -> 
		  (hEnterPIN_2' = actExecuting)
		& (hEnterCard' = true)
		& (submitted' = true)
	;
	// hEnterPIN_2: Erroenous Ready->Done Omission
	[EOFMTaskTransition] ((execution = Error) & (hEnterPIN_2 = actReady) & (aEnterPin = actExecuting) & ready) -> 
		  (hEnterPIN_2' = actDone)
	;
	// hEnterPIN_2: Erroenous Ready->Ready Delay
	[EOFMTaskTransition] ((execution = Error) & (hEnterPIN_2 = actReady) & (aEnterPin = actExecuting) & ready) -> 
		  (hEnterPIN_2' = actReady)
		& (submitted' = true)
	;
	// hEnterPIN_2: Done->Ready  allows the actions to be reset normatively for activities that are done erroneously when the parent is ready
	[EOFMTaskTransition] ((hEnterPIN_2 = actDone) & (aEnterPin = actReady)) -> 
		  (hEnterPIN_2' = actReady)
	;
	// hEnterPIN_2: Wrong Value / Action on Wrong Object with value IncorrectPIN
	[EOFMTaskTransition] ((execution = Error) & (CorrectPIN != IncorrectPIN) & ((hEnterPIN_2 = actReady) & (aEnterPin = actExecuting))) -> 
		  (hEnterPIN_2' = actExecuting)
		& (hEnterPIN' = IncorrectPIN)
		& (submitted' = true)
	;

	// Normative transitions for aEnterCashValue
	// aEnterCashValue: Normative Ready -> Executing
	[EOFMTaskTransition] (((planning = NoError) & (interpretation = NoError)) & (((aEnterCashValue = actReady) & aGetCash = actExecuting & aEnterPin = actDone)  &  (iInterfaceState = Withdraw) &  !  (iInterfaceState != Withdraw)  &  (aEnterCashValue != actExecuting & hEnterCashVal_3 != actExecuting))) -> 
		  (aEnterCashValue' = actExecuting)
	;
	// aEnterCashValue: Normative Executing -> Done
	[EOFMTaskTransition] (((planning = NoError) & (interpretation = NoError)) & (((aEnterCashValue = actExecuting) & hEnterCashVal_3 = actDone)  & (iInterfaceState != Withdraw))) -> 
		  (aEnterCashValue' = actDone)
	;
	// aEnterCashValue: Normative Executing -> Executing with Reset
	[EOFMTaskTransition] (((planning = NoError) & (interpretation = NoError)) & (((aEnterCashValue = actReady) & aGetCash = actExecuting & aEnterPin = actDone)  & (iInterfaceState != Withdraw))) -> 
		  (aEnterCashValue' = actDone)
	;
	// aEnterCashValue:  Normative Executing -> Executing with Reset
	[EOFMTaskTransition] (((planning = NoError) & (interpretation = NoError)) & (((aEnterCashValue = actExecuting) & hEnterCashVal_3 = actDone)  &  (iInterfaceState = Withdraw)  &   !  (iInterfaceState != Withdraw))) -> 
		  (aEnterCashValue' = actExecuting)
		& (hEnterCashVal_3' = actReady)
	;

	// Erroneous transitions for aEnterCashValue
	// aEnterCashValue: Erroneous Ready->Done Omission
	[EOFMTaskTransition] ((aEnterCashValue = actReady) & ((planning = Error) | (interpretation = Error)) & ((aEnterCashValue = actReady) & aGetCash = actExecuting & aEnterPin = actDone) &  ! (iInterfaceState != Withdraw)) -> 
		  (aEnterCashValue' = actDone)
	;
	// aEnterCashValue: Erroenous Ready->Ready Delay
	[EOFMTaskTransition] ((aEnterCashValue = actReady) & ((planning = Error) | (interpretation = Error)) & ((aEnterCashValue = actReady) & aGetCash = actExecuting & aEnterPin = actDone) & (iInterfaceState = Withdraw) &  ! (iInterfaceState != Withdraw)) -> 
		  (aEnterCashValue' = actReady)
	;
	// aEnterCashValue: Erroneous Ready->Exeucting Intrusion
	[EOFMTaskTransition] ((aEnterCashValue = actReady) & (((planning = Error) & ( ! ((aEnterCashValue = actReady) & aGetCash = actExecuting & aEnterPin = actDone) |  ! (iInterfaceState = Withdraw) | (iInterfaceState != Withdraw))) | ((interpretation = Error) & ( ! (iInterfaceState = Withdraw) | (iInterfaceState != Withdraw))))) -> 
		  (aEnterCashValue' = actExecuting)
	;
	// aEnterCashValue: Erroneous Executing->Executing Delay
	[EOFMTaskTransition] ((aEnterCashValue = actExecuting) & (((planning = Error) | (interpretation = Error)) & (((aEnterCashValue = actExecuting) & hEnterCashVal_3 = actDone)) & ((iInterfaceState != Withdraw) | (iInterfaceState = Withdraw)))) -> 
		  (aEnterCashValue' = actExecuting)
	;
	// aEnterCashValue: Erroneous Executing->Executing with Reset (Restart)
	[EOFMTaskTransition] ((aEnterCashValue = actExecuting) & ((planning = Error) & ( ! (((aEnterCashValue = actExecuting) & hEnterCashVal_3 = actDone)) |  ! (iInterfaceState = Withdraw) | (iInterfaceState != Withdraw)) | (interpretation = Error) & ( ! (iInterfaceState = Withdraw) | (iInterfaceState != Withdraw)))) -> 
		  (aEnterCashValue' = actExecuting)
		& (hEnterCashVal_3' = actReady)
	;
	// aEnterCashValue: Erroneous Executing->Done Omission
	[EOFMTaskTransition] ((aEnterCashValue = actExecuting) & ((planning = Error) & ( ! ((aEnterCashValue = actExecuting) & hEnterCashVal_3 = actDone) |  ! (iInterfaceState != Withdraw)) | ((interpretation = Error) &  ! (iInterfaceState != Withdraw)))) -> 
		  (aEnterCashValue' = actDone)
	;
	// aEnterCashValue: Erroneous Done->Executing Intrusion
	[EOFMTaskTransition] ((aEnterCashValue = actDone) & ((planning = Error))) -> 
		  (aEnterCashValue' = actExecuting)
		& (hEnterCashVal_3' = actReady)
	;
	// aEnterCashValue: allows the actions to be reset normatively for activities that are done erroneously when the parent is ready
	[EOFMTaskTransition] ((aEnterCashValue = actDone) & (aGetCash = actReady)) -> 
		  (aEnterCashValue' = actReady)
		& (hEnterCashVal_3' = actReady)
	;

	// Normative transitions for hEnterCashVal_3
	// hEnterCashVal_3: Normative Ready->Executing
	[EOFMTaskTransition] ((execution = NoError) & (hEnterCashVal_3 = actReady) & (aEnterCashValue = actExecuting) & ready) -> 
		  (hEnterCashVal_3' = actExecuting)
		& (hEnterCashVal' = lDesiredValue)
		& (submitted' = true)
	;

	// Erroneous transitions for hEnterCashVal_3
	// hEnterCashVal_3: Erroenous Ready->Executing or Done->Executing sequence error / intrusion
	[EOFMTaskTransition] ((execution = Error) & (((hEnterCashVal_3 = actReady) &  ! (aEnterCashValue = actExecuting)) | (hEnterCashVal_3 = actDone)) & ready) -> 
		  (hEnterCashVal_3' = actExecuting)
		& (hEnterCashVal' = lDesiredValue)
		& (submitted' = true)
	;
	// hEnterCashVal_3: Erroenous Ready->Executing or Done->Executing doing the a wrong action in place of the right one
	[EOFMTaskTransition] ((execution = Error) & (hEnterCashVal_3 = actReady) & (aEnterCashValue = actExecuting) & ready) -> 
		  (hEnterCashVal_3' = actExecuting)
		& (hEnterPIN' = CorrectPIN)
		& (submitted' = true)
	;
	// hEnterCashVal_3: Erroenous Ready->Executing or Done->Executing doing the a wrong action in place of the right one
	[EOFMTaskTransition] ((execution = Error) & (hEnterCashVal_3 = actReady) & (aEnterCashValue = actExecuting) & ready) -> 
		  (hEnterCashVal_3' = actExecuting)
		& (hTakeCard' = true)
		& (submitted' = true)
	;
	// hEnterCashVal_3: Erroenous Ready->Executing or Done->Executing doing the a wrong action in place of the right one
	[EOFMTaskTransition] ((execution = Error) & (hEnterCashVal_3 = actReady) & (aEnterCashValue = actExecuting) & ready) -> 
		  (hEnterCashVal_3' = actExecuting)
		& (hTakeCash' = true)
		& (submitted' = true)
	;
	// hEnterCashVal_3: Erroenous Ready->Executing or Done->Executing doing the a wrong action in place of the right one
	[EOFMTaskTransition] ((execution = Error) & (hEnterCashVal_3 = actReady) & (aEnterCashValue = actExecuting) & ready) -> 
		  (hEnterCashVal_3' = actExecuting)
		& (hEnterCard' = true)
		& (submitted' = true)
	;
	// hEnterCashVal_3: Erroenous Ready->Done Omission
	[EOFMTaskTransition] ((execution = Error) & (hEnterCashVal_3 = actReady) & (aEnterCashValue = actExecuting) & ready) -> 
		  (hEnterCashVal_3' = actDone)
	;
	// hEnterCashVal_3: Erroenous Ready->Ready Delay
	[EOFMTaskTransition] ((execution = Error) & (hEnterCashVal_3 = actReady) & (aEnterCashValue = actExecuting) & ready) -> 
		  (hEnterCashVal_3' = actReady)
		& (submitted' = true)
	;
	// hEnterCashVal_3: Done->Ready  allows the actions to be reset normatively for activities that are done erroneously when the parent is ready
	[EOFMTaskTransition] ((hEnterCashVal_3 = actDone) & (aEnterCashValue = actReady)) -> 
		  (hEnterCashVal_3' = actReady)
	;
	// hEnterCashVal_3: Wrong Value / Action on Wrong Object with value NoValue
	[EOFMTaskTransition] ((execution = Error) & (lDesiredValue != NoValue) & ((hEnterCashVal_3 = actReady) & (aEnterCashValue = actExecuting))) -> 
		  (hEnterCashVal_3' = actExecuting)
		& (hEnterCashVal' = NoValue)
		& (submitted' = true)
	;
	// hEnterCashVal_3: Wrong Value / Action on Wrong Object with value IncorrectValue
	[EOFMTaskTransition] ((execution = Error) & (lDesiredValue != IncorrectValue) & ((hEnterCashVal_3 = actReady) & (aEnterCashValue = actExecuting))) -> 
		  (hEnterCashVal_3' = actExecuting)
		& (hEnterCashVal' = IncorrectValue)
		& (submitted' = true)
	;
	// hEnterCashVal_3: Wrong Value / Action on Wrong Object with value CorrectValue
	[EOFMTaskTransition] ((execution = Error) & (lDesiredValue != CorrectValue) & ((hEnterCashVal_3 = actReady) & (aEnterCashValue = actExecuting))) -> 
		  (hEnterCashVal_3' = actExecuting)
		& (hEnterCashVal' = CorrectValue)
		& (submitted' = true)
	;

	// Normative transitions for aRetreiveOutputs
	// aRetreiveOutputs: Normative Ready -> Executing
	[EOFMTaskTransition] (((planning = NoError) & (interpretation = NoError)) & (((aRetreiveOutputs = actReady) & aGetCash = actExecuting & aEnterCashValue = actDone) &  !  (hTakeCash_4 = actDone)  &  (aRetreiveOutputs != actExecuting & aAquireCash != actExecuting & hTakeCash_4 != actExecuting & aRetreiveCard != actExecuting & hTakeCard_5 != actExecuting))) -> 
		  (aRetreiveOutputs' = actExecuting)
	;
	// aRetreiveOutputs: Normative Executing -> Done
	[EOFMTaskTransition] (((planning = NoError) & (interpretation = NoError)) & (((aRetreiveOutputs = actExecuting) & aAquireCash = actDone & aRetreiveCard = actDone)  & (hTakeCash_4 = actDone))) -> 
		  (aRetreiveOutputs' = actDone)
	;
	// aRetreiveOutputs: Normative Executing -> Executing with Reset
	[EOFMTaskTransition] (((planning = NoError) & (interpretation = NoError)) & (((aRetreiveOutputs = actReady) & aGetCash = actExecuting & aEnterCashValue = actDone)  & (hTakeCash_4 = actDone))) -> 
		  (aRetreiveOutputs' = actDone)
	;

	// Erroneous transitions for aRetreiveOutputs
	// aRetreiveOutputs: Erroneous Ready->Done Omission
	[EOFMTaskTransition] ((aRetreiveOutputs = actReady) & ((planning = Error) | (interpretation = Error)) & ((aRetreiveOutputs = actReady) & aGetCash = actExecuting & aEnterCashValue = actDone) &  ! (hTakeCash_4 = actDone)) -> 
		  (aRetreiveOutputs' = actDone)
	;
	// aRetreiveOutputs: Erroenous Ready->Ready Delay
	[EOFMTaskTransition] ((aRetreiveOutputs = actReady) & ((planning = Error) | (interpretation = Error)) & ((aRetreiveOutputs = actReady) & aGetCash = actExecuting & aEnterCashValue = actDone) &  ! (hTakeCash_4 = actDone)) -> 
		  (aRetreiveOutputs' = actReady)
	;
	// aRetreiveOutputs: Erroneous Ready->Exeucting Intrusion
	[EOFMTaskTransition] ((aRetreiveOutputs = actReady) & (((planning = Error) & ( ! ((aRetreiveOutputs = actReady) & aGetCash = actExecuting & aEnterCashValue = actDone) | (hTakeCash_4 = actDone))) | ((interpretation = Error) & ((hTakeCash_4 = actDone))))) -> 
		  (aRetreiveOutputs' = actExecuting)
	;
	// aRetreiveOutputs: Erroneous Executing->Executing Delay
	[EOFMTaskTransition] ((aRetreiveOutputs = actExecuting) & (((planning = Error) | (interpretation = Error)) & (((aRetreiveOutputs = actExecuting) & aAquireCash = actDone & aRetreiveCard = actDone)) & (hTakeCash_4 = actDone))) -> 
		  (aRetreiveOutputs' = actExecuting)
	;
	// aRetreiveOutputs: Erroneous Executing->Executing with Reset (Restart)
	[EOFMTaskTransition] ((aRetreiveOutputs = actExecuting) & ((planning = Error) & ( ! (((aRetreiveOutputs = actExecuting) & aAquireCash = actDone & aRetreiveCard = actDone)) | (hTakeCash_4 = actDone)) | (interpretation = Error) & ((hTakeCash_4 = actDone)))) -> 
		  (aRetreiveOutputs' = actExecuting)
		& (aAquireCash' = actReady)
		& (hTakeCash_4' = actReady)
		& (aRetreiveCard' = actReady)
		& (hTakeCard_5' = actReady)
	;
	// aRetreiveOutputs: Erroneous Executing->Done Omission
	[EOFMTaskTransition] ((aRetreiveOutputs = actExecuting) & ((planning = Error) & ( ! ((aRetreiveOutputs = actExecuting) & aAquireCash = actDone & aRetreiveCard = actDone) |  ! (hTakeCash_4 = actDone)) | ((interpretation = Error) &  ! (hTakeCash_4 = actDone)))) -> 
		  (aRetreiveOutputs' = actDone)
	;
	// aRetreiveOutputs: Erroneous Done->Executing Intrusion
	[EOFMTaskTransition] ((aRetreiveOutputs = actDone) & ((planning = Error))) -> 
		  (aRetreiveOutputs' = actExecuting)
		& (aAquireCash' = actReady)
		& (hTakeCash_4' = actReady)
		& (aRetreiveCard' = actReady)
		& (hTakeCard_5' = actReady)
	;
	// aRetreiveOutputs: allows the actions to be reset normatively for activities that are done erroneously when the parent is ready
	[EOFMTaskTransition] ((aRetreiveOutputs = actDone) & (aGetCash = actReady)) -> 
		  (aRetreiveOutputs' = actReady)
		& (aAquireCash' = actReady)
		& (hTakeCash_4' = actReady)
		& (aRetreiveCard' = actReady)
		& (hTakeCard_5' = actReady)
	;

	// Normative transitions for aAquireCash
	// aAquireCash: Normative Ready -> Executing
	[EOFMTaskTransition] (((planning = NoError) & (interpretation = NoError)) & (((aAquireCash = actReady) & aRetreiveOutputs = actExecuting)  &  (iCashOut != NoValue)  &  (aAquireCash != actExecuting & hTakeCash_4 != actExecuting))) -> 
		  (aAquireCash' = actExecuting)
	;
	// aAquireCash: Normative Executing -> Done
	[EOFMTaskTransition] (((planning = NoError) & (interpretation = NoError)) & (((aAquireCash = actExecuting) & hTakeCash_4 = actDone)  &   !  (iCashOut != NoValue))) -> 
		  (aAquireCash' = actDone)
	;
	// aAquireCash:  Normative Executing -> Executing with Reset
	[EOFMTaskTransition] (((planning = NoError) & (interpretation = NoError)) & (((aAquireCash = actExecuting) & hTakeCash_4 = actDone)  &  (iCashOut != NoValue))) -> 
		  (aAquireCash' = actExecuting)
		& (hTakeCash_4' = actReady)
	;

	// Erroneous transitions for aAquireCash
	// aAquireCash: Erroneous Ready->Done Omission
	[EOFMTaskTransition] ((aAquireCash = actReady) & (planning = Error) & ((aAquireCash = actReady) & aRetreiveOutputs = actExecuting)) -> 
		  (aAquireCash' = actDone)
	;
	// aAquireCash: Erroenous Ready->Ready Delay
	[EOFMTaskTransition] ((aAquireCash = actReady) & ((planning = Error) | (interpretation = Error)) & ((aAquireCash = actReady) & aRetreiveOutputs = actExecuting) & (iCashOut != NoValue)) -> 
		  (aAquireCash' = actReady)
	;
	// aAquireCash: Erroneous Ready->Exeucting Intrusion
	[EOFMTaskTransition] ((aAquireCash = actReady) & (((planning = Error) & ( ! ((aAquireCash = actReady) & aRetreiveOutputs = actExecuting) |  ! (iCashOut != NoValue))) | ((interpretation = Error) & ( ! (iCashOut != NoValue))))) -> 
		  (aAquireCash' = actExecuting)
	;
	// aAquireCash: Erroneous Executing->Executing Delay
	[EOFMTaskTransition] ((aAquireCash = actExecuting) & (((planning = Error) | (interpretation = Error)) & (((aAquireCash = actExecuting) & hTakeCash_4 = actDone)) & (iCashOut != NoValue))) -> 
		  (aAquireCash' = actExecuting)
	;
	// aAquireCash: Erroneous Executing->Executing with Reset (Restart)
	[EOFMTaskTransition] ((aAquireCash = actExecuting) & ((planning = Error) & ( ! (((aAquireCash = actExecuting) & hTakeCash_4 = actDone)) |  ! (iCashOut != NoValue)) | (interpretation = Error) & ( ! (iCashOut != NoValue)))) -> 
		  (aAquireCash' = actExecuting)
		& (hTakeCash_4' = actReady)
	;
	// aAquireCash: Erroneous Executing->Done Omission
	[EOFMTaskTransition] ((aAquireCash = actExecuting) & ((planning = Error) & ( ! ((aAquireCash = actExecuting) & hTakeCash_4 = actDone)))) -> 
		  (aAquireCash' = actDone)
	;
	// aAquireCash: Erroneous Done->Executing Intrusion
	[EOFMTaskTransition] ((aAquireCash = actDone) & ((planning = Error))) -> 
		  (aAquireCash' = actExecuting)
		& (hTakeCash_4' = actReady)
	;
	// aAquireCash: allows the actions to be reset normatively for activities that are done erroneously when the parent is ready
	[EOFMTaskTransition] ((aAquireCash = actDone) & (aRetreiveOutputs = actReady)) -> 
		  (aAquireCash' = actReady)
		& (hTakeCash_4' = actReady)
	;

	// Normative transitions for hTakeCash_4
	// hTakeCash_4: Normative Ready->Executing
	[EOFMTaskTransition] ((execution = NoError) & (hTakeCash_4 = actReady) & (aAquireCash = actExecuting) & ready) -> 
		  (hTakeCash_4' = actExecuting)
		& (hTakeCash' = true)
		& (submitted' = true)
	;

	// Erroneous transitions for hTakeCash_4
	// hTakeCash_4: Erroenous Ready->Executing or Done->Executing sequence error / intrusion
	[EOFMTaskTransition] ((execution = Error) & (((hTakeCash_4 = actReady) &  ! (aAquireCash = actExecuting)) | (hTakeCash_4 = actDone)) & ready) -> 
		  (hTakeCash_4' = actExecuting)
		& (hTakeCash' = true)
		& (submitted' = true)
	;
	// hTakeCash_4: Erroenous Ready->Executing or Done->Executing doing the a wrong action in place of the right one
	[EOFMTaskTransition] ((execution = Error) & (hTakeCash_4 = actReady) & (aAquireCash = actExecuting) & ready) -> 
		  (hTakeCash_4' = actExecuting)
		& (hEnterPIN' = CorrectPIN)
		& (submitted' = true)
	;
	// hTakeCash_4: Erroenous Ready->Executing or Done->Executing doing the a wrong action in place of the right one
	[EOFMTaskTransition] ((execution = Error) & (hTakeCash_4 = actReady) & (aAquireCash = actExecuting) & ready) -> 
		  (hTakeCash_4' = actExecuting)
		& (hTakeCard' = true)
		& (submitted' = true)
	;
	// hTakeCash_4: Erroenous Ready->Executing or Done->Executing doing the a wrong action in place of the right one
	[EOFMTaskTransition] ((execution = Error) & (hTakeCash_4 = actReady) & (aAquireCash = actExecuting) & ready) -> 
		  (hTakeCash_4' = actExecuting)
		& (hEnterCashVal' = lDesiredValue)
		& (submitted' = true)
	;
	// hTakeCash_4: Erroenous Ready->Executing or Done->Executing doing the a wrong action in place of the right one
	[EOFMTaskTransition] ((execution = Error) & (hTakeCash_4 = actReady) & (aAquireCash = actExecuting) & ready) -> 
		  (hTakeCash_4' = actExecuting)
		& (hEnterCard' = true)
		& (submitted' = true)
	;
	// hTakeCash_4: Erroenous Ready->Done Omission
	[EOFMTaskTransition] ((execution = Error) & (hTakeCash_4 = actReady) & (aAquireCash = actExecuting) & ready) -> 
		  (hTakeCash_4' = actDone)
	;
	// hTakeCash_4: Erroenous Ready->Ready Delay
	[EOFMTaskTransition] ((execution = Error) & (hTakeCash_4 = actReady) & (aAquireCash = actExecuting) & ready) -> 
		  (hTakeCash_4' = actReady)
		& (submitted' = true)
	;
	// hTakeCash_4: Done->Ready  allows the actions to be reset normatively for activities that are done erroneously when the parent is ready
	[EOFMTaskTransition] ((hTakeCash_4 = actDone) & (aAquireCash = actReady)) -> 
		  (hTakeCash_4' = actReady)
	;

	// Normative transitions for aRetreiveCard
	// aRetreiveCard: Normative Ready -> Executing
	[EOFMTaskTransition] (((planning = NoError) & (interpretation = NoError)) & (((aRetreiveCard = actReady) & aRetreiveOutputs = actExecuting)  &  (iCardPresent)  &  (aRetreiveCard != actExecuting & hTakeCard_5 != actExecuting))) -> 
		  (aRetreiveCard' = actExecuting)
	;
	// aRetreiveCard: Normative Executing -> Done
	[EOFMTaskTransition] (((planning = NoError) & (interpretation = NoError)) & (((aRetreiveCard = actExecuting) & hTakeCard_5 = actDone)  &   !  (iCardPresent))) -> 
		  (aRetreiveCard' = actDone)
	;
	// aRetreiveCard:  Normative Executing -> Executing with Reset
	[EOFMTaskTransition] (((planning = NoError) & (interpretation = NoError)) & (((aRetreiveCard = actExecuting) & hTakeCard_5 = actDone)  &  (iCardPresent))) -> 
		  (aRetreiveCard' = actExecuting)
		& (hTakeCard_5' = actReady)
	;

	// Erroneous transitions for aRetreiveCard
	// aRetreiveCard: Erroneous Ready->Done Omission
	[EOFMTaskTransition] ((aRetreiveCard = actReady) & (planning = Error) & ((aRetreiveCard = actReady) & aRetreiveOutputs = actExecuting)) -> 
		  (aRetreiveCard' = actDone)
	;
	// aRetreiveCard: Erroenous Ready->Ready Delay
	[EOFMTaskTransition] ((aRetreiveCard = actReady) & ((planning = Error) | (interpretation = Error)) & ((aRetreiveCard = actReady) & aRetreiveOutputs = actExecuting) & (iCardPresent)) -> 
		  (aRetreiveCard' = actReady)
	;
	// aRetreiveCard: Erroneous Ready->Exeucting Intrusion
	[EOFMTaskTransition] ((aRetreiveCard = actReady) & (((planning = Error) & ( ! ((aRetreiveCard = actReady) & aRetreiveOutputs = actExecuting) |  ! (iCardPresent))) | ((interpretation = Error) & ( ! (iCardPresent))))) -> 
		  (aRetreiveCard' = actExecuting)
	;
	// aRetreiveCard: Erroneous Executing->Executing Delay
	[EOFMTaskTransition] ((aRetreiveCard = actExecuting) & (((planning = Error) | (interpretation = Error)) & (((aRetreiveCard = actExecuting) & hTakeCard_5 = actDone)) & (iCardPresent))) -> 
		  (aRetreiveCard' = actExecuting)
	;
	// aRetreiveCard: Erroneous Executing->Executing with Reset (Restart)
	[EOFMTaskTransition] ((aRetreiveCard = actExecuting) & ((planning = Error) & ( ! (((aRetreiveCard = actExecuting) & hTakeCard_5 = actDone)) |  ! (iCardPresent)) | (interpretation = Error) & ( ! (iCardPresent)))) -> 
		  (aRetreiveCard' = actExecuting)
		& (hTakeCard_5' = actReady)
	;
	// aRetreiveCard: Erroneous Executing->Done Omission
	[EOFMTaskTransition] ((aRetreiveCard = actExecuting) & ((planning = Error) & ( ! ((aRetreiveCard = actExecuting) & hTakeCard_5 = actDone)))) -> 
		  (aRetreiveCard' = actDone)
	;
	// aRetreiveCard: Erroneous Done->Executing Intrusion
	[EOFMTaskTransition] ((aRetreiveCard = actDone) & ((planning = Error))) -> 
		  (aRetreiveCard' = actExecuting)
		& (hTakeCard_5' = actReady)
	;
	// aRetreiveCard: allows the actions to be reset normatively for activities that are done erroneously when the parent is ready
	[EOFMTaskTransition] ((aRetreiveCard = actDone) & (aRetreiveOutputs = actReady)) -> 
		  (aRetreiveCard' = actReady)
		& (hTakeCard_5' = actReady)
	;

	// Normative transitions for hTakeCard_5
	// hTakeCard_5: Normative Ready->Executing
	[EOFMTaskTransition] ((execution = NoError) & (hTakeCard_5 = actReady) & (aRetreiveCard = actExecuting) & ready) -> 
		  (hTakeCard_5' = actExecuting)
		& (hTakeCard' = true)
		& (submitted' = true)
	;

	// Erroneous transitions for hTakeCard_5
	// hTakeCard_5: Erroenous Ready->Executing or Done->Executing sequence error / intrusion
	[EOFMTaskTransition] ((execution = Error) & (((hTakeCard_5 = actReady) &  ! (aRetreiveCard = actExecuting)) | (hTakeCard_5 = actDone)) & ready) -> 
		  (hTakeCard_5' = actExecuting)
		& (hTakeCard' = true)
		& (submitted' = true)
	;
	// hTakeCard_5: Erroenous Ready->Executing or Done->Executing doing the a wrong action in place of the right one
	[EOFMTaskTransition] ((execution = Error) & (hTakeCard_5 = actReady) & (aRetreiveCard = actExecuting) & ready) -> 
		  (hTakeCard_5' = actExecuting)
		& (hEnterPIN' = CorrectPIN)
		& (submitted' = true)
	;
	// hTakeCard_5: Erroenous Ready->Executing or Done->Executing doing the a wrong action in place of the right one
	[EOFMTaskTransition] ((execution = Error) & (hTakeCard_5 = actReady) & (aRetreiveCard = actExecuting) & ready) -> 
		  (hTakeCard_5' = actExecuting)
		& (hEnterCashVal' = lDesiredValue)
		& (submitted' = true)
	;
	// hTakeCard_5: Erroenous Ready->Executing or Done->Executing doing the a wrong action in place of the right one
	[EOFMTaskTransition] ((execution = Error) & (hTakeCard_5 = actReady) & (aRetreiveCard = actExecuting) & ready) -> 
		  (hTakeCard_5' = actExecuting)
		& (hTakeCash' = true)
		& (submitted' = true)
	;
	// hTakeCard_5: Erroenous Ready->Executing or Done->Executing doing the a wrong action in place of the right one
	[EOFMTaskTransition] ((execution = Error) & (hTakeCard_5 = actReady) & (aRetreiveCard = actExecuting) & ready) -> 
		  (hTakeCard_5' = actExecuting)
		& (hEnterCard' = true)
		& (submitted' = true)
	;
	// hTakeCard_5: Erroenous Ready->Done Omission
	[EOFMTaskTransition] ((execution = Error) & (hTakeCard_5 = actReady) & (aRetreiveCard = actExecuting) & ready) -> 
		  (hTakeCard_5' = actDone)
	;
	// hTakeCard_5: Erroenous Ready->Ready Delay
	[EOFMTaskTransition] ((execution = Error) & (hTakeCard_5 = actReady) & (aRetreiveCard = actExecuting) & ready) -> 
		  (hTakeCard_5' = actReady)
		& (submitted' = true)
	;
	// hTakeCard_5: Done->Ready  allows the actions to be reset normatively for activities that are done erroneously when the parent is ready
	[EOFMTaskTransition] ((hTakeCard_5 = actDone) & (aRetreiveCard = actReady)) -> 
		  (hTakeCard_5' = actReady)
	;
	[EOFMTaskTransition] (true) -> 
		  (submitted' = submitted)
	;
	[EOFMHandshake] (submitted  &   !  ready) -> 
		  (submitted' = false)
		& (hEnterCard_1' = (hEnterCard_1 = actExecuting) ? actDone : hEnterCard_1)
		& (hEnterPIN_2' = (hEnterPIN_2 = actExecuting) ? actDone : hEnterPIN_2)
		& (hEnterCashVal_3' = (hEnterCashVal_3 = actExecuting) ? actDone : hEnterCashVal_3)
		& (hTakeCash_4' = (hTakeCash_4 = actExecuting) ? actDone : hTakeCash_4)
		& (hTakeCard_5' = (hTakeCard_5 = actExecuting) ? actDone : hTakeCard_5)
		& (hEnterCard' = false)
		& (hTakeCash' = false)
		& (hTakeCard' = false)
		& (hCancel' = false)
	;
endmodule

module sys

	ready 			: bool 						init true;
	iInterfaceState : [Welcome..OutputCard] 	init Welcome;
	iCardPresent 	: bool 						init false;
	iCashOut 		: [NoValue..IncorrectValue] init NoValue;
	
	[EOFMHandshake] (submitted  &   !  ready) -> 
		  (ready' = true)
	;
	[Welcome_to_EnterPIN] (iInterfaceState = Welcome & hEnterCard) & (ready & submitted) -> 
		  (ready' = false)
		& (iInterfaceState' = EnterPIN)
	;
	[EnterPIN_to_OutputCard] (iInterfaceState = EnterPIN & hCancel) & (ready & submitted) -> 
		  (ready' = false)
		& (iInterfaceState' = OutputCard)
	;
	[EnterPIN_to_Withdraw] (iInterfaceState = EnterPIN & hEnterPIN_2 = actExecuting & hEnterPIN = CorrectPIN) & (ready & submitted) -> 
		  (ready' = false)
		& (iInterfaceState' = Withdraw)
	;
	[EnterPIN_to_EnterPIN] (iInterfaceState = EnterPIN & hEnterPIN_2 = actExecuting & hEnterPIN = IncorrectPIN) & (ready & submitted) -> 
		  (ready' = false)
		& (iInterfaceState' = EnterPIN)
	;
	[Withdraw_to_OutputCard] (iInterfaceState = Withdraw & hCancel) & (ready & submitted) -> 
		  (ready' = false)
		& (iInterfaceState' = OutputCard)
		& (iCardPresent' = true)
	;
	[Withdraw_to_OutputCash] (iInterfaceState = Withdraw & hEnterCashVal_3 = actExecuting & hEnterCashVal > NoValue) & (ready & submitted) -> 
		  (ready' = false)
		& (iInterfaceState' = OutputCash)
		& (iCashOut' = hEnterCashVal)
	;
	[Withdraw_to_Withdraw] (iInterfaceState = Withdraw & hEnterCashVal_3 = actExecuting & hEnterCashVal = NoValue) & (ready & submitted) -> 
		  (ready' = false)
		& (iInterfaceState' = Withdraw)
	;
	[OutputCash_to_OutputCard] (iInterfaceState = OutputCash & hTakeCash) & (ready & submitted) -> 
		  (ready' = false)
		& (iInterfaceState' = OutputCard)
		& (iCashOut' = NoValue)
		& (iCardPresent' = true)
	;
	[OutputCard_to_Welcome] (iInterfaceState = OutputCard & hTakeCard) & (ready & submitted) -> 
		  (ready' = false)
		& (iInterfaceState' = Welcome)
		& (iCardPresent' = false)
	;
endmodule

//label "cardleft"   = ((aGetCash=actDone)&(iCardPresent));
//label "success"    = ((aGetCash=actDone)&(!iCardPresent)&(iCashOut=NoValue));
//label "cashleft"   = ((aGetCash=actDone)&(iCashOut!=NoValue));

label "cardleft"   = ((aGetCash=actDone)&(( iCardPresent)&(iCashOut=NoValue)));
label "cashleft"   = ((aGetCash=actDone)&((!iCardPresent)&(iCashOut>NoValue)));
label "notsuccess" = ((aGetCash=actDone)&(( iCardPresent)|(iCashOut>NoValue)));

