DTV12 — incorrect CLIF definition of time interval plus time interval

In clause 8.2.5, the verb concept 'time interval1 plus time interval2 is time interval3'

has 4 CLIF Definitions. Actually, each of these is an Axiom and together they make up a definition of sorts.

Further , each of them uses 'iff' incorrectly. The first has the form:

(forall (t1 t2 t3)

(if

(or

("time interval1 is before time interval2" t1 t2)

("time interval1 properly overlaps time interval2" t1 t2))

(iff

("time interval1 plus time interval2 is time interval3" t1 t2 t3)

(and

("time interval1 starts time interval2" t1 t3)

("time interval1 finishes time interval2" t2 t3))

)))

It should be:

(forall (t1 t2 t3)

(if

(and

("time interval1 plus time interval2 is time interval3" t1 t2 t3)

(or

("time interval1 is before time interval2" t1 t2)

("time interval1 properly overlaps time interval2" t1 t2)))

(and

("time interval1 starts time interval2" t1 t3)

("time interval1 finishes time interval2" t2 t3))

))

and similarly for the others.

The suggested text is no improvement; the Definition remains fragmented, and it loses the conditional equivalences. The OCL Definition is a definition. The others aren’t. As the issue says, the 4 “CLIF Definitions” are axioms. They should be identified as such.