CONTEXT Delivery -- DATE: zo 24-04-2011  13:14:37,34
-- (file:  Delivery.pat ) -- 
PATTERN Deliveries

 from :: Order * Client [UNI] PRAGMA "" " was ordered by "
  = [ ("C45666"                  , "Applegate")
    ; ("Order 22/09/2006 Cookies", "Brown"    )
    ; ("C45683"                  , "Conway"   )
    ].

 item :: Order * Product PRAGMA "" " mentions " " as an order item".
 PURPOSE RELATION item[Order*Product]
 {+An order becomes useful only if it mentions products to be ordered.
 Each order item corresponds to a line on the order form.
 For the sake of simplicity, we have left out quantity, product codes, etcetera. 
 -}
 item :: Delivery * Product PRAGMA "" " has " " as an order item"
  = [ ("Jelly beans #4921"  , "Jelly beans"  )
    ; ("Cookies #0382"      , "Cookies"      )
    ; ("Peanut butter #1993", "Peanut butter")
    ].
 PURPOSE RELATION item[Delivery*Product]
 {+A delivery becomes useful only if there are items to be delivered.
 Each delivery item corresponds to a line on the delivery form.
 For the sake of simplicity, we have left out quantity, product codes, etcetera. 
 -}

 PURPOSE RELATION of
 {+Each delivery must correspond to one particular order.
 This is registered in relation `of`.
 -}
 of :: Delivery -> Order PRAGMA "" " corresponds to "
  = [ ("Cookies #0382"      , "Order 22/09/2006 Cookies")
    ; ("Jelly beans #4921"  , "C45666"                  )
    ; ("Peanut butter #1993", "C45683"                  )
    ].

RULE "correct delivery":
  item[Delivery*Product] |- of;item
  PHRASE IN ENGLISH "Each item in a delivery is mentioned on the order."
PURPOSE RULE "correct delivery" IN ENGLISH
{+We want orders to be delivered correctly, with only items that are mentioned on the order.
-}

RULE "complete delivery": of;item |- item[Delivery*Product]
PHRASE IN ENGLISH "Every item on an order must also be in the corresponding delivery."
PURPOSE RULE "complete delivery" IN ENGLISH
{+We want orders to be delivered completely, with no items missing.
-}

 provided :: Provider * Delivery [SUR,INJ] PRAGMA "" " has delivered "
  = [ ("Candy's candy", "Cookies #0382")
    ; ("Carter"       , "Jelly beans #4921")
    ; ("Carter"       , "Peanut butter #1993")
    ].

 accepted :: Provider * Order [INJ] PRAGMA "" "has accepted"
  = [ ("Candy's candy", "Order 22/09/2006 Cookies")
    ; ("Carter"       , "C45666"                  )
    ; ("Carter"       , "C45683"                  )
    ].
 rejected :: Provider * Order [INJ] PRAGMA "" "has rejected"
  = [ ("Candy's candy", "Order 22/09/2006 Cookies")
    ; ("Carter"       , "C45666"                  )
    ; ("Carter"       , "C45683"                  )
    ].

--RULE "accept or reject": -(accepted /\ rejected)
-- PHRASE IN ENGLISH "An order cannot be accepted and rejected at the same time."

 addressedTo :: Order -> Provider PRAGMA "" " was issued to "
  = [ ("Order 22/09/2006 Cookies", "Candy's candy")
    ; ("C45666"                  , "Carter"       )
    ; ("C45683"                  , "Carter"       )
    ].

 RULE "proper address": (accepted\/rejected) |- addressedTo~ -- \ref{rule 0} % uit het artikel
 PHRASE IN ENGLISH "A provider can only accept or reject orders that are addressed to that provider."
PURPOSE RULE "proper address" IN ENGLISH
{+Accepting an order is always done by the provider to whom the order was addressed.
To prevent an order to be accepted or rejected by anyone else, we need this requirement.
-}

 deliveredTo :: Delivery -> Client PRAGMA "" " is delivered to "
  = [ ("Jelly beans #4921", "Applegate")
    ; ("Cookies #0382", "Brown")
    ; ("Peanut butter #1993", "Conway")
    ].

RULE "order based delivery":    provided  |- accepted;of~
PHRASE IN ENGLISH "For every delivery a provider has made, there exists an accepted order."
PURPOSE RULE "order based delivery" IN ENGLISH
{+In this context, providers only deliver when there is an order.
So, if a delivery is made by a provider, we assume the existence of an order that is accepted by that provider.
-}

 sentTo :: Invoice -> Client PRAGMA "" " was sent to "
  = [ ("5362a", "Applegate")
    ; ("721i" , "Brown"    )
    ; ("9443a", "Conway"   )
    ].

 delivery :: Invoice -> Delivery PRAGMA "" " covers "
  = [ ("5362a", "Jelly beans #4921")
    ; ("721i" , "Cookies #0382"    )
    ; ("9443a", "Peanut butter #1993"   )
    ].

 from :: Invoice -> Provider PRAGMA "" " has been sent by "
  = [ ("721i" , "Candy's candy")
    ; ("5362a", "Carter"       )
    ; ("9443a", "Carter"       )
    ].

 paid :: Client * Invoice [INJ] PRAGMA "" " has paid "
  = [ ("Applegate", "5362a")
    ; ("Brown", "721i")
    ; ("Conway", "9443a")
    ].
 RULE "correct payments": paid |- sentTo~ PHRASE IN ENGLISH "Payments are made only for invoices sent."
PURPOSE RULE "correct payments" IN ENGLISH
{+To prevent arbitrary payments, we enforce that every invoice is paid by the client to whom it was sent.
-}
 RULE "correct invoices": sentTo |- delivery;of;from
 PHRASE IN ENGLISH "Invoices are sent to a customer only if there is a delivery made to that customer."
PURPOSE RULE "correct invoices" IN ENGLISH
{+To make sure that deliveries are billed to the right customer,
 there must be a delivery for each invoice sent.
-}
 
ENDPATTERN
--[Sessions]----------------------------------------------
PATTERN Sessions

 sProvider :: Session * Provider [UNI] PRAGMA "" " is being run by ".
 sClient   :: Session * Client   [UNI] PRAGMA "" " is being run by ".

ENDPATTERN
--[Delivery Process]--------------------------------------
PROCESS Delivery

RULE "login": I[Session] |- (sProvider;V/\-sClient;V) \/ (sClient;V\/-sProvider;V)
PHRASE "Every session is being run by either a Provider or a Client"
ROLE Client MAINTAINS "login"
ROLE Client EDITS  sClient[Session*Client]
ROLE Provider MAINTAINS "login"
ROLE Provider EDITS sProvider[Session*Provider]

RULE "create orders": I[Order] |- from; from~
PHRASE IN ENGLISH "Each order is created by precisely one client."
PURPOSE RULE "create orders" IN ENGLISH
{+Orders should be deliverable and payable. For such purposes, it is necessary to know the client (customer) that created the order-}
ROLE Client MAINTAINS "create orders"
ROLE Client EDITS  from[Order*Client], item[Order*Product]

RULE "accept orders": addressedTo~ |- accepted\/rejected
PHRASE IN ENGLISH "Orders addressed to a provider must be accepted or rejected by that provider."
PURPOSE RULE "accept orders" IN ENGLISH
{+Not every order received by a provider leads to a delivery.
The provider may decide to accept or to reject an order.
Eventually, all orders must be acknowledged, either positively (accept) or negatively (reject).
-}
PURPOSE RULE "accept orders" IN DUTCH
{+Orders worden verstrekt door klanten om een verkooptransactie te starten.
Op enig moment moet een leverancier deze order accepteren of afwijzen.
In het huidige (simplistische) model wordt elke order uiteindelijk geaccepteerd.
In een meer realistisch model moet tenminste worden gegarandeerd dat orders niet verloren gaan.
-}
PURPOSE RULE "accept orders" IN ENGLISH
{+Orders are issued by clients for the purpose of making a sales transaction.
At some point in time, a provider must accept or reject the order.
In this simplistic model, every order will be accepted.
A more realistic model should at least ensure that orders will not be lost.
-}
ROLE Provider MAINTAINS "accept orders"
ROLE Provider EDITS accepted,rejected

RULE "ship orders": accepted |- provided;of
PHRASE IN ENGLISH "Each order that has been accepted by a provider must (eventually) be shipped by that provider."
PURPOSE RULE "ship orders" IN ENGLISH
{+Ultimately, each order accepted must be shipped by the provider who has accepted that order.
The provider will be signalled of orders waiting to be shipped.
-}
ROLE Provider MAINTAINS "ship orders"
ROLE Provider EDITS item[Delivery*Product]

RULE "pay invoices": sentTo~ |- paid
PHRASE IN ENGLISH "All invoices sent to a customer must be paid by that customer."
PURPOSE RULE "pay invoices" IN ENGLISH
{+A client who receives an invoice must eventually pay.
-}
ROLE Client MAINTAINS "pay invoices"
ROLE Client EDITS paid

RULE "receive goods": of;from |- deliveredTo
PHRASE IN ENGLISH "Every delivery must be acknowledged by the client who placed the corresponding order."
PURPOSE RULE "receive goods" IN ENGLISH
{+The ordered goods must be delivered at some point in time to the client.
This is done in one delivery.
-}
ROLE Client MAINTAINS "receive goods"
ROLE Client EDITS deliveredTo

RULE "send invoices": delivery;of;from |- sentTo
PHRASE IN ENGLISH "After a delivery has been made to a customer, an invoice must be sent."
PURPOSE RULE "send invoices" IN ENGLISH
 {+In order to induce payment, a provider sends an invoice for deliveries made.
-}
ROLE Provider MAINTAINS "send invoices"
ROLE Provider EDITS item[Delivery*Product]

ENDPROCESS
--[Services]----------------------------------------------
SERVICE Login(sClient,sProvider) : I /\ -(sClient;sClient~ \/ sProvider;sProvider~)
 = [ "Login as Provider"  : sProvider[Session*Provider]
   , "or login as Client" : sClient[Session*Client]
   ]

--!t.b.v.  RULE "order creation": I[Order] |- from; from~
SERVICE Orders(from[Order*Client],addressedTo,item[Order*Product]) : (I /\ sClient;sClient~);V;(I[Order] /\ -(from[Order*Client];from[Order*Client]~))
 = [ "Client"          : from[Order*Client]
   , "Provider"        : addressedTo[Order*Provider]
   , "Items"           : item[Order*Product]
   ]

--!t.b.v.  RULE "accept orders": addressedTo~ |- accepted\/rejected   (door Provider)
SERVICE Orders(accepted,rejected) : sProvider;addressedTo~;(I[Order] /\ -(accepted~ \/ rejected~);V)
 = [ "Client"          : from[Order*Client]
   , "Items"           : item[Order*Product]
   , "Accepted by"     : accepted[Provider*Order]~
   , "Rejected by"     : rejected[Provider*Order]~
   ]

--!t.b.v.  RULE "ship orders": accepted |- provided;of   (door Provider)
SERVICE Deliveries(of[Delivery*Order]) : sProvider;accepted[Provider*Order];(I /\ -of[Delivery*Order]~;V)
 = [ "Delivery"      : of[Delivery*Order]~
   , "Client"        : from[Order*Client]
   , "Items"         : item[Order*Product]
   ]

--!t.b.v.  RULE "send invoices": delivery;of;from |- sentTo
SERVICE SendInvoice(sentTo[Invoice*Client],delivery[Invoice*Delivery],from[Invoice*Provider]) : sProvider;accepted[Provider*Order];of[Delivery*Order]~;(I[Delivery] /\ -(delivery~;(I[Invoice]/\sentTo;sentTo~ /\from[Invoice*Provider];from[Invoice*Provider]~));delivery)
 = [ "invoice"  : delivery[Invoice*Delivery]~
   = [ "Sent to" : sentTo[Invoice*Client]
     , "Sent by" : from[Invoice*Provider]
   ] ]

--!t.b.v.  RULE "pay invoices": sentTo~ |- paid
SERVICE PayInvoice(paid[Client*Invoice]) : sClient;(from[Order*Client]~;of[Delivery*Order]~;delivery[Invoice*Delivery]~/\-paid[Client*Invoice])
 = [ "Delivery"      : delivery[Invoice*Delivery]
   = [ "Order"       : of[Delivery*Order]
     = [ "Items"       : item[Order*Product]
     ] ]
   , "paid by"       : paid[Client*Invoice]~
   ]

--!t.b.v.  RULE "receive goods": of[Delivery*Order];from[Order*Client] |- deliveredTo[Delivery*Client]
SERVICE SignDeliveryReceipt(deliveredTo) : I[Delivery]
 = [ "Order"         : of[Delivery*Order]
   = [ "Client"        : from[Order*Client]
     , "Items"         : item[Order*Product]
     ]
   , "Delivered items" : item[Delivery*Product]
   ]

-- deliveredTo :: Delivery -> Client PRAGMA "" " is delivered to "

--[Miscellaneous Populations]------------------------------

POPULATION item[Order*Product] CONTAINS
    [ ("C45666"                  , "Jelly beans"  )
    ; ("Order 22/09/2006 Cookies", "Cookies"      )
    ; ("C45683"                  , "Peanut butter")
    ]

{-===================================================================-}
ENDCONTEXT