begin_problem(SAPAuthorizations).

list_of_descriptions.
name({* Analzsis of Authorizations in SAP R/3*}).
author({* Manuel Lamotte-Schubert *}).
status(satisfiable).
description({* Check for saturation, i.e. that the model does not contain
any contradiction. *}).
end_of_list.


list_of_symbols.
  functions[
% -------------- constants
% authorizations
	(STAR,0),   % All
	(01,0),	    % Create or Generate
	(02,0),	    % Change
	(03,0),	    % Display
	(06,0),	    % Delete
	(08,0),	    % Display Change Documents
	(09,0),	    % Display Prices
            
% authorization objects
	(S_TCODE,0),	 % Verifcation of Transaction Code
	(M_BANF_WRK,0),	 % Plant in BANF
	(M_BANF_BSA,0),	 % Document Type in BANF
	(M_BANF_EKG,0),	 % Purchasing Group in BANF
	(M_BEST_EKO,0),	 % Purchasing Organization in Order
	(M_BEST_BSA,0),	 % Document Type in Order
	(M_BEST_WRK,0),	 % Plant in Order
	(M_BEST_EKG,0),	 % Purchasing Group in Order
	(M_EINK_FRG,0),	 % Release Code and Release Group in Purchase
	(M_EINK_MKL,0),  % manual authorization object (non-SAP-default): Material Group
	(M_EINK_GWT,0),  % manual authorization object (non-SAP-default:): Overall Value
            
% authorization object fields
 	(TCD,0),
 	(ACTVT,0),
  (WERKS,0),
  (BSART,0),
  (EKGRP,0),
	(EKORG,0),
	(FRGGR,0),
	(FRGCO,0),
	(MATKL,0),
	(GSWRT,0),
   		
% (authorization) values
 	(INF,0),							% same value for WERKS (Plant) and EKORG (Purchasing Organization, Infotainment company)
	(ADSU,0),							% WERKS, EKORG (Advertisement subsidiary)
	(GRSU,0),							% WERKS, EKORG (Graphics subsidiary)
	(NB,0),								% BSART (Purchasing Document Type)
	(DIRECT,0),						% BSART (Purchasing Document Type)
	(I26,0),							% EKGRP (Purchasing Group)
	(I27,0),							% EKGRP (Purchasing Group)
	(W1,0),								% Release Code W1
	(W2,0),								% Release Code W2
	(RGRP_01,0),					% Release Group RGRP_01
	(B0002,0),						% Value for MATKL: Office Material
	(LESS_EQUAL_1000_EUR,0),			% Value for GSWRT: Amount less than or equal 500 EUR
	(GREATER_1000_LESS_10000_EUR,0),	% Value for GSWRT: Amount greater than 500 EUR
	(GREATER_10000_EUR,0),
	(GREATER_20000_EUR,0),

% release strategies, names...
	(KF,0),                 % Release Strategy: Cost Center Release
	(VF,0),                 % Release Strategy: Management Release
	(FRG_EBAN,0),           % Release Class for Requisitions
	(FRG_CEBAN_EKGRP,0),    % Property EKGRP
	(FRG_CEBAN_WERKS,0),    % Property WERKS
	(FRG_CEBAN_MATKL,0),    % Property MATKL
	(FRG_CEBAN_GSWRT,0),    % Property GSWRT
	


% transactions
	(ME51N,0),			% Create Requisition
	(ME52N,0),			% Change Requisition
	(ME53N,0),			% View Requisition
	(ME54N,0),			% Single Release
%	(ME56,0),			% Map Distributor to Requisition
	(ME21N,0),			% Create Order
	(ME22N,0),			% Change Order
	(ME23N,0),			% View Order
	(ME21NOFF,0),   % Create limited Order (no requisition required)
            
% users
	(LAMOTTE,0),
	(MUELLER,0),
	(KAISER,0),
	(MEIER,0),
	(SCHMITT,0),
			
% role names
	(ZBANF_WRK_INF_ED,0),
	(ZRELEASE_WRK_INF_BASE,0),		% Base Role for Releases in Plant INF
	(ZRELEASE_WRK_INF_W1,0),		% Cost Center Release (Grp=1, Code=W1), use only in combination
										% with role Z_LAMOTTE_RELEASE_INF_BASE
	(ZRELEASE_WRK_INF_W2,0),		% Management Release (Grp=1, Code=W2)
	(ZORDER_WRK_INF_BASE,0),
	(ZORDER_WRK_INF_TYPE_ALL,0),
	(ZORDER_WRK_INF_TYPE_OFFICE,0),
	(ZORDER_WRK_INF_ALL,0),
	(ZORDER_WRK_INF_OFFICE,0),
	(ZBANF_WRK_ADSU_ED,0),
	(ZORDER_WRK_ADSU_ED,0),
	(ZRELEASE_WRK_INF_W1_MULTI,0),
	(ZRELEASE_WRK_INF_W2_MULTI,0),

% business roles
	(BANF,0),
	(ORDER,0),
            
% -------------- functions
	(userProfileEntry,2),
	(authObj,3),
	(profileEntry,2),
	(singleRoleEntry,2),
	(compositeRoleEntry,2),
	(property,2),
	(class,2)
           
  ].
          	
          	
  predicates[
	(DirectPurchase,1),
	(StandardPurchase,1),
	(User,1),
 	(UserProfile,1),
	(SingleRole,1),
	(CompositeRole,1),
	(Profile,1),
	(ReleaseRequirement,3),			% defines, which release codes are necessary to release
	(ReleaseStrategy,3),			% defines the conditions whether a release strategy is applied to a requisition or not
	(Access,2),       				% checks the value of an authorization object to the value inside the users profile -> grant access or not
	(Enfolds,2),      				% checks if authorization object 1 enfolds authorization object 2 (i.e. the value)
	(Holds,2),						% relation which indicates, which (single,composite)roles/profiles an user holds
	(Requisition,9),				% denotes the "wish" to order an item
	(RequisitionCreated,10),		% denotes that a requisition has been created
	(RequisitionReleasedStep,13),	% denotes that a requisition matching the release code and group is released (inside the release process)
	(RequisitionReleased,10),		% denotes that a requisition is completely released
	(OrderCreated,10)				% denotes that an order has been created
  ].
end_of_list.

list_of_formulae(axioms).

% ============== Profile Layer ==============

% only for readability
%formula(User(LAMOTTE)).
%formula(User(MUELLER)).
%formula(User(KAISER)).
%formula(User(MEIER)).
%formula(User(SCHMITT)).


% -------- Single Roles --------
% ZBANF_WRK_ADSU_ED: Authorization to create requisitions for and with plant ADSU, purchase group I26
formula(SingleRole(singleRoleEntry(ZBANF_WRK_ADSU_ED,authObj(S_TCODE,TCD,ME51N)))).
formula(SingleRole(singleRoleEntry(ZBANF_WRK_ADSU_ED,authObj(S_TCODE,TCD,ME52N)))).
formula(SingleRole(singleRoleEntry(ZBANF_WRK_ADSU_ED,authObj(S_TCODE,TCD,ME53N)))).
formula(SingleRole(singleRoleEntry(ZBANF_WRK_ADSU_ED,authObj(M_BANF_WRK,ACTVT,01)))).
formula(SingleRole(singleRoleEntry(ZBANF_WRK_ADSU_ED,authObj(M_BANF_WRK,ACTVT,02)))).
formula(SingleRole(singleRoleEntry(ZBANF_WRK_ADSU_ED,authObj(M_BANF_WRK,ACTVT,03)))).
formula(SingleRole(singleRoleEntry(ZBANF_WRK_ADSU_ED,authObj(M_BANF_WRK,WERKS,ADSU)))).
formula(SingleRole(singleRoleEntry(ZBANF_WRK_ADSU_ED,authObj(M_BANF_BSA,ACTVT,STAR)))).
formula(SingleRole(singleRoleEntry(ZBANF_WRK_ADSU_ED,authObj(M_BANF_BSA,BSART,STAR)))).
formula(SingleRole(singleRoleEntry(ZBANF_WRK_ADSU_ED,authObj(M_BANF_EKG,ACTVT,STAR)))).
formula(SingleRole(singleRoleEntry(ZBANF_WRK_ADSU_ED,authObj(M_BANF_EKG,EKGRP,I26)))).

% ZBANF_WRK_INF_ED
% role to create requisitions for plant INF, purchase group I26
formula(SingleRole(singleRoleEntry(ZBANF_WRK_INF_ED,authObj(S_TCODE,TCD,ME51N)))).
formula(SingleRole(singleRoleEntry(ZBANF_WRK_INF_ED,authObj(M_BANF_WRK,ACTVT,01)))).
formula(SingleRole(singleRoleEntry(ZBANF_WRK_INF_ED,authObj(M_BANF_WRK,ACTVT,02)))).
formula(SingleRole(singleRoleEntry(ZBANF_WRK_INF_ED,authObj(M_BANF_WRK,ACTVT,03)))).
formula(SingleRole(singleRoleEntry(ZBANF_WRK_INF_ED,authObj(M_BANF_WRK,WERKS,INF)))).
formula(SingleRole(singleRoleEntry(ZBANF_WRK_INF_ED,authObj(M_BANF_BSA,ACTVT,STAR)))).
formula(SingleRole(singleRoleEntry(ZBANF_WRK_INF_ED,authObj(M_BANF_BSA,BSART,STAR)))).
formula(SingleRole(singleRoleEntry(ZBANF_WRK_INF_ED,authObj(M_BANF_EKG,ACTVT,STAR)))).
formula(SingleRole(singleRoleEntry(ZBANF_WRK_INF_ED,authObj(M_BANF_EKG,EKGRP,I26)))).



% ZRELEASE_WRK_INF_BASE
% permits access to release and view requisitions, but does not specify a release group or code
% --> see extensions
formula(SingleRole(singleRoleEntry(ZRELEASE_WRK_INF_BASE,authObj(S_TCODE,TCD,ME53N)))).
formula(SingleRole(singleRoleEntry(ZRELEASE_WRK_INF_BASE,authObj(S_TCODE,TCD,ME54N)))).
formula(SingleRole(singleRoleEntry(ZRELEASE_WRK_INF_BASE,authObj(M_BANF_BSA,ACTVT,02)))).
formula(SingleRole(singleRoleEntry(ZRELEASE_WRK_INF_BASE,authObj(M_BANF_BSA,ACTVT,03)))).
formula(SingleRole(singleRoleEntry(ZRELEASE_WRK_INF_BASE,authObj(M_BANF_BSA,ACTVT,08)))).
formula(SingleRole(singleRoleEntry(ZRELEASE_WRK_INF_BASE,authObj(M_BANF_BSA,BSART,NB)))).
formula(SingleRole(singleRoleEntry(ZRELEASE_WRK_INF_BASE,authObj(M_BANF_EKG,ACTVT,02)))).
formula(SingleRole(singleRoleEntry(ZRELEASE_WRK_INF_BASE,authObj(M_BANF_EKG,ACTVT,03)))).
formula(SingleRole(singleRoleEntry(ZRELEASE_WRK_INF_BASE,authObj(M_BANF_EKG,ACTVT,08)))).
formula(SingleRole(singleRoleEntry(ZRELEASE_WRK_INF_BASE,authObj(M_BANF_EKG,EKGRP,I26)))).
%formula(SingleRole(singleRoleEntry(ZRELEASE_WRK_INF_BASE,authObj(M_BANF_EKO,ACTVT,03)))).
%formula(SingleRole(singleRoleEntry(ZRELEASE_WRK_INF_BASE,authObj(M_BANF_EKO,ACTVT,08)))).
%formula(SingleRole(singleRoleEntry(ZRELEASE_WRK_INF_BASE,authObj(M_BANF_EKO,EKORG,INF)))).
formula(SingleRole(singleRoleEntry(ZRELEASE_WRK_INF_BASE,authObj(M_BANF_WRK,ACTVT,02)))).
formula(SingleRole(singleRoleEntry(ZRELEASE_WRK_INF_BASE,authObj(M_BANF_WRK,ACTVT,03)))).
formula(SingleRole(singleRoleEntry(ZRELEASE_WRK_INF_BASE,authObj(M_BANF_WRK,ACTVT,08)))).
formula(SingleRole(singleRoleEntry(ZRELEASE_WRK_INF_BASE,authObj(M_BANF_WRK,WERKS,INF)))).

% extension 1 to role RELEASE_INF_BASE:
% permits the release of requisitions with release group 01 (=single row release) and code W1 (=cost center release)
formula(SingleRole(singleRoleEntry(ZRELEASE_WRK_INF_W1,authObj(M_EINK_FRG,FRGCO,W1)))).
formula(SingleRole(singleRoleEntry(ZRELEASE_WRK_INF_W1,authObj(M_EINK_FRG,FRGGR,RGRP_01)))).

% extension 2 to role RELEASE_INF_BASE:
% permits the release of requisitions with release group 01 (=single row release) and code W2 (=management)
formula(SingleRole(singleRoleEntry(ZRELEASE_WRK_INF_W2,authObj(M_EINK_FRG,FRGCO,W2)))).
formula(SingleRole(singleRoleEntry(ZRELEASE_WRK_INF_W2,authObj(M_EINK_FRG,FRGGR,RGRP_01)))).


% ZORDER_WRK_INF_BASE
% base role to create/change/view orders
formula(SingleRole(singleRoleEntry(ZORDER_WRK_INF_BASE,authObj(S_TCODE,TCD,ME21N)))).
formula(SingleRole(singleRoleEntry(ZORDER_WRK_INF_BASE,authObj(S_TCODE,TCD,ME22N)))).
formula(SingleRole(singleRoleEntry(ZORDER_WRK_INF_BASE,authObj(S_TCODE,TCD,ME23N)))).
formula(SingleRole(singleRoleEntry(ZORDER_WRK_INF_BASE,authObj(M_BEST_EKO,ACTVT,01)))).
formula(SingleRole(singleRoleEntry(ZORDER_WRK_INF_BASE,authObj(M_BEST_EKO,ACTVT,02)))).
formula(SingleRole(singleRoleEntry(ZORDER_WRK_INF_BASE,authObj(M_BEST_EKO,ACTVT,03)))).
formula(SingleRole(singleRoleEntry(ZORDER_WRK_INF_BASE,authObj(M_BEST_EKO,ACTVT,08)))).
formula(SingleRole(singleRoleEntry(ZORDER_WRK_INF_BASE,authObj(M_BEST_EKO,ACTVT,09)))).
formula(SingleRole(singleRoleEntry(ZORDER_WRK_INF_BASE,authObj(M_BEST_EKO,EKORG,INF)))).
formula(SingleRole(singleRoleEntry(ZORDER_WRK_INF_BASE,authObj(M_BEST_BSA,ACTVT,01)))).
formula(SingleRole(singleRoleEntry(ZORDER_WRK_INF_BASE,authObj(M_BEST_BSA,ACTVT,02)))).
formula(SingleRole(singleRoleEntry(ZORDER_WRK_INF_BASE,authObj(M_BEST_BSA,ACTVT,03)))).
formula(SingleRole(singleRoleEntry(ZORDER_WRK_INF_BASE,authObj(M_BEST_BSA,ACTVT,08)))).
formula(SingleRole(singleRoleEntry(ZORDER_WRK_INF_BASE,authObj(M_BEST_BSA,ACTVT,09)))).
%formula(SingleRole(singleRoleEntry(ZORDER_WRK_INF_BASE,authObj(M_BEST_BSA,BSART,NB)))).
formula(SingleRole(singleRoleEntry(ZORDER_WRK_INF_BASE,authObj(M_BANF_BSA,ACTVT,01)))).
%formula(SingleRole(singleRoleEntry(ZORDER_WRK_INF_BASE,authObj(M_BANF_BSA,BSART,NB)))).
formula(SingleRole(singleRoleEntry(ZORDER_WRK_INF_BASE,authObj(M_BEST_WRK,ACTVT,01)))).
formula(SingleRole(singleRoleEntry(ZORDER_WRK_INF_BASE,authObj(M_BEST_WRK,ACTVT,02)))).
formula(SingleRole(singleRoleEntry(ZORDER_WRK_INF_BASE,authObj(M_BEST_WRK,ACTVT,03)))).
formula(SingleRole(singleRoleEntry(ZORDER_WRK_INF_BASE,authObj(M_BEST_WRK,ACTVT,08)))).
formula(SingleRole(singleRoleEntry(ZORDER_WRK_INF_BASE,authObj(M_BEST_WRK,ACTVT,09)))).
formula(SingleRole(singleRoleEntry(ZORDER_WRK_INF_BASE,authObj(M_BEST_WRK,WERKS,INF)))).
formula(SingleRole(singleRoleEntry(ZORDER_WRK_INF_BASE,authObj(M_BEST_EKG,ACTVT,01)))).
formula(SingleRole(singleRoleEntry(ZORDER_WRK_INF_BASE,authObj(M_BEST_EKG,ACTVT,02)))).
formula(SingleRole(singleRoleEntry(ZORDER_WRK_INF_BASE,authObj(M_BEST_EKG,ACTVT,03)))).
formula(SingleRole(singleRoleEntry(ZORDER_WRK_INF_BASE,authObj(M_BEST_EKG,ACTVT,08)))).
formula(SingleRole(singleRoleEntry(ZORDER_WRK_INF_BASE,authObj(M_BEST_EKG,ACTVT,09)))).
formula(SingleRole(singleRoleEntry(ZORDER_WRK_INF_BASE,authObj(M_BEST_EKG,EKGRP,I26)))).

% extension 1:
% -> direct order allowed: transaction code ME21NOFF, but
%   - limit to office material,
%   - limit the amount of money
formula(SingleRole(singleRoleEntry(ZORDER_WRK_INF_TYPE_OFFICE,authObj(S_TCODE,TCD,ME21NOFF)))).
formula(SingleRole(singleRoleEntry(ZORDER_WRK_INF_TYPE_OFFICE,authObj(M_EINK_MKL,MATKL,B0002)))).
formula(SingleRole(singleRoleEntry(ZORDER_WRK_INF_TYPE_OFFICE,authObj(M_EINK_GWT,GSWRT,LESS_EQUAL_1000_EUR)))).
formula(SingleRole(singleRoleEntry(ZORDER_WRK_INF_TYPE_OFFICE,authObj(M_BEST_BSA,BSART,DIRECT)))).
formula(SingleRole(singleRoleEntry(ZORDER_WRK_INF_TYPE_OFFICE,authObj(M_BANF_BSA,BSART,DIRECT)))).

% extension 2:
% - no limits -
formula(SingleRole(singleRoleEntry(ZORDER_WRK_INF_TYPE_ALL,authObj(M_EINK_MKL,MATKL,STAR)))).
formula(SingleRole(singleRoleEntry(ZORDER_WRK_INF_TYPE_ALL,authObj(M_EINK_GWT,GSWRT,STAR)))).
formula(SingleRole(singleRoleEntry(ZORDER_WRK_INF_TYPE_ALL,authObj(M_BEST_BSA,BSART,STAR)))).
formula(SingleRole(singleRoleEntry(ZORDER_WRK_INF_TYPE_ALL,authObj(M_BANF_BSA,BSART,STAR)))).


% ZORDER_WRK_ADSU_ED
% order role for plant ADSU
formula(SingleRole(singleRoleEntry(ZORDER_WRK_ADSU_ED,authObj(S_TCODE,TCD,ME21N)))).
formula(SingleRole(singleRoleEntry(ZORDER_WRK_ADSU_ED,authObj(M_BEST_EKO,ACTVT,01)))).
formula(SingleRole(singleRoleEntry(ZORDER_WRK_ADSU_ED,authObj(M_BEST_EKO,ACTVT,02)))).
formula(SingleRole(singleRoleEntry(ZORDER_WRK_ADSU_ED,authObj(M_BEST_EKO,ACTVT,03)))).
formula(SingleRole(singleRoleEntry(ZORDER_WRK_ADSU_ED,authObj(M_BEST_EKO,ACTVT,08)))).
formula(SingleRole(singleRoleEntry(ZORDER_WRK_ADSU_ED,authObj(M_BEST_EKO,ACTVT,09)))).
formula(SingleRole(singleRoleEntry(ZORDER_WRK_ADSU_ED,authObj(M_BEST_EKO,EKORG,ADSU)))).
formula(SingleRole(singleRoleEntry(ZORDER_WRK_ADSU_ED,authObj(M_BEST_BSA,ACTVT,01)))).
formula(SingleRole(singleRoleEntry(ZORDER_WRK_ADSU_ED,authObj(M_BEST_BSA,ACTVT,02)))).
formula(SingleRole(singleRoleEntry(ZORDER_WRK_ADSU_ED,authObj(M_BEST_BSA,ACTVT,03)))).
formula(SingleRole(singleRoleEntry(ZORDER_WRK_ADSU_ED,authObj(M_BEST_BSA,ACTVT,08)))).
formula(SingleRole(singleRoleEntry(ZORDER_WRK_ADSU_ED,authObj(M_BEST_BSA,ACTVT,09)))).
formula(SingleRole(singleRoleEntry(ZORDER_WRK_ADSU_ED,authObj(M_BEST_BSA,BSART,NB)))).
formula(SingleRole(singleRoleEntry(ZORDER_WRK_ADSU_ED,authObj(M_BANF_BSA,ACTVT,01)))).
formula(SingleRole(singleRoleEntry(ZORDER_WRK_ADSU_ED,authObj(M_BANF_BSA,BSART,NB)))).
formula(SingleRole(singleRoleEntry(ZORDER_WRK_ADSU_ED,authObj(M_BEST_WRK,ACTVT,01)))).
formula(SingleRole(singleRoleEntry(ZORDER_WRK_ADSU_ED,authObj(M_BEST_WRK,ACTVT,02)))).
formula(SingleRole(singleRoleEntry(ZORDER_WRK_ADSU_ED,authObj(M_BEST_WRK,ACTVT,03)))).
formula(SingleRole(singleRoleEntry(ZORDER_WRK_ADSU_ED,authObj(M_BEST_WRK,ACTVT,08)))).
formula(SingleRole(singleRoleEntry(ZORDER_WRK_ADSU_ED,authObj(M_BEST_WRK,ACTVT,09)))).
formula(SingleRole(singleRoleEntry(ZORDER_WRK_ADSU_ED,authObj(M_BEST_WRK,WERKS,ADSU)))).
formula(SingleRole(singleRoleEntry(ZORDER_WRK_ADSU_ED,authObj(M_BEST_EKG,ACTVT,01)))).
formula(SingleRole(singleRoleEntry(ZORDER_WRK_ADSU_ED,authObj(M_BEST_EKG,ACTVT,02)))).
formula(SingleRole(singleRoleEntry(ZORDER_WRK_ADSU_ED,authObj(M_BEST_EKG,ACTVT,03)))).
formula(SingleRole(singleRoleEntry(ZORDER_WRK_ADSU_ED,authObj(M_BEST_EKG,ACTVT,08)))).
formula(SingleRole(singleRoleEntry(ZORDER_WRK_ADSU_ED,authObj(M_BEST_EKG,ACTVT,09)))).
formula(SingleRole(singleRoleEntry(ZORDER_WRK_ADSU_ED,authObj(M_BEST_EKG,EKGRP,I26)))).
formula(SingleRole(singleRoleEntry(ZORDER_WRK_ADSU_ED,authObj(M_EINK_MKL,MATKL,STAR)))).
formula(SingleRole(singleRoleEntry(ZORDER_WRK_ADSU_ED,authObj(M_EINK_GWT,GSWRT,STAR)))).



% -------- Composite Roles  --------
% permits releasing of requisitions: plant INF, single position release, release code W1 (cost center)
formula(CompositeRole(compositeRoleEntry(ZRELEASE_WRK_INF_W1_MULTI,ZRELEASE_WRK_INF_BASE))).
formula(CompositeRole(compositeRoleEntry(ZRELEASE_WRK_INF_W1_MULTI,ZRELEASE_WRK_INF_W1))).

% permits releasing of requisitions: plant INF, single position release, release code W2 (management)
formula(CompositeRole(compositeRoleEntry(ZRELEASE_WRK_INF_W2_MULTI,ZRELEASE_WRK_INF_BASE))).
formula(CompositeRole(compositeRoleEntry(ZRELEASE_WRK_INF_W2_MULTI,ZRELEASE_WRK_INF_W2))).


% create arbitrary orders
formula(CompositeRole(compositeRoleEntry(ZORDER_WRK_INF_ALL,ZORDER_WRK_INF_BASE))).
formula(CompositeRole(compositeRoleEntry(ZORDER_WRK_INF_ALL,ZORDER_WRK_INF_TYPE_ALL))).

% create orders only for office material with limited amount of money
formula(CompositeRole(compositeRoleEntry(ZORDER_WRK_INF_OFFICE,ZORDER_WRK_INF_BASE))).
formula(CompositeRole(compositeRoleEntry(ZORDER_WRK_INF_OFFICE,ZORDER_WRK_INF_TYPE_OFFICE))).



% -------- Assign Roles to Users --------
formula(Holds(KAISER,ZRELEASE_WRK_INF_W1_MULTI)).
formula(Holds(MEIER,ZRELEASE_WRK_INF_W2_MULTI)).

formula(Holds(MUELLER,ZBANF_WRK_INF_ED)).			% create requisitions

%formula(Holds(LAMOTTE,ZBANF_WRK_INF_ED)).			% create requisitions
%formula(Holds(LAMOTTE,ZRELEASE_WRK_INF_W1_MULTI)).	% release requisitions with code W1
%formula(Holds(LAMOTTE,ZRELEASE_WRK_INF_W2_MULTI)).	% together with code W2 is prohibited

%formula(Holds(LAMOTTE,ZORDER_WRK_ADSU_ED)).
formula(Holds(SCHMITT,ZORDER_WRK_INF_ALL)).
%formula(Holds(LAMOTTE,ZORDER_WRK_INF_OFFICE)).

formula(Holds(LAMOTTE,ZORDER_WRK_INF_OFFICE)).




formula(DirectPurchase(DIRECT)).
formula(StandardPurchase(NB)).

formula(forall([v_bsart],
		not(and(
			DirectPurchase(v_bsart),
			StandardPurchase(v_bsart)
		))
	)).	
	
% ============== Code Layer ==============

% -------- Customizing: Release Strategy --------
% Release Requirements
formula(ReleaseRequirement(KF,RGRP_01,W1)).
formula(ReleaseRequirement(VF,RGRP_01,W1)).
formula(ReleaseRequirement(VF,RGRP_01,W2)).

% e.g. ReleaseStrategy(cost center release [KF]/management release [VF], release group 01, class(FRG_EBAN, property(...)))
formula(ReleaseStrategy(KF,RGRP_01,class(FRG_EBAN,property(FRG_CEBAN_EKGRP,I26)))).
formula(ReleaseStrategy(KF,RGRP_01,class(FRG_EBAN,property(FRG_CEBAN_WERKS,INF)))).
formula(ReleaseStrategy(KF,RGRP_01,class(FRG_EBAN,property(FRG_CEBAN_GSWRT,GREATER_1000_LESS_10000_EUR)))).

formula(ReleaseStrategy(VF,RGRP_01,class(FRG_EBAN,property(FRG_CEBAN_EKGRP,I26)))).
formula(ReleaseStrategy(VF,RGRP_01,class(FRG_EBAN,property(FRG_CEBAN_WERKS,INF)))).
formula(ReleaseStrategy(VF,RGRP_01,class(FRG_EBAN,property(FRG_CEBAN_GSWRT,GREATER_10000_EUR)))).


formula(forall([v_releasestrategy,
		v_releasegroup],
		implies(
			ReleaseStrategy(v_releasestrategy,v_releasegroup,class(FRG_EBAN,property(FRG_CEBAN_WERKS,INF))),
			and(
				not(ReleaseStrategy(v_releasestrategy,v_releasegroup,class(FRG_EBAN,property(FRG_CEBAN_WERKS,ADSU)))),
				not(ReleaseStrategy(v_releasestrategy,v_releasegroup,class(FRG_EBAN,property(FRG_CEBAN_WERKS,GRSU))))
			)
		)
	)).
formula(forall([v_releasestrategy,
		v_releasegroup],
		implies(
			ReleaseStrategy(v_releasestrategy,v_releasegroup,class(FRG_EBAN,property(FRG_CEBAN_WERKS,GRSU))),
			and(
				not(ReleaseStrategy(v_releasestrategy,v_releasegroup,class(FRG_EBAN,property(FRG_CEBAN_WERKS,ADSU)))),
				not(ReleaseStrategy(v_releasestrategy,v_releasegroup,class(FRG_EBAN,property(FRG_CEBAN_WERKS,INF))))
			)
		)
	)).
formula(forall([v_releasestrategy,
		v_releasegroup],
		implies(
			ReleaseStrategy(v_releasestrategy,v_releasegroup,class(FRG_EBAN,property(FRG_CEBAN_WERKS,ADSU))),
			and(
				not(ReleaseStrategy(v_releasestrategy,v_releasegroup,class(FRG_EBAN,property(FRG_CEBAN_WERKS,INF)))),
				not(ReleaseStrategy(v_releasestrategy,v_releasegroup,class(FRG_EBAN,property(FRG_CEBAN_WERKS,GRSU))))
			)
		)
	)).
formula(forall([v_releasestrategy,
		v_releasegroup],
		implies(
			ReleaseStrategy(v_releasestrategy,v_releasegroup,class(FRG_EBAN,property(FRG_CEBAN_GSWRT,GREATER_1000_LESS_10000_EUR))),
			and(
				not(ReleaseStrategy(v_releasestrategy,v_releasegroup,class(FRG_EBAN,property(FRG_CEBAN_GSWRT,GREATER_10000_EUR)))),
				not(ReleaseStrategy(v_releasestrategy,v_releasegroup,class(FRG_EBAN,property(FRG_CEBAN_GSWRT,LESS_EQUAL_1000_EUR))))
			)
		)
	)).
formula(forall([v_releasestrategy,
		v_releasegroup],
		implies(
			ReleaseStrategy(v_releasestrategy,v_releasegroup,class(FRG_EBAN,property(FRG_CEBAN_GSWRT,GREATER_10000_EUR))),
			and(
				not(ReleaseStrategy(v_releasestrategy,v_releasegroup,class(FRG_EBAN,property(FRG_CEBAN_GSWRT,GREATER_1000_LESS_10000_EUR)))),
				not(ReleaseStrategy(v_releasestrategy,v_releasegroup,class(FRG_EBAN,property(FRG_CEBAN_GSWRT,LESS_EQUAL_1000_EUR))))
			)
		)
	)).
formula(forall([v_releasestrategy,
		v_releasegroup],
		implies(
			ReleaseStrategy(v_releasestrategy,v_releasegroup,class(FRG_EBAN,property(FRG_CEBAN_GSWRT,LESS_EQUAL_1000_EUR))),
			and(
				not(ReleaseStrategy(v_releasestrategy,v_releasegroup,class(FRG_EBAN,property(FRG_CEBAN_GSWRT,GREATER_1000_LESS_10000_EUR)))),
				not(ReleaseStrategy(v_releasestrategy,v_releasegroup,class(FRG_EBAN,property(FRG_CEBAN_GSWRT,GREATER_10000_EUR))))
			)
		)
	)).
formula(forall([v_releasestrategy,
		v_releasegroup],
		implies(
			ReleaseStrategy(v_releasestrategy,v_releasegroup,class(FRG_EBAN,property(FRG_CEBAN_EKGRP,I26))),
			and(
				not(ReleaseStrategy(v_releasestrategy,v_releasegroup,class(FRG_EBAN,property(FRG_CEBAN_EKGRP,I27))))
			)
		)
	)).
formula(forall([v_releasestrategy,
		v_releasegroup],
		implies(
			ReleaseStrategy(v_releasestrategy,v_releasegroup,class(FRG_EBAN,property(FRG_CEBAN_EKGRP,I27))),
			and(
				not(ReleaseStrategy(v_releasestrategy,v_releasegroup,class(FRG_EBAN,property(FRG_CEBAN_EKGRP,I26))))
			)
		)
	)).


% -------- Access() --------
% Check of an authorization object with its value, the user profile must have the same authorization object
% with an equal value or STAR
formula(forall([v_user,
		v_authObjectName,
		v_authObjectField,
		v_authorization],
			implies(
				UserProfile(userProfileEntry(v_user,authObj(v_authObjectName,v_authObjectField,v_authorization))),
	  			Access(v_user,authObj(v_authObjectName,v_authObjectField,v_authorization))
			)
		)).
formula(forall([v_user,
		v_authObjectName,
		v_authObjectField,
		v_authorization],
			implies(
				UserProfile(userProfileEntry(v_user,authObj(v_authObjectName,v_authObjectField,STAR))),
	  			Access(v_user,authObj(v_authObjectName,v_authObjectField,v_authorization))
			)
		)).

% special cases for money amounts
formula(forall([v_user,
		v_authObjectName,
		v_authObjectField],
			implies(
				or(
					UserProfile(userProfileEntry(v_user,authObj(v_authObjectName,v_authObjectField,GREATER_1000_LESS_10000_EUR))),
					UserProfile(userProfileEntry(v_user,authObj(v_authObjectName,v_authObjectField,GREATER_10000_EUR)))
				),
	  			Access(v_user,authObj(v_authObjectName,v_authObjectField,LESS_EQUAL_1000_EUR))
			)
		)).
formula(forall([v_user,
		v_authObjectName,
		v_authObjectField],
			implies(
				UserProfile(userProfileEntry(v_user,authObj(v_authObjectName,v_authObjectField,GREATER_10000_EUR))),
	  			Access(v_user,authObj(v_authObjectName,v_authObjectField,GREATER_1000_LESS_10000_EUR))
			)
		)).


% -------- Profile/(Single,Composite)Role -> Userprofile() --------
% A composite role contains other roles
% Each authorization in a profile or single/composite role will be inserted into the user profile
formula(forall([v_user,
		v_profileName,
		v_singleRoleName,
		v_compositeRoleName,
		v_authObjectName,
		v_authObjectField,
		v_authorization],
			implies(
				or(
					and(
						Profile(profileEntry(v_profileName,authObj(v_authObjectName,v_authObjectField,v_authorization))),
						Holds(v_user,v_profileName)
					),
					and(
						SingleRole(singleRoleEntry(v_singleRoleName,authObj(v_authObjectName,v_authObjectField,v_authorization))),
						Holds(v_user,v_singleRoleName)
					),
					and(
						CompositeRole(compositeRoleEntry(v_compositeRoleName,v_singleRoleName)),
						SingleRole(singleRoleEntry(v_singleRoleName,authObj(v_authObjectName,v_authObjectField,v_authorization))),
						Holds(v_user,v_compositeRoleName)
					)
				),
				UserProfile(userProfileEntry(v_user,authObj(v_authObjectName,v_authObjectField,v_authorization)))
			)
		)).



% --------------- Abstraction -------------------
% -------- ME51N - Create Requisitions --------
formula(forall([v_user,
		v_werks,
		v_bsart,
		v_ekgrp],
			implies(
				and(
					Access(v_user,authObj(S_TCODE,TCD,ME51N)),
					Access(v_user,authObj(M_BANF_WRK,ACTVT,01)),
					Access(v_user,authObj(M_BANF_WRK,WERKS,v_werks)),
					Access(v_user,authObj(M_BANF_BSA,ACTVT,01)),
					Access(v_user,authObj(M_BANF_BSA,BSART,v_bsart)),
					Access(v_user,authObj(M_BANF_EKG,ACTVT,01)),
					Access(v_user,authObj(M_BANF_EKG,EKGRP,v_ekgrp))
				),
				Access(v_user,ME51N)
			)
		)).
		
% -------- ME52N - Change Requisitions --------
formula(forall([v_user,
		v_werks,
		v_bsart,
		v_ekgrp],
			implies(
				and(
					Access(v_user,authObj(S_TCODE,TCD,ME52N)),
					Access(v_user,authObj(M_BANF_WRK,ACTVT,02)),
					Access(v_user,authObj(M_BANF_WRK,WERKS,v_werks)),
					Access(v_user,authObj(M_BANF_BSA,ACTVT,02)),
					Access(v_user,authObj(M_BANF_BSA,ACTVT,08)),
					Access(v_user,authObj(M_BANF_BSA,BSART,v_bsart)),
					Access(v_user,authObj(M_BANF_EKG,ACTVT,02)),
					Access(v_user,authObj(M_BANF_EKG,EKGRP,v_ekgrp))
				),
				Access(v_user,ME52N)
			)
		)).

% -------- ME53N - View Requisitions --------
formula(forall([v_user,
		v_werks,
		v_bsart,
		v_ekgrp],
			implies(
				and(				
					Access(v_user,authObj(S_TCODE,TCD,ME53N)),
					Access(v_user,authObj(M_BANF_WRK,ACTVT,03)),
					Access(v_user,authObj(M_BANF_WRK,WERKS,v_werks)),
					Access(v_user,authObj(M_BANF_BSA,ACTVT,03)),
					Access(v_user,authObj(M_BANF_BSA,ACTVT,08)),
					Access(v_user,authObj(M_BANF_BSA,BSART,v_bsart)),
					Access(v_user,authObj(M_BANF_EKG,ACTVT,03)),
					Access(v_user,authObj(M_BANF_EKG,EKGRP,v_ekgrp))
				),
				Access(v_user,ME53N)
			)
		)).


% -------- ME54N - Release Requisitions  --------
formula(forall([v_user,
		v_werks,
		v_bsart,
		v_ekgrp,
		v_frggr,
		v_frgco],
			implies(
				and(
					% check tcd code				
					Access(v_user,authObj(S_TCODE,TCD,ME54N)),

					% check access to view requisitions
					Access(v_user,ME53N),
					Access(v_user,authObj(M_BANF_WRK,WERKS,v_werks)),
					Access(v_user,authObj(M_BANF_BSA,BSART,v_bsart)),
					Access(v_user,authObj(M_BANF_EKG,EKGRP,v_ekgrp)),

					% check release group and code
					Access(v_user,authObj(M_EINK_FRG,FRGGR,v_frggr)),
					Access(v_user,authObj(M_EINK_FRG,FRGCO,v_frgco)),

					% check access to save the changes (similar to ME52N - Change Requisition,
					% BUT without the transaction code check and the already checked authorization objects)
					%Access(v_user,ME52N) % this line would include the transaction code
					Access(v_user,authObj(M_BANF_WRK,ACTVT,02)),
					%Access(v_user,authObj(M_BANF_WRK,WERKS,v_werks)), % already checked
					Access(v_user,authObj(M_BANF_BSA,ACTVT,02)),
					Access(v_user,authObj(M_BANF_BSA,ACTVT,08)),
					%Access(v_user,authObj(M_BANF_BSA,BSART,v_bsart)), % already checked
					Access(v_user,authObj(M_BANF_EKG,ACTVT,02))
					%Access(v_user,authObj(M_BANF_EKG,EKGRP,v_ekgrp))  % already checked
				),
				Access(v_user,ME54N)
			)
		)).


% -------- ME56 - Map Distributor to Requsition  --------
%formula(forall([v_user,
%		v_werks,
%		v_bsart,
%		v_ekgrp],
%			implies(
%				and(				
%					Access(v_user,authObj(S_TCODE,TCD,ME56))),
%					Access(v_user,authObj(M_BANF_WRK,ACTVT,02)),
%					Access(v_user,authObj(M_BANF_WRK,ACTVT,08)),
%					Access(v_user,authObj(M_BANF_WRK,WERKS,v_werks)),
%					Access(v_user,authObj(M_BANF_BSA,ACTVT,02)),
%					Access(v_user,authObj(M_BANF_BSA,ACTVT,08)),
%					Access(v_user,authObj(M_BANF_BSA,BSART,v_bsart)),
%					Access(v_user,authObj(M_BANF_EKG,ACTVT,02)),
%					Access(v_user,authObj(M_BANF_EKG,ACTVT,08)),
%					Access(v_user,authObj(M_BANF_EKG,EKGRP,v_ekgrp)),
%					Access(v_user,,authObj(M_BANF_BSA,ACTVT,01)),
%					Access(v_user,ME53N)
%				),
%				Access(v_user,ME56)
%			)
%		)).


% -------- ME21N - Create Order  --------
formula(forall([v_user,
		v_werks,
		v_bsart,
		v_ekgrp,
		v_ekorg],
			implies(
				and(				
					Access(v_user,authObj(S_TCODE,TCD,ME21N)),
					Access(v_user,authObj(M_BEST_EKO,ACTVT,01)),
					Access(v_user,authObj(M_BEST_EKO,ACTVT,09)),
					Access(v_user,authObj(M_BEST_EKO,EKORG,v_ekorg)),
					Access(v_user,authObj(M_BEST_BSA,ACTVT,01)),
					Access(v_user,authObj(M_BEST_BSA,ACTVT,09)),
					Access(v_user,authObj(M_BEST_BSA,BSART,v_bsart)),
					Access(v_user,authObj(M_BANF_BSA,ACTVT,01)),
					Access(v_user,authObj(M_BANF_BSA,BSART,v_bsart)),
					Access(v_user,authObj(M_BEST_WRK,ACTVT,01)),
					Access(v_user,authObj(M_BEST_WRK,ACTVT,08)),
					Access(v_user,authObj(M_BEST_WRK,ACTVT,09)),
					Access(v_user,authObj(M_BEST_WRK,WERKS,v_werks)),
					Access(v_user,authObj(M_BEST_EKG,ACTVT,01)),
					Access(v_user,authObj(M_BEST_EKG,ACTVT,09)),
					Access(v_user,authObj(M_BEST_EKG,EKGRP,v_ekgrp))
				),
				Access(v_user,ME21N)
			)
		)).
		
% -------- ME22N - Change Order  --------
formula(forall([v_user,
		v_werks,
		v_bsart,
		v_ekgrp,
		v_ekorg],
			implies(
				and(				
					Access(v_user,authObj(S_TCODE,TCD,ME22N)),
					Access(v_user,authObj(M_BEST_EKO,ACTVT,02)),
					Access(v_user,authObj(M_BEST_EKO,ACTVT,08)),
					Access(v_user,authObj(M_BEST_EKO,ACTVT,09)),
					Access(v_user,authObj(M_BEST_EKO,EKORG,v_ekorg)),
					Access(v_user,authObj(M_BEST_BSA,ACTVT,02)),
					Access(v_user,authObj(M_BEST_BSA,ACTVT,08)),
					Access(v_user,authObj(M_BEST_BSA,ACTVT,09)),
					Access(v_user,authObj(M_BEST_BSA,BSART,v_bsart)),
					Access(v_user,authObj(M_BANF_BSA,ACTVT,01)),
					Access(v_user,authObj(M_BANF_BSA,BSART,v_bsart)),
					Access(v_user,authObj(M_BEST_WRK,ACTVT,02)),
					Access(v_user,authObj(M_BEST_WRK,ACTVT,08)),
					Access(v_user,authObj(M_BEST_WRK,ACTVT,09)),
					Access(v_user,authObj(M_BEST_WRK,WERKS,v_werks)),
					Access(v_user,authObj(M_BEST_EKG,ACTVT,02)),
					Access(v_user,authObj(M_BEST_EKG,ACTVT,08)),
					Access(v_user,authObj(M_BEST_EKG,ACTVT,09)),
					Access(v_user,authObj(M_BEST_EKG,EKGRP,v_ekgrp))
				),
				Access(v_user,ME22N)
			)
		)).


% -------- ME23N - View Order  --------
formula(forall([v_user,
		v_werks,
		v_bsart,
		v_ekgrp,
		v_ekorg],
			implies(
				and(				
					Access(v_user,authObj(S_TCODE,TCD,ME23N)),
					Access(v_user,authObj(M_BEST_EKO,ACTVT,03)),
					Access(v_user,authObj(M_BEST_EKO,ACTVT,08)),
					Access(v_user,authObj(M_BEST_EKO,ACTVT,09)),
					Access(v_user,authObj(M_BEST_EKO,EKORG,v_ekorg)),
					Access(v_user,authObj(M_BEST_BSA,ACTVT,03)),
					Access(v_user,authObj(M_BEST_BSA,ACTVT,08)),
					Access(v_user,authObj(M_BEST_BSA,ACTVT,09)),
					Access(v_user,authObj(M_BEST_BSA,BSART,v_bsart)),
					Access(v_user,authObj(M_BANF_BSA,ACTVT,01)),
					Access(v_user,authObj(M_BANF_BSA,BSART,v_bsart)),
					Access(v_user,authObj(M_BEST_WRK,ACTVT,03)),
					Access(v_user,authObj(M_BEST_WRK,WERKS,v_werks)),
					Access(v_user,authObj(M_BEST_EKG,ACTVT,03)),
					Access(v_user,authObj(M_BEST_EKG,ACTVT,08)),
					Access(v_user,authObj(M_BEST_EKG,ACTVT,09)),
					Access(v_user,authObj(M_BEST_EKG,EKGRP,v_ekgrp))
				),
				Access(v_user,ME23N)
			)
		)).




% ======== Business process steps ========
% Role: Requisition, includes create/change/view requisitions
% If there is a requisition and an user has access to create the requisition object, then
% the requisition object is created by this user
formula(forall([v_user,
		v_werks,
		v_bsart,
		v_ekgrp,
		v_matkl,
		v_pos,
		v_material,
		v_ekorg,
		v_gswrt,
		v_id],
			implies(
				and(	
					% a requisition row
					Requisition(v_bsart,v_pos,v_material,v_werks,v_ekgrp,v_ekorg,v_matkl,v_gswrt,v_id),
					
					StandardPurchase(v_bsart),

					% and user is allowed to access ME51N,ME52N,ME53N and the constraints match
					Access(v_user,ME51N),

% typical extension: a user who is authorized to create is also authorized to view and change requisitions
%					Access(v_user,ME52N),
%					Access(v_user,ME53N),

					Access(v_user,authObj(M_BANF_WRK,WERKS,v_werks)),
					Access(v_user,authObj(M_BANF_BSA,BSART,v_bsart)),
					Access(v_user,authObj(M_BANF_EKG,EKGRP,v_ekgrp))
				),
				RequisitionCreated(v_user,v_bsart,v_pos,v_material,v_werks,v_ekgrp,v_ekorg,v_matkl,v_gswrt,v_id)
			)
		)).


% Role: Release
formula(forall([v_user1,
		v_user2,
		v_werks,
		v_bsart,
		v_ekgrp,
		v_ekorg,
		v_matkl,
		v_pos,
		v_material,
		v_gswrt,
		v_releasestrategy,
		v_frggr,
		v_frgco,
		v_class,
		v_id],
			implies(
				and(
					% the requisition has been created
					RequisitionCreated(v_user1,v_bsart,v_pos,v_material,v_werks,v_ekgrp,v_ekorg,v_matkl,v_gswrt,v_id),

					% and the release strategy matches
					ReleaseStrategy(v_releasestrategy,v_frggr,class(v_class,property(FRG_CEBAN_EKGRP,v_ekgrp))),
					ReleaseStrategy(v_releasestrategy,v_frggr,class(v_class,property(FRG_CEBAN_WERKS,v_werks))),
					ReleaseStrategy(v_releasestrategy,v_frggr,class(v_class,property(FRG_CEBAN_GSWRT,v_gswrt))),

					% and the release codes match
					ReleaseRequirement(v_releasestrategy,v_frggr,v_frgco),

					% and the user has the necessary authorizations to the release strategy
					Access(v_user2,authObj(M_EINK_FRG,FRGGR,v_frggr)),
					Access(v_user2,authObj(M_EINK_FRG,FRGCO,v_frgco)),					

					% and access to the release transaction
					Access(v_user2,ME54N),
					Access(v_user2,authObj(M_BANF_WRK,WERKS,v_werks)),
					Access(v_user2,authObj(M_BANF_BSA,BSART,v_bsart)),
					Access(v_user2,authObj(M_BANF_EKG,EKGRP,v_ekgrp))
				),
				% then the requisition row is released with the code "v_releasecode"
				RequisitionReleasedStep(v_user2,v_frggr,v_releasestrategy,v_frgco,v_bsart,v_pos,v_material,v_werks,v_ekgrp,v_ekorg,v_matkl,v_gswrt,v_id)
			)
		)).

% no release strategy matches
formula(forall([v_user,
		v_werks,
		v_bsart,
		v_ekgrp,
		v_ekorg,
		v_matkl,
		v_pos,
		v_material,
		v_gswrt,
		v_frggr,
		v_class,
		v_id],
			implies(
				and(
					% the requisition has been created
					RequisitionCreated(v_user,v_bsart,v_pos,v_material,v_werks,v_ekgrp,v_ekorg,v_matkl,v_gswrt,v_id),

					% and none of the release strategies match, i.e. there is an attribute in each strategy which doesn't match
					or(
						not(ReleaseStrategy(KF,v_frggr,class(v_class,property(FRG_CEBAN_EKGRP,v_ekgrp)))),
						not(ReleaseStrategy(KF,v_frggr,class(v_class,property(FRG_CEBAN_WERKS,v_werks)))),
						not(ReleaseStrategy(KF,v_frggr,class(v_class,property(FRG_CEBAN_GSWRT,v_gswrt))))
					),
					or(
						not(ReleaseStrategy(VF,v_frggr,class(v_class,property(FRG_CEBAN_EKGRP,v_ekgrp)))),
						not(ReleaseStrategy(VF,v_frggr,class(v_class,property(FRG_CEBAN_WERKS,v_werks)))),
						not(ReleaseStrategy(VF,v_frggr,class(v_class,property(FRG_CEBAN_GSWRT,v_gswrt))))
					)
				),
				RequisitionReleased(v_user,v_bsart,v_pos,v_material,v_werks,v_ekgrp,v_ekorg,v_matkl,v_gswrt,v_id)
			)
		)).




% Customizing: Definition of the release codes which are necessary to release a requisition (only if the strategy matches).
formula(forall([v_user1,
		v_user2,
		v_werks,
		v_bsart,
		v_ekgrp,
		v_ekorg,
		v_matkl,
		v_pos,
		v_material,
		v_gswrt,
		v_id],
			implies(
				or(
					and(
						% strategy KF requires release code W1
						RequisitionReleasedStep(v_user2,RGRP_01,KF,W1,v_bsart,v_pos,v_material,v_werks,v_ekgrp,v_ekorg,v_matkl,v_gswrt,v_id)
					),
					and(
						% strategy VF requires release code W1 and W2 for release and the users owning these two release codes must be distinct
						RequisitionReleasedStep(v_user1,RGRP_01,VF,W1,v_bsart,v_pos,v_material,v_werks,v_ekgrp,v_ekorg,v_matkl,v_gswrt,v_id),
						RequisitionReleasedStep(v_user2,RGRP_01,VF,W2,v_bsart,v_pos,v_material,v_werks,v_ekgrp,v_ekorg,v_matkl,v_gswrt,v_id)
					)
				),
				RequisitionReleased(v_user2,v_bsart,v_pos,v_material,v_werks,v_ekgrp,v_ekorg,v_matkl,v_gswrt,v_id)
			)
		)).


% Role: Order
% If a requisition has been created and has already been released and the user has access to create order objects, then
% the order (object) will be created by the user
formula(forall([v_user1,
		v_user2,
		v_werks,
		v_bsart,
		v_ekgrp,
		v_matkl,
		v_ekorg,
		v_pos,
		v_material,
		v_gswrt,
		v_id],
			implies(
				and(	
					% requisition has been released
					RequisitionReleased(v_user1,v_bsart,v_pos,v_material,v_werks,v_ekgrp,v_ekorg,v_matkl,v_gswrt,v_id),
						
					% and user is allowed to access ME21N, ME22N, ME23N and the constraints match
					Access(v_user2,ME21N),
					Access(v_user2,ME22N),
					Access(v_user2,ME23N),
					Access(v_user2,authObj(M_BEST_WRK,WERKS,v_werks)),
					Access(v_user2,authObj(M_BANF_BSA,BSART,v_bsart)),
					Access(v_user2,authObj(M_BEST_BSA,BSART,v_bsart)),
					Access(v_user2,authObj(M_BEST_EKG,EKGRP,v_ekgrp)),
					Access(v_user2,authObj(M_BEST_EKO,EKORG,v_ekorg)),

					% the value is normally STAR in a buyer role: no restrictions
					Access(v_user2,authObj(M_EINK_MKL,MATKL,v_matkl)),
					Access(v_user2,authObj(M_EINK_GWT,GSWRT,v_gswrt))
				),
				OrderCreated(v_user2,v_bsart,v_pos,v_material,v_werks,v_ekgrp,v_ekorg,v_matkl,v_gswrt,v_id)
			)
		)).

% special case: direct order (e.g. office material)
formula(forall([v_user1,
        v_user2,
        v_user3,
		v_werks,
		v_bsart,
		v_ekgrp,
		v_matkl,
		v_ekorg,
		v_pos,
		v_material,
		v_gswrt,
		v_id],
			implies(
				and(	
					% the user has direct access to create the requisition
					Requisition(v_bsart,v_pos,v_material,v_werks,v_ekgrp,v_ekorg,v_matkl,v_gswrt,v_id),
					
					DirectPurchase(v_bsart),
					
					Access(v_user1,authObj(M_EINK_MKL,MATKL,v_matkl)),
					Access(v_user1,authObj(M_EINK_GWT,GSWRT,v_gswrt)),
					
					% special transaction code for limited requisitions
					Access(v_user1,authObj(S_TCODE,TCD,ME21NOFF)),

					% and user is allowed to access ME21N, ME22N, ME23N and the constraints match
					Access(v_user1,ME21N),
					Access(v_user1,ME22N),
					Access(v_user1,ME23N),
					Access(v_user1,authObj(M_BEST_WRK,WERKS,v_werks)),
					Access(v_user1,authObj(M_BANF_BSA,BSART,v_bsart)),
					Access(v_user1,authObj(M_BEST_BSA,BSART,v_bsart)),
					Access(v_user1,authObj(M_BEST_EKG,EKGRP,v_ekgrp)),
					Access(v_user1,authObj(M_BEST_EKO,EKORG,v_ekorg))
				),
				and(
					OrderCreated(v_user1,v_bsart,v_pos,v_material,v_werks,v_ekgrp,v_ekorg,v_matkl,v_gswrt,v_id),
					not(RequisitionCreated(v_user2,v_bsart,v_pos,v_material,v_werks,v_ekgrp,v_ekorg,v_matkl,v_gswrt,v_id)),	
					not(RequisitionReleased(v_user3,v_bsart,v_pos,v_material,v_werks,v_ekgrp,v_ekorg,v_matkl,v_gswrt,v_id))
				)
			)
		)).



% ============== Business Policies ==============
% there exists no user, which is allowed to perform the complete purchase process:
% - create a requisition
% - to release a requisition
% - to create an order
formula(not(exists([v_user,
		v_werks,
		v_ekgrp,
		v_ekorg,
		v_matkl,
		v_bsart,
		v_pos,
		v_material,
		v_gswrt,
		v_id],
			implies(
				Requisition(v_bsart,v_pos,v_material,v_werks,v_ekgrp,v_ekorg,v_matkl,v_gswrt,v_id),
				and(			
					RequisitionCreated(v_user,v_bsart,v_pos,v_material,v_werks,v_ekgrp,v_ekorg,v_matkl,v_gswrt,v_id),
					RequisitionReleased(v_user,v_bsart,v_pos,v_material,v_werks,v_ekgrp,v_ekorg,v_matkl,v_gswrt,v_id),
					OrderCreated(v_user,v_bsart,v_pos,v_material,v_werks,v_ekgrp,v_ekorg,v_matkl,v_gswrt,v_id)
				)
			)
		
	))).

% it is prohibited to create orders greater than 1000 EUR without a requisition
formula(forall([v_user1,
		v_werks,
		v_matkl,
		v_ekgrp,
		v_ekorg,
		v_bsart,
		v_pos,
		v_material,
		v_id],
		exists([v_user2],
			implies(
				OrderCreated(v_user1,v_bsart,v_pos,v_material,v_werks,v_ekgrp,v_ekorg,v_matkl,GREATER_1000_LESS_10000_EUR,v_id),
				RequisitionCreated(v_user2,v_bsart,v_pos,v_material,v_werks,v_ekgrp,v_ekorg,v_matkl,GREATER_1000_LESS_10000_EUR,v_id)
			)
		)
	)).
formula(forall([v_user1,
		v_werks,
		v_matkl,
		v_ekgrp,
		v_ekorg,
		v_bsart,
		v_pos,
		v_material,
		v_id],
		exists([v_user2],
			implies(
				OrderCreated(v_user1,v_bsart,v_pos,v_material,v_werks,v_ekgrp,v_ekorg,v_matkl,GREATER_10000_EUR,v_id),
				RequisitionCreated(v_user2,v_bsart,v_pos,v_material,v_werks,v_ekgrp,v_ekorg,v_matkl,GREATER_10000_EUR,v_id)
			)
		)
	)).

end_of_list.


list_of_formulae(conjectures).
formula(exists([v_werks,
		v_ekgrp,
		v_ekorg,
		v_matkl,
		v_bsart,
		v_pos,
		v_material,
		v_gswrt,
		v_id],
			implies(
				Requisition(v_bsart,v_pos,v_material,v_werks,INF,v_ekorg,v_matkl,v_gswrt,v_id),
				RequisitionCreated(MUELLER,v_bsart,v_pos,v_material,INF,v_ekgrp,v_ekorg,v_matkl,v_gswrt,v_id)
			)
	)).
end_of_list.

list_of_settings(SPASS).
{*
	set_flag(DocProof,1).
*}
end_of_list.

end_problem.