%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% @model PurchaseOrder
% @author Jan Martijn van der Werf, Artem Polyvyanyy
% @year 2019
% @version 1.1
% @created 29-11-2019
% @modified 13-12-2019
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%
% This information model describes a simple scenario of handling Purchase Orders
%
% Entity types:
% - product
% - supplier
% - order
%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% ENSURING CORRECT TYPING IN RELATION PREDICATES (IMPLICIT FROM THE DEFINITION)
% supplies(S,P): Supplier S *supplies* Product P
tff(supplies_domain, conjecture,
! [S: universe, P: universe] :
( supplies(S,P) => ( supplier(S) & product(P) ) )
).
% contains(O,P): Order O *contains* Product P
tff(contains_domain, conjecture,
! [O: universe, P: universe] :
( contains(O,P) => ( order(O) & product(P) ) )
).
% bids(S,O): Supplier S *bids* Order O
tff(bids_domain, conjecture,
! [S: universe, O: universe] :
( bids(S,O) => ( supplier(S) & order(O) ) )
).
% receives(S,O): Supplier S *receives* Order O
tff(receives_domain, conjecture,
! [S: universe, O: universe] :
( receives(S,O) => ( supplier(S) & order(O) ) )
).
% delivers(S,O): Supplier S *delivers* Order O
tff(receives_domain, conjecture,
! [S: universe, O: universe] :
( delivers(S,O) => ( supplier(S) & order(O) ) )
).
% CONTROLING SUBTYPE RELATIONS OVER ENTITY TYPES (ENTITY TYPES ARE DISJOINT)
% Supplier is not a Product or Order
tff(supplier_subtype, conjecture,
! [I: universe] :
( supplier(I) => ( ~product(I) & ~order(I) ) )
).
% Order is not a Product or Supplier
tff(order_subtype, conjecture,
! [I: universe] :
( order(I) => ( ~product(I) & ~supplier(I) ) )
).
% Product is not an Order or Supplier
tff(product_subtype, conjecture,
! [I: universe] :
( product(I) => ( ~order(I) & ~supplier(I) ) )
).
% UNIQUENESS CONSTRAINTS
% Order O *contains* at most one Product
tff(contains_uniqueness_at_most_one_product, conjecture,
! [O: universe, P1: universe, P2: universe] :
( ( contains(O,P1) & contains(O,P2) ) => ( P1 = P2 ) )
).
% Order O is *delivered* (delivers) by at most one Supplier
tff(delivers_uniqueness_at_most_one_supplier, conjecture,
! [S1: universe, S2: universe, O: universe] :
( ( delivers(S1,O) & delivers(S2,O) ) => ( S1 = S2 ) )
).
% Order O is *received* (receives) by at most one Supplier
tff(receives_uniqueness_at_most_one_supplier, conjecture,
! [S1: universe, S2: universe, O: universe] :
( ( receives(S1,O) & receives(S2,O) ) => ( S1 = S2 ) )
).
% MANDATORY CONSTRAINTS
% Every Order O *contains* a Product
tff(order_mandatory_contains, conjecture,
! [O: universe] :
( order(O) => ( ? [P: universe] : contains(O,P) ) )
).
% SUBSET CONSTRAINTS
% Every Order O *received* (receives) by a Supplier S has a *bid* (bids) by the
% same Supplier S
tff(receives_subset_bids, conjecture,
! [S: universe, O: universe] :
( receives(S,O) => bids(S,O) )
).
% Every Order O *delivered* (delivers) by a Supplier S was *received* (receives)
% by the same Supplier S
tff(delivers_subset_receives, conjecture,
! [S: universe, O: universe] :
( delivers(S,O) => receives(S,O) )
).
% OTHER CONSTRAINTS
% A Supplier S can only *bid* (bids) an Order O if they provide Product P
% *contained* (contains) in the Order o
tff(domain_constraint_bid_only_if_supplies, conjecture,
! [S: universe, O: universe] :
( bids(S,O) => ( ? [P: universe] :
( supplies(S,P) & contains(O,P) )
)
)
).
% If Supplier S1 *receives* (receive) Order O, then some other Supplier S2
% made a *bid* (bids) for the same Order O
tff(domain_constraint_at_least_two_bids, conjecture,
! [S1: universe, O: universe] :
( receives(S1,O) => ( ? [S2: universe] :
( (S1 != S2) & bids(S2,O) )
)
)
).
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%