%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%% file:  ['aberdeen.db']. 

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%           Representation of PC Configuration Example 
%                     Definition of The Domain 
%                     Aberdeen Site Definition
%                         
%                        Jessica Chen-Burger 
%
% In this document, we will adopt a convention that words starting 
% with a capital letter stand for variables, whereas words starting
% with a lower case letter stand for constants.
% 
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

:- multifile property/3, def_predicate/2, axiom/2. 

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Description of boards 
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

property(processor, capability, [processor]). 
property(processor, length,     long).
property(processor, extra_power_data, extra).

property(disk_controller, capability, [disk_io]). 
property(disk_controller, length,     long).
property(disk_controller, extra_power_data, normal). 

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% static_constraint(List_of_typing, 
%                   List_of_hypothesis, 
%                   List_of_conclusions)
%
% 1. For all constraint rules, unless stated, all 
%    variables are universaly quantified. 
% 2. The existence quantification is defined using the  
%    predicate exist/1.
% 3. The universal quantification is defined using the
%    predicate forall/1.
% 4. When quantifications are involved in a complicated  
%    ordered sequence, such order is specified in 
%    the order described in the List_of_hypothesis. 
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

static_constraint([instance_of(Slot1, slot), 
                   instance_of(Slot2, slot),
                   instance_of(X, disk_controller), 
                   instance_of(Y, processor)], 

                  [allocate(X, Slot1),
                   allocate(Y, Slot2)], 

                  [next_to(Slot1, Slot2)]).

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Axiom of predicate next_to(A, B). Not used.  
% 
% next_to(A, B) :-
%     instance_of(A, slot), 
%     instance_of(B, slot), 
%     ( next_to(A, B);
%       next_to(B, A)). 
% 

axiom(next_to(A, B), [ not(A = B) ]).

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Definition of predicate: 
%  allocate(Board, Slot): 
%  A Board (type) has been allocated to a Slot. 
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

property(io, capability,       [other_io]). 
property(io, length,           short).
property(io, extra_power_data, normal). 

property(optionI, capability, [fast_graphics]).
property(optionI, length,     long).
property(optionI, extra_power_data, extra). 


static_constraint([instance_of(Slot1, slot), 
                   instance_of(Slot2, slot), 
                   instance_of(X, optionI), 
                   instance_of(Y, processor)], 
 
                  [allocate(X,  Slot1),
                   allocate(Y,  Slot2) ],

                  [next_to(Slot1, Slot2)]).

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%% static_constratin(Pre_conditions, Conclusions). 
%% both arguments are described in conjunctive normal form.  
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

property(optionII, capability, [fast_graphics, video_in]).
property(optionII, length, short).
property(optionII, extra_power_data, extra). 

property(optionIII, capability,       [sound]).
property(optionIII, length,           long).
property(optionIII, extra_power_data, normal). 


static_constraint([instance_of(Slot1, slot), 
                   instance_of(Slot2, slot), 
                   instance_of(X, optionIII), 
                   instance_of(Y, io) ], 

                  [allocate(X,  Slot1),
                   allocate(Y,  Slot2)], 

                  [next_to(Slot1, Slot2)] ).

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

property(optionIV, capability,       [video_in]).
property(optionIV, length,           short).
property(optionIV, extra_power_data, normal). 
property(optionIV, cost,             50).

static_constraint([instance_of(Slot1, slot), 
                   instance_of(Slot2, slot), 
                   instance_of(X, optionIV), 
                   instance_of(Y, disk_controller)],

                  [allocate(X,  Slot1),
                   allocate(Y,  Slot2) ], 

                  [next_to(Slot1, Slot2)] ). 

/*********************************************************************
 in(M, X) indicates the set logical operator, membership: M is a member
 of the Set X. 

 The user requirement axiom can then be described below, using 
 existential quantification: 

    exist(Board) ^ exist(C) ^ exist(B) ^ exist(List) ^ exist(Slot) ^ 
    special_req(Board, capability, C) ^ 

    instance_of(B, Board) ^ property(Board, capability, List) ^
    ^ in(C, List) 
    allocate(B, Slot) ^ instance_of(Slot, slot)

*********************************************************************/

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% end of file 
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%