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 | -p, <a>X
   10%
   11%         A v B
   12%   (v) -------------
   13%         A | B
   14%
   15%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
   16
   17:-module(pdl_dGM, 
   18    [
   19        eventualities/2,
   20        simplify_X/2,
   21        reduce_local/9
   22    ]).   23
   24:- dynamic
   25        eventualities/2,
   26        simplify_X/2,
   27        reduce_local/9.   28
   29%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
   30
   31eventualities([], []).
   32
   33eventualities([pr(State,FmlList)|Branch], Eventualities) :-
   34    eventualities_fml(State,FmlList, Eventualities1), !,
   35    eventualities(Branch, Eventualities2),
   36    sort(Eventualities1, SortedEventualities1),
   37    sort(Eventualities2, SortedEventualities2),
   38    merge_set(SortedEventualities1, SortedEventualities2, Eventualities).
   39eventualities([isCopyOf(_,_)|Branch], Eventualities) :-
   40    eventualities(Branch, Eventualities).
   41
   42eventualities_fml(_,[], []).
   43
   44eventualities_fml(State, [Fml|FmlList], Eventualities) :-
   45    eventualities_fml(State, Fml, Eventualities1), !,
   46    eventualities_fml(State, FmlList, Eventualities2),
   47    sort(Eventualities1, SortedEventualities1),
   48    sort(Eventualities2, SortedEventualities2),
   49    merge_set(SortedEventualities1, SortedEventualities2, Eventualities).
   50    
   51eventualities_fml(State, x(X,Fml), [ev(State,x(X,Fml))|Eventualities]) :-
   52    eventualities_fml(State, Fml, Eventualities).
   53
   54%eventualities_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%
   61%eventualities_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%
   68%eventualities_fml(not(A), Eventualities) :-
   69%    eventualities_fml(A, Eventualities).
   70%
   71%eventualities_fml(test(A), Eventualities) :-
   72%    eventualities_fml(A, Eventualities).
   73%
   74%eventualities_fml(star(R), Eventualities) :-
   75%    eventualities_fml(R, Eventualities).
   76%
   77%eventualities_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%
   84%eventualities_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%
   91%eventualities_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, [], [], [], DT, DT).
  152
  153reduce_local([true|Unexpanded], X, Workedoff, NewWorkedoff, 
  154        Universal, Existential, Eventualities, IDT, ODT) :- !,
  155    extend_unexpanded([true], Workedoff, Unexpanded, NewUnexpanded, X, true),
  156    reduce_local(NewUnexpanded, X, [true|Workedoff], 
  157            NewWorkedoff, Universal, Existential, Eventualities, IDT, ODT).
  158
  159reduce_local([or(A,B)|Unexpanded], X, Workedoff, NewWorkedoff,
  160        Universal, Existential, Eventualities, IDT, ODT) :- 
  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, [l|IDT], ODT).
  176
  177reduce_local([or(A,B)|Unexpanded], X, Workedoff, NewWorkedoff,
  178        Universal, Existential, Eventualities, IDT, ODT) :- 
  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, [r|IDT], ODT).
  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, _IDT, _ODT) :- 
  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, IDT, ODT) :- !,
  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, IDT, ODT).
  209
  210reduce_local([dia(or(R,S),A)|Unexpanded], X, Workedoff, NewWorkedoff,
  211        Universal, Existential, Eventualities, IDT, ODT) :- % 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, [l|IDT], ODT).
  219
  220reduce_local([dia(or(R,S),A)|Unexpanded], X, Workedoff, NewWorkedoff,
  221        Universal, Existential, Eventualities, IDT, ODT) :- !,
  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, [r|IDT], ODT).
  232
  233reduce_local([dia(comp(R,S),A)|Unexpanded], X, Workedoff, NewWorkedoff, 
  234        Universal, Existential, Eventualities, IDT, ODT) :- !,
  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, IDT, ODT).
  239
  240reduce_local([dia(star(R),A)|Unexpanded], X, Workedoff, NewWorkedoff, 
  241        Universal, Existential, Eventualities, IDT, ODT) :- !,
  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, IDT, ODT).
  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], IDT, ODT) :- % 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, [l|IDT], ODT).
  264
  265reduce_local([x(Y,dia(star(R),A))|Unexpanded], X, Workedoff, NewWorkedoff, 
  266        Universal, Existential, Eventualities, IDT, ODT) :- !,
  267%    is_unsatisfiable(_),
  268% Remember that (de Giacomo and Massacci, 2001) uses complement splitting at
  269% this point.
  270    complement(A, NotA),
  271    get_branch_point_counter(Count),
  272    pdl_on_write('In reduce_local, RIGHT branch of X, reduce_local: '), pdl_on_write(Count), pdl_on_nl,
  273    increment_branch_point_counter(-1),
  274    extend_unexpanded([NotA,dia(R,x(Y,dia(star(R),A)))], Workedoff, 
  275                Unexpanded, NewUnexpanded, 
  276                X, ['X-RIGHT',x(Y,dia(star(R),A))]), 
  277    reduce_local(NewUnexpanded, X, [x(Y,dia(star(R),A))|Workedoff], 
  278            NewWorkedoff, Universal, Existential, Eventualities, [r|IDT], ODT).
  279
  280reduce_local([dia(test(A),B)|Unexpanded], X, Workedoff, NewWorkedoff,
  281        Universal, Existential, Eventualities, IDT, ODT) :- !,
  282    extend_unexpanded([A,B], Workedoff, Unexpanded, NewUnexpanded, 
  283                X, ['dia-test',dia(test(A),B)]), 
  284    reduce_local(NewUnexpanded, X, [dia(test(A),B)|Workedoff], 
  285            NewWorkedoff, Universal, Existential, Eventualities, IDT, ODT).
  286
  287reduce_local([dia(R,A)|Unexpanded], X, Workedoff, NewWorkedoff,
  288        Universal, [dia(R,A)|Existential], Eventualities, IDT, ODT) :- !,
  289    atom(R),  % important
  290    reduce_local(Unexpanded, X, [dia(R,A)|Workedoff], 
  291            NewWorkedoff, Universal, Existential, Eventualities, IDT, ODT).
  292
  293reduce_local([not(dia(or(R,S),A))|Unexpanded], X, Workedoff, NewWorkedoff,
  294        Universal, Existential, Eventualities, IDT, ODT) :- !,
  295    extend_unexpanded([not(dia(R,A)),not(dia(S,A))], Workedoff, Unexpanded, NewUnexpanded, 
  296                X, ['box-or',not(dia(or(R,S),A))]), 
  297    reduce_local(NewUnexpanded, X, [not(dia(or(R,S),A))|Workedoff], 
  298            NewWorkedoff, Universal, Existential, Eventualities, IDT, ODT).
  299
  300reduce_local([not(dia(comp(R,S),A))|Unexpanded], X, Workedoff, NewWorkedoff,
  301        Universal, Existential, Eventualities, IDT, ODT) :- !,
  302    extend_unexpanded([not(dia(R,dia(S,A)))], Workedoff, Unexpanded, NewUnexpanded, 
  303                X, ['box-comp',not(dia(comp(R,S),A))]), 
  304    reduce_local(NewUnexpanded, X, [not(dia(comp(R,S),A))|Workedoff], 
  305            NewWorkedoff, Universal, Existential, Eventualities, IDT, ODT).
  306
  307reduce_local([not(dia(star(R),A))|Unexpanded], X, Workedoff, NewWorkedoff, 
  308        Universal, Existential, Eventualities, IDT, ODT) :- !,
  309    complement(A, NotA),
  310    extend_unexpanded([NotA,not(dia(R,dia(star(R),A)))], Workedoff, Unexpanded, NewUnexpanded, 
  311                X, ['box-star',not(dia(star(R),A))]), 
  312    reduce_local(NewUnexpanded, X, [not(dia(star(R),A))|Workedoff], 
  313            NewWorkedoff, Universal, Existential, Eventualities, IDT, ODT).
  314
  315reduce_local([not(dia(test(A),B))|Unexpanded], X, Workedoff, NewWorkedoff, 
  316        Universal, Existential, Eventualities, IDT, ODT) :- % no cut
  317    complement(A, NotA),
  318    get_branch_point_counter(Count),
  319    pdl_on_write('In reduce_local, LEFT branch of BOX-TEST, reduce_local: '), pdl_on_write(Count), pdl_on_nl,
  320    increment_branch_point_counter(1),
  321    extend_unexpanded([NotA], Workedoff, Unexpanded, NewUnexpanded, 
  322                X, ['box-test-LEFT',not(dia(test(A),B))]), 
  323    reduce_local(NewUnexpanded, X, [not(dia(test(A),B))|Workedoff], 
  324            NewWorkedoff, Universal, Existential, Eventualities, [l|IDT], ODT).
  325
  326reduce_local([not(dia(test(A),B))|Unexpanded], X, Workedoff, NewWorkedoff,
  327        Universal, Existential, Eventualities, IDT, ODT) :- !,
  328%    is_unsatisfiable(_),
  329    complement(B, NotB),
  330    get_branch_point_counter(Count),
  331    pdl_on_write('In reduce_local, RIGHT branch of BOX-TEST, reduce_local: '), pdl_on_write(Count), pdl_on_nl,
  332    increment_branch_point_counter(-1),
  333    extend_unexpanded([NotB], Workedoff, Unexpanded, NewUnexpanded, 
  334                X, ['box-test-RIGHT',not(dia(test(A),B))]), 
  335    reduce_local(NewUnexpanded, X, [not(dia(test(A),B))|Workedoff], 
  336            NewWorkedoff, Universal, Existential, Eventualities, [r|IDT], ODT).
  337
  338reduce_local([not(dia(R,A))|Unexpanded], X, Workedoff, NewWorkedoff, 
  339        [not(dia(R,A))|Universal], Existential, Eventualities, IDT, ODT) :- !,
  340    atom(R),  % important
  341    reduce_local(Unexpanded, X, [not(dia(R,A))|Workedoff], 
  342            NewWorkedoff, Universal, Existential, Eventualities, IDT, ODT).
  343
  344reduce_local([Literal|Unexpanded], X, Workedoff, NewWorkedoff,
  345        Universal, Existential, Eventualities, IDT, ODT) :- !,
  346    reduce_local(Unexpanded, X, [Literal|Workedoff], 
  347            NewWorkedoff, Universal, Existential, Eventualities, IDT, ODT)