-- Copyright (c) 2003-2007 ETH Zurich, Switzerland
--                    2016 The University of Sheffield, UK
-- 
-- All rights reserved.
-- 
-- Redistribution and use in source and binary forms, with or without
-- modification, are permitted provided that the following conditions are met:
-- 
-- * Redistributions of source code must retain the above copyright notice, this
--   list of conditions and the following disclaimer.
-- 
-- * Redistributions in binary form must reproduce the above copyright notice,
--   this list of conditions and the following disclaimer in the documentation
--   and/or other materials provided with the distribution.
-- 
-- THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS"
-- AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE
-- IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE
-- DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT HOLDER OR CONTRIBUTORS BE LIABLE
-- FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL
-- DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR
-- SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER
-- CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY,
-- OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE
-- OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
-- 
-- SPDX-License-Identifier: BSD-2-Clause
--

------------------------------------------
-- Case 1
------------------------------------------
package InvoicingOrders
  -- 
  -- 1) Constraining the Data Model
  -- ==============================

  -- The stock of a Product is always a natural number, i.e., it is a 
  -- positive Integer. This also ensures the definedness of the stock.  
  context Product 
    inv isNat: self.stock >= 0  

  -- The Product id is unique.
   context Product
     inv idUnique: Product::allInstances()
                      ->forAll(p1:Product, p2:Product | p1.id <> p2.id)  

  -- The quantity of an Order is always a natural number, i.e., it is 
  -- a positive Integer. This also ensures the definedness of the 
  -- quantity.
  context Order 
    inv isNat: self.quantity >= 0  

  -- The state of an Order should either be `pending'  or `invoiced'. 
  -- As a direct support for enumeration is not well developed in most 
  -- CASE tools, we use a String and constrain it to the two 
  -- alternatives using an invariant. 
  context Order
    inv stateRange:    (self.state = 'pending') 
                    or (self.state = 'invoiced') 

  -- The Order id is unique.
   context Order 
     inv idUnique: Order::allInstances()
                      ->forAll(o1:Order, o2:Order | o1.id <> o2.id)  



  -- 
  -- 2) Constraining the Dynamic Part
  -- ================================

  -- Initialize the state of an Order
  context Order::state : String
    init: 'pending'

  -- Create a new Order
  context Order::Order(prd:Product, qty:Integer):OclVoid
    pre: qty > 0
    pre: self.warehouse.products->exists(x:Product | x = prd)
    pre: not prd.oclIsUndefined()
    post: self.oclIsNew() and  self.quantity = qty
       --   and self.orderedProduct = prd

  -- The state of the order will be changed into "invoiced" if the ordered quantity 
  -- is either less or equal to the quantity which is in stock according to the 
  -- reference of the ordered product. 
   context Order::invoice() : Boolean
     pre: self.state = 'pending' 
--          and self.quantity <= self.orderedProduct.stock
     post: self.state = 'invoiced' and self.quantity = self.quantity@pre
--           and self.orderedProduct = self.orderedProduct@pre
--           and self.orderedProduct.stock = self.orderedProduct@pre.stock - self.quantity

  -- Cancel order as an opposite operation to invoice order
  context Order::cancel() : Boolean		
    pre:  self.state = 'invoiced'
    post: self.state = 'pending'   
          and self.quantity = self.quantity@pre and self.product = self.product@pre
          and self.product.stock = self.product@pre.stock + self@pre.quantity

  -- Create a new Order
  context Product::Product():Boolean
    pre : true
    post: self.stock = 0 and self.oclIsNew() 
    
  -- Add quantity of the product to the stock
  context Product::supply(qty:Integer):Boolean
    pre: qty > 0
    post: self.stock = self.stock@pre + qty

  -- Remove quantity of the product from the stock
  context Product::release(qty:Integer):Boolean
    pre:  self.stock >= qty
    post: self.stock = self.stock@pre - qty

endpackage


-- ------------------------------------------
-- -- Case 2
-- ------------------------------------------
package InvoicingOrders
  -- 
  -- 1) Constraining the Data Model
  -- ==============================
  -- First, we present several invariants on the static data model. These 
  -- type constraints

  -- There is one and only one Warehouse.
   context Warehouse
     inv isStatic: self.allInstances()->size() = 1



  -- All products are in the Warehouse.
  context Product 
    inv isInWarehouse : 
         not self.warehouse.oclIsUndefined()

  --  -- All orders are in the Warehouse.
  context Order 
    inv isInWarehouse: not self.warehouse.oclIsUndefined()



  -- 
  -- 2) Constraining the Dynamic Part
  -- ================================


   -- Create a new Order
  context Order::Order(prd:Product,qty:Integer):OclVoid
    pre: self.warehouse.products->exists(x:Product | x = prd)


-- Warehouse management
--  context Warehouse::getFirstInvoicable():Order
--    pre: self.orders->exists(x:Order | 
--                x.state = 'pending' and x.quantity <= x.product.stock)
--    body: self.orders->any(x:Order | 
--                x.state = 'pending' and x.quantity <= x.product.stock)

endpackage