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)