/* moduleName: Date-Time Vocabulary
   moduleAbbreviation: DTV
   moduleVersion: 1.3
   moduleAbstract: This file contains OCL for portions of the Date-Time Vocabulary.  See http://www.omg.org/spec/DTV1.3.
   filename: dtv.ocl
   documentNumber: dtc/16-02-24
   documentURL: http:/www.omg.org/spec/DTV/20160301/dtv.ocl
   isNormative: true
   contentType: vocabulary
   contentLanguage: http://www.omg.org/spec/OCL/2.4 
   format: OCL
   directSource: http:/www.omg.org/cgi-bin/doc?dtc/16-02-20
   copyright: Copyright (c) 2015, Object Management Group
*/

/* -- Time Infrastructure -- */

/* For each time interval1, there is at least one time interval2 that is a proper part of time interval1.*/
context _'time interval'
inv: self._'time interval1 is proper part of time interval2'::
_'time interval1'->notEmpty()

/* If a time interval1 overlaps a time interval2, then the time interval1 is not before the time interval2.*/
context _'time interval'
inv: _'time interval'.allInstances->    
    forAll(t2 | self.overlaps(t2) implies not self._'is before'(t2))

/* If a time interval1 does not overlap a time interval2, then the time interval1 is before the time interval2 or the time interval2 is before the time interval1.*/
context _'time interval'
inv: _'time interval'.allInstances-> 
    forAll(t2 | 
      not self.overlaps(t2) 
      implies (self._'is before'(t2) or t2._'is before'(self)))

/* A given time interval is not before the time interval.*/
context _'time interval'
inv: not self._'is before'(self)

/* If a time interval1 is before a time interval2, then the time interval2 is not before the time interval1.*/
context _'time interval'
inv: _'time interval'.allInstances-> 
    forAll(t2 | 
     self._'is before'(t2) 
        implies not t2._'is before'(self))

/* Each time interval1 overlaps each time interval2 and time interval1 is not before time interval2 and time interval2 is not before time interval1, or time interval1 is before time interval2 and time interval1 does not overlap time interval2 and time interval2 is not before time interval1, or time interval2 is before time interval1 and time interval1 does not overlap time interval2 and time interval1 is not before time interval2.*/
context _'time interval'
inv: _'time interval'.allInstances->
    forAll(t2 |
     (self.overlaps(t2) 
       and not self._'is before'(t2)
       and not t2._'is before'(self))
    or (self._'is before'(t2)
        and not self.overlaps(t2)
        and not t2._'is before'(self))
    or (t2._'is before'(self)
        and not self.overlaps(t2)
        and not self._'is before'(t2)))

/* If a time interval1 is before a time interval2 and the time interval2 is before a time interval3 then the time interval1 is before the time interval3.*/
context _'time interval'
inv: _'time interval'.allInstances->
     forAll(t2, t3 |
       self._'is before'(t2)
       and t2._'is before'(t3)
       implies self._'is before'(t3))

/* time interval1 is before time interval2 and some time interval3 is after time interval1 and is before time interval2*/
context _'time interval'
def: _'time interval1 is properly before time interval2' (t2: _'time interval'): Boolean = 
     self._'is before'(t2) and
     'time interval'.allInstances->exists(t3 | self._'is before'(t3) and t3._'is before'(t2))

/* the time interval1 is part of the time interval2 and the time interval2 is part of the time interval1*/
context _'time interval'
def: _'time interval1 equals time interval2' (t2: _'time interval'): Boolean =
     self._'is part of'(t2) and t2._'is part of'(self)

/* A time interval1 equals a time interval2 if and only if time interval1 is time interval2*/
context _'time interval'
inv: _'time interval'.allInstances->
forAll(t2 |
  self.equals(t2) implies self.is(t2)
  and (self.is(t2) implies self.equals(t2) ))

/* time interval1 is before time interval2 and no time interval3 is after time interval1 and is before time interval2*/
context _'time interval'
def: _'time interval1 meets time interval2'(t2: _'time interval'): Boolean = 
     self._'is before'(t2) and
     not _'time interval'.allInstances->
       exists(t3 | self._'is before'(t3) and t3._'is before'(t2))

/* time interval1 overlaps time interval2 and some part of time interval1 is before time interval2*/
context _'time interval'
def: _'time interval1 properly overlaps time interval2' (t2: _'time interval'): Boolean = 
     self.overlaps(t2) and
     'time interval'.allInstances-> 
       exists(t3 | t3._'is a proper part of'(self) and t3._'is before'(t2))

/* time interval1 is part of time interval2 and some part of time interval2 is before time interval1  and some part of time interval2 is after time interval1*/
context _'time interval'
def: _'time interval1 is properly during time interval2' (t2: _'time interval'): Boolean = 
     self._'is a proper part of'(t2) and
     'time interval'.allInstances-> 
         exists(t3, t4 |
          t3._'is a proper part of'(t2) and t4._'is a proper part of'(t2) and
           t3._'is before'(self) and self._'is before'(t4))

/* time interval1 is a proper part of time interval2 and no part of time interval2 is before time interval1*/
context _'time interval'
def: _'time interval1 starts time interval2' (t2: _'time interval'): Boolean = 
     self._'is a proper part of'(t2) and
     not 'time interval'.allInstances-> 
       exists(t3 | t3._'is a proper part of'(t2) and t3._'is before'(self))

/* time interval1 is a proper part of time interval2 and no part of time interval2 is after time interval1*/
context _'time interval'
def: _'time interval1 finishes time interval2'(t2: _'time interval'): Boolean = 
     self._'is a proper part of'(t2) and
     not _'time interval'.allInstances-> 
       exists(t3 | t3._'is a proper part of'(t2) and self._'is before'(t3))

/* some time interval3 is part of time interval1 and is before time interval2 */
context _'time interval'
def: _'starts before'(t2: _'time interval'): Boolean =
'time interval'.allInstances->
  exists(t3 |
    t3._'is  part of'(self)
    and t3._'is before'(t2))

/* time interval1 starts time interval2 or time interval2 starts time interval1 or time interval1 equals time interval2 */
context _'time interval'
def: _'time interval1 starts with time interval2'(t2: _'time interval'): Boolean =
   self.starts(t2) or t2.starts(self) or  self.equals(t2)

/* c */
context _'time interval'
inv:_'time interval'.allInstances
->
forAll(t2 |
  self._'time interval1 starts with time interval2'(t2)
    implies t2. _'time interval1 starts with time interval2'(self))

/* some time interval3 starts time interval1 and is part of time interval2 */
context _'time interval'
def: _'starts during'(t2: _'time interval'): Boolean =
'time interval'.allInstances->
  exists(t3 |
    t3._'is  part of'(t2)
    and t3.starts(self))

/* time interval1 finishes time interval2 or time interval2 finishes time interval1 or time interval1 equals time interval2 */
context _'time interval'
def: _'time interval1 finishes with time interval2'(t2: _'time interval'): Boolean =
  t1.finishes(t2) or t2.finishes(t1) or  t1.equals(t2)

/* If time interval1 finishes with time interval2 then time interval2 finishes with time interval1 */
context _'time interval'
inv:_'time interval'.allInstances -> 
forAll(t2 |
  self._'time interval1 finishes with time interval2'(t2)
    implies t2. _'time interval1 finishes with time interval2'(self))

/* some time interval3 is part of time interval1 and is after time interval2 */
context _'time interval'
def: _'finishes after'(t2: _'time interval'): Boolean =
'time interval'.allInstances->
  exists(t3 |
    t3._'is  part of'(self)
    and t2._'is before'(t3))

/* some time interval3 finishes time interval1 and is part of time interval2 */
context _'time interval'
def: _'ends during'(t2: _'time interval'): Boolean =
'time interval'.allInstances->
  exists(t3 |
    t3._'is  part of'(t2)
    and t3.finishes(self))

/* time interval1 is after time interval2 and  time interval1 is before time interval3 */
context _'time interval'
def: _'time interval1 is between time interval2 and time interval3'
     (t2: _'time interval', t3: _'time interval'): Boolean = 
     t2.precedes(self) and self.precedes(t3)

/* time interval3 includes time interval1 and time interval3 includes time interval2 and time interval3 is part of each time interval that includes time interval1 and time interval2*/
context _'time interval'
def: _'plus time interval2 is time interval3'
   (t2: _'time interval', t3: _'time interval'): Boolean =
      self._'is part of'(t3) and t2._'is part of'(t3) and
      _'time interval'.allInstances->forAll
            (t4 | self._'is part of'(t4) and t2._'is part of'(t4) 
                 implies t3._'is part of'(t4))

/* if a time interval1 is before a time interval2 or time interval1 properly overlaps time interval2, then time interval1 plus time interval2 is started by time interval1 and is finished by time interval2*/
context _'time interval'
inv: _'time interval'.allInstances->(forAll t2 |
   (self._'is before'(t2) or self._'properly overlaps'(t2)) implies
   (self.starts(self.plus(t2)) and t2.finishes(self.plus(t2)) )

/* if a time interval1 is after a time interval2 or time interval1 is properly overlapped by time interval2, then time interval1 plus time interval2 is started by time interval2 and is finished by time interval1.*/
context _'time interval'
inv: _'time interval'.allInstances->(forAll t2 |
   (t2._'is before'(self) or t2._'properly overlaps'(self)) implies
   (t2.starts(self.plus(t2)) and self.finishes(self.plus(t2)) )

/* if a time interval1 is part of a time interval2, then time interval1 plus time interval2 is time interval2.*/
context _'time interval'
inv: _'time interval'.allInstances->(forAll t2 |
   (self._'is part of'(t2) implies self.plus(t2) = t2 ) 

/* if a time interval2 is part of a time interval1, then time interval1 plus time interval2 is time interval1.*/
context _'time interval'
inv: _'time interval'.allInstances->(forall t2 |
   (t2._'is part of'(self) implies self.plus(t2) = self ) 

/* For each time interval1 and each time interval2, there is a time interval3 that is time interval1 plus time interval2.*/
context _'time interval'
inv: _'time interval'.allInstances->forAll(t2 |
'time interval'.allInstances->exists(t3 |
self._'time interval1 plus time interval2 is time interval3'(t2, t3)))

/* A time interval1 plus a time interval2 is exactly one time interval3.*/
context _'time interval'
inv: _'time interval'.allInstances->
    forAll(t2 |
      'time interval'.allInstances->
       one(t4 | t4 = self.plus(t2)))

/* time interval1 starts time interval2 and time interval3 finishes time interval2 and time interval1 meets time interval3*/
context _'time interval'
def: _'starts time interval2 complementing time interval3' 
     (t2: _'time interval', t3: _'time interval'): Boolean =
  self.starts(t2) and t3.finishes(t2) and self.meets(t3)

/* If a time interval1 starts a time interval2, then some time interval3 finishes time interval2 complementing time interval1. */
context 'time interval'
inv: _'time interval'.allInstances->forAll(t2 |
self.starts(t2) implies 
'time interval'.allInstances->exists(t3 |
t3._'finishes time interval2 complementing time interval3'
     (t2, self)))

/* If a time interval1 starts a time interval2 complementing a time interval3, then each time interval4 that is part of the time interval2 and that does not overlap the time interval1 is part of the time interval3.*/
context _'time interval'
inv: _'time interval'.allInstances-> 
     forAll(t2, t3, t4 | 
     (t3 = t2._'minus starting interval'(self)
     and (t4._'is part of'(t2)
     and not t4.overlaps(self))
     implies t4._'is part of'(t3)))

/* If a time interval1 starts a time interval2 then the time interval1 starts the time interval2 complementing exactly one time interval3.*/
context _'time interval'
inv: _'time interval'.allInstances -> 
     forAll(t2 |
      'time interval'.allInstances ->
       isUnique(t2._'minus starting interval'(self))

/* time interval1 finishes time interval2 and time interval3 starts time interval2 and time interval1 is met by time interval3*/
context _'time interval'
def: _'finishes time interval2 complementing time interval3'
       (t2: _'time interval', t3: _'time interval'): Boolean =
  self.finishes(t2) and t3.starts(t2) and t3.meets(self)

/* If a time interval1 finishes a time interval2, then some time interval3 starts time interval2 complementing time interval1. */
context 'time interval'
inv: _'time interval'.allInstances->forAll(t2 |
self.finishes(t2) implies 
'time interval'.allInstances->exists(t3 |
t3._'starts time interval2 complementing time interval3'
     (t2, self)))

/* If a time interval1 finishes a time interval2 complementing a time interval3, then each time interval4 that is part of the time interval2 and that does not overlap the time interval1 is part of the time interval3.*/
context _'time interval'
inv: _'time interval'.allInstances-> 
     forAll(t2, t3, t4 | 
     (t3 = t2._'minus finishing interval'(self)
     and (t4._'is part of'(t2)
     and not t4.overlaps(self))
     implies t4_.'is part of'(t3)))

/* If a time interval1 finishes a time interval2 then the time interval1 finishes the time interval2 complementing exactly one time interval3.*/
context _'time interval'
inv: _'time interval'.allInstances -> 
     forAll(t2 |
      'time interval'.allInstances ->
       isUnique(t2._'minus finishing interval'(self))

/* For each time interval1 and each time interval2 that is properly during time interval1, there is a time interval4 that finishes time interval1 and is met by time interval2.*/
context _'time interval'
inv: _'time interval'.allInstances-> 
      forAll(t2 | t2._'is properly during'(self) 
      implies _'time interval'.allInstances
       -> exists(t3 | t3.starts(self) and t3.meets(t2)))

/* For each time interval1 and each time interval2 that is properly during time interval1, there is a time interval4 that finishes time interval1 and is met by time interval2.*/
context _'time interval'
inv: _'time interval'.allInstances-> 
       forAll(t2 | t2._'is properly during'(self)
         implies _'time interval'.
             allInstances-> exists(t3 | t3.ends(self) and t2.meets(t3)))

/* time interval1 is part of time interval2 and time interval1 is part of time interval3 and time interval1 includes each time interval that is part of time interval2 and time interval3*/
context _'time interval'
def: _'is intersection of '(t2: _'time interval', t3: _'time interval'):  
              Boolean =
      self._'is part of'(t2) and self._'is part of'(t3) and
      _'time interval'.allInstances->
            forAll(t4 | (t4._'is part of'(t2) and t4._'is part of'(t3)) 
                 implies t4._'is part of'(self))

/* if time interval2 is part of time interval3, then time interval1 equals time interval3, and if time interval3 is part of time interval2, then time interval1 equals time interval2, and if time interval2 properly overlaps time interval3, then time interval1 finishes time interval2 and time interval1 starts time interval3, and if time interval3 properly overlaps time interval2, then time interval1 finishes time interval3 and time interval1 starts time interval2*/
context _'time interval'
def: _'is intersection of '(t2: _'time interval', t3: _'time interval'):  
              Boolean =
      (t2.includes(t3) implies self.equals(t3)) and
      (t3.includes(t2) implies self.equals(t2)) and
      (t2._'properly overlaps'(t3) implies  
          self.finishes(t2) and self.starts(t3) ) and
      (t3._'properly overlaps'(t2) implies  
          self.finishes(t3) and self.starts(t2) ) 

/* If a time interval1 overlaps a time interval2, then some time interval3 intersects time interval1 with time interval2. */
context 'time interval'
inv: _'time interval'.allInstances->forAll(t2 |
self.overlaps(t2) implies 
'time interval'.allInstances->exists(t3 |
  t3._'is intersection of'(self, t2)))

/* If a time interval1 intersects a time interval2 with a time interval3 and a time interval4 is part of the time interval1 and the time interval4 is part of the time interval2, then the time interval4 is part of the time interval3.*/
context _'time interval'
inv: _'time interval'.allInstances-> 
     forAll(t2, t3, t4 |
        (self.overlaps(t2) and t4._'is part of'(self) and t4_.'is part of'(t2))
       implies
        t4._'is part of'(self._'intersected with'(t2)))

/* If a time interval1 overlaps a time interval2, then the time interval1 intersects a time interval2 with exactly one time interval3.*/
context _'time interval'
inv: _'time interval'.allInstances->forAll(t2 |
      self.overlaps(t2) implies
      'time interval'.allInstances->
      isUnique(self._'intersected with'(t2)))

/* If a time interval1 is properly before a time interval2 then the time interval1 meets a time interval3 and the time interval3 meets the time interval2 and the time interval1 plus the time interval2 is a time interval4 and the time interval1 starts the time interval4 complementing a time interval5 and the time interval2 finishes the time interval4 complementing a time interval6 and the time interval5 intersects the time interval6 with the time interval3.*/
context _'time interval'
inv: _'time interval'.allInstances->   
    forAll(t2|
     self._'is properly before'(t2)
     implies
     'time interval'.allInstances-> 
       exists(t3, t4, t5, t6|
        self.meets(t3)
        and t3.meets(t2)
        and t4 = self.plus(t2)
        and t5 = t4._'minus starting interval'(self)
        and t6 = t4._'minus finishing interval(t2)
         and t3 = t5._'intersected with"(t6)))

/* time interval1 starts before time interval2, and time interval1 starts time interval3, and time interval2 finishes time interval3 */
context _'time interval'
def: _'through time interval2 is time interval3' 
      (t2: _'time interval', t3: _'time interval'): Boolean =
     self._'starts before'(t2) and 
     self.starts(t3) and t2.finishes(t3)

/* time interval1 through time interval2 (noun form)*/
context _'time interval'
def: _'through time interval' (t2: _'time interval'): _'time interval' =
  _'time interval'.allInstances-> (t3 | 
    self.starts(t3) and t2.finishes(t3))

/* For each time interval1 that starts before a given time interval2, exactly one time interval3 is time interval1 through time interval2.*/
context _'time interval'
inv: _'time interval'.allInstances->
    forAll(t2 |
      self._'starts_before'(t2) implies
      _'time interval'.allInstances-> 
           one(t3 | t3 = self._'through time interval'(t2)) )

/* time interval1 is before time interval2, and time interval3 is time interval1 if time interval1 meets time interval2, and time interval3 is the time interval that meets time interval2 and is started by time interval1 if time interval1 is properly before time interval2 */
context _'time interval'
def: _'to time interval2 is time interval3' 
      (t2: _'time interval', t3: _'time interval'): Boolean =
     self._'is before'(t2) and 
     (if self.meets(t2) then t3 = self
         else self.starts(t3) and t3.meets(t2))

/* time interval1 to time interval2 (noun form) */
context _'time interval'
def: _'to time interval' (t2: _'time interval'): _'time interval' =
    if (not (self._'is before(t2)) then null
    else if (self.meets(t2)) then self
    else _'time interval'.allInstances-> 
            forall(t3 | t3.meets(t2)and self.starts(t3))

/* For each time interval1 that is before a given time interval2, exactly one time interval3 is time interval1 to time interval2.*/
context _'time interval'
inv: _'time interval'.allInstances->
    forAll(t2 |
      self.before(t2) implies
      _'time interval'.allInstances-> 
           one(t3 | t3 = self._'to time interval'(t2)) )

/* eternity: the time interval that includes each time interval*/
context _'time interval'
inv: self.'is part of'(eternity)

/* primordiality: the time interval that is before each time interval that is not primordiality or eternity.*/
context 'time interval'
inv: self = primordiality or self = eternity 
     or primordiality._'is before'(self)

/* perpetuity: the time interval that is after each time interval that is not perpetuity or eternity.*/
context 'time interval'
inv: self = perpetuity or self = eternity 
     or self._'is before'(perpetuity)

/* Each duration is less or equal the duration.*/
context duration
inv: self._'is less or equal'(self))

/* Each duration1 is less or equal each duration2 or duration2 is less or equal duration1.*/
context duration
inv: duration.allInstances->forAll(d2 |
     self._'is less or equal(d2)
     or d2._'is less or equal'(self)

/* If some duration1 is less or equal some duration2 and the duration2 is less or equal the duration1, then the duration1 equals the duration2.*/
context duration
inv: duration.allInstances->forAll(d2 |
     self._'is less or equal'(d2)
     and d2._'is less or equal'(self)
     implies self = d2)

/* If some duration1 is less or equal some duration2 and the duration2 is less or equal the duration3 then the duration1 is less or equal the duration3.*/
context duration
inv: duration.allInstances->forAll(d2, d3 |
    self._'is less or equal'(d2)
    and d2._'is less or equal(d3)
    implies self._'is less or equal'(d3))

/* If some duration1 = some duration2 and the duration2 = some duration3 then the duration1 = the duration3.*/
context duration
inv: duration.allInstances->forAll(d2, d3 |
    self._equals(d2) and d2.equals(d3)
    implies self.equals(d3))

/* duration1 is less or equal duration2 and duration1 does not equal duration2 */
context duration
def: _'is less than'(d2: duration): Boolean =
     self._'is less or equal'(d2)
     and not self.equals(d2)

/* For each duration1 and each duration2 some duration3 equals duration1 plus duration2.*/
context duration
inv: 
duration->allInstances(forAll d2 | 
   duration->allInstances(exists d3 | d3 = self.plus(d2)) )

/* If a duration4 equals a duration1 plus a duration2, and a duration5 equals duration4 plus duration3, and a duration6 equals duration2 plus duration3, then duration5 equals duration1 plus duration6.*/
context duration
inv: duration.allInstances->
   forAll(d2, d3 |
     (self._'plus duration'(d2)
      ._'plus duration'(d3))
       .equals(self._'plus duration'
         (d2._'plus duration'(d3))))

/* Each duration1 plus duration2 equals duration2 plus duration1.*/
context duration
inv: duration.allInstances->forAll(d2 |
     self._'plus duration'(d2).equals
     (d2._'plus duration'(self)))

/* Each duration plus D0 = the duration.*/
context duration
inv: self = self._'plus duration'(D0)

/* D0 equals each duration1 plus some duration2.*/
context duration
inv: duration.allInstances->exists(d2 |
      D0 = self + d2)

/* For each number and each duration1, some duration2 is number times duration1.*/
context duration
inv: Integer.allInstances->forAll(n |
     self._'times number'(n)
      .oclIsKindOf(duration))

/* If a duration3 equals a number1 times (a duration1 plus a duration2) then duration3 equals (number1 times duration1) plus (number1 times duration2).*/
context duration
inv: duration.allInstances->forAll(d2 |
     Integer.allInstances->forAll(n |
     self._'plus duration'(d2)
      ._'times number'(n).equals(
        self._'times number'(n)
         .self._'plus duration'(
           d2._'times number'(n)))))

/* If a (number1 plus a number2) times a duration1 equals a duration2, then duration2 equals (number1 times duration1) plus (number2 times duration1).*/
context duration
inv: Integer.allInstances->
 forAll(n1, n2 |
  self._'times number'(n1 + n2).equals(
   self._'times number'(n1)._'plus duration'
    (self_.'times number'(n2))))

/* D0 equals 0 times each duration1.*/
context duration
inv: self._'times number'(0) = D0

/* D0 equals a number1 times a duration1 if and only if number1 equals 0 or duration1 equals D0.*/
context duration
inv: Integer.allInstances(forAll n |
    (self._'times number'(n) = D0) eqv (self = D0 or n = 0) )) 

/* If a duration1 does not equal D0, then a duration2 equals a number1 times duration1.*/
context duration
inv: if (not (self = D0)) then
    self.duration.allInstances->(forAll d |
      Integer.allInstances(exists n |
        self._'times number'(n) = d)  ) 

/* Each time interval has exactly one duration.*/
context _'time interval'
inv: 
self._'particular duration'->size() = 1

/* The duration of each time interval is greater than D0.*/
context _'time interval'
inv: self.duration > D0

/* The duration of no time interval equals D0.*/
context _'time interval'
inv: not self.duration = D0

/* For each time interval1 there is no time interval2 such that the duration of time interval1 plus the duration of time interval2 equals D0.*/
context _'time interval'
inv: _
'time interval'.allInstances->forAll(t2 |
  not ((self.duration() + t2.duration()) = D0))

/* For each time interval1 and each time interval2 that is a part of time interval1, the duration of time interval2 is less than or equal to the duration of time interval1.*/
context _'time interval'
inv: 
'time interval'.allInstances->forAll(t2 |
  self._'is part of'(t2)
  implies self_.'particular duration'._'is less than'(
                d2._'particular duration'))

/* For each time interval1 and each time interval2 that meets a time interval1, the duration of  time interval1 plus time interval2 is equal to the duration of time interval1 plus the duration of time interval2.*/
context _'time interval'
inv: 
'time interval'_.allInstances->forAll(t2 |
  self.meets(t2)
  implies self.plus(t2)._'particular duration'
   .equals(self._'particular duration'
    ._'plus duration'(t2._'particular duration')))

/* For each time interval2 and each time interval3 that finishes time interval2, the duration of  the time interval1 that starts time interval2 complementing time interval3 is equal to the duration of time interval2 minus the duration of time interval3.*/
context _'time interval'
inv: 
'time interval'.allInstances->forAll(t2 |
  self.starts(t2)
  implies t2._'minus starting interval'(self)
    ._'particular duration'.equals(
      t2._'particular duration'.
         _'minus duration'(self._'particular duration')))

/* For each time interval2 and each time interval3 that starts time interval2, the duration of  the time interval1 that finishes time interval2 complementing time interval3 is equal to the duration of time interval2 minus the duration of time interval3.*/
context _'time interval'
 inv:
'time interval'.allInstances->forAll(t2 |
  self.finishes(t2)
  implies t2._'minus finishing interval'(self)
    ._'particular duration'.equals(
      t2._'particular duration'._'minus duration'(
       self._'particular duration')))

/* Each duration that is between a time interval1 and a time interval2 is greater than or equal to D0. */
context _'time interval'
def: _'is duration before'(d: duration): _'time interval' = 
     'time interval'.allInstances->
         exists(t2, t3 |
          t2._'is before'(self)
          and t2.meets(t3)
          and t3.meets(self)
          and t3._'particular duration'
                .equals(d))

/* time interval1 starts with the time interval3 that has the duration and meets time interval2 */
context _'time interval'
def: _'starts duration before'
    (d: duration, t2: _'time interval'): Boolean =
'time interval'.allInstances->
exists(t3 |
self._'starts with'(t3)
and t3.meets(t2)
and t3._'particular duration'.equals(d))

/* time interval1 finishes with the time interval3 that has the duration and is met by time interval2 */
context _'time interval'
def: _'finishes duration after'(d: duration, t2: _'time interval')
:Boolean =
'time interval'.allInstances->
exists(t3 |
self._'finishes with'(t3)
and t2.meets(t3)
and t3._'particular duration'.equals(d))

/* time interval1 is the time interval that has the duration and meets time interval2*/
context _'time interval'
def: _'is the duration preceding'(d: duration, t2:'time interval'): Boolean =
self.meets(t2)
and self._'particular duration'.equals(d))

/* For each time interval2 and for each duration, exactly one time interval1 is the duration preceding time interval2.*/
context _'time interval'
inv: _'time interval'.allInstances->
    forAll(t2 |
      duration.allInstances ->forAll(d |
        'time interval'.allInstances->one(t3 | 
          t3 = self._'is the duration preceding'(d, t2))))

/* time interval1 is the time interval that has the duration and is met by time interval2 */
context _'time interval'
def: _'is the duration following'
(d: duration, t2:'time interval'): Boolean' =
t2.meets(self)
and self._'particular duration'.equals(d))

/* For each time interval2 and for each duration, exactly one time interval1 is the duration following time interval2.*/
context _'time interval'
inv: _'time interval'.allInstances->
    forAll(t2 |
      duration.allInstances ->forAll(d |
        'time interval'.allInstances->one(t3 | 
           t3 = self._'is the duration following'(d, t2))))

/* -- Situations -- */

/* the occurrence happens continuously, without interruption, in each time interval2 that is part of the time interval*/
context occurrence
inv: _'time interval'->allInstances(one t | 
    self._'occurrence interval' = t)

/* the occurrence occurs throughout some time interval2 that is part of the time interval*/
context _'occurrence'
def: _'occurrence occurs within time interval'
      (t: _'time interval') : Boolean
      t._'part of'->exists(t2 | 
        self._'occurrence occurs throughout
         time interval'(t2))

/* the occurrence occurs throughout the occurrence interval and the occurrence does not occur within some time interval2 that meets the occurrence interval and the occurrence does not occur within some time interval3 that is met by the occurrence interval*/
context _'occurrence'
def: _'occurrence occurs for time interval'
     (t: _'time interval') : Boolean
     self._'occurrence occurs throughout time interval'
       (t)
     and self._'is met by'->forAll(t2 |
         not self._'occurrence occurs throughout
                   time interval'(t2))
     and self._'meets"->forAll(t3 |
         not self._'occurrence occurs throughout
                   time interval'(t3))

/* the occurrence occurs for some occurrence interval and the duration is the duration of the occurrence interval*/
context _'occurrence'
def: _'occurrence lasts for duration'(d: duration): Boolean =
     self._'occurrence occurs for time interval'.duration = d

/* the occurrence interval of the occurrence is before the time interval*/
context occurrence
def: _'occurs before time interval'(t: time interval): Boolean =
    self._'occurrence interval'._'is before'(t)

/* the occurrence interval of the occurrence is after the time interval*/
context occurrence
def: _'occurs after time interval'(t: time interval): Boolean =
    t._'is before'(self._'occurrence interval')

/* the occurrence interval of the occurrence starts during the time interval */
context occurrence
def: _'starts during'(t2: _'time interval'): Boolean =
   self._'occurrence interval'._'starts during'(t2)

/* the occurrence interval of the occurrence ends during the time interval */
context occurrence
def: _'ends during'(t2: _'time interval'): Boolean =
   self._'occurrence interval'._'ends during'(t2)

/* the occurrence interval of occurrence1 precedes the occurrence interval of occurrence2*/
context _'occurrence'
def: _'occurrence1 precedes occurrence2'
     (o2: _'occurrence') : Boolean
     self._'occurs for' < o2._'occurs for'

/* If some occurrence1 precedes some occurrence2, and if the occurrence2 precedes some occurrence3, then occurrence1 precedes occurrence3.*/
context _'occurrence'
inv: self._'precedes'->exists(o2 | 
       o2._'precedes'->exists(o3 | implies 
        self._'precedes'->contains(o3)))

/* the occurrence interval of occurrence1 starts before the occurrence interval of occurrence2*/
context _'occurrence'
def: _'occurrence1 starts before occurrence2'
     (o2: _'occurrence') : Boolean
  self._'occurs for'.
   'time interval starts before time interval'(o2._'occurs for')

/* the occurrence interval of occurrence1 ends before the occurrence interval of occurrence2  */
context _'occurrence'
def: _'occurrence1 ends before occurrence2'
     (o2: _'occurrence') : Boolean
  self._'occurs for'.
   'time interval ends before time interval'(o2._'occurs for')

/* the occurrence interval of occurrence1 overlaps the occurrence interval of occurrence2*/
context _'occurrence'
def: _'occurrence1 overlaps occurrence2'
      (o2: _'occurrence') : Boolean
      self._'occurs for'._overlaps(o2._'occurs for')

/* the first occurrence exemplifies the situation kind and the first occurrence occurs after the time interval and no occurrence that exemplifies the situation kind and that occurs after the time interval starts before the first occurrence */
context _'situation kind'
def: _'has first occurrence after time interval'(ti: _'time interval'): occurrence = 
     occurrence->allInstances(fo | 
     fo.exemplifies(sk) and fo._'occurs after'(ti) and
     not occurrence->allInstances(exists occ | 
         occ.exemplifies(sk) and occ._'occurs after'(ti) 
         and occ._'starts before'(fo)))

/* the first occurrence exemplifies the situation kind and no occurrence that exemplifies the situation kind starts before the first occurrence */
context _'situation kind'
def: self._'first occurrence': occurrence) = 
    occurrence->allInstances(fo | 
     fo.exemplifies(sk) and 
     not occurrence->allInstances(exists occ |
       occ._'starts before'(fo)))

/* the last occurrence exemplifies the situation kind and no occurrence that exemplifies the situation kind ends after the last occurrence */
context _'situation kind'
def: self._'last occurrence': occurrence) = 
    occurrence->allInstances(lo | 
     lo.exemplifies(sk) and 
     not occurrence->allInstances(exists occ |
         lo._'ends before'(occ)))

/* the last occurrence exemplifies the situation kind and the last occurrence occurs before the time interval and no occurrence that exemplifies the situation kind and that occurs before the time interval ends after the last occurrence */
context _'situation kind'
def: _'has last occurrence before time interval'(ti: _'time interval'): occurrence = 
     occurrence->allInstances(lo | 
     lo.exemplifies(sk) and lo._'occurs before'(ti) and
     not occurrence->allInstances(exists occ | 
         occ.exemplifies(sk) and occ._'occurs before'(ti) 
         and lo._'ends before'(occ)))

/* each occurrence of situation kind1 precedes each occurrence of situation kind2  */
context _'situation kind'
def: _'situation kind1 precedes situation kind2'
     (s2: _'situation kind') : Boolean
     self._'occurrence'.precedes(s2._'occurrence')

/* each occurrence of situation kind1 starts before each occurrence of situation kind*/
context _'situation kind'
def: _'situation kind1 
starts before
 
situation kind2'
     (s2: _'situation kind') : Boolean
     self.occurrence._'starts before'(s2.occurrence)

/* each occurrence of situation kind1 ends before each occurrence of situation kind2 */
context _'situation kind'
def: _'situation kind1 
ends before
 
situation kind2'
     (s2: _'situation kind') : Boolean
     self.occurrence._'ends before'(s2.occurrence)

/* each occurrence of situation kind1 overlaps some occurrence of situation kind2*/
context _'situation kind' 
def: _'situation kind1 overlaps situation kind2' 
     (s2: _'situation kind') : Boolean =  
     self.occurrence.overlaps (s2.occurrence)

/* -- Schedules -- */

/* the schedule entry is in the schedule entry set of the schedule.*/
context schedule
def: _'schedule has schedule entry'(se: _'schedule entry') : Boolean =
  self._'schedule entry set'.includes(se)

/* Each schedule entry has exactly one situation kind.*/
context _'schedule entry'
inv: self._'situation kind'->size() = 1

/* Each schedule entry has exactly one time interval.*/
context _'schedule entry'
inv: self._'time interval'->size() = 1

/* Each schedule entry set includes at least one schedule entry.*/
context _'schedule entry set'
inv: self.includes->size()>0

/* Each schedule defines exactly one schedule entry set.*/
context _'schedule entry'
inv: self._'schedule entry set'->size() = 1

/* the occurrence exemplifies the situation kind of a schedule entry  of the schedule and the occurrence interval of the occurrence overlaps the time interval of the schedule entry */
context schedule
def: _'schedule has occurrence'(o: occurrence) : Boolean =
    self._'schedule entry' ->exists(se |
        o.exemplifies(se._'situation kind')
        and o._'occurrence interval'.overlaps(se._'time interval))

/* the earliest time is the time interval of some schedule entry of the schedule and the earliest time does not start after the time interval of each schedule entry of the schedule*/
context schedule
def: _'earliest time'(et: _'time interval') : Boolean = 
   self._'schedule entry' -> exists (se1 | se1._'time interval'.equals(et))
   and  self._'schedule entry' ->  forAll(se2 |
             not et._'starts after'(se2._' time interval'))

/* the earliest time is the time interval of some schedule entry of the schedule and the earliest time does not start after the time interval of each schedule entry of the schedule*/
context schedule
def: _'schedule has earliest time'() : _'time interval' = 
  self._'schedule entry'._'time interval'->
    select(ti |self._'earliest time'(ti))   

/* the latest time is the time interval of some schedule entry of the schedule and the latest time ends after the time interval of each schedule entry of the schedule*/
context schedule
def: _'schedule has latest time'(lt: _'time interval') : Boolean = 
   self._'schedule entry'-> exists(se1 | lt.equals(se1._'time interval'))
 and self._'schedule entry'->forAll(se2:  | 
                   lt._'ends after'(se2._'time interval'))

/* the latest time is the time interval of some schedule entry of the schedule and the latest time ends after the time interval of each schedule entry of the schedule*/
context schedule
def: _'latest time of schedule'() : _'time interval' = 
  self._'schedule entry'._'time interval'->
    select(ti |self._'schedule has latest time'(ti)) 

/* the time span equals the earliest time of the schedule through the latest time of the schedule*/
context 
schedule
def: _'schedule has time span'(ts: _'time interval') : Boolean =
    ts.equals(self._'earliest time'.plus(self._'latest time'))

/* the time span equals the earliest time of the schedule through the latest time of the schedule*/
context schedule
def: _'time span of schedule'() : _'time interval' =
   self._'earliest time'.plus(self._'latest time')

/* Each schedule has exactly one time span.*/
context schedule
inv: schedule._'time span'->size() = 1

/* No regular schedule is an ad hoc schedule.*/
context _'regular schedule'
inv: not self.oclIsTypeOf(_'ad hoc schedule')

/* A regular schedule is for exactly one situation kind.*/
context _'regular schedule'
inv: _'regular schedule'._'situation kind'->size() = 1

/* Each regular schedule has exactly one start time.*/
context _'regular schedule'
inv: _'regular schedule'._'start time'->size() = 1

/* Each regular schedule has exactly one recurrence duration.*/
context _'regular schedule'
inv: _'regular schedule'._'recurrence duration'->size() = 1

/* Each regular schedule has at most one recurrence count.*/
context _'regular schedule'
inv: _'regular schedule'._'recurrence count'->size() = 1

/* Each regular schedule has at most one initial stub.*/
context _'regular schedule'
inv: _'regular schedule'._'initial stub'->size() <= 1

/* Each regular schedule has at most one final stub.*/
context _'regular schedule'
inv: _'regular schedule'._final stub'->size() <= 1

/* The schedule entry set of a regular schedule is the regular entry set of the regular schedule plus each initial stub of the regular schedule plus each final stub of the regular schedule. */
context _'regular schedule'
inv: self._'schedule entry set' = self._'regular entry set' 
   .plus(self._'initial stub').plus(self._'final stub')

/* No ad hoc schedule is a regular schedule.*/
context _'ad hoc schedule'
inv: not self.oclIsTypeOf(_'regular schedule')

/* -- Sequences -- */

/* If the index1 of some sequence position1 of some sequence equals the index2 of some sequence position2 of the sequence then sequence position1 is sequence position2.*/
context sequence:
inv: self._'sequence position'->forAll(sp1 | 
      self._'sequence position'->forAll(sp2 | 
       indexOf(sp1) = indexOf(sp2) implies sp1 = sp2))

/* Each sequence position has at most one next sequence position. */
context _'sequence position'
inv: self._'sequence position1 precedes sequence position2'
      ( self._'next sequence position')
     and self._'sequence position2'->forAll(sp2 |
         self._'next sequence position'.index <= sp2.index)

/* the member is the member of a sequence position of the sequence*/
context sequence
def: _'member participates in sequence'
     (member: thing, s: sequence)
     : Boolean = 
     self._'sequence position'->exists(sp | 
      sp.member = member)

/* The sequence has a sequence position that has an index that equals the index, and the sequence position has a member that is the member.*/
context sequence
def: _'member has index in sequence'
     (member: thing, i: integer, s: sequence)
     : Boolean =
     self._'sequence position'->exists(sp | 
       sp.index = index and sp.member = member)

/* The sequence has a sequence position that has an index that equals the index, and the sequence position has a member that is the member.*/
context sequence
def: _'member with index in sequence'
            (index: integer, s sequence): thing =
     self._'sequence position'->select(sp | sp.index = index).member
)

/* The concept corresponds to each member of the sequence.*/
context sequence
def: _'sequence is of concept'(c: concept): Boolean =
     sequence._'sequence position'.member->forAll(m | 
                  'concept corresponds to instance'(c m))

/* Each sequence has at most one index origin member.*/
context sequence
inv: sizeOf(self._'index origin member') <= 1

/* Each sequence has at most one index origin value.*/
context sequence
inv: sizeOf(self._'index origin value') <= 1

/* The index of the index origin position equals the index origin value of the sequence.*/
context sequence
inv: sequence._'index origin value' = 
       sequence._'index origin position'.index

/* sequence that each sequence position of the sequence that is not the first position of the sequence is next after a sequence position2, and the index of the sequence position equals 1 plus the index of the sequence position2*/
context _'consecutive sequence'
inv: self._'sequence position'->forAll(sp |
      not (self._'first position'->exists()
        and sp = self._'first position')
        implies self._'sequence position'.indexOf(sp) =
          1 + self._'sequence position' 
              ->indexOf(sp._'previous sequence position'))

/* sequence that has no member that is the member of more than one sequence position of the sequence*/
context _'unique sequence'
inv: self.member->forall(m | 
        self._'sequence position'.member->isUnique (m2 |
           m = m2))

/* Each thing has at most one index in each unique sequence. */
context _'unique sequence'
inv: self.member->forAll(m1 | 
       self._'sequence position'.member->select (m2 |
           m1 = m2) .index->size()=1

/* member1 participates in the unique sequence and member2 participates in the unique sequence and each sequence position1 of member1 in the unique sequence precedes each sequence position2 of member2 in the unique sequence*/
context sequence
def: _'member1 precedes member2 in unique sequence'
     (m1: thing, m2: thing) : Boolean =
    self.member->includes(m1)
      and self.member->includes(m2)
      and m1._'sequence position'->forall(sp1 |
           m2._'sequence position'->forall(sp2 |
            'sequence position1 precedes 
               sequence position2'(sp1, sp2)))

/* the first member is the member of the first position of the sequence*/
context _'sequence'
def: _'sequence has first member'
      (s: _'sequence') : thing = self._'first position'.member

/* the last member is the member of the last position of the sequence*/
context _'sequence'
def: _'sequence has last member
      (s: sequence) : thing = self._'last position'.member

/* thing is the member of exactly one sequence position in the unique sequence and next member is the member of some sequence position of the unique sequence that succeeds the sequence position of the thing*/
context 'unique sequence'
def: 'next member is next after thing in unique sequence'
      (nm: thing, m: thing) : Boolean =
      self._'sequence position'.member->count(m) = 1
      and self._'sequence position'->select(member = m).
         _'next sequence position' = nm

/* The last member of each sequence has no next member.*/
context sequence
inv: self._'last member'->exists() implies
     not self._'last member'._'next member'->exists()

/* Each member that participates in a unique sequence and that has no next member in the unique sequence is the last member of the unique sequence.*/
context _'unique sequence'
inv: self.member->forAll(m |
       not m._'next member'->exists()
           implies m = self._'last member')

/* thing is the member of exactly one sequence position in the unique sequence and previous member is the member of some sequence position of the unique sequence that is just before the sequence position of the thing*/
context _'unique sequence'
def: _'previous member is just before member in unique 
      sequence'(pm: thing, m: thing) : Boolean =
      self._'sequence position'.member->count(m) = 1
      and self._'sequence position'->select(member = m).
        'previous sequence position'.member = pm

/* The first member of each sequence has no previous member.*/
context sequence
inv: self._'first member'->exists() implies
     not self._'first member'._'previous member'->exists()

/* Each member that participates in a unique sequence and that has no previous member in the unique sequence is the first member of the unique sequence.*/
context _'unique sequence'
inv: self.member->forAll(m |
       not m._'previous member'->exists()
           implies m = self._'first member')

/* -- Sets -- */

/* each element of the set is an instance of the concept*/
context set
def: _'set is of concept'(c: concept) : Boolean =
     set.element->forAll(e | 
       c._'concept corresponds to instance'(e))

/* set1 includes the thing and set1 includes each element of set2, and each element of set1 is the thing or an element of set2*/
context set 
def: _'set1 is set2 plus thing'(s2: set, t: thing) : Boolean =
       self.includes(t) and s2->forAll(t2: self.includes(t2))
       and self.element->forAll(e: e = t or s2.includes(e))

/* set1 includes the thing and set1 includes each element of set2, and each element of set1 is the thing or an element of set2*/
context set
def: _'plus thing'(t: thing) : set =
  self.element->union(t)

/* -- Quantities -- */

/* Each quantity has exactly one quantity kind.*/
context quantity
inv: _'quantity kind'->allInstances(one qk | 
    self._'quantity kind' = qk)

/* Each system of units is for exactly one system of quantities.*/
context _'system of units'
  self._'system of quantities'->size() = 1

/* -- Mereology -- */

/* Each part is part of the part.*/
context thing
inv: self.part->exists(self)

/* If the part is part of the whole and the whole is part of the part then the part is the whole.*/
context thing
inv: self.whole->exists(p | 
                  p.whole->exists(self))
     implies self = self.whole

/* If the part is part of some whole and the whole is part of some part3 then the part is part of part3.*/
context thing
inv: self.whole->exists(whole |
      whole.whole->exists(part3 |
       part3 implies self._'part of'(part3)))

/* there exists a thing that is part of thing1 and that is part of thing2*/
context thing
   def: self.overlaps(thing2:thing) : Boolean =
      self.part->exists(thing3 | thing2.part->exists(thing3) )

/* If a thing1 overlaps a thing2, then thing2 overlaps thing1.*/
context thing
inv: self.overlaps(thing2) eqv thing2.overlaps(self)

/* the part is part of the whole and the whole is not part of the part*/
context thing
inv: self._'proper part'->forall(pp | 
      pp <> self)

/* If a part1 is a proper part of a whole then there exists a part2 that is a proper part of the whole and part2 does not overlap part1.*/
context thing
inv: self._'proper part'->forAll(part1 |
      self._'proper part'->exists(part2 |
        not part2.overlaps(part1)))