Modified lines:  18, 19, 20, 23, 24, 25, 26, 27, 28, 29, 30, 33, 34, 35
Added line:  21, 32, 33, 34, 35, 36, 42, 43, 44
Removed line:  None
Generated by diff2html
© Yves Bailly, MandrakeSoft S.A. 2001
diff2html is licensed under the GNU GPL.
  support-v2.1/time.lisp       support-v2.2/time.lisp
  229 lines
6454 bytes
Last modified : Wed Jun 29 13:32:46 2005
       238 lines
6993 bytes
Last modified : Wed Jun 29 13:34:20 2005
1 ;;; Mode: Lisp; Package: ocml     1 ;;; Mode: Lisp; Package: ocml
2     2
3 ;;; The Open University     3 ;;; The Open University
4     4
5 (in-package "OCML")     5 (in-package "OCML")
6     6
7 ;;;A minimalist set of time-related definitions.     7 ;;;A minimalist set of time-related definitions.
8 ;;;We may want to extend this in the future     8 ;;;We may want to extend this in the future
9     9
10 (in-ontology akt-support-ontology)     10 (in-ontology akt-support-ontology)
11     11
12 (def-class YEAR-IN-TIME (integer) ?x     12 (def-class YEAR-IN-TIME (integer) ?x
13 "A year-in-time must be an integer and integer can be a year-in-time"     13 "A year-in-time must be an integer and integer can be a year-in-time"
14 :iff-def (integer ?x)     14 :iff-def (integer ?x)
15         :avoid-infinite-loop t)     15         :avoid-infinite-loop t)
16     16
17 (def-class MONTH-IN-TIME (positive-integer)?x     17 (def-class MONTH-IN-TIME (positive-integer)?x
18 "A month-in-time is an integer in the interval 1-12"     18   "A month-in-time is an integer in the interval 1-12"
19 :iff-def (and (positive-integer ?x)(< ?x 13) )     19   :iff-def (and (positive-integer ?x)(< ?x 13) )
20         :avoid-infinite-loop t)     20   :prove-by (member ?x '(1 2 3 4 5 6 7 8 9 10 11 12 ))
      3d) 21   :no-proofs-by (:iff-def))
21     22
22 (def-class DAY-IN-TIME (positive-integer)?x     23 (def-class DAY-IN-TIME (positive-integer)?x
23 "A day-in-time is an integer in the interval 1-31"     24   "A day-in-time is an integer in the interval 1-31"
24 :iff-def (and (positive-integer ?x)(< ?x 32) )     25   :iff-def (and (positive-integer ?x)(< ?x 32) )
25         :avoid-infinite-loop t)     26   :prove-by (member ?x '(1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23
26     27                           24 25 26 27 28 29 30 31))
27 (def-class HOUR-IN-TIME (non-negative-integer)?x     28
28 "A hour-in-time is an integer in the interval 0-23"   3d) 29   :no-proofs-by (:iff-def))
29 :iff-def (and (non-negative-integer ?x)(< ?x 24) )     30
30         :avoid-infinite-loop t)     31 (def-class HOUR-IN-TIME (non-negative-integer) ?x
        32   "A hour-in-time is an integer in the interval 0-23"
        33   :iff-def (and (non-negative-integer ?x)(< ?x 24) )
        34   :prove-by (member ?x '(0 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23))
      3d) 35   :no-proofs-by (:iff-def))
        36
31     37
32 (def-class MINUTE-IN-TIME (non-negative-integer) ?x     38 (def-class MINUTE-IN-TIME (non-negative-integer) ?x
33 "A minute-in-time is an integer in the interval 0-59"     39   "A minute-in-time is an integer in the interval 0-59"
34 :iff-def (and (non-negative-integer ?x)(< ?x 60) )     40   :iff-def (and (non-negative-integer ?x)(< ?x 60) )
35         :avoid-infinite-loop t)   3d) 41   :prove-by (member ?x '(0 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29
        42                           30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58
        43                           59))
        44   :no-proofs-by (:iff-def))
36     45
37     46
38     47
39 (def-class SECOND-IN-TIME (real-number)?x     48 (def-class SECOND-IN-TIME (real-number)?x
40   "A second-in-time is a real number greater or equal to 0, less than 60"     49   "A second-in-time is a real number greater or equal to 0, less than 60"
41   :iff-def (and (real-number ?x)(not (< ?x 0))(< ?x 60))     50   :iff-def (and (real-number ?x)(not (< ?x 0))(< ?x 60))
42   :avoid-infinite-loop t)     51   :avoid-infinite-loop t)
43     52
44     53
45 (def-class TIME-POSITION (intangible-thing)     54 (def-class TIME-POSITION (intangible-thing)
46   "A time position is either a time interval or a time point.     55   "A time position is either a time interval or a time point.
47    Any time position is relative to a time zone"     56    Any time position is relative to a time zone"
48   ((in-timezone :default-value "+00:00" :type timezone)))     57   ((in-timezone :default-value "+00:00" :type timezone)))
49     58
50 (def-class TIMEZONE (string)     59 (def-class TIMEZONE (string)
51   "We represent a time zone as a string with the format     60   "We represent a time zone as a string with the format
52    {-/+}hh:mm ")     61    {-/+}hh:mm ")
53     62
54     63
55     64
56     65
57 (def-class TIME-POINT (time-position)     66 (def-class TIME-POINT (time-position)
58   "A point in time"     67   "A point in time"
59   ((second-of :type second-in-time :max-cardinality 1 )     68   ((second-of :type second-in-time :max-cardinality 1 )
60    (minute-of :type minute-in-time :max-cardinality 1 )     69    (minute-of :type minute-in-time :max-cardinality 1 )
61    (hour-of :type hour-in-time :max-cardinality 1 )     70    (hour-of :type hour-in-time :max-cardinality 1 )
62    (day-of :type day-in-time :max-cardinality 1)     71    (day-of :type day-in-time :max-cardinality 1)
63    (month-of :type month-in-time :max-cardinality 1)     72    (month-of :type month-in-time :max-cardinality 1)
64    (year-of :type year-in-time :max-cardinality 1 ))     73    (year-of :type year-in-time :max-cardinality 1 ))
65   :constraint (and (not (and (month-of ?x 2)     74   :constraint (and (not (and (month-of ?x 2)
66                              (> (the ?day (day-of ?x ?day))     75                              (> (the ?day (day-of ?x ?day))
67                                 29)))     76                                 29)))
68                     (not (and (member-of ?x (4 6 9 11))     77                     (not (and (member-of ?x (4 6 9 11))
69                               (> (the ?day (day-of ?x ?day))     78                               (> (the ?day (day-of ?x ?day))
70                                 30)))))     79                                 30)))))
71     80
72     81
73     82
74     83
75     84
76     85
77 (def-class CALENDAR-DATE (time-point)     86 (def-class CALENDAR-DATE (time-point)
78  "A calendar date is a time point in which month, day and year have     87  "A calendar date is a time point in which month, day and year have
79   been specified but hour, minute and second have not"     88   been specified but hour, minute and second have not"
80   ((minute-of :type minute-in-time :max-cardinality 0 )     89   ((minute-of :type minute-in-time :max-cardinality 0 )
81    (second-of :type second-in-time :max-cardinality 0 )     90    (second-of :type second-in-time :max-cardinality 0 )
82    (hour-of :type hour-in-time :max-cardinality 0 )     91    (hour-of :type hour-in-time :max-cardinality 0 )
83    (day-of :type day-in-time :cardinality 1)     92    (day-of :type day-in-time :cardinality 1)
84    (month-of :type month-in-time :cardinality 1)     93    (month-of :type month-in-time :cardinality 1)
85    (year-of :type year-in-time :cardinality 1)))     94    (year-of :type year-in-time :cardinality 1)))
86     95
87     96
88     97
89     98
90 (def-class TIME-INTERVAL (time-position)     99 (def-class TIME-INTERVAL (time-position)
91   "An interval is defined by two time points or a duration.     100   "An interval is defined by two time points or a duration.
92    Classes of intervals, e.g., a day, can be defined by specifying only     101    Classes of intervals, e.g., a day, can be defined by specifying only
93    a duration. A time interval has no gaps"     102    a duration. A time interval has no gaps"
94     103
95   ((begins-at-time-point :type time-point :max-cardinality 1)     104   ((begins-at-time-point :type time-point :max-cardinality 1)
96    (ends-at-time-point :type time-point :max-cardinality 1)     105    (ends-at-time-point :type time-point :max-cardinality 1)
97    (has-duration :type duration :max-cardinality 1)))     106    (has-duration :type duration :max-cardinality 1)))
98     107
99 (def-class DAY (time-interval)     108 (def-class DAY (time-interval)
100   ((has-duration :value 24-hour-duration)))     109   ((has-duration :value 24-hour-duration)))
101     110
102 (def-class WEEK (time-interval)     111 (def-class WEEK (time-interval)
103   ((has-duration :value 7-day-duration)))     112   ((has-duration :value 7-day-duration)))
104     113
105 (def-class MONTH (time-interval))     114 (def-class MONTH (time-interval))
106     115
107 (def-class JANUARY (month)     116 (def-class JANUARY (month)
108   ((has-duration :value 31-day-duration)))     117   ((has-duration :value 31-day-duration)))
109     118
110 (def-class FEBRUARY (month)     119 (def-class FEBRUARY (month)
111   ((has-duration :default-value 28-day-duration)))     120   ((has-duration :default-value 28-day-duration)))
112     121
113 (def-class FEBRUARY-IN-LEAP-YEARS (february)     122 (def-class FEBRUARY-IN-LEAP-YEARS (february)
114   ((has-duration :value 29-day-duration)))     123   ((has-duration :value 29-day-duration)))
115     124
116     125
117 (def-class MARCH (month)     126 (def-class MARCH (month)
118   ((has-duration :value 31-day-duration)))     127   ((has-duration :value 31-day-duration)))
119     128
120 (def-class APRIL (month)     129 (def-class APRIL (month)
121   ((has-duration :value 30-day-duration)))     130   ((has-duration :value 30-day-duration)))
122     131
123 (def-class MAY (month)     132 (def-class MAY (month)
124   ((has-duration :value 31-day-duration)))     133   ((has-duration :value 31-day-duration)))
125     134
126 (def-class JUNE (month)     135 (def-class JUNE (month)
127   ((has-duration :value 30-day-duration)))     136   ((has-duration :value 30-day-duration)))
128     137
129 (def-class JULY (month)     138 (def-class JULY (month)
130   ((has-duration :value 31-day-duration)))     139   ((has-duration :value 31-day-duration)))
131     140
132 (def-class AUGUST (month)     141 (def-class AUGUST (month)
133   ((has-duration :value 31-day-duration)))     142   ((has-duration :value 31-day-duration)))
134     143
135 (def-class SEPTEMBER (month)     144 (def-class SEPTEMBER (month)
136   ((has-duration :value 30-day-duration)))     145   ((has-duration :value 30-day-duration)))
137     146
138 (def-class OCTOBER (month)     147 (def-class OCTOBER (month)
139   ((has-duration :value 31-day-duration)))     148   ((has-duration :value 31-day-duration)))
140     149
141 (def-class NOVEMBER (month)     150 (def-class NOVEMBER (month)
142   ((has-duration :value 30-day-duration)))     151   ((has-duration :value 30-day-duration)))
143     152
144 (def-class DECEMBER (month)     153 (def-class DECEMBER (month)
145   ((has-duration :value 31-day-duration)))     154   ((has-duration :value 31-day-duration)))
146     155
147 (def-class YEAR (time-interval)     156 (def-class YEAR (time-interval)
148   ((has-duration :value 12-month-duration)))     157   ((has-duration :value 12-month-duration)))
149     158
150 (def-class DURATION (physical-quantity)     159 (def-class DURATION (physical-quantity)
151   "A measure of time, e.g., 5 hours"     160   "A measure of time, e.g., 5 hours"
152   ((has-unit-of-measure :type time-measure)     161   ((has-unit-of-measure :type time-measure)
153    ))     162    ))
154     163
155 (def-instance 24-HOUR-DURATION duration     164 (def-instance 24-HOUR-DURATION duration
156   ((has-unit-of-measure time-measure-hour)     165   ((has-unit-of-measure time-measure-hour)
157    (has-magnitude 24)))     166    (has-magnitude 24)))
158     167
159 (def-instance 7-DAY-DURATION duration     168 (def-instance 7-DAY-DURATION duration
160   ((has-unit-of-measure time-measure-day)     169   ((has-unit-of-measure time-measure-day)
161    (has-magnitude 7)))     170    (has-magnitude 7)))
162     171
163 (def-instance 28-DAY-DURATION duration     172 (def-instance 28-DAY-DURATION duration
164   ((has-unit-of-measure time-measure-day)     173   ((has-unit-of-measure time-measure-day)
165    (has-magnitude 28)))     174    (has-magnitude 28)))
166     175
167 (def-instance 29-DAY-DURATION duration     176 (def-instance 29-DAY-DURATION duration
168   ((has-unit-of-measure time-measure-day)     177   ((has-unit-of-measure time-measure-day)
169    (has-magnitude 29)))     178    (has-magnitude 29)))
170     179
171 (def-instance 30-DAY-DURATION duration     180 (def-instance 30-DAY-DURATION duration
172   ((has-unit-of-measure time-measure-day)     181   ((has-unit-of-measure time-measure-day)
173    (has-magnitude 30)))     182    (has-magnitude 30)))
174     183
175 (def-instance 31-DAY-DURATION duration     184 (def-instance 31-DAY-DURATION duration
176   ((has-unit-of-measure time-measure-day)     185   ((has-unit-of-measure time-measure-day)
177    (has-magnitude 31)))     186    (has-magnitude 31)))
178     187
179 (def-instance 12-MONTH-DURATION duration     188 (def-instance 12-MONTH-DURATION duration
180   ((has-unit-of-measure time-measure-year)     189   ((has-unit-of-measure time-measure-year)
181    (has-magnitude 12)))     190    (has-magnitude 12)))
182     191
183 (def-class TIME-MEASURE (unit-of-measure)     192 (def-class TIME-MEASURE (unit-of-measure)
184   "The class of all unit of measures used to measure time,     193   "The class of all unit of measures used to measure time,
185    e.g., minute, second, hour, etc...")     194    e.g., minute, second, hour, etc...")
186     195
187 (def-instance TIME-MEASURE-SECOND time-measure)     196 (def-instance TIME-MEASURE-SECOND time-measure)
188     197
189 (def-instance TIME-MEASURE-MINUTE time-measure)     198 (def-instance TIME-MEASURE-MINUTE time-measure)
190     199
191 (def-instance TIME-MEASURE-HOUR time-measure)     200 (def-instance TIME-MEASURE-HOUR time-measure)
192     201
193 (def-instance TIME-MEASURE-DAY time-measure)     202 (def-instance TIME-MEASURE-DAY time-measure)
194     203
195 (def-instance TIME-MEASURE-MONTH time-measure)     204 (def-instance TIME-MEASURE-MONTH time-measure)
196     205
197 (def-instance TIME-MEASURE-YEAR time-measure)     206 (def-instance TIME-MEASURE-YEAR time-measure)
198     207
199 (def-instance TIME-MEASURE-CENTURY time-measure)     208 (def-instance TIME-MEASURE-CENTURY time-measure)
200     209
201     210
202 (def-axiom DURATION-IS-BEGIN-TIME-MINUS-END-TIME     211 (def-axiom DURATION-IS-BEGIN-TIME-MINUS-END-TIME
203   "This axiom states the relation between duration, begin time     212   "This axiom states the relation between duration, begin time
204    and end time in an interval"     213    and end time in an interval"
205   (=> (and (time-interval ?x)     214   (=> (and (time-interval ?x)
206            (begins-at-time-point ?x ?tp1)     215            (begins-at-time-point ?x ?tp1)
207            (ends-at-time-point ?x ?tp2))     216            (ends-at-time-point ?x ?tp2))
208       (= (has-duration ?x (time-difference     217       (= (has-duration ?x (time-difference
209                            (the ?tp1 (begins-at-time-point ?x ?tp1))     218                            (the ?tp1 (begins-at-time-point ?x ?tp1))
210                            (the ?tp2 (ends-at-time-point ?x ?tp2)))))))     219                            (the ?tp2 (ends-at-time-point ?x ?tp2)))))))
211     220
212     221
213 (def-function TIME-DIFFERENCE (?tp1 ?tp2) -> ?d     222 (def-function TIME-DIFFERENCE (?tp1 ?tp2) -> ?d
214   "The duration between two time points.     223   "The duration between two time points.
215    No operational definition is given here, only a spec"     224    No operational definition is given here, only a spec"
216   :def (and (time-point ?tp1)     225   :def (and (time-point ?tp1)
217             (time-point ?tp2)     226             (time-point ?tp2)
218             (duration ?d)))     227             (duration ?d)))
219     228
220     229
221     230
222     231
223     232
224     233
225     234
226     235
227     236
228     237
229     238
Generated by diff2html on Wed Jun 29 13:51:27 2005
Command-line: ./diff2html support-v2.1/time.lisp support-v2.2/time.lisp