%
% $Id: hekate_case_cashpoint-mdl.pl,v 1.2 2009-10-29 01:15:14 kinio Exp $
%
% The well known Thermostat case model from Negnevtisky,
% original analysis  G, J, Nalepa and A, Ligeza
% ARD+ analysis + VARDA modelling by I, Wojnicki and G,J, Nalepa
%
%
%     Copyright (C) 2006-9 by the HeKatE Project
%
%     VARDA has been develped by the HeKatE Project, 
%     see http://hekate,ia,agh,edu,pl
%
%     This file is part of VARDA,
%
%     VARDA is free software: you can redistribute it and/or modify
%     it under the terms of the GNU General Public License as published by
%     the Free Software Foundation, either version 3 of the License, or
%     (at your option) any later version,
%
%     VARDA is distributed in the hope that it will be useful,
%     but WITHOUT ANY WARRANTY; without even the implied warranty of
%     MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE,  See the
%     GNU General Public License for more details,
%
%     You should have received a copy of the GNU General Public License
%     along with VARDA,  If not, see <http://www,gnu,org/licenses/>,
%


varda_model_desc :- write('The CashPoint use case $Id: hekate_case_cashpoint-mdl.pl,v 1.2 2009-10-29 01:15:14 kinio Exp $').

varda_model_cashpoint :-

     ard_att_add('CashPoint'),
     ard_property_add(['CashPoint']),

     ard_att_add('UserRequestedAction'),
     ard_att_add('ActionEnvironment'),
     ard_att_add('CashPointActivity'),
     ard_finalize(['CashPoint'], ['UserRequestedAction', 'ActionEnvironment', 'CashPointActivity']),
     ard_split(
          ['UserRequestedAction', 'ActionEnvironment', 'CashPointActivity'],
          [
               ['UserRequestedAction'], ['ActionEnvironment'], ['CashPointActivity']
          ],
          [
               [['UserRequestedAction'], ['CashPointActivity']],
               [['ActionEnvironment'], ['CashPointActivity']]
          ]
     ),
     
     ard_att_add('userRequestedAction'),
     ard_finalize(['UserRequestedAction'], ['userRequestedAction']),
     %ard_split(
     %     ['userRequestedAction'],
     %     [
     %          ['userRequestedAction']
     %     ],
     %     [
     %          [['userRequestedAction'], ['CashPointActivity']]
     %     ]
     %),
     
     ard_att_add('cashPointActivity'),
     ard_finalize(['CashPointActivity'], ['cashPointActivity']),
     %ard_split(
     %     ['cashPointActivity'],
     %     [
     %          ['cashPointActivity']
     %     ],
     %     [
     %          [['userRequestedAction'], ['cashPointActivity']]
     %     ]
     %),
          
     ard_att_add('Authorization'),
     ard_att_add('Founds'),
     ard_finalize(['ActionEnvironment'], ['Authorization', 'Founds']),
     ard_split(
          ['Authorization', 'Founds'],
          [
               ['Authorization'], ['Founds']
          ],
          [
               [['Authorization'], ['cashPointActivity']],
               [['Founds'], ['cashPointActivity']]
          ]
     ),
     
     ard_att_add('desiredAmount'),
     ard_att_add('UserResources'),
     ard_att_add('CashPointResources'),
     ard_att_add('EnoughResources'),
     ard_finalize(['Founds'], ['desiredAmount', 'UserResources', 'CashPointResources', 'EnoughResources']),
     ard_split(
          ['desiredAmount', 'UserResources', 'CashPointResources', 'EnoughResources'],
          [
               ['desiredAmount'], ['UserResources'], ['CashPointResources'], ['EnoughResources']
          ],
          [
               [['desiredAmount'], ['EnoughResources']],
               [['UserResources'], ['EnoughResources']],
               [['CashPointResources'], ['EnoughResources']],
               [['EnoughResources'], ['cashPointActivity']]
          ]
     ),
     
     ard_att_add('userAccountAmount'),
     ard_finalize(['UserResources'], ['userAccountAmount']),
     %ard_split(
     %     ['userAccountAmount'],
     %     [
     %          ['userAccountAmount']
     %     ],
     %     [
     %          [['userAccountAmount'], ['EnoughResources']]
     %     ]
     %),
     
     ard_att_add('cashPointAmount'),
     ard_finalize(['CashPointResources'], ['cashPointAmount']),
     %ard_split(
     %     ['cashPointAmount'],
     %     [
     %          ['cashPointAmount']
     %     ],
     %     [
     %          [['cashPointAmount'], ['EnoughResources']]
     %     ]
     %),
     
     ard_att_add('enteredPin'),
     ard_att_add('correctPin'),
     ard_att_add('pinDifference'),
     ard_att_add('authorizated'),
     ard_att_add('failedAttempts'),
     ard_finalize(['Authorization'], ['enteredPin', 'correctPin', 'pinDifference', 'authorizated', 'failedAttempts']),
     ard_split(
          ['enteredPin', 'correctPin', 'pinDifference', 'authorizated', 'failedAttempts'],
          [
               ['enteredPin'], ['correctPin'], ['pinDifference'], ['authorizated'], ['failedAttempts']
          ],
          [
               [['enteredPin'], ['pinDifference']],
               [['correctPin'], ['pinDifference']],
               [['pinDifference'], ['authorizated']],
               [['pinDifference'], ['failedAttempts']],
               [['authorizated'], ['cashPointActivity']],
               [['failedAttempts'], ['cashPointActivity']]
          ]
     ),
     
     ard_att_add('cdAmountDifference'),
     ard_att_add('udAmountDifference'),
     ard_finalize(['EnoughResources'], ['cdAmountDifference', 'udAmountDifference']),
     ard_split(
          ['cdAmountDifference', 'udAmountDifference'],
          [
               ['cdAmountDifference'], ['udAmountDifference']
          ],
          [
               [['desiredAmount'], ['cdAmountDifference']],
               [['cashPointAmount'], ['cdAmountDifference']],
               [['cdAmountDifference'], ['cashPointActivity']],
               [['desiredAmount'], ['udAmountDifference']],
               [['userAccountAmount'], ['udAmountDifference']],
               [['udAmountDifference'], ['cashPointActivity']]
          ]
     ).

:- varda_model_cashpoint.