Issue 16992: Corollaries to Axiom D.4 in 8.2.3 are misstated (date-time-ftf) Source: NIST (Mr. Edward J. Barkmeyer, edbark(at)nist.gov) Nature: Uncategorized Issue Severity: Summary: In clause 8.2.3 (p.54), the first corollary to axiom D.4 is stated in mathematical English: If t1 and t2 are time intervals such that t1 starts t2, then D(t1 starts t2 complementing t3) = D(t2) ­ D(t1). But "t1 starts t2 complementing t3" is a proposition, which does not have a duration. The intent is: If t1, t2 and t3 are time intervals such that t1 starts t2 complementing t3, then D(t3) = D(t2) ­ D(t1). There is a further requirement, namely that time interval t2 is "finite" (which does not seem to be a concept in clause 8). 'Time interval has particular duration' cannot always be satisfied. So it appears that the term 'finite time interval' must be defined: A time interval that has a duration. The CLIF formulation of this corollary is also incorrect. It should read: (forall ((t1 "time interval") (t2 "time interval") (t3 "time interval")) (if (and (exists ((d duration)) ("time interval has duration" t2 d) ("time interval1 starts time interval2 complementing time interval3" t1 t2 t3)) (= ("duration of" t3) (- ("duration of" t2) ("duration of" t1))) )) If the concept 'finite time interval' is added, then this can be simplified: (forall ((t1 "finite time interval") (t2 "finite time interval") (t3 "finite time interval")) (if ("time interval1 starts time interval2 complementing time interval3" t1 t2 t3) (= ("duration of" t3) (- ("duration of" t2) ("duration of" t1))) )) The second Corollary has the same problem. It reads: If t1 and t2 are time intervals such that t1 finishes t2, then D(t1 finishes t2 complementing t3) = D(t2) ­ D(t1). It should read: If t1, t2 and t3 are time intervals such that t1 finishes t2 complementing t3, then D(t3) = D(t2) ­ D(t1). The CLIF formulation of the second corollary is also incorrect. It should read: (forall ((t1 "finite time interval") (t2 "finite time interval") (t3 "finite time interval")) (if ("time interval1 finishes time interval2 complementing time interval3" t1 t2 t3) (= ("duration of" t3) (- ("duration of" t2) ("duration of" t1))) )) In both cases, the existence of time interval t3 is the subject of a different axiom. So it suffices to say, for any three time intervals that are related in a certain way, their durations are related in a certain way. The remaining issue is that Clause 8.2 does not define the CLIF function for the SBVR attributive construct 'duration of'. Axiom D.2 suddenly introduces the notation "duration of" as a function. The intent is that the fact type 'time interval has duration' introduces both a CLIF predicate "time interval has duration" AND a CLIF function, which can be defined axiomatically as: (forall ((t "finite time interval") (d duration)) (iff ("time interval has duration" t d) (= ("duration of" t) d) )) This declaration should be added to the entry for the fact type that introduces the "attributive role" 'duration'. Note also that construction of a CLIF function from an SBVR attributive role pattern only behaves as expected when the role is played by a unique thing for each possible value of the function argument. If it is possible that the role is empty or multivalued for a valid argument, the CLIF function would have to be described as returning a set. So this construct does not follow some general pattern. It must be appropriately declared in each case. In this case, the supporting axiom: Necessity: Each time interval has at most one particular duration. should be stated, and then the above function axiom completes the model. Resolution: Revised Text: Actions taken: January 11, 2012: received issue Discussion: End of Annotations:===== te: Wed, 11 Jan 2012 14:22:21 -0500 From: Ed Barkmeyer Reply-To: edbark@nist.gov Organization: NIST User-Agent: Thunderbird 2.0.0.23 (Windows/20090812) To: issues@omg.org Subject: DTV Issue: Corollaries to Axiom D.4 in 8.2.3 are misstated X-NISTMEL-MailScanner-Information: Please contact postmaster@mel.nist.gov for more information X-NISTMEL-MailScanner-ID: q0BJMRl7003261 X-NISTMEL-MailScanner: Found to be clean X-NISTMEL-MailScanner-SpamCheck: X-NISTMEL-MailScanner-From: edbark@nist.gov X-NISTMEL-MailScanner-Watermark: 1326914547.62214@E6oYqx+l9cCQgvmtXU9rXw X-Spam-Status: No X-NIST-MailScanner: Found to be clean X-NIST-MailScanner-From: edbark@nist.gov Specification: Date Time Vocabulary Version: beta-1 Title: Corollaries to Axiom D.4 in 8.2.3 are misstated Source: Ed Barkmeyer, NIST, edbark@nist.gov' Summary: In clause 8.2.3 (p.54), the first corollary to axiom D.4 is stated in mathematical English: If t1 and t2 are time intervals such that t1 starts t2, then D(t1 starts t2 complementing t3) = D(t2) ­ D(t1). But "t1 starts t2 complementing t3" is a proposition, which does not have a duration. The intent is: If t1, t2 and t3 are time intervals such that t1 starts t2 complementing t3, then D(t3) = D(t2) ­ D(t1). There is a further requirement, namely that time interval t2 is "finite" (which does not seem to be a concept in clause 8). 'Time interval has particular duration' cannot always be satisfied. So it appears that the term 'finite time interval' must be defined: A time interval that has a duration. The CLIF formulation of this corollary is also incorrect. It should read: (forall ((t1 "time interval") (t2 "time interval") (t3 "time interval")) (if (and (exists ((d duration)) ("time interval has duration" t2 d) ("time interval1 starts time interval2 complementing time interval3" t1 t2 t3)) (= ("duration of" t3) (- ("duration of" t2) ("duration of" t1))) )) If the concept 'finite time interval' is added, then this can be simplified: (forall ((t1 "finite time interval") (t2 "finite time interval") (t3 "finite time interval")) (if ("time interval1 starts time interval2 complementing time interval3" t1 t2 t3) (= ("duration of" t3) (- ("duration of" t2) ("duration of" t1))) )) The second Corollary has the same problem. It reads: If t1 and t2 are time intervals such that t1 finishes t2, then D(t1 finishes t2 complementing t3) = D(t2) ­ D(t1). It should read: If t1, t2 and t3 are time intervals such that t1 finishes t2 complementing t3, then D(t3) = D(t2) ­ D(t1). The CLIF formulation of the second corollary is also incorrect. It should read: (forall ((t1 "finite time interval") (t2 "finite time interval") (t3 "finite time interval")) (if ("time interval1 finishes time interval2 complementing time interval3" t1 t2 t3) (= ("duration of" t3) (- ("duration of" t2) ("duration of" t1))) )) In both cases, the existence of time interval t3 is the subject of a different axiom. So it suffices to say, for any three time intervals that are related in a certain way, their durations are related in a certain way. The remaining issue is that Clause 8.2 does not define the CLIF function for the SBVR attributive construct 'duration of'. Axiom D.2 suddenly introduces the notation "duration of" as a function. The intent is that the fact type 'time interval has duration' introduces both a CLIF predicate "time interval has duration" AND a CLIF function, which can be defined axiomatically as: (forall ((t "finite time interval") (d duration)) (iff ("time interval has duration" t d) (= ("duration of" t) d) )) This declaration should be added to the entry for the fact type that introduces the "attributive role" 'duration'. Note also that construction of a CLIF function from an SBVR attributive role pattern only behaves as expected when the role is played by a unique thing for each possible value of the function argument. If it is possible that the role is empty or multivalued for a valid argument, the CLIF function would have to be described as returning a set. So this construct does not follow some general pattern. It must be appropriately declared in each case. In this case, the supporting axiom: Necessity: Each time interval has at most one particular duration. should be stated, and then the above function axiom completes the model. -- Edward J. Barkmeyer Email: edbark@nist.gov National Institute of Standards & Technology Manufacturing Systems Integration Division 100 Bureau Drive, Stop 8263 Tel: +1 301-975-3528 Gaithersburg, MD 20899-8263 Cel: +1 240-672-5800 Date: Tue, 13 Mar 2012 17:58:28 -0400 From: Ed Barkmeyer Reply-To: edbark@nist.gov Organization: NIST User-Agent: Thunderbird 2.0.0.23 (Windows/20090812) To: OMG DateTimeVoc FTF Subject: DTV Issue 16992 - correct axiom D.4 X-NISTMEL-MailScanner-Information: Please contact postmaster@mel.nist.gov for more information X-NISTMEL-MailScanner-ID: q2DLwWEK003622 X-NISTMEL-MailScanner: Found to be clean X-NISTMEL-MailScanner-SpamCheck: X-NISTMEL-MailScanner-From: edbark@nist.gov X-NISTMEL-MailScanner-Watermark: 1332280716.79109@0rJJTlzWBUasWKsliVOMSg X-Spam-Status: No X-NIST-MailScanner: Found to be clean X-NIST-MailScanner-From: edbark@nist.gov Actually the issue identifies a number of problems in 8.2.3. It is just that Axiom D.4 highlights most of them. I attach a first draft of the resolution. It needs help from an OCL expert. -Ed -- Edward J. Barkmeyer Email: edbark@nist.gov National Institute of Standards & Technology Manufacturing Systems Integration Division 100 Bureau Drive, Stop 8263 Tel: +1 301-975-3528 Gaithersburg, MD 20899-8263 Cel: +1 240-672-5800 Issue 16992- Axiom D4-d1.doc To: date-time-ftf@omg.org Subject: Re: DTV Issue 16992 - correct axiom D.4 X-KeepSent: 638B1CC7:D7853D1D-852579CC:005FE62E; type=4; name=$KeepSent X-Mailer: Lotus Notes Release 8.5.1FP5 SHF29 November 12, 2010 From: Mark H Linehan Date: Sun, 25 Mar 2012 13:36:43 -0400 X-MIMETrack: Serialize by Router on D01MC604/01/M/IBM(Release 8.5.3 ZX853HP5|January 12, 2012) at 03/25/2012 13:36:44 X-Content-Scanned: Fidelis XPS MAILER x-cbid: 12032517-4242-0000-0000-00000125A588 I added many comments to this proposed resolution. Most importantly, I disagree that we need to define the "finite time interval" concept. There are many time intervals that are "indefinite", meaning that their beginning or end (and hence duration) are unknown. But the axioms and corollaries in 8.2.3 are valid with respect to such time intervals. For business purposes, every state of affairs both begins and ends sooner or later. As a concrete example, my life occurs for some time interval. None of us know when that time interval ends, but it definitely will end at some point. So the various axioms and corollaries in 8.2.3 do apply to the duration of my life, even though we do not presently know that duration. "Infinite time intervals" arise in physics, philosophy, and religion, for example when discussing when the universe begins or ends. But those matters are not relevant to business and need not be addressed in our Vocabulary. -------------------------------- Mark H. Linehan STSM, Model Driven Business Transformation IBM Research From: Ed Barkmeyer To: OMG DateTimeVoc FTF Date: 03/13/2012 06:01 PM Subject: DTV Issue 16992 - correct axiom D.4 -------------------------------------------------------------------------------- Actually the issue identifies a number of problems in 8.2.3. It is just that Axiom D.4 highlights most of them. I attach a first draft of the resolution. It needs help from an OCL expert. -Ed -- Edward J. Barkmeyer Email: edbark@nist.gov National Institute of Standards & Technology Manufacturing Systems Integration Division 100 Bureau Drive, Stop 8263 Tel: +1 301-975-3528 Gaithersburg, MD 20899-8263 Cel: +1 240-672-5800 [attachment "Issue 16992- Axiom D4-d1.doc" deleted by Mark H Linehan/Watson/IBM] Issue 16992- Axiom D4-d1 MHL.doc Disposition: Resolved OMG Issue No: 16992 Title: Corollaries to Axiom D.4 in 8.2.3 are misstated Source: Ed Barkmeyer, NIST, edbark@nist.gov Summary: In clause 8.2.3 (p.54), the first corollary to axiom D.4 is stated in mathematical English: If t1 and t2 are time intervals such that t1 starts t2, then D(t1 starts t2 complementing t3) = D(t2) . D(t1). But "t1 starts t2 complementing t3" is a proposition, which does not have a duration. The intent is: If t1, t2 and t3 are time intervals such that t1 starts t2 complementing t3, then D(t3) = D(t2) . D(t1). There is a further requirement, namely that time interval t2 is "finite" (which does not seem to be a concept in clause 8). 'Time interval has particular duration' cannot always be satisfied. So it appears that the term 'finite time interval' must be defined: A time interval that has a duration. The CLIF formulation of this corollary is also incorrect. It should read: (forall ((t1 "time interval") (t2 "time interval") (t3 "time interval")) (if (and (exists ((d duration)) ("time interval has duration" t2 d) ("time interval1 starts time interval2 complementing time interval3" t1 t2 t3)) (= ("duration of" t3) (- ("duration of" t2) ("duration of" t1))) )) If the concept 'finite time interval' is added, then this can be simplified: (forall ((t1 "finite time interval") (t2 "finite time interval") (t3 "finite time interval")) (if ("time interval1 starts time interval2 complementing time interval3" t1 t2 t3) (= ("duration of" t3) (- ("duration of" t2) ("duration of" t1))) )) The second Corollary has the same problem. It reads: If t1 and t2 are time intervals such that t1 finishes t2, then D(t1 finishes t2 complementing t3) = D(t2) . D(t1). It should read: If t1, t2 and t3 are time intervals such that t1 finishes t2 complementing t3, then D(t3) = D(t2) . D(t1). The CLIF formulation of the second corollary is also incorrect. It should read: (forall ((t1 "finite time interval") (t2 "finite time interval") (t3 "finite time interval")) (if ("time interval1 finishes time interval2 complementing time interval3" t1 t2 t3) (= ("duration of" t3) (- ("duration of" t2) ("duration of" t1))) )) In both cases, the existence of time interval t3 is the subject of a different axiom. So it suffices to say, for any three time intervals that are related in a certain way, their durations are related in a certain way. The remaining issue is that Clause 8.2 does not define the CLIF function for the SBVR attributive construct 'duration of'. Axiom D.2 suddenly introduces the notation "duration of" as a function. The intent is that the fact type 'time interval has duration' introduces both a CLIF predicate "time interval has duration" AND a CLIF function, which can be defined axiomatically as: (forall ((t "finite time interval") (d duration)) (iff ("time interval has duration" t d) (= ("duration of" t) d) )) This declaration should be added to the entry for the fact type that introduces the "attributive role" 'duration'. Note also that construction of a CLIF function from an SBVR attributive role pattern only behaves as expected when the role is played by a unique thing for each possible value of the function argument. If it is possible that the role is empty or multivalued for a valid argument, the CLIF function would have to be described as returning a set. So this construct does not follow some general pattern. It must be appropriately declared in each case. In this case, the supporting axiom: Necessity: Each time interval has at most one particular duration. should be stated, and then the above function axiom completes the model. Resolution: As recommended, except that the CLIF formulations are revised per Issue 17225. Define the CLIF function "duration of". Define 'finite time interval' and correct the definition of 'particular duration' and the related axioms. Revised Text: 1. In clause 8.2.3, paragraph 2, REPLACE the first sentence: Each time interval has a unique duration attribute that is a measure of its size, i.e., the amount of time the time interval occupies. with: A time interval that has a beginning and an end is a finite time interval. Each finite time interval has a unique particular duration attribute that is a measure of the amount of time in the time interval. 2. In clause 8.2.3, in the entry for 'particular duration', DELETE the two Definitions and the Reference Scheme: Definition: particular quantity of quantity kind 'duration' Definition: duration of some time interval Reference Scheme: a duration value that quantifies the particular duration and INSERT: Definition: the amount of time in a given time interval 3. In Clause 8.2.3, in the entry for 'time interval has particular duration', before the Example, INSERT: Definition: the particular duration is the duration that is the amount of time in the time interval Note: This is a primitive concept. CLIF Definition: (forall (t d) (iff (= d ("duration of time interval" t)) (and ("time interval" t) (duration d) ("time interval has duration" t d) ))) 4. In Clause 8.2.3, before Axiom D.1, INSERT a new entry: finite time interval Definition: time interval that has a particular duration CLIF Definition: (forall (t) (iff ("finite time interval" t) (exists ((d duration)) ("time interval has duration" t d)) )) OCL Definition: ??? Note: The only time intervals that do not have a particular duration extend indefinitely into the past or indefinitely into the future . 5. In Clause 8.2.3, in the entry for Axiom D.1, CHANGE "exactly one" TO "at most one" in the Axiom title, and in the Necessity that follows. 6. In Clause 8.2.3, at the end of the entry for Axiom D.1, INSERT: Corollary: Each finite time interval has exactly one particular duration . 7. In 8.2.3, in the entry for Axiom D.2, CHANGE all four occurrences of "time interval " TO "finite time interval" in the Axiom title and in three paragraphs that follow. 8. In 8.2.3, in the Corollary following Axiom D.2 that begins " No time interval has a duration that is the additive inverse .", REPLACE all of the following: Necessity: D0 does not equal D0 minus the duration of a time interval. CLIF Axiom: (forall ((t "time interval")) (not (= D0 (- (D0 t))))) OCL Constraint: context "time interval" inv: not D0 = (D0 . self.duration) with: Necessity: For each time interval1 there is no time interval2 such that the duration of time interval1 plus the duration of time interval2 equals D0 . CLIF Axiom: (not (exists t1 t2 ) ("duration3 = duration1 plus duration2" D0 ("duration of time interval" t1) ("duration of time interval" t2)) )) OCL Constraint: ?? OCL Constraint: context "time interval" inv: "time interval".allInstances-->forAll(t2 | not ((self.duration() + t2.duration()) = D0)) 9. In 8.2.3, in the entry for Axiom D.4, REPLACE the two paragraphs: Necessity: If a time interval1 meets a time interval2, then the duration3 of time interval1 plus time interval2 is equal to the duration1 of time interval1 plus the duration2 of time interval2. CLIF Axiom: (forall ((t1 "time interval") (t2 "time interval")) with: Necessity: If a finite time interval 1 meets a finite time interval2, then the duration of finite time interval1 + finite time interval2 is equal to the duration of finite time interval1 plus the duration of finite time interval2. CLIF Axiom: (forall ((t1 "finite time interval") (t2 "finite time interval")) 10. In 8.2.3, after Axiom D.4, REPLACE both Corollaries and all of their subordinate paragraphs: Corollary: If t1 and t2 are time intervals such that t1 starts t2, then D(t1 starts t2 complementing t3) = D(t2) . D(t1). Necessity: If a time interval1 starts a time interval2 complementing a time interval3, then the duration3 of time interval3 is equal to the duration2 of time interval2 minus the duration1 of time interval1. CLIF Axiom: (forall ((t1 "time interval") (t2 "time interval")) (exists ((t3 "time interval")) (if ("time interval1 starts time interval2 complementing time interval3" t1 t2 t3) (= ("duration of" t3) (- ("duration of" t2) ("duration of" t1)))))) OCL Constraint: context "time interval" inv: self.starts-->forAll(t2 | self."time interval1 starts time interval2 complementing time interval3"(t2).duration = (t2.duration)- t1.duration Corollary: If t1 and t2 are time intervals such that t1 finishes t2, then D(t1 finishes t2 complementing t3) = D(t2) . D(t1). Necessity: If a time interval1 finishes a time interval2 complementing a time interval3, then the duration3 of time interval3 is equal to the duration2 of time interval2 minus the duration1 of time interval1. CLIF Axiom: (forall ((t1 "time interval") (t2 "time interval")) (exists ((t3 "time interval")) (if ("time interval1 finishes time interval2 complementing time interval3" t1 t2 t3) (= ("duration of" t3) (- ("duration of" t2) ("duration of" t1)))))) OCL Constraint: context "time interval" inv: self.finishes-->forAll(t2 | self."time interval1 finishes time interval2 complementing time interval3"(t2).duration = (t2.duration)- t1.duration with the following: Corollary: If t1, t2, and t3 are finite time intervals such that t1 starts t2 complementing t3, then D(t3) = D(t2) . D(t1). Necessity: If a finite time interval1 starts a finite time interval2 complementing a finite time interval3, then the duration of finite time interval3 is equal to the duration of finite time interval2 minus the duration of finite time interval1. CLIF Axiom: (forall ((t1 "finite time interval") (t2 "finite time interval") (t3 "finite time interval")) (if ("time interval1 starts time interval2 complementing time interval3" t1 t2 t3) (= ("duration of" t3) (- ("duration of" t2) ("duration of" t1)) ) )) OCL Constraint: context "finite time interval" Corollary: If t1, t2, and t3 are finite time intervals such that t1 finishes t2 complementing t3, then D(t3) = D(t2) . D(t1). Necessity: If a finite time interval1 finishes a finite time interval2 complementing a finite time interval3, then the duration of finite time interval3 is equal to the duration of finite time interval2 minus the duration of finite time interval1. CLIF Axiom: (forall ((t1 "finite time interval") (t2 "finite time interval") (t3 "finite time interval")) (if ("time interval1 finishes time interval2 complementing time interval3" t1 t2 t3) (= ("duration of" t3) (- ("duration of" t2) ("duration of" t1)) ) )) OCL Constraint: context "finite time interval" Disposition: Resolved Date: Mon, 26 Mar 2012 14:16:43 -0400 From: Ed Barkmeyer Reply-To: edbark@nist.gov Organization: NIST User-Agent: Thunderbird 2.0.0.23 (Windows/20090812) To: Mark H Linehan CC: "date-time-ftf@omg.org" Subject: Re: DTV Issue 16992 - correct axiom D.4 X-NISTMEL-MailScanner-Information: Please contact postmaster@mel.nist.gov for more information X-NISTMEL-MailScanner-ID: q2QIGmaw015703 X-NISTMEL-MailScanner: Found to be clean X-NISTMEL-MailScanner-SpamCheck: X-NISTMEL-MailScanner-From: edbark@nist.gov X-NISTMEL-MailScanner-Watermark: 1333390610.58117@LOXPY5vZBtVSmIs5xGcewQ X-Spam-Status: No X-NIST-MailScanner: Found to be clean X-NIST-MailScanner-From: edbark@nist.gov At today's conference call, we agreed that 'indefinite time intervals' have a duration; we just don't know what it is. Actually, the situation is much worse than that. An 'indefinite time interval' is like an 'indefinite person' -- we don't know which time interval/person it is. If we only know when it starts, that is like knowing the person is male. There are infinitely many time intervals that start with any given interval. No interval is ever clearly during an indefinite time interval, nor does any interval properly overlap it. An indefinite time interval beginning 25 March 2012 may or may not include April 1, 2012. What we mean is that there are some past and future times that are our horizons, and every indefinite interval extends to at least the horizon. It does not necessarily extend beyond that, but we don't care. That at least tells us that a rule that is effective "from 25.3.2012 on" is effective on 1.4.2012. Whereas, a rule that is effective in a truly indefinite time interval beginning 25.3.2012 might only be effective until 26.3.2012. Indefinite intervals that extend to the horizon, however, can be treated as finite. They do have a duration, and we may be able to approximate it. -Ed Mark H Linehan wrote: I added many comments to this proposed resolution. Most importantly, I disagree that we need to define the "finite time interval" concept. There are many time intervals that are "indefinite", meaning that their beginning or end (and hence duration) are unknown. But the axioms and corollaries in 8.2.3 are valid with respect to such time intervals. For business purposes, every state of affairs both begins and ends sooner or later. As a concrete example, my life occurs for some time interval. None of us know when that time interval ends, but it definitely will end at some point. So the various axioms and corollaries in 8.2.3 do apply to the duration of my life, even though we do not presently know that duration. "Infinite time intervals" arise in physics, philosophy, and religion, for example when discussing when the universe begins or ends. But those matters are not relevant to business and need not be addressed in our Vocabulary. -------------------------------- Mark H. Linehan STSM, Model Driven Business Transformation IBM Research From: Ed Barkmeyer To: OMG DateTimeVoc FTF Date: 03/13/2012 06:01 PM Subject: DTV Issue 16992 - correct axiom D.4 ------------------------------------------------------------------------ Actually the issue identifies a number of problems in 8.2.3. It is just that Axiom D.4 highlights most of them. I attach a first draft of the resolution. It needs help from an OCL expert. -Ed -- Edward J. Barkmeyer Email: edbark@nist.gov National Institute of Standards & Technology Manufacturing Systems Integration Division 100 Bureau Drive, Stop 8263 Tel: +1 301-975-3528 Gaithersburg, MD 20899-8263 Cel: +1 240-672-5800 [attachment "Issue 16992- Axiom D4-d1.doc" deleted by Mark H Linehan/Watson/IBM] -- Edward J. Barkmeyer Email: edbark@nist.gov National Institute of Standards & Technology Manufacturing Systems Integration Division 100 Bureau Drive, Stop 8263 Tel: +1 301-975-3528 Gaithersburg, MD 20899-8263 Cel: +1 240-672-5800 "The opinions expressed above do not reflect consensus of NIST, and have not been reviewed by any Government authority." From: Mike Bennett To: "edbark@nist.gov" CC: "date-time-ftf@omg.org" Subject: RE: DTV Issue 16992 - correct axiom D.4 Thread-Topic: DTV Issue 16992 - correct axiom D.4 Thread-Index: AQHNAWSR+9hH3/xnU02r0KEqfI2kxJZ7zj+AgAGdgoD//4smoA== Date: Mon, 26 Mar 2012 18:20:55 +0000 Accept-Language: en-US X-MS-Has-Attach: X-MS-TNEF-Correlator: x-originating-ip: [86.135.194.164] X-MIME-Autoconverted: from quoted-printable to 8bit by amethyst.omg.org id q2QIL2Qw014989 Presumably there is also a distinction to be made between models made under an open world assumption, and those under a closed world assumption. I don't know but I'm guessing that the UML models will assume CWA, while the OWL models will of course be framed under the OWA. Which does SBVR follow? I assume OWA since it's a semantic model notation? Mike -- Mike Bennett Head of Semantics and Standards EDM Council Tel: +44 20 7917 9522 Cell: +44 7721 420 730 www.edmcouncil.org Semantics Repository: www.hypercube.co.uk/edmcouncil -----Original Message----- From: Ed Barkmeyer [mailto:edbark@nist.gov] Sent: Monday, March 26, 2012 2:17 PM To: Mark H Linehan Cc: date-time-ftf@omg.org Subject: Re: DTV Issue 16992 - correct axiom D.4 At today's conference call, we agreed that 'indefinite time intervals' have a duration; we just don't know what it is. Actually, the situation is much worse than that. An 'indefinite time interval' is like an 'indefinite person' -- we don't know which time interval/person it is. If we only know when it starts, that is like knowing the person is male. There are infinitely many time intervals that start with any given interval. No interval is ever clearly during an indefinite time interval, nor does any interval properly overlap it. An indefinite time interval beginning 25 March 2012 may or may not include April 1, 2012. What we mean is that there are some past and future times that are our horizons, and every indefinite interval extends to at least the horizon. It does not necessarily extend beyond that, but we don't care. That at least tells us that a rule that is effective "from 25.3.2012 on" is effective on 1.4.2012. Whereas, a rule that is effective in a truly indefinite time interval beginning 25.3.2012 might only be effective until 26.3.2012. Indefinite intervals that extend to the horizon, however, can be treated as finite. They do have a duration, and we may be able to approximate it. -Ed Mark H Linehan wrote: > I added many comments to this proposed resolution. > > Most importantly, I disagree that we need to define the "finite time > interval" concept. There are many time intervals that are > "indefinite", meaning that their beginning or end (and hence duration) > are unknown. But the axioms and corollaries in 8.2.3 are valid with > respect to such time intervals. For business purposes, every state of > affairs both begins and ends sooner or later. > > As a concrete example, my life occurs for some time interval. None of > us know when that time interval ends, but it definitely will end at > some point. So the various axioms and corollaries in 8.2.3 do apply > to the duration of my life, even though we do not presently know that > duration. > > "Infinite time intervals" arise in physics, philosophy, and religion, > for example when discussing when the universe begins or ends. But > those matters are not relevant to business and need not be addressed > in our Vocabulary. > -------------------------------- > Mark H. Linehan > STSM, Model Driven Business Transformation > IBM Research > > > > From: Ed Barkmeyer > To: OMG DateTimeVoc FTF > Date: 03/13/2012 06:01 PM > Subject: DTV Issue 16992 - correct axiom D.4 > ------------------------------------------------------------------------ > > > > Actually the issue identifies a number of problems in 8.2.3. It is just > that Axiom D.4 highlights most of them. > > I attach a first draft of the resolution. It needs help from an OCL > expert. > > -Ed > > -- > Edward J. Barkmeyer Email: edbark@nist.gov > National Institute of Standards & Technology > Manufacturing Systems Integration Division > 100 Bureau Drive, Stop 8263 Tel: +1 301-975-3528 > Gaithersburg, MD 20899-8263 Cel: +1 240-672-5800 > > > [attachment "Issue 16992- Axiom D4-d1.doc" deleted by Mark H > Linehan/Watson/IBM] -- Edward J. Barkmeyer Email: edbark@nist.gov National Institute of Standards & Technology Manufacturing Systems Integration Division 100 Bureau Drive, Stop 8263 Tel: +1 301-975-3528 Gaithersburg, MD 20899-8263 Cel: +1 240-672-5800 "The opinions expressed above do not reflect consensus of NIST, and have not been reviewed by any Government authority." Date: Tue, 27 Mar 2012 11:40:56 -0400 From: Edward Barkmeyer Reply-To: edbark@nist.gov Organization: NIST User-Agent: Thunderbird 2.0.0.23 (Windows/20090812) To: Mike Bennett CC: "date-time-ftf@omg.org" Subject: Re: DTV Issue 16992 - correct axiom D.4 X-NIST-MailScanner: Found to be clean X-NIST-MailScanner-From: edward.barkmeyer@nist.gov Mike Bennett wrote: Presumably there is also a distinction to be made between models made under an open world assumption, and those under a closed world assumption. The problem for time intervals is that we don't have the concept of a starting instant and an ending instant. We just have the concept of an interval that starts with and finishes with other intervals. For every finite time interval, we know that there is a set of time intervals that it finishes with, but we may not know what any of them are. That is the OWA. But we still need a means of identifying the interval itself. It has to be the occurrence interval of some situation that we take to be terminating at some time, possibly in the distant future beyond our concern. I don't know but I'm guessing that the UML models will assume CWA, while the OWL models will of course be framed under the OWA. That is a different matter. OWL is explicitly OWA. But as to UML, there is a whole literature on "the types of nothing" in computational models. The semantics of "no stored value at this time" may be "has no value", or "has a value but we don't know what it is", or "we don't know whether it has a value". There was a famous debate between the database gurus Codd and Date on the subject of null values in rows, long about 1980. Ted Codd published a set of different classifications of "null", including those three and a few more. Date thought the whole idea of describing a column as "may be null" was bad practice -- potentially null columns should be mandatory columns in separate tables. ISO 11404, now called General-Purpose Datatypes, distinguishes Null, which is a value, interpreted as "no value", from "Undefined" which is a state of something that could or should have a value. The idea (per Codd and Ada) is that two null values are equal, and 3 is not equal to null, but if you compare 3 to undefined, or null to undefined, or undefined to undefined, the result is 'undefined'. I think UML is silent on the subject, but I'm not sure about fUML. Which does SBVR follow? I assume OWA since it's a semantic model notation? SBVR formally says that the default interpretation of a 'fact model' (or whatever they changed that term to) is Open World. But you can say in a conceptual schema that a given noun concept or verb concept is 'closed' in every corresponding fact model, that is, every instance of the concept that exists in the world described by a given fact model must explicitly appear in the fact model. There is also a way to say that an attributive role is relatively closed, that is, for every instance of the owning noun concept that explicitly appears in the fact model, every instance of the attributive relationship also explicitly appears. So if "estate has mortgage" is an attributive relationship to 'estate' and is relatively closed in the schema, and the fact model explicitly contains an estate "The Willows", then "The Willows" has exactly the mortgages that appear explicitly in the fact model and no others. One may still infer that there are estates not explicitly mentioned, and they may or may not have mortgages whose existence cannot be inferred. Of course, if 'estate' is also said to be closed, then there are no estates that are not explicitly mentioned, either. (This is all about using SBVR to model CWA databases, of course. A 'fact model' is an instantaneous population of the database. And 'reference scheme' is subtly overloaded to be somewhere between 'keys' and 'mandatory columns'. Standards regularly succumb to the diverse motivations of their participants.) -Ed Mike -- Edward J. Barkmeyer Email: edbark@nist.gov National Institute of Standards & Technology Manufacturing Systems Integration Division 100 Bureau Drive, Stop 8263 Tel: +1 301-975-3528 Gaithersburg, MD 20899-8263 Cel: +1 240-672-5800 Date: Mon, 4 Jun 2012 19:17:42 -0400 From: Edward Barkmeyer Reply-To: Organization: NIST User-Agent: Thunderbird 2.0.0.23 (Windows/20090812) To: Mark H Linehan , OMG DateTimeVoc FTF Subject: Re: Fw: DTV Issue 16992 - correct axiom D.4 Mark H Linehan wrote: I added many comments to this proposed resolution. Most importantly, I disagree that we need to define the "finite time interval" concept. There are many time intervals that are "indefinite", meaning that their beginning or end (and hence duration) are unknown. But the axioms and corollaries in 8.2.3 are valid with respect to such time intervals. For business purposes, every state of affairs both begins and ends sooner or later. As a concrete example, my life occurs for some time interval. None of us know when that time interval ends, but it definitely will end at some point. So the various axioms and corollaries in 8.2.3 do apply to the duration of my life, even though we do not presently know that duration. "Infinite time intervals" arise in physics, philosophy, and religion, for example when discussing when the universe begins or ends. But those matters are not relevant to business and need not be addressed in our Vocabulary. I have looked at these comments, and I agree that we don't need 'finite time interval'. All time intervals are finite. (I do think that means we should delete the 'forever' object, which is said to be a time interval. I am not sure how this relates to Issue 16993.) I marked up the draft with my comments following Mark's. If we remove the 'finite time interval' stuff, most of the remaining points of disagreement are confusion about 'particular duration'. 'time interval has particular duration' is a primitive concept -- it is the fundamental relationship between time intervals and durations. So it can only have an informal definition. 'particular duration' is an attributive role of 'duration', and we define 'duration of' and 'particular duration of' to be synonyms. Mark points out that a 'particular duration' is a 'particular quantity'. But as I read D.3.1, it means the concept 'particular duration' is an instance of the concept type 'particular quantity', and 'particular quantity' is itself a specialization of 'attributive role'. An instance of particular duration is a duration, not a particular quantity. 'particular quantity' in D.3.1 is weird -- there is no fact type 'thing has particular quantity' for 'time interval has particular duration' to specialize. We can formally define a CLIF "function" ("particular duration of" ti) in terms of the primitive verb concept, we can declare a UML operation on time interval that returns its particular duration. So, I will try to create another draft that eliminates the 'finite time interval' stuff and attempts to clarify the changes to 'particular duration'. -Ed -------------------------------- Mark H. Linehan STSM, Model Driven Business Transformation IBM Research From: Ed Barkmeyer To: OMG DateTimeVoc FTF Date: 03/13/2012 06:01 PM Subject: DTV Issue 16992 - correct axiom D.4 ------------------------------------------------------------------------ Actually the issue identifies a number of problems in 8.2.3. It is just that Axiom D.4 highlights most of them. I attach a first draft of the resolution. It needs help from an OCL expert. -Ed -- Edward J. Barkmeyer Email: edbark@nist.gov National Institute of Standards & Technology Manufacturing Systems Integration Division 100 Bureau Drive, Stop 8263 Tel: +1 301-975-3528 Gaithersburg, MD 20899-8263 Cel: +1 240-672-5800 [attachment "Issue 16992- Axiom D4-d1.doc" deleted by Mark H Linehan/Watson/IBM] -- Edward J. Barkmeyer Email: edbark@nist.gov National Institute of Standards & Technology Manufacturing Systems Integration Division 100 Bureau Drive, Stop 8263 Tel: +1 301-975-3528 Gaithersburg, MD 20899-8263 Cel: +1 240-672-5800 "The opinions expressed above do not reflect consensus of NIST, and have not been reviewed by any Government authority." Issue 16992- Axiom D4-d1 joint.doc Disposition: Resolved OMG Issue No: 16992 Title: Corollaries to Axiom D.4 in 8.2.3 are misstated Source: Ed Barkmeyer, NIST, edbark@nist.gov Summary: In clause 8.2.3 (p.54), the first corollary to axiom D.4 is stated in mathematical English: If t1 and t2 are time intervals such that t1 starts t2, then D(t1 starts t2 complementing t3) = D(t2) . D(t1). But "t1 starts t2 complementing t3" is a proposition, which does not have a duration. The intent is: If t1, t2 and t3 are time intervals such that t1 starts t2 complementing t3, then D(t3) = D(t2) . D(t1). There is a further requirement, namely that time interval t2 is "finite" (which does not seem to be a concept in clause 8). 'Time interval has particular duration' cannot always be satisfied. So it appears that the term 'finite time interval' must be defined: A time interval that has a duration. The CLIF formulation of this corollary is also incorrect. It should read: (forall ((t1 "time interval") (t2 "time interval") (t3 "time interval")) (if (and (exists ((d duration)) ("time interval has duration" t2 d) ("time interval1 starts time interval2 complementing time interval3" t1 t2 t3)) (= ("duration of" t3) (- ("duration of" t2) ("duration of" t1))) )) If the concept 'finite time interval' is added, then this can be simplified: (forall ((t1 "finite time interval") (t2 "finite time interval") (t3 "finite time interval")) (if ("time interval1 starts time interval2 complementing time interval3" t1 t2 t3) (= ("duration of" t3) (- ("duration of" t2) ("duration of" t1))) )) The second Corollary has the same problem. It reads: If t1 and t2 are time intervals such that t1 finishes t2, then D(t1 finishes t2 complementing t3) = D(t2) . D(t1). It should read: If t1, t2 and t3 are time intervals such that t1 finishes t2 complementing t3, then D(t3) = D(t2) . D(t1). The CLIF formulation of the second corollary is also incorrect. It should read: (forall ((t1 "finite time interval") (t2 "finite time interval") (t3 "finite time interval")) (if ("time interval1 finishes time interval2 complementing time interval3" t1 t2 t3) (= ("duration of" t3) (- ("duration of" t2) ("duration of" t1))) )) In both cases, the existence of time interval t3 is the subject of a different axiom. So it suffices to say, for any three time intervals that are related in a certain way, their durations are related in a certain way. The remaining issue is that Clause 8.2 does not define the CLIF function for the SBVR attributive construct 'duration of'. Axiom D.2 suddenly introduces the notation "duration of" as a function. The intent is that the fact type 'time interval has duration' introduces both a CLIF predicate "time interval has duration" AND a CLIF function, which can be defined axiomatically as: (forall ((t "finite time interval") (d duration)) (iff ("time interval has duration" t d) (= ("duration of" t) d) )) This declaration should be added to the entry for the fact type that introduces the "attributive role" 'duration'. Note also that construction of a CLIF function from an SBVR attributive role pattern only behaves as expected when the role is played by a unique thing for each possible value of the function argument. If it is possible that the role is empty or multivalued for a valid argument, the CLIF function would have to be described as returning a set. So this construct does not follow some general pattern. It must be appropriately declared in each case. In this case, the supporting axiom: Necessity: Each time interval has at most one particular duration. should be stated, and then the above function axiom completes the model. Resolution: As recommended, except that the CLIF formulations are revised per Issue 17225. Define the CLIF function "duration of". Define 'finite time interval' and correct the definition of 'particular duration' and the related axioms. Revised Text: 1. In clause 8.2.3, paragraph 2, REPLACE the first sentence: Each time interval has a unique duration attribute that is a measure of its size, i.e., the amount of time the time interval occupies. with: A time interval that has a beginning and an end is a finite time interval. Each finite time interval has a unique particular duration attribute that is a measure of the amount of time in the time interval. 2. In clause 8.2.3, in the entry for 'particular duration', DELETE the two Definitions and the Reference Scheme: Definition: particular quantity of quantity kind 'duration' Definition: duration of some time interval Reference Scheme: a duration value that quantifies the particular duration and INSERT: Definition: the amount of time in a given time interval 3. In Clause 8.2.3, in the entry for 'time interval has particular duration', before the Example, INSERT: Definition: the particular duration is the duration that is the amount of time in the time interval Note: This is a primitive concept. CLIF Definition: (forall (t d) (iff (= d ("duration of time interval" t)) (and ("time interval" t) (duration d) ("time interval has duration" t d) ))) 4. In Clause 8.2.3, before Axiom D.1, INSERT a new entry: finite time interval Definition: time interval that has a particular duration CLIF Definition: (forall (t) (iff ("finite time interval" t) (exists ((d duration)) ("time interval has duration" t d)) )) OCL Definition: ??? Note: The only time intervals that do not have a particular duration extend indefinitely into the past or indefinitely into the future . 5. In Clause 8.2.3, in the entry for Axiom D.1, CHANGE "exactly one" TO "at most one" in the Axiom title, and in the Necessity that follows. 6. In Clause 8.2.3, at the end of the entry for Axiom D.1, INSERT: Corollary: Each finite time interval has exactly one particular duration . 7. In 8.2.3, in the entry for Axiom D.2, CHANGE all four occurrences of "time interval " TO "finite time interval" in the Axiom title and in three paragraphs that follow. 8. In 8.2.3, in the Corollary following Axiom D.2 that begins " No time interval has a duration that is the additive inverse .", REPLACE all of the following: Necessity: D0 does not equal D0 minus the duration of a time interval. CLIF Axiom: (forall ((t "time interval")) (not (= D0 (- (D0 t))))) OCL Constraint: context "time interval" inv: not D0 = (D0 . self.duration) with: Necessity: For each time interval1 there is no time interval2 such that the duration of time interval1 plus the duration of time interval2 equals D0 . CLIF Axiom: (not (exists t1 t2 ) ("duration3 = duration1 plus duration2" D0 ("duration of time interval" t1) ("duration of time interval" t2)) )) OCL Constraint: ?? OCL Constraint: context "time interval" inv: "time interval".allInstances-->forAll(t2 | not ((self.duration() + t2.duration()) = D0)) 9. In 8.2.3, in the entry for Axiom D.4, REPLACE the two paragraphs: Necessity: If a time interval1 meets a time interval2, then the duration3 of time interval1 plus time interval2 is equal to the duration1 of time interval1 plus the duration2 of time interval2. CLIF Axiom: (forall ((t1 "time interval") (t2 "time interval")) with: Necessity: If a finite time interval 1 meets a finite time interval2, then the duration of finite time interval1 + finite time interval2 is equal to the duration of finite time interval1 plus the duration of finite time interval2. CLIF Axiom: (forall ((t1 "finite time interval") (t2 "finite time interval")) 10. In 8.2.3, after Axiom D.4, REPLACE both Corollaries and all of their subordinate paragraphs: Corollary: If t1 and t2 are time intervals such that t1 starts t2, then D(t1 starts t2 complementing t3) = D(t2) . D(t1). Necessity: If a time interval1 starts a time interval2 complementing a time interval3, then the duration3 of time interval3 is equal to the duration2 of time interval2 minus the duration1 of time interval1. CLIF Axiom: (forall ((t1 "time interval") (t2 "time interval")) (exists ((t3 "time interval")) (if ("time interval1 starts time interval2 complementing time interval3" t1 t2 t3) (= ("duration of" t3) (- ("duration of" t2) ("duration of" t1)))))) OCL Constraint: context "time interval" inv: self.starts-->forAll(t2 | self."time interval1 starts time interval2 complementing time interval3"(t2).duration = (t2.duration)- t1.duration Corollary: If t1 and t2 are time intervals such that t1 finishes t2, then D(t1 finishes t2 complementing t3) = D(t2) . D(t1). Necessity: If a time interval1 finishes a time interval2 complementing a time interval3, then the duration3 of time interval3 is equal to the duration2 of time interval2 minus the duration1 of time interval1. CLIF Axiom: (forall ((t1 "time interval") (t2 "time interval")) (exists ((t3 "time interval")) (if ("time interval1 finishes time interval2 complementing time interval3" t1 t2 t3) (= ("duration of" t3) (- ("duration of" t2) ("duration of" t1)))))) OCL Constraint: context "time interval" inv: self.finishes-->forAll(t2 | self."time interval1 finishes time interval2 complementing time interval3"(t2).duration = (t2.duration)- t1.duration with the following: Corollary: If t1, t2, and t3 are finite time intervals such that t1 starts t2 complementing t3, then D(t3) = D(t2) . D(t1). Necessity: If a finite time interval1 starts a finite time interval2 complementing a finite time interval3, then the duration of finite time interval3 is equal to the duration of finite time interval2 minus the duration of finite time interval1. CLIF Axiom: (forall ((t1 "finite time interval") (t2 "finite time interval") (t3 "finite time interval")) (if ("time interval1 starts time interval2 complementing time interval3" t1 t2 t3) (= ("duration of" t3) (- ("duration of" t2) ("duration of" t1)) ) )) OCL Constraint: context "finite time interval" Corollary: If t1, t2, and t3 are finite time intervals such that t1 finishes t2 complementing t3, then D(t3) = D(t2) . D(t1). Necessity: If a finite time interval1 finishes a finite time interval2 complementing a finite time interval3, then the duration of finite time interval3 is equal to the duration of finite time interval2 minus the duration of finite time interval1. CLIF Axiom: (forall ((t1 "finite time interval") (t2 "finite time interval") (t3 "finite time interval")) (if ("time interval1 finishes time interval2 complementing time interval3" t1 t2 t3) (= ("duration of" t3) (- ("duration of" t2) ("duration of" t1)) ) )) OCL Constraint: context "finite time interval" Disposition: Resolved Date: Tue, 5 Jun 2012 14:05:56 -0400 From: Ed Barkmeyer Reply-To: Organization: NIST User-Agent: Thunderbird 2.0.0.23 (Windows/20090812) To: Mark H Linehan CC: OMG DateTimeVoc FTF Subject: Re: Fw: DTV Issue 16992 - correct axiom D.4 X-NISTMEL-MailScanner-Information: Please contact postmaster@mel.nist.gov for more information X-NISTMEL-MailScanner-ID: q55I62q8003176 X-NISTMEL-MailScanner: Found to be clean X-NISTMEL-MailScanner-SpamCheck: X-NISTMEL-MailScanner-From: edbark@nist.gov X-NISTMEL-MailScanner-Watermark: 1339524367.18391@0bsp0ICPIHzXKJg9roMgwQ X-Spam-Status: No Follow up: I attach a revised draft for 16992, eliminating 'finite time interval' and all the comments that are addressed by the text. There is still some question about the OCL, and there may be other hidden problems. comments? -Ed Edward Barkmeyer wrote: Mark H Linehan wrote: I added many comments to this proposed resolution. Most importantly, I disagree that we need to define the "finite time interval" concept. There are many time intervals that are "indefinite", meaning that their beginning or end (and hence duration) are unknown. But the axioms and corollaries in 8.2.3 are valid with respect to such time intervals. For business purposes, every state of affairs both begins and ends sooner or later. As a concrete example, my life occurs for some time interval. None of us know when that time interval ends, but it definitely will end at some point. So the various axioms and corollaries in 8.2.3 do apply to the duration of my life, even though we do not presently know that duration. "Infinite time intervals" arise in physics, philosophy, and religion, for example when discussing when the universe begins or ends. But those matters are not relevant to business and need not be addressed in our Vocabulary. I have looked at these comments, and I agree that we don't need 'finite time interval'. All time intervals are finite. (I do think that means we should delete the 'forever' object, which is said to be a time interval. I am not sure how this relates to Issue 16993.) I marked up the draft with my comments following Mark's. If we remove the 'finite time interval' stuff, most of the remaining points of disagreement are confusion about 'particular duration'. 'time interval has particular duration' is a primitive concept -- it is the fundamental relationship between time intervals and durations. So it can only have an informal definition. 'particular duration' is an attributive role of 'duration', and we define 'duration of' and 'particular duration of' to be synonyms. Mark points out that a 'particular duration' is a 'particular quantity'. But as I read D.3.1, it means the concept 'particular duration' is an instance of the concept type 'particular quantity', and 'particular quantity' is itself a specialization of 'attributive role'. An instance of particular duration is a duration, not a particular quantity. 'particular quantity' in D.3.1 is weird -- there is no fact type 'thing has particular quantity' for 'time interval has particular duration' to specialize. We can formally define a CLIF "function" ("particular duration of" ti) in terms of the primitive verb concept, we can declare a UML operation on time interval that returns its particular duration. So, I will try to create another draft that eliminates the 'finite time interval' stuff and attempts to clarify the changes to 'particular duration'. -Ed -------------------------------- Mark H. Linehan STSM, Model Driven Business Transformation IBM Research From: Ed Barkmeyer To: OMG DateTimeVoc FTF Date: 03/13/2012 06:01 PM Subject: DTV Issue 16992 - correct axiom D.4 ------------------------------------------------------------------------ Actually the issue identifies a number of problems in 8.2.3. It is just that Axiom D.4 highlights most of them. I attach a first draft of the resolution. It needs help from an OCL expert. -Ed -- Edward J. Barkmeyer Email: edbark@nist.gov National Institute of Standards & Technology Manufacturing Systems Integration Division 100 Bureau Drive, Stop 8263 Tel: +1 301-975-3528 Gaithersburg, MD 20899-8263 Cel: +1 240-672-5800 [attachment "Issue 16992- Axiom D4-d1.doc" deleted by Mark H Linehan/Watson/IBM] -- Edward J. Barkmeyer Email: edbark@nist.gov National Institute of Standards & Technology Manufacturing Systems Integration Division 100 Bureau Drive, Stop 8263 Tel: +1 301-975-3528 Gaithersburg, MD 20899-8263 Cel: +1 240-672-5800 "The opinions expressed above do not reflect consensus of NIST, and have not been reviewed by any Government authority." Issue 16992- Axiom D4-d2.doc Disposition: Resolved OMG Issue No: 16992 Title: Corollaries to Axiom D.4 in 8.2.3 are misstated Source: Ed Barkmeyer, NIST, edbark@nist.gov Summary: In clause 8.2.3 (p.54), the first corollary to axiom D.4 is stated in mathematical English: If t1 and t2 are time intervals such that t1 starts t2, then D(t1 starts t2 complementing t3) = D(t2) . D(t1). But "t1 starts t2 complementing t3" is a proposition, which does not have a duration. The intent is: If t1, t2 and t3 are time intervals such that t1 starts t2 complementing t3, then D(t3) = D(t2) . D(t1). There is a further requirement, namely that time interval t2 is "finite" (which does not seem to be a concept in clause 8). 'Time interval has particular duration' cannot always be satisfied. So it appears that the term 'finite time interval' must be defined: A time interval that has a duration. The CLIF formulation of this corollary is also incorrect. It should read: (forall ((t1 "time interval") (t2 "time interval") (t3 "time interval")) (if (and (exists ((d duration)) ("time interval has duration" t2 d) ("time interval1 starts time interval2 complementing time interval3" t1 t2 t3)) (= ("duration of" t3) (- ("duration of" t2) ("duration of" t1))) )) If the concept 'finite time interval' is added, then this can be simplified: (forall ((t1 "finite time interval") (t2 "finite time interval") (t3 "finite time interval")) (if ("time interval1 starts time interval2 complementing time interval3" t1 t2 t3) (= ("duration of" t3) (- ("duration of" t2) ("duration of" t1))) )) The second Corollary has the same problem. It reads: If t1 and t2 are time intervals such that t1 finishes t2, then D(t1 finishes t2 complementing t3) = D(t2) . D(t1). It should read: If t1, t2 and t3 are time intervals such that t1 finishes t2 complementing t3, then D(t3) = D(t2) . D(t1). The CLIF formulation of the second corollary is also incorrect. It should read: (forall ((t1 "finite time interval") (t2 "finite time interval") (t3 "finite time interval")) (if ("time interval1 finishes time interval2 complementing time interval3" t1 t2 t3) (= ("duration of" t3) (- ("duration of" t2) ("duration of" t1))) )) In both cases, the existence of time interval t3 is the subject of a different axiom. So it suffices to say, for any three time intervals that are related in a certain way, their durations are related in a certain way. The remaining issue is that Clause 8.2 does not define the CLIF function for the SBVR attributive construct 'duration of'. Axiom D.2 suddenly introduces the notation "duration of" as a function. The intent is that the fact type 'time interval has duration' introduces both a CLIF predicate "time interval has duration" AND a CLIF function, which can be defined axiomatically as: (forall ((t "finite time interval") (d duration)) (iff ("time interval has duration" t d) (= ("duration of" t) d) )) This declaration should be added to the entry for the fact type that introduces the "attributive role" 'duration'. Note also that construction of a CLIF function from an SBVR attributive role pattern only behaves as expected when the role is played by a unique thing for each possible value of the function argument. If it is possible that the role is empty or multivalued for a valid argument, the CLIF function would have to be described as returning a set. So this construct does not follow some general pattern. It must be appropriately declared in each case. In this case, the supporting axiom: Necessity: Each time interval has at most one particular duration. should be stated, and then the above function axiom completes the model. Resolution: The technical changes to the CLIF formulations are accepted in principle. The formulation of the Corollaries is corrected. The CLIF function "duration of" is defined. The definition of 'particular duration' and the related axioms are modified. The style of the CLIF formulations, however, follows Issue 17225. The FTF disagrees that the concept .finite time interval. is needed. It is the intent of the DTV that all time intervals are .finite. . they have a beginning and an end. But the open world assumption may apply: Time intervals can be .indefinite. in the sense that we don.t know the beginning or the end. This is clarified in the text. There are other errors in the formulation of the axioms in 8.2.3 with respect to the .duration of. role, and they are also corrected. Revised Text: 1. In clause 8.1, in the entry for .time interval., after the Definition, add the following: Note: Every time interval conceptually has a beginning and an end. It is .finite., a bounded segment of the Time Axis. We can, however, acknowledge the existence of time intervals whose beginning or end we do not know. Such time intervals are not .infinite. or .unbounded., and they are not necessarily .indefinite. . they can be well-defined by reference to events that we lack the information to locate in time. 2. In clause 8.2.3, in the entry for 'particular duration', DELETE the two Definitions and the Reference Scheme: Definition: particular quantity of quantity kind 'duration' Definition: duration of some time interval Reference Scheme: a duration value that quantifies the particular duration and INSERT: Definition: the amount of time in a given time interval Note: particular duration is an instance of particular quantity whose values are of the quantity kind 'duration'. 3. In Clause 8.2.3, in the entry for 'time interval has particular duration', before the Example, INSERT: Definition: the particular duration is the duration that is the amount of time in the time interval Note: This is a primitive concept. It is the fundamental relationship between time intervals and durations. It has no formal definition. But there is a corresponding CLIF function, and a corresponding UML operation, and they can be formally defined in terms of the primitive verb concept. CLIF Definition: (forall (d ti) (iff (= d ("duration of time interval" ti)) (and ("time interval" ti) (duration d) ("time interval has duration" ti d) ))) 4. In 8.2.3, in the Corollary following Axiom D.2 that begins " No time interval has a duration that is the additive inverse .", REPLACE all of the following: Necessity: D0 does not equal D0 minus the duration of a time interval. CLIF Axiom: (forall ((t "time interval")) (not (= D0 (- (D0 t))))) OCL Constraint: context "time interval" inv: not D0 = (D0 . self.duration) with: Necessity: For each time interval1 there is no time interval2 such that the duration of time interval1 plus the duration of time interval2 equals D0. CLIF Axiom: (not (exists t1 t2) ("duration3 = duration1 plus duration2" D0 ("duration of time interval" t1) ("duration of time interval" t2)) )) OCL Constraint: context "time interval" inv: "time interval".allInstances-->forAll(t2 | not ((self.duration() + t2.duration()) = D0)) 5. In 8.2.3, in the entry for Axiom D.3, REPLACE the Necessity: Necessity: If a time interval1 is a part of a time interval2, then the duration1 of time interval1 is less than or equal to the duration2 of time interval2. with: Necessity: 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. 6. In 8.2.3, in the entry for Axiom D.4, REPLACE the Necessity: Necessity: If a time interval1 meets a time interval2, then the duration3 of time interval1 plus time interval2 is equal to the duration1 of time interval1 plus the duration2 of time interval2. with: Necessity: For each time interval1 and each time interval2 that meets time interval1, the duration of time interval1 plus time interval2 is equal to the duration of time interval1 plus the duration of time interval2. 7. In 8.2.3, after Axiom D.4, REPLACE both Corollaries and all of their subordinate paragraphs: Corollary: If t1 and t2 are time intervals such that t1 starts t2, then D(t1 starts t2 complementing t3) = D(t2) . D(t1). Necessity: If a time interval1 starts a time interval2 complementing a time interval3, then the duration3 of time interval3 is equal to the duration2 of time interval2 minus the duration1 of time interval1. CLIF Axiom: (forall ((t1 "time interval") (t2 "time interval")) (exists ((t3 "time interval")) (if ("time interval1 starts time interval2 complementing time interval3" t1 t2 t3) (= ("duration of" t3) (- ("duration of" t2) ("duration of" t1)))))) OCL Constraint: context "time interval" inv: self.starts-->forAll(t2 | self."time interval1 starts time interval2 complementing time interval3"(t2).duration = (t2.duration)- t1.duration Corollary: If t1 and t2 are time intervals such that t1 finishes t2, then D(t1 finishes t2 complementing t3) = D(t2) . D(t1). Necessity: If a time interval1 finishes a time interval2 complementing a time interval3, then the duration3 of time interval3 is equal to the duration2 of time interval2 minus the duration1 of time interval1. CLIF Axiom: (forall ((t1 "time interval") (t2 "time interval")) (exists ((t3 "time interval")) (if ("time interval1 finishes time interval2 complementing time interval3" t1 t2 t3) (= ("duration of" t3) (- ("duration of" t2) ("duration of" t1)))))) OCL Constraint: context "time interval" inv: self.finishes-->forAll(t2 | self."time interval1 finishes time interval2 complementing time interval3"(t2).duration = (t2.duration)- t1.duration with the following: Corollary: If t1, t2, and t3 are time intervals such that t1 starts t2 complementing t3, then D(t1) = D(t2) . D(t3). Necessity: 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. CLIF Axiom: (forall (t1 t2 t3) (if ("time interval1 starts time interval2 complementing time interval3" t1 t2 t3) (= ("duration of" t1) (- ("duration of" t2) ("duration of" t3)) ) )) OCL Constraint: context "time interval" inv: self.starts-->forAll(t2 | self."time interval1 starts time interval2 complementing time interval3"(t2) .duration = (t2.duration)- t1.duration OCL Constraint: context "time interval1 starts time interval2 complementing time interval3" inv: self."time interval1".duration = self."time interval2".duration - self."time interval3".duration Corollary: If t1, t2, and t3 are time intervals such that t1 finishes t2 complementing t3, then D(t1) = D(t2) . D(t3). Necessity: 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. CLIF Axiom: (forall (t1 t2 t3) (if ("time interval1 finishes time interval2 complementing time interval3" t1 t2 t3) (= ("duration of" t1) (- ("duration of" t2) ("duration of" t3)) ) )) CLIF Axiom: context "time interval1 finishes time interval2 complementing time interval3" inv: self."time interval1".duration = self."time interval2".duration - self."time interval3".duration Disposition: Resolved To: date-time-ftf@omg.org Subject: Date-Time Issues 17540, 16992, 16993, 16997 - indefinite time intervals X-KeepSent: F730BBD9:97319387-85257A71:0012AAA4; type=4; name=$KeepSent X-Mailer: Lotus Notes Release 8.5.3 September 15, 2011 From: Mark H Linehan Date: Wed, 5 Sep 2012 23:30:47 -0400 X-MIMETrack: Serialize by Router on D01ML604/01/M/IBM(Release 8.5.3FP2IF1|July 25, 2012) at 09/05/2012 23:30:49 X-Content-Scanned: Fidelis XPS MAILER x-cbid: 12090603-7182-0000-0000-00000282D100 This set of four proposed resolutions addresses the issues around "indefinite" time intervals. They are based on today's discussion between Mike and I. 17540 adds concepts 'primordial' and 'perpetuity' and renames & redefines 'forever' as 'eternity'. (I am not crazy about these terms, particularly 'primordial', which is an adjective.) 16993 adds verb concepts such as 'time interval through occurrence'. 16997 is a duplicate of 17540. 16992 is mostly about durations, but was blocked by 17540. This version rewrites the Notes proposed to be added to 'time interval'. During conversation, we thought the last two Corollaries need some change, but on further review I think they are ok as proposed. ----------------------------- Mark H. Linehan STSM, IBM Research Date-Time Issue 16992- Corollaries to Axiom D.4 in 8.2.3 are misstated.doc Date-Time Issue 16993 - no syntax for indefinite time periods.doc Date-Time Issue 16997 - forever is misdefined.doc Date-Time Issue 17540 - Need to Support Infinite and Indefinite Time Constructs.doc Disposition: Resolved OMG Issue No: 16992 Title: Corollaries to Axiom D.4 in 8.2.3 are misstated Source: Ed Barkmeyer, NIST, edbark@nist.gov Summary: In clause 8.2.3 (p.54), the first corollary to axiom D.4 is stated in mathematical English: If t1 and t2 are time intervals such that t1 starts t2, then D(t1 starts t2 complementing t3) = D(t2) . D(t1). But "t1 starts t2 complementing t3" is a proposition, which does not have a duration. The intent is: If t1, t2 and t3 are time intervals such that t1 starts t2 complementing t3, then D(t3) = D(t2) . D(t1). There is a further requirement, namely that time interval t2 is "finite" (which does not seem to be a concept in clause 8). 'Time interval has particular duration' cannot always be satisfied. So it appears that the term 'finite time interval' must be defined: A time interval that has a duration. The CLIF formulation of this corollary is also incorrect. It should read: (forall ((t1 "time interval") (t2 "time interval") (t3 "time interval")) (if (and (exists ((d duration)) ("time interval has duration" t2 d) ("time interval1 starts time interval2 complementing time interval3" t1 t2 t3)) (= ("duration of" t3) (- ("duration of" t2) ("duration of" t1))) )) If the concept 'finite time interval' is added, then this can be simplified: (forall ((t1 "finite time interval") (t2 "finite time interval") (t3 "finite time interval")) (if ("time interval1 starts time interval2 complementing time interval3" t1 t2 t3) (= ("duration of" t3) (- ("duration of" t2) ("duration of" t1))) )) The second Corollary has the same problem. It reads: If t1 and t2 are time intervals such that t1 finishes t2, then D(t1 finishes t2 complementing t3) = D(t2) . D(t1). It should read: If t1, t2 and t3 are time intervals such that t1 finishes t2 complementing t3, then D(t3) = D(t2) . D(t1). The CLIF formulation of the second corollary is also incorrect. It should read: (forall ((t1 "finite time interval") (t2 "finite time interval") (t3 "finite time interval")) (if ("time interval1 finishes time interval2 complementing time interval3" t1 t2 t3) (= ("duration of" t3) (- ("duration of" t2) ("duration of" t1))) )) In both cases, the existence of time interval t3 is the subject of a different axiom. So it suffices to say, for any three time intervals that are related in a certain way, their durations are related in a certain way. The remaining issue is that Clause 8.2 does not define the CLIF function for the SBVR attributive construct 'duration of'. Axiom D.2 suddenly introduces the notation "duration of" as a function. The intent is that the fact type 'time interval has duration' introduces both a CLIF predicate "time interval has duration" AND a CLIF function, which can be defined axiomatically as: (forall ((t "finite time interval") (d duration)) (iff ("time interval has duration" t d) (= ("duration of" t) d) )) This declaration should be added to the entry for the fact type that introduces the "attributive role" 'duration'. Note also that construction of a CLIF function from an SBVR attributive role pattern only behaves as expected when the role is played by a unique thing for each possible value of the function argument. If it is possible that the role is empty or multivalued for a valid argument, the CLIF function would have to be described as returning a set. So this construct does not follow some general pattern. It must be appropriately declared in each case. In this case, the supporting axiom: Necessity: Each time interval has at most one particular duration. should be stated, and then the above function axiom completes the model. Resolution: The technical changes to the CLIF formulations are accepted in principle. The formulation of the Corollaries is corrected. The CLIF function "duration of" is defined. The definition of 'particular duration' and the related axioms are modified. The style of the CLIF formulations, however, follows Issue 17225. The FTF disagrees that the concept .finite time interval. is needed. It is the intent of the DTV that all time intervals are .finite. . they have a beginning and an end. But the open world assumption may apply: Time intervals can be .indefinite. in the sense that we don.t know the beginning or the end. This is clarified in the text. There are other errors in the formulation of the axioms in 8.2.3 with respect to the .duration of. role, and they are also corrected. Revised Text: 1. In clause 8.1, in the entry for .time interval., after the Definition, add the following: Note: Every time interval has a beginning, an end, and a duration, even if not known. Every time interval is .finite., a bounded segment of the Time Axis. The beginning or end of a time interval may be defined by reference to events that occur for a time interval that is not known. Note: Time intervals may also be .indefinite., meaning that their beginning is .primordial. or their end is .perpetuity., or both (.eternity.). 2. In clause 8.2.3, in the entry for 'particular duration', DELETE the two Definitions and the Reference Scheme: Definition: particular quantity of quantity kind 'duration' Definition: duration of some time interval Reference Scheme: a duration value that quantifies the particular duration and INSERT: Definition: the amount of time in a given time interval Note: particular duration is an instance of particular quantity whose values are of the quantity kind 'duration'. 3. In Clause 8.2.3, in the entry for 'time interval has particular duration', before the Example, INSERT: Definition: the particular duration is the duration that is the amount of time in the time interval Note: This is a primitive concept. It is the fundamental relationship between time intervals and durations. It has no formal definition. But there is a corresponding CLIF function, and a corresponding UML operation, and they can be formally defined in terms of the primitive verb concept. CLIF Definition: (forall (d ti) (iff (= d ("duration of time interval" ti)) (and ("time interval" ti) (duration d) ("time interval has duration" ti d) ))) 4. In 8.2.3, in the Corollary following Axiom D.2 that begins " No time interval has a duration that is the additive inverse .", REPLACE all of the following: Necessity: D0 does not equal D0 minus the duration of a time interval. CLIF Axiom: (forall ((t "time interval")) (not (= D0 (- (D0 t))))) OCL Constraint: context "time interval" inv: not D0 = (D0 . self.duration) with: Necessity: For each time interval1 there is no time interval2 such that the duration of time interval1 plus the duration of time interval2 equals D0. CLIF Axiom: (not (exists t1 t2) ("duration3 = duration1 plus duration2" D0 ("duration of time interval" t1) ("duration of time interval" t2)) )) OCL Constraint: context "time interval" inv: "time interval".allInstances-->forAll(t2 | not ((self.duration() + t2.duration()) = D0)) 5. In 8.2.3, in the entry for Axiom D.3, REPLACE the Necessity: Necessity: If a time interval1 is a part of a time interval2, then the duration1 of time interval1 is less than or equal to the duration2 of time interval2. with: Necessity: 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. 6. In 8.2.3, in the entry for Axiom D.4, REPLACE the Necessity: Necessity: If a time interval1 meets a time interval2, then the duration3 of time interval1 plus time interval2 is equal to the duration1 of time interval1 plus the duration2 of time interval2. with: Necessity: For each time interval1 and each time interval2 that meets time interval1, the duration of time interval1 plus time interval2 is equal to the duration of time interval1 plus the duration of time interval2. 7. In 8.2.3, after Axiom D.4, REPLACE both Corollaries and all of their subordinate paragraphs: Corollary: If t1 and t2 are time intervals such that t1 starts t2, then D(t1 starts t2 complementing t3) = D(t2) . D(t1). Necessity: If a time interval1 starts a time interval2 complementing a time interval3, then the duration3 of time interval3 is equal to the duration2 of time interval2 minus the duration1 of time interval1. CLIF Axiom: (forall ((t1 "time interval") (t2 "time interval")) (exists ((t3 "time interval")) (if ("time interval1 starts time interval2 complementing time interval3" t1 t2 t3) (= ("duration of" t3) (- ("duration of" t2) ("duration of" t1)))))) OCL Constraint: context "time interval" inv: self.starts-->forAll(t2 | self."time interval1 starts time interval2 complementing time interval3"(t2).duration = (t2.duration)- t1.duration Corollary: If t1 and t2 are time intervals such that t1 finishes t2, then D(t1 finishes t2 complementing t3) = D(t2) . D(t1). Necessity: If a time interval1 finishes a time interval2 complementing a time interval3, then the duration3 of time interval3 is equal to the duration2 of time interval2 minus the duration1 of time interval1. CLIF Axiom: (forall ((t1 "time interval") (t2 "time interval")) (exists ((t3 "time interval")) (if ("time interval1 finishes time interval2 complementing time interval3" t1 t2 t3) (= ("duration of" t3) (- ("duration of" t2) ("duration of" t1)))))) OCL Constraint: context "time interval" inv: self.finishes-->forAll(t2 | self."time interval1 finishes time interval2 complementing time interval3"(t2).duration = (t2.duration)- t1.duration with the following: Corollary: If t1, t2, and t3 are time intervals such that t1 starts t2 complementing t3, then D(t1) = D(t2) . D(t3). Necessity: 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. CLIF Axiom: (forall (t1 t2 t3) (if ("time interval1 starts time interval2 complementing time interval3" t1 t2 t3) (= ("duration of" t1) (- ("duration of" t2) ("duration of" t3)) ) )) OCL Constraint: context "time interval" inv: self.starts-->forAll(t2 | self."time interval1 starts time interval2 complementing time interval3"(t2) .duration = (t2.duration)- t1.duration OCL Constraint: context "time interval1 starts time interval2 complementing time interval3" inv: self."time interval1".duration = self."time interval2".duration - self."time interval3".duration Corollary: If t1, t2, and t3 are time intervals such that t1 finishes t2 complementing t3, then D(t1) = D(t2) . D(t3). Necessity: 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. CLIF Axiom: (forall (t1 t2 t3) (if ("time interval1 finishes time interval2 complementing time interval3" t1 t2 t3) (= ("duration of" t1) (- ("duration of" t2) ("duration of" t3)) ) )) CLIF Axiom: context "time interval1 finishes time interval2 complementing time interval3" inv: self."time interval1".duration = self."time interval2".duration - self."time interval3".duration Disposition: Resolved