// January 19, 2014
//----------------------------------------------------------------------------------------
// 	Withdraw money from ATM
// 	from 
// 	Mikhail Auguston, Example 7 in Monterey Phoenix System and Software Architecture
// 	 Modeling Language (Draft): Examples of architecture models  
// 	 Naval Postgraduate School, Monterey, CA, USA
// 	http://faculty.nps.edu/maugusto/
// 	for eagle6: Runs up to the scope 3
//---------------------------------------------------------------------------------------- 

//SCHEMA ATM_withdrawal

ROOT Customer: (* insert_card
                  ( ( identification_succeeds
                   request_withdrawal
                   ( get_money | not_sufficient_funds ) ) |
                 identification_fails )                    *);

ROOT ATM_system: (* read_card validate_id
                    ( ( id_successful check_balance
                      ( ( sufficient_balance dispense_money ) |
                       unsufficient_balance ) )            |

	              id_failed )                          *);

ROOT Data_Base: (* ( validate_id | check_balance ) *);

Data_Base, ATM_system SHARE ALL validate_id, check_balance;

//-----------------------------------------------------------------
// simulating COORDINATE with SHARE ALL
//-----------------------------------------------------------------
//COORDINATE (* $x:insert_card *) FROM Customer,
//           (* $y:read_card *) FROM ATM_system             ADD $x PRECEDES $y;
//COORDINATE (* $x:request_withdrawal *) FROM Customer,
//           (* $y:check_balance *) FROM ATM_system         ADD $x PRECEDES $y;
//COORDINATE (* $x:identification_succeeds *) FROM Customer,
//           (* $y:id_successful *) FROM ATM_system         ADD $y PRECEDES $x;
//COORDINATE (* $x:get_money *) FROM Customer,
//           (* $y:dispense_money *) FROM ATM_system        ADD $y PRECEDES $x;
//COORDINATE (* $x:not_sufficient_funds *) FROM Customer,
//           (* $y:unsufficient_balance *) FROM ATM_system  ADD $y PRECEDES $x;
//COORDINATE (* $x:identification_fails *) FROM Customer,
//           (* $y:id_failed *) FROM ATM_system             ADD $y PRECEDES $x;
//------------------------------------------------------------------
ROOT 	Card: (* (insert_card read_card) *);
Customer, Card 		SHARE ALL 	insert_card;
ATM_System, Card	SHARE ALL 	read_card;

ROOT 	AuthenticationSuccess: (* (id_successful  identification_succeeds) *);
Customer, AuthenticationSuccess 	SHARE ALL 	identification_succeeds;
ATM_System, AuthenticationSuccess 	SHARE ALL 	id_successful;

ROOT 	AuthenticationFailure: (* (id_failed  identification_fails) *);
Customer, AuthenticationFailure 	SHARE ALL 	identification_fails;
ATM_System, AuthenticationFailure 	SHARE ALL 	id_failed;

ROOT 	WithdrawalRequest: (* (request_withdrawal check_balance) *);
Customer, WithdrawalRequest 	SHARE ALL 	request_withdrawal;
ATM_System, WithdrawalRequest 	SHARE ALL 	check_balance;

ROOT 	LowBalance: (* (unsufficient_balance  not_sufficient_funds) *);
Customer, LowBalance 	SHARE ALL 	not_sufficient_funds;
ATM_System, LowBalance	SHARE ALL 	unsufficient_balance;

ROOT 	Money: (* (dispense_money  get_money) *);
Customer, Money 	SHARE ALL 	get_money;
ATM_System, Money 	SHARE ALL 	dispense_money;