1%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% 2% 3% Copyright 2003, Renate Schmidt, University of Manchester 4% Modified 2009-10, Ullrich Hustadt, University of Manchester 5% 6% Uses 7% X_{<a*>p} 8% (X)-------------- 9% p | -p, <a>X 10% 11% A v B 12% (v) ------------- 13% A | -A, B 14% 15% 'fcs' is short for 'full complement splitting' 16% 17%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% 18 19:-module(pdl_dGM, 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% This version of the calculus uses full complement splitting. So, 184% not(A) is added to the right branch. 185 get_branch_point_counter(Count), 186 pdl_on_write('In reduce_local, RIGHT branch of OR, reduce_local: '), pdl_on_write(Count), pdl_on_nl, 187 increment_branch_point_counter(-1), 188 complement(A, NotA), 189 extend_unexpanded([NotA,B], Workedoff, Unexpanded, NewUnexpanded, 190 X, ['or-RIGHT',or(A,B)]), 191 reduce_local(NewUnexpanded, X, [or(A,B)|Workedoff], 192 NewWorkedoff, Universal, Existential, Eventualities). 193 194% Condition 4 in Definition 23 in (De Giacomo and Massacci, 2000): 195% If both [A|S] and [B|S] are \bot-sets, then [or(A,B)|S] is a \bot-set 196reduce_local([or(A,B)|Unexpanded], _X, Workedoff, _NewWorkedoff, 197 _Universal, _Existential, _Eventualities) :- 198 !, 199% write('both branches of an or have been closed; recording inconsistency'), nl, 200 append([or(A,B)|Unexpanded],Workedoff,Fmls), 201 store_inconsistent(Fmls), 202 fail. 203 204reduce_local([not(or(A,B))|Unexpanded], X, Workedoff, NewWorkedoff, 205 Universal, Existential, Eventualities) :- !, 206 complement(A, NotA), 207 complement(B, NotB), 208 extend_unexpanded([NotA,NotB], Workedoff, Unexpanded, NewUnexpanded, 209 X, ['and',not(or(A,B))]), 210 reduce_local(NewUnexpanded, X, [not(or(A,B))|Workedoff], 211 NewWorkedoff, Universal, Existential, Eventualities). 212 213reduce_local([dia(or(R,S),A)|Unexpanded], X, Workedoff, NewWorkedoff, 214 Universal, Existential, Eventualities) :- % no cut 215 get_branch_point_counter(Count), 216 pdl_on_write('In reduce_local, LEFT branch of DIA-OR, reduce_local: '), pdl_on_write(Count), pdl_on_nl, 217 increment_branch_point_counter(1), 218 extend_unexpanded([dia(R,A)], Workedoff, Unexpanded, NewUnexpanded, 219 X, ['dia-or-LEFT',dia(or(R,S),A)]), 220 reduce_local(NewUnexpanded, X, [dia(or(R,S),A)|Workedoff], 221 NewWorkedoff, Universal, Existential, Eventualities). 222 223reduce_local([dia(or(R,S),A)|Unexpanded], X, Workedoff, NewWorkedoff, 224 Universal, Existential, Eventualities) :- !, 225 % Expand the right branch only when the left one is closed 226% is_unsatisfiable(_), 227% complement(dia(R,A), NotDiaRA), 228 get_branch_point_counter(Count), 229 pdl_on_write('In reduce_local, RIGHT branch of DIA-OR, reduce_local: '), pdl_on_write(Count), pdl_on_nl, 230 increment_branch_point_counter(-1), 231 extend_unexpanded([dia(S,A)], Workedoff, Unexpanded, NewUnexpanded, 232 X, ['dia-or-RIGHT',dia(or(R,S),A)]), 233 reduce_local(NewUnexpanded, X, [dia(or(R,S))|Workedoff], 234 NewWorkedoff, Universal, Existential, Eventualities). 235 236reduce_local([dia(comp(R,S),A)|Unexpanded], X, Workedoff, NewWorkedoff, 237 Universal, Existential, Eventualities) :- !, 238 extend_unexpanded([dia(R,dia(S,A))], Workedoff, Unexpanded, NewUnexpanded, 239 X, ['dia-comp',dia(comp(R,S),A)]), 240 reduce_local(NewUnexpanded, X, [dia(comp(R,S),A)|Workedoff], 241 NewWorkedoff, Universal, Existential, Eventualities). 242 243reduce_local([dia(star(R),A)|Unexpanded], X, Workedoff, NewWorkedoff, 244 Universal, Existential, Eventualities) :- !, 245 extend_unexpanded([x(X,dia(star(R),A))], Workedoff, Unexpanded, NewUnexpanded, 246 X, ['dia-star',dia(star(R),A)]), 247 reduce_local(NewUnexpanded, X, [dia(star(R),A)|Workedoff], 248 NewWorkedoff, Universal, Existential, Eventualities). 249 250%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% 251% Note that (de Giacomo and Massacci, 2001) uses complement splitting when 252% dealing with <A*>F. Thus, on the right branch created for <A*>F, (not F) 253% is true, making it impossible for the current state/world to be the one 254% fulfilling <A*>F. On the other hand, on the left branch, we make F true 255% and <A*>F is fulfilled. We record this by adding fulfilled(...) to the 256% list of (fulfilled) eventualities. 257reduce_local([x(Y,dia(star(R),A))|Unexpanded], X, Workedoff, NewWorkedoff, 258 Universal, Existential, 259 [fulfilled(X, x(Y,dia(star(R),A)))|Eventualities]) :- % no cut 260 get_branch_point_counter(Count), 261 pdl_on_write('In reduce_local, LEFT branch of X, reduce_local: '), pdl_on_write(Count), pdl_on_nl, 262 increment_branch_point_counter(1), 263 extend_unexpanded([A], Workedoff, Unexpanded, NewUnexpanded, 264 X, ['X-LEFT',x(Y,dia(star(R),A))]), 265 reduce_local(NewUnexpanded, X, [x(Y,dia(star(R),A))|Workedoff], 266 NewWorkedoff, Universal, Existential, Eventualities). 267 268reduce_local([x(Y,dia(star(R),A))|Unexpanded], X, Workedoff, NewWorkedoff, 269 Universal, Existential, Eventualities) :- !, 270% is_unsatisfiable(_), 271% Remember that (de Giacomo and Massacci, 2001) uses complement splitting at 272% this point and so does this version of the calculus. 273 complement(A, NotA), 274 get_branch_point_counter(Count), 275 pdl_on_write('In reduce_local, RIGHT branch of X, reduce_local: '), pdl_on_write(Count), pdl_on_nl, 276 increment_branch_point_counter(-1), 277 extend_unexpanded([NotA,dia(R,x(Y,dia(star(R),A)))], Workedoff, 278 Unexpanded, NewUnexpanded, 279 X, ['X-RIGHT',x(Y,dia(star(R),A))]), 280 reduce_local(NewUnexpanded, X, [x(Y,dia(star(R),A))|Workedoff], 281 NewWorkedoff, Universal, Existential, Eventualities). 282 283reduce_local([dia(test(A),B)|Unexpanded], X, Workedoff, NewWorkedoff, 284 Universal, Existential, Eventualities) :- !, 285 extend_unexpanded([A,B], Workedoff, Unexpanded, NewUnexpanded, 286 X, ['dia-test',dia(test(A),B)]), 287 reduce_local(NewUnexpanded, X, [dia(test(A),B)|Workedoff], 288 NewWorkedoff, Universal, Existential, Eventualities). 289 290reduce_local([dia(R,A)|Unexpanded], X, Workedoff, NewWorkedoff, 291 Universal, [dia(R,A)|Existential], Eventualities) :- !, 292 atom(R), % important 293 reduce_local(Unexpanded, X, [dia(R,A)|Workedoff], 294 NewWorkedoff, Universal, Existential, Eventualities). 295 296reduce_local([not(dia(or(R,S),A))|Unexpanded], X, Workedoff, NewWorkedoff, 297 Universal, Existential, Eventualities) :- !, 298 extend_unexpanded([not(dia(R,A)),not(dia(S,A))], Workedoff, Unexpanded, NewUnexpanded, 299 X, ['box-or',not(dia(or(R,S),A))]), 300 reduce_local(NewUnexpanded, X, [not(dia(or(R,S),A))|Workedoff], 301 NewWorkedoff, Universal, Existential, Eventualities). 302 303reduce_local([not(dia(comp(R,S),A))|Unexpanded], X, Workedoff, NewWorkedoff, 304 Universal, Existential, Eventualities) :- !, 305 extend_unexpanded([not(dia(R,dia(S,A)))], Workedoff, Unexpanded, NewUnexpanded, 306 X, ['box-comp',not(dia(comp(R,S),A))]), 307 reduce_local(NewUnexpanded, X, [not(dia(comp(R,S),A))|Workedoff], 308 NewWorkedoff, Universal, Existential, Eventualities). 309 310reduce_local([not(dia(star(R),A))|Unexpanded], X, Workedoff, NewWorkedoff, 311 Universal, Existential, Eventualities) :- !, 312 complement(A, NotA), 313 extend_unexpanded([NotA,not(dia(R,dia(star(R),A)))], Workedoff, Unexpanded, NewUnexpanded, 314 X, ['box-star',not(dia(star(R),A))]), 315 reduce_local(NewUnexpanded, X, [not(dia(star(R),A))|Workedoff], 316 NewWorkedoff, Universal, Existential, Eventualities). 317 318reduce_local([not(dia(test(A),B))|Unexpanded], X, Workedoff, NewWorkedoff, 319 Universal, Existential, Eventualities) :- % no cut 320 complement(A, NotA), 321 get_branch_point_counter(Count), 322 pdl_on_write('In reduce_local, LEFT branch of BOX-TEST, reduce_local: '), pdl_on_write(Count), pdl_on_nl, 323 increment_branch_point_counter(1), 324 extend_unexpanded([NotA], Workedoff, Unexpanded, NewUnexpanded, 325 X, ['box-test-LEFT',not(dia(test(A),B))]), 326 reduce_local(NewUnexpanded, X, [not(dia(test(A),B))|Workedoff], 327 NewWorkedoff, Universal, Existential, Eventualities). 328 329reduce_local([not(dia(test(A),B))|Unexpanded], X, Workedoff, NewWorkedoff, 330 Universal, Existential, Eventualities) :- !, 331% is_unsatisfiable(_), 332 complement(B, NotB), 333 get_branch_point_counter(Count), 334 pdl_on_write('In reduce_local, RIGHT branch of BOX-TEST, reduce_local: '), pdl_on_write(Count), pdl_on_nl, 335 increment_branch_point_counter(-1), 336 extend_unexpanded([NotB], Workedoff, Unexpanded, NewUnexpanded, 337 X, ['box-test-RIGHT',not(dia(test(A),B))]), 338 reduce_local(NewUnexpanded, X, [not(dia(test(A),B))|Workedoff], 339 NewWorkedoff, Universal, Existential, Eventualities). 340 341reduce_local([not(dia(R,A))|Unexpanded], X, Workedoff, NewWorkedoff, 342 [not(dia(R,A))|Universal], Existential, Eventualities) :- !, 343 atom(R), % important 344 reduce_local(Unexpanded, X, [not(dia(R,A))|Workedoff], 345 NewWorkedoff, Universal, Existential, Eventualities). 346 347reduce_local([Literal|Unexpanded], X, Workedoff, NewWorkedoff, 348 Universal, Existential, Eventualities) :- !, 349 reduce_local(Unexpanded, X, [Literal|Workedoff], 350 NewWorkedoff, Universal, Existential, Eventualities)