```    1%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
2%
3% Copyright 2003,    Renate Schmidt, University of Manchester
4%  Modified 2009-10, Ullrich Hustadt, University of Liverpool
5%
6% Uses
7%       X_{<a*>p}
8%   (X)-----------
9%       p | <a>X
10%
11%         A v B
12%   (v) -------------
13%         A | B
14%
15% 'nd' is short for `not disjoint' branches
16%
17%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
18
19:-module(pdl_dGM_nd,
20    [
21        eventualities/2,
22        simplify_X/2,
23        reduce_local/7
24    ]).   25
26:- dynamic
27        eventualities/2,
28        simplify_X/2,
29        reduce_local/7.   30
31%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
32
33eventualities([], []).
34
35eventualities([pr(_,FmlList)|Branch], Eventualities) :-
36    eventualities_fml(FmlList, Eventualities1), !,
37    eventualities(Branch, Eventualities2),
38    sort(Eventualities1, SortedEventualities1),
39    sort(Eventualities2, SortedEventualities2),
40    merge_set(SortedEventualities1, SortedEventualities2, Eventualities).
41
42eventualities_fml([], []).
43
44eventualities_fml([Fml|FmlList], Eventualities) :-
45    eventualities_fml(Fml, Eventualities1), !,
46    eventualities_fml(FmlList, Eventualities2),
47    sort(Eventualities1, SortedEventualities1),
48    sort(Eventualities2, SortedEventualities2),
49    merge_set(SortedEventualities1, SortedEventualities2, Eventualities).
50
51eventualities_fml(x(X,Fml), [x(X,Fml)|Eventualities]) :-
52    eventualities_fml(Fml, Eventualities).
53
54eventualities_fml(and(A,B), Eventualities) :-
55    eventualities_fml(A, EventualitiesA),
56    eventualities_fml(B, EventualitiesB),
57    sort(EventualitiesA, SortedEventualitiesA),
58    sort(EventualitiesB, SortedEventualitiesB),
59    merge_set(SortedEventualitiesA, SortedEventualitiesB, Eventualities).
60
61eventualities_fml(or(A,B), Eventualities) :-
62    eventualities_fml(A, EventualitiesA),
63    eventualities_fml(B, EventualitiesB),
64    sort(EventualitiesA, SortedEventualitiesA),
65    sort(EventualitiesB, SortedEventualitiesB),
66    merge_set(SortedEventualitiesA, SortedEventualitiesB, Eventualities).
67
68eventualities_fml(not(A), Eventualities) :-
69    eventualities_fml(A, Eventualities).
70
71eventualities_fml(test(A), Eventualities) :-
72    eventualities_fml(A, Eventualities).
73
74eventualities_fml(star(R), Eventualities) :-
75    eventualities_fml(R, Eventualities).
76
77eventualities_fml(comp(R,S), Eventualities) :-
78    eventualities_fml(R, EventualitiesR),
79    eventualities_fml(S, EventualitiesS),
80    sort(EventualitiesR, SortedEventualitiesR),
81    sort(EventualitiesS, SortedEventualitiesS),
82    merge_set(SortedEventualitiesR, SortedEventualitiesS, Eventualities).
83
84eventualities_fml(dia(R,A), Eventualities) :-
85    eventualities_fml(R, EventualitiesR),
86    eventualities_fml(A, EventualitiesA),
87    sort(EventualitiesR, SortedEventualitiesR),
88    sort(EventualitiesA, SortedEventualitiesA),
89    merge_set(SortedEventualitiesR, SortedEventualitiesA, Eventualities).
90
91eventualities_fml(box(R,A), Eventualities) :-
92    eventualities_fml(R, EventualitiesR),
93    eventualities_fml(A, EventualitiesA),
94    sort(EventualitiesR, SortedEventualitiesR),
95    sort(EventualitiesA, SortedEventualitiesA),
96    merge_set(SortedEventualitiesR, SortedEventualitiesA, Eventualities).
97
98eventualities_fml(_,[]).
99
100
101%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
102
103simplify_X([], []).
104
105simplify_X([Fml|FmlList], [SimplifiedFml|SimplifiedFmlList]) :-
106    simplify_X_fml(Fml, SimplifiedFml), !,
107    simplify_X(FmlList, SimplifiedFmlList).
108
109simplify_X_fml(x(_,Fml), x(SimplifiedFml)) :-
110    simplify_X_fml(Fml, SimplifiedFml).
111
112simplify_X_fml(and(A,B), and(SimplifiedA,SimplifiedB)) :-
113    simplify_X_fml(A, SimplifiedA),
114    simplify_X_fml(B, SimplifiedB).
115
116simplify_X_fml(or(A,B), or(SimplifiedA,SimplifiedB)) :-
117    simplify_X_fml(A, SimplifiedA),
118    simplify_X_fml(B, SimplifiedB).
119
120simplify_X_fml(not(A), not(SimplifiedA)) :-
121    simplify_X_fml(A, SimplifiedA).
122
123simplify_X_fml(dia(R,A), dia(SimplifiedR,SimplifiedA)) :-
124    simplify_X_fml(R, SimplifiedR),
125    simplify_X_fml(A, SimplifiedA).
126
127simplify_X_fml(box(R,A), box(SimplifiedR,SimplifiedA)) :-
128    simplify_X_fml(R, SimplifiedR),
129    simplify_X_fml(A, SimplifiedA).
130
131simplify_X_fml(comp(R,S), comp(SimplifiedR,SimplifiedS)) :-
132    simplify_X_fml(R, SimplifiedR),
133    simplify_X_fml(S, SimplifiedS).
134
135simplify_X_fml(test(R), test(SimplifiedR)) :-
136    simplify_X_fml(R, SimplifiedR).
137
138simplify_X_fml(A,A).
139
140%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
141%
142% reduce_local(+Unexpanded, +State, +Workedoff, -NewWorkedoff,
143%        -Universal, -Existential, -Eventualities)
144%
145% - Applies the local reduction rules of the tableau calculus;
146%   all except existential, universal and theory rules
147% - Note that -Eventualities is the list of eventualities <A*> F
148%   such that the formula F has just been added to the branch; thus
149%   <A*>F is fulfilled.
150
151reduce_local([], _, Workedoff, Workedoff, [], [], []).
152
153reduce_local([true|Unexpanded], X, Workedoff, NewWorkedoff,
154        Universal, Existential, Eventualities) :- !,
155    extend_unexpanded([true], Workedoff, Unexpanded, NewUnexpanded, X, true),
156    reduce_local(NewUnexpanded, X, [true|Workedoff],
157            NewWorkedoff, Universal, Existential, Eventualities).
158
159reduce_local([or(A,B)|Unexpanded], X, Workedoff, NewWorkedoff,
160        Universal, Existential, Eventualities) :-
161% Note: no Prolog cut at this point ->
162%       The disjunction or(A,B) creates two branches in our search
163%       space / branches in the tableau tree.
164%       We first explore the branch on which A is true; this is done by the
165%       remaining literals of this rule.
166%       If the first branch does not result in a model, then Prolog
167%       backtracking will take us back to this point and then to the next
168%       rule below.
169    get_branch_point_counter(Count),
170    pdl_on_write('In reduce_local, LEFT branch of OR, reduce_local: '), pdl_on_write(Count), pdl_on_nl,
171    increment_branch_point_counter(1),
172    extend_unexpanded([A], Workedoff, Unexpanded, NewUnexpanded,
173                 X, ['or-LEFT',or(A,B)]),
174    reduce_local(NewUnexpanded, X, [or(A,B)|Workedoff],
175            NewWorkedoff, Universal, Existential, Eventualities).
176
177reduce_local([or(A,B)|Unexpanded], X, Workedoff, NewWorkedoff,
178        Universal, Existential, Eventualities) :-
179% Note: We are still dealing with the same disjunction or(A,B) as the
180%       previous rule. We only get to this point if the branch on which
181%       A is true did not result in a model. So, we now explore the branch
182%       of the search space / tableau tree on which B is true.
183    get_branch_point_counter(Count),
184    pdl_on_write('In reduce_local, RIGHT branch of OR, reduce_local: '), pdl_on_write(Count), pdl_on_nl,
185    increment_branch_point_counter(-1),
186    extend_unexpanded([B], Workedoff, Unexpanded, NewUnexpanded,
187                 X, ['or-RIGHT',or(A,B)]),
188    reduce_local(NewUnexpanded, X, [or(A,B)|Workedoff],
189            NewWorkedoff, Universal, Existential, Eventualities).
190
191% Condition 4 in Definition 23 in (De Giacomo and Massacci, 2000):
192% If both [A|S] and [B|S] are \bot-sets, then [or(A,B)|S] is a \bot-set
193reduce_local([or(A,B)|Unexpanded], _X, Workedoff, _NewWorkedoff,
194             _Universal, _Existential, _Eventualities) :-
195    !,
196%    write('both branches of an or have been closed; recording inconsistency'), nl,
197    append([or(A,B)|Unexpanded],Workedoff,Fmls),
198    store_inconsistent(Fmls),
199    fail.
200
201reduce_local([not(or(A,B))|Unexpanded], X, Workedoff, NewWorkedoff,
202        Universal, Existential, Eventualities) :- !,
203    complement(A, NotA),
204    complement(B, NotB),
205    extend_unexpanded([NotA,NotB], Workedoff, Unexpanded, NewUnexpanded,
206                 X, ['and',not(or(A,B))]),
207    reduce_local(NewUnexpanded, X, [not(or(A,B))|Workedoff],
208            NewWorkedoff, Universal, Existential, Eventualities).
209
210reduce_local([dia(or(R,S),A)|Unexpanded], X, Workedoff, NewWorkedoff,
211        Universal, Existential, Eventualities) :- % no cut
212    get_branch_point_counter(Count),
213    pdl_on_write('In reduce_local, LEFT branch of DIA-OR, reduce_local: '), pdl_on_write(Count), pdl_on_nl,
214    increment_branch_point_counter(1),
215    extend_unexpanded([dia(R,A)], Workedoff, Unexpanded, NewUnexpanded,
216                 X, ['dia-or-LEFT',dia(or(R,S),A)]),
217    reduce_local(NewUnexpanded, X, [dia(or(R,S),A)|Workedoff],
218            NewWorkedoff, Universal, Existential, Eventualities).
219
220reduce_local([dia(or(R,S),A)|Unexpanded], X, Workedoff, NewWorkedoff,
221        Universal, Existential, Eventualities) :- !,
222    % Expand the right branch only when the left one is closed
223%    is_unsatisfiable(_),
224%    complement(dia(R,A), NotDiaRA),
225    get_branch_point_counter(Count),
226    pdl_on_write('In reduce_local, RIGHT branch of DIA-OR, reduce_local: '), pdl_on_write(Count), pdl_on_nl,
227    increment_branch_point_counter(-1),
228    extend_unexpanded([dia(S,A)], Workedoff, Unexpanded, NewUnexpanded,
229                X, ['dia-or-RIGHT',dia(or(R,S),A)]),
230    reduce_local(NewUnexpanded, X, [dia(or(R,S))|Workedoff],
231            NewWorkedoff, Universal, Existential, Eventualities).
232
233reduce_local([dia(comp(R,S),A)|Unexpanded], X, Workedoff, NewWorkedoff,
234        Universal, Existential, Eventualities) :- !,
235    extend_unexpanded([dia(R,dia(S,A))], Workedoff, Unexpanded, NewUnexpanded,
236                X, ['dia-comp',dia(comp(R,S),A)]),
237    reduce_local(NewUnexpanded, X, [dia(comp(R,S),A)|Workedoff],
238            NewWorkedoff, Universal, Existential, Eventualities).
239
240reduce_local([dia(star(R),A)|Unexpanded], X, Workedoff, NewWorkedoff,
241        Universal, Existential, Eventualities) :- !,
242    extend_unexpanded([x(X,dia(star(R),A))], Workedoff, Unexpanded, NewUnexpanded,
243                X, ['dia-star',dia(star(R),A)]),
244    reduce_local(NewUnexpanded, X, [dia(star(R),A)|Workedoff],
245            NewWorkedoff, Universal, Existential, Eventualities).
246
247%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
248% Note that (de Giacomo and Massacci, 2001) uses complement splitting when
249% dealing with <A*>F. Thus, on the right branch created for <A*>F, (not F)
250% is true, making it impossible for the current state/world to be the one
251% fulfilling <A*>F. On the other hand, on the left branch, we make F true
252% and <A*>F is fulfilled. We record this by adding fulfilled(...) to the
253% list of (fulfilled) eventualities.
254reduce_local([x(Y,dia(star(R),A))|Unexpanded], X, Workedoff, NewWorkedoff,
255        Universal, Existential,
256        [fulfilled(X, x(Y,dia(star(R),A)))|Eventualities]) :- % no cut
257    get_branch_point_counter(Count),
258    pdl_on_write('In reduce_local, LEFT branch of X, reduce_local: '), pdl_on_write(Count), pdl_on_nl,
259    increment_branch_point_counter(1),
260    extend_unexpanded([A], Workedoff, Unexpanded, NewUnexpanded,
261                X, ['X-LEFT',x(Y,dia(star(R),A))]),
262    reduce_local(NewUnexpanded, X, [x(Y,dia(star(R),A))|Workedoff],
263            NewWorkedoff, Universal, Existential, Eventualities).
264
265reduce_local([x(Y,dia(star(R),A))|Unexpanded], X, Workedoff, NewWorkedoff,
266        Universal, Existential, Eventualities) :- !,
267%    is_unsatisfiable(_),
268% Remember that (de Giacomo and Massacci, 2001) uses complement splitting at
269% this point. This variant of the calculus does not.
270    get_branch_point_counter(Count),
271    pdl_on_write('In reduce_local, RIGHT branch of X, reduce_local: '), pdl_on_write(Count), pdl_on_nl,
272    increment_branch_point_counter(-1),
273    extend_unexpanded([dia(R,x(Y,dia(star(R),A)))], Workedoff,
274                Unexpanded, NewUnexpanded,
275                X, ['X-RIGHT',x(Y,dia(star(R),A))]),
276    reduce_local(NewUnexpanded, X, [x(Y,dia(star(R),A))|Workedoff],
277            NewWorkedoff, Universal, Existential, Eventualities).
278
279reduce_local([dia(test(A),B)|Unexpanded], X, Workedoff, NewWorkedoff,
280        Universal, Existential, Eventualities) :- !,
281    extend_unexpanded([A,B], Workedoff, Unexpanded, NewUnexpanded,
282                X, ['dia-test',dia(test(A),B)]),
283    reduce_local(NewUnexpanded, X, [dia(test(A),B)|Workedoff],
284            NewWorkedoff, Universal, Existential, Eventualities).
285
286reduce_local([dia(R,A)|Unexpanded], X, Workedoff, NewWorkedoff,
287        Universal, [dia(R,A)|Existential], Eventualities) :- !,
288    atom(R),  % important
289    reduce_local(Unexpanded, X, [dia(R,A)|Workedoff],
290            NewWorkedoff, Universal, Existential, Eventualities).
291
292reduce_local([not(dia(or(R,S),A))|Unexpanded], X, Workedoff, NewWorkedoff,
293        Universal, Existential, Eventualities) :- !,
294    extend_unexpanded([not(dia(R,A)),not(dia(S,A))], Workedoff, Unexpanded, NewUnexpanded,
295                X, ['box-or',not(dia(or(R,S),A))]),
296    reduce_local(NewUnexpanded, X, [not(dia(or(R,S),A))|Workedoff],
297            NewWorkedoff, Universal, Existential, Eventualities).
298
299reduce_local([not(dia(comp(R,S),A))|Unexpanded], X, Workedoff, NewWorkedoff,
300        Universal, Existential, Eventualities) :- !,
301    extend_unexpanded([not(dia(R,dia(S,A)))], Workedoff, Unexpanded, NewUnexpanded,
302                X, ['box-comp',not(dia(comp(R,S),A))]),
303    reduce_local(NewUnexpanded, X, [not(dia(comp(R,S),A))|Workedoff],
304            NewWorkedoff, Universal, Existential, Eventualities).
305
306reduce_local([not(dia(star(R),A))|Unexpanded], X, Workedoff, NewWorkedoff,
307        Universal, Existential, Eventualities) :- !,
308    complement(A, NotA),
309    extend_unexpanded([NotA,not(dia(R,dia(star(R),A)))], Workedoff, Unexpanded, NewUnexpanded,
310                X, ['box-star',not(dia(star(R),A))]),
311    reduce_local(NewUnexpanded, X, [not(dia(star(R),A))|Workedoff],
312            NewWorkedoff, Universal, Existential, Eventualities).
313
314reduce_local([not(dia(test(A),B))|Unexpanded], X, Workedoff, NewWorkedoff,
315        Universal, Existential, Eventualities) :- % no cut
316    complement(A, NotA),
317    get_branch_point_counter(Count),
318    pdl_on_write('In reduce_local, LEFT branch of BOX-TEST, reduce_local: '), pdl_on_write(Count), pdl_on_nl,
319    increment_branch_point_counter(1),
320    extend_unexpanded([NotA], Workedoff, Unexpanded, NewUnexpanded,
321                X, ['box-test-LEFT',not(dia(test(A),B))]),
322    reduce_local(NewUnexpanded, X, [not(dia(test(A),B))|Workedoff],
323            NewWorkedoff, Universal, Existential, Eventualities).
324
325reduce_local([not(dia(test(A),B))|Unexpanded], X, Workedoff, NewWorkedoff,
326        Universal, Existential, Eventualities) :- !,
327%    is_unsatisfiable(_),
328    complement(B, NotB),
329    get_branch_point_counter(Count),
330    pdl_on_write('In reduce_local, RIGHT branch of BOX-TEST, reduce_local: '), pdl_on_write(Count), pdl_on_nl,
331    increment_branch_point_counter(-1),
332    extend_unexpanded([NotB], Workedoff, Unexpanded, NewUnexpanded,
333                X, ['box-test-RIGHT',not(dia(test(A),B))]),
334    reduce_local(NewUnexpanded, X, [not(dia(test(A),B))|Workedoff],
335            NewWorkedoff, Universal, Existential, Eventualities).
336
337reduce_local([not(dia(R,A))|Unexpanded], X, Workedoff, NewWorkedoff,
338        [not(dia(R,A))|Universal], Existential, Eventualities) :- !,
339    atom(R),  % important
340    reduce_local(Unexpanded, X, [not(dia(R,A))|Workedoff],
341            NewWorkedoff, Universal, Existential, Eventualities).
342
343reduce_local([Literal|Unexpanded], X, Workedoff, NewWorkedoff,
344        Universal, Existential, Eventualities) :- !,
345    reduce_local(Unexpanded, X, [Literal|Workedoff],
346            NewWorkedoff, Universal, Existential, Eventualities)```