Bug in [cop-1] and [nui-1]

[alanruttenberg]

Would allow a model

p1    i1      p2
|-------------|
        |
        p3

if p1 and p2 (first and last instant) were not part of i1.

Fixed by allowing possibility that t1 is start and t2 is end.

(forall (i start end)
 (if
  (and (instance-of i temporal-interval i)
   (has-first-instant i start) (has-last-instant i end))
  (forall (t1 t2)
   (if
    (and (or (temporal-part-of t1 i) (= t1 start))  <-----
     (or (temporal-part-of t2 i) (= t2 end))   <-----
     (instance-of t1 temporal-instant t1)
     (instance-of t2 temporal-instant t2) (precedes t1 t2)
     (not
      (exists (t3)
       (and (instance-of t3 temporal-instant t3) (precedes t1 t3)
        (precedes t3 t2)))))
    (exists (fill)
     (and (instance-of fill temporal-interval fill)
      (has-first-instant fill t1) (has-last-instant fill t2)
      (temporal-part-of fill i)))))))

[alanruttenberg]

Actually another edge case in [nui-1]

p1    i1      p2
|-------------|
|--------|
    i2        p3

i2 wasn't being inferred to be part of i1 unless p1 was part of i1. I was confused about the case where p1 was part of i2 and p1 wasn't part of i1 but that shouldn't be a model. If I cared about the endpoints being parts it was wrong anyways, if p1 wasn't part of i2.

Revised:

(forall (i start end)
 (if
  (and (instance-of i temporal-interval i)
   (has-first-instant i start) (has-last-instant i end))
  (not
   (exists (gap gap-start gap-end)
    (and (not (instance-of gap temporal-instant gap))
     (has-first-instant gap gap-start) (has-last-instant gap gap-end)
     (or (precedes gap-end end) (= gap-end end))
     (or (precedes start gap-start) (= gap-start start))
     (not (temporal-part-of gap i)))))))

[alanruttenberg]

Not sure about nui-1 now. Have to account for the fact that there can be several intervals with the same first and last instant, depending on which of the first and last instant are part of the interval.