-- 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
--

package Vehicles

  context Person
    inv AtLeastOneTruckPerPerson: self.truck->notEmpty()
    inv NumberOfDrivenTrucksNotZero: self.truck->size() <> 0
    inv AllPersonsWithDriversLicenseAdult:
        self.driversLicense->notEmpty() implies self.age > 17
  inv AllDriversAllowedToDriveTheirTrucks :
      self.truck->forAll( t:Truck | self.isAllowedToDriveTruck( 
           self.driversLicense.licenseClass, t.oclAsType(Vehicles.Vehicle).tons))

  context Person
   inv FeatureOfLicenseClassCE:
     Truck::allInstances()->forAll( t : Truck |
       self.isAllowedToDriveTruck( 'CE', t.tons ) )

  context Person
   inv NoPersonMoreThan18Points:
     self.ticket->iterate( t : Ticket ; sum : Integer = 0 |
       sum + t.points ) <= 18

  context 
   Person::isAllowedToDriveTruck(licenseClass:String, tons:Real):Boolean
   post: result = if licenseClass='CE' or licenseClass='C' 
                  then true
                  else if licenseClass='C1' or licenseClass='C1E' 
                       then tons<=7.5 
                       else false 
                       endif 
                  endif

  context DriversLicense
    inv AllLicenseOwnersAdult: person.age > 17

  context Truck
    inv MinimumDimension:
        self.lengthLoadingSpace > 5.0 and self.widthLoadingSpace > 1.0 and
        self.heightLoadingSpace > 2.0
    inv MinimumCapacity: self.capacityLoadingSpace() > 10.0

  context Truck::capacityLoadingSpace():Real
    post: result = lengthLoadingSpace * widthLoadingSpace 
                   * heightLoadingSpace

  context Ticket
    inv PointsNotNegative: self.points >= 0
    inv NoTicketMoreThan18Points: self.points <= 18
    inv NoTicketWithoutTruck: self.person.truck->notEmpty()

endpackage