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)