1:-include(library('ec_planner/ec_test_incl')). 2:-expects_dialect(pfc). 3 % loading(always,'foundations/DEC.e').
4%;
5%; Copyright (c) 2005 IBM Corporation and others.
6%; All rights reserved. This program and the accompanying materials
7%; are made available under the terms of the Common Public License v1.0
8%; which accompanies this distribution, and is available at
9%; http://www.eclipse.org/legal/cpl-v10.html
10%;
11%; Contributors:
12%; IBM - Initial implementation
13%;
14%; Discrete Event Calculus (DEC)
15%;
16%; @article{Mueller:2004a,
17%; author = "Erik T. Mueller",
18%; year = "2004",
19%; title = "Event calculus reasoning through satisfiability",
20%; journal = "Journal of Logic and Computation",
21%; volume = "14",
22%; number = "5",
23%; pages = "703--730",
24%; }
25%;
26
27% sort time: integer
28==> subsort(time,integer).
29
30% sort offset: integer
31==> subsort(offset,integer).
32
33% reified sort fluent
34 % reified_sort(fluent).
35==> mpred_prop(fluent,reified_sort).
36
37% reified sort event
38 % reified_sort(event).
39==> mpred_prop(event,reified_sort).
40
41% predicate Happens(event,time)
42 % predicate(happens(event,time)).
43==> mpred_prop(happens(event,time),predicate).
44==> meta_argtypes(happens(event,time)).
45
46% predicate HoldsAt(fluent,time)
47 % predicate(holds_at(fluent,time)).
48==> mpred_prop(holds_at(fluent,time),predicate).
49==> meta_argtypes(holds_at(fluent,time)).
50
51% predicate ReleasedAt(fluent,time)
52 % predicate(releasedAt(fluent,time)).
53==> mpred_prop(releasedAt(fluent,time),predicate).
54==> meta_argtypes(releasedAt(fluent,time)).
55
56% predicate Initiates(event,fluent,time)
57 % predicate(initiates(event,fluent,time)).
58==> mpred_prop(initiates(event,fluent,time),predicate).
59==> meta_argtypes(initiates(event,fluent,time)).
60
61% predicate Terminates(event,fluent,time)
62 % predicate(terminates(event,fluent,time)).
63==> mpred_prop(terminates(event,fluent,time),predicate).
64==> meta_argtypes(terminates(event,fluent,time)).
65
66% predicate Releases(event,fluent,time)
67 % predicate(releases(event,fluent,time)).
68==> mpred_prop(releases(event,fluent,time),predicate).
69==> meta_argtypes(releases(event,fluent,time)).
70
71
79axiom(holds_at(Fluent, start),
80
81 [ not(happens(Event, t)),
82 holds_at(Fluent, t),
83 not(releasedAt(Fluent, t+1)),
84 b(t, start),
85 ignore(t+1=start)
86 ]).
87axiom(holds_at(Fluent, start),
88
89 [ not(terminates(Event, Fluent, t)),
90 holds_at(Fluent, t),
91 not(releasedAt(Fluent, t+1)),
92 b(t, start),
93 ignore(t+1=start)
94 ]).
95
96
104axiom(not(holds_at(Fluent, start)),
105
106 [ not(happens(Event, t)),
107 not(holds_at(Fluent, t)),
108 not(releasedAt(Fluent, t+1)),
109 b(t, start),
110 ignore(t+1=start)
111 ]).
112axiom(not(holds_at(Fluent, start)),
113
114 [ not(initiates(Event, Fluent, t)),
115 not(holds_at(Fluent, t)),
116 not(releasedAt(Fluent, t+1)),
117 b(t, start),
118 ignore(t+1=start)
119 ]).
120
121
128axiom(not(releasedAt(Fluent, Time+1)),
129
130 [ not(happens(Event, Time)),
131 not(releasedAt(Fluent, Time))
132 ]).
133axiom(not(releasedAt(Fluent, Time+1)),
134
135 [ not(releases(Event, Fluent, Time)),
136 not(releasedAt(Fluent, Time))
137 ]).
138
139
148axiom(releasedAt(Fluent, Time+1),
149 [not(happens(Event, Time)), releasedAt(Fluent, Time)]).
150axiom(releasedAt(Fluent, Time+1),
151
152 [ not(initiates(Event, Fluent, Time)),
153 not(terminates(Event, Fluent, Time)),
154 releasedAt(Fluent, Time)
155 ]).
156
157
162
163 166
167 174axiom(not(happens(Happens_Param, t)),
175
176 [ not(holds_at(Holds_at_Param, start)),
177 initiates(Happens_Param, Holds_at_Param, t),
178 b(t, start),
179 ignore(t+1=start)
180 ]).
181axiom(not(happens(Happens_Param, t)),
182
183 [ releasedAt(Holds_at_Param, t+1),
184 initiates(Happens_Param, Holds_at_Param, t)
185 ]).
186
187 193axiom(not(initiates(Initiates_Param, Holds_at_Param8, t)),
194
195 [ not(holds_at(Holds_at_Param8, start)),
196 happens(Initiates_Param, t),
197 b(t, start),
198 ignore(t+1=start)
199 ]).
200axiom(not(initiates(Initiates_Param, Holds_at_Param8, t)),
201 [releasedAt(Holds_at_Param8, t+1), happens(Initiates_Param, t)]).
202
203 207axiom(holds_at(Holds_at_Param10, start),
208
209 [ happens(Happens_Param11, t),
210 initiates(Happens_Param11, Holds_at_Param10, t),
211 b(t, start),
212 ignore(t+1=start)
213 ]).
214
215 219axiom(not(releasedAt(ReleasedAt_Param, Maptime12+1)),
220
221 [ happens(Happens_Param14, Maptime12),
222 initiates(Happens_Param14, ReleasedAt_Param, Maptime12)
223 ]).
224
225
230
231 234
235 242axiom(not(happens(Happens_Param, t)),
243
244 [ holds_at(Holds_at_Param, start),
245 terminates(Happens_Param, Holds_at_Param, t),
246 b(t, start),
247 ignore(t+1=start)
248 ]).
249axiom(not(happens(Happens_Param, t)),
250
251 [ releasedAt(Holds_at_Param, t+1),
252 terminates(Happens_Param, Holds_at_Param, t)
253 ]).
254
255 261axiom(not(terminates(Terminates_Param, Holds_at_Param8, t)),
262
263 [ holds_at(Holds_at_Param8, start),
264 happens(Terminates_Param, t),
265 b(t, start),
266 ignore(t+1=start)
267 ]).
268axiom(not(terminates(Terminates_Param, Holds_at_Param8, t)),
269 [releasedAt(Holds_at_Param8, t+1), happens(Terminates_Param, t)]).
270
271 275axiom(not(holds_at(Holds_at_Param10, start)),
276
277 [ happens(Happens_Param11, t),
278 terminates(Happens_Param11, Holds_at_Param10, t),
279 b(t, start),
280 ignore(t+1=start)
281 ]).
282
283 287axiom(not(releasedAt(ReleasedAt_Param, Maptime12+1)),
288
289 [ happens(Happens_Param14, Maptime12),
290 terminates(Happens_Param14, ReleasedAt_Param, Maptime12)
291 ]).
292
293
299axiom(releasedAt(Fluent, Time+1),
300
301 [ happens(Event, Time),
302 releases(Event, Fluent, Time)
303 ]).
304
305