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 | <a>X
   10%
   11%         A v B
   12%   (v) -------------
   13%         A | -A, B
   14%
   15% 'bcs' is short for 'boolean 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 boolean 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. This version of the calculus does not.
  273    get_branch_point_counter(Count),
  274    pdl_on_write('In reduce_local, RIGHT branch of X, reduce_local: '), pdl_on_write(Count), pdl_on_nl,
  275    increment_branch_point_counter(-1),
  276    extend_unexpanded([dia(R,x(Y,dia(star(R),A)))], Workedoff, 
  277                Unexpanded, NewUnexpanded, 
  278                X, ['X-RIGHT',x(Y,dia(star(R),A))]), 
  279    reduce_local(NewUnexpanded, X, [x(Y,dia(star(R),A))|Workedoff], 
  280            NewWorkedoff, Universal, Existential, Eventualities).
  281
  282reduce_local([dia(test(A),B)|Unexpanded], X, Workedoff, NewWorkedoff,
  283        Universal, Existential, Eventualities) :- !,
  284    extend_unexpanded([A,B], Workedoff, Unexpanded, NewUnexpanded, 
  285                X, ['dia-test',dia(test(A),B)]), 
  286    reduce_local(NewUnexpanded, X, [dia(test(A),B)|Workedoff], 
  287            NewWorkedoff, Universal, Existential, Eventualities).
  288
  289reduce_local([dia(R,A)|Unexpanded], X, Workedoff, NewWorkedoff,
  290        Universal, [dia(R,A)|Existential], Eventualities) :- !,
  291    atom(R),  % important
  292    reduce_local(Unexpanded, X, [dia(R,A)|Workedoff], 
  293            NewWorkedoff, Universal, Existential, Eventualities).
  294
  295reduce_local([not(dia(or(R,S),A))|Unexpanded], X, Workedoff, NewWorkedoff,
  296        Universal, Existential, Eventualities) :- !,
  297    extend_unexpanded([not(dia(R,A)),not(dia(S,A))], Workedoff, Unexpanded, NewUnexpanded, 
  298                X, ['box-or',not(dia(or(R,S),A))]), 
  299    reduce_local(NewUnexpanded, X, [not(dia(or(R,S),A))|Workedoff], 
  300            NewWorkedoff, Universal, Existential, Eventualities).
  301
  302reduce_local([not(dia(comp(R,S),A))|Unexpanded], X, Workedoff, NewWorkedoff,
  303        Universal, Existential, Eventualities) :- !,
  304    extend_unexpanded([not(dia(R,dia(S,A)))], Workedoff, Unexpanded, NewUnexpanded, 
  305                X, ['box-comp',not(dia(comp(R,S),A))]), 
  306    reduce_local(NewUnexpanded, X, [not(dia(comp(R,S),A))|Workedoff], 
  307            NewWorkedoff, Universal, Existential, Eventualities).
  308
  309reduce_local([not(dia(star(R),A))|Unexpanded], X, Workedoff, NewWorkedoff, 
  310        Universal, Existential, Eventualities) :- !,
  311    complement(A, NotA),
  312    extend_unexpanded([NotA,not(dia(R,dia(star(R),A)))], Workedoff, Unexpanded, NewUnexpanded, 
  313                X, ['box-star',not(dia(star(R),A))]), 
  314    reduce_local(NewUnexpanded, X, [not(dia(star(R),A))|Workedoff], 
  315            NewWorkedoff, Universal, Existential, Eventualities).
  316
  317reduce_local([not(dia(test(A),B))|Unexpanded], X, Workedoff, NewWorkedoff, 
  318        Universal, Existential, Eventualities) :- % no cut
  319    complement(A, NotA),
  320    get_branch_point_counter(Count),
  321    pdl_on_write('In reduce_local, LEFT branch of BOX-TEST, reduce_local: '), pdl_on_write(Count), pdl_on_nl,
  322    increment_branch_point_counter(1),
  323    extend_unexpanded([NotA], Workedoff, Unexpanded, NewUnexpanded, 
  324                X, ['box-test-LEFT',not(dia(test(A),B))]), 
  325    reduce_local(NewUnexpanded, X, [not(dia(test(A),B))|Workedoff], 
  326            NewWorkedoff, Universal, Existential, Eventualities).
  327
  328reduce_local([not(dia(test(A),B))|Unexpanded], X, Workedoff, NewWorkedoff,
  329        Universal, Existential, Eventualities) :- !,
  330%    is_unsatisfiable(_),
  331    complement(B, NotB),
  332    get_branch_point_counter(Count),
  333    pdl_on_write('In reduce_local, RIGHT branch of BOX-TEST, reduce_local: '), pdl_on_write(Count), pdl_on_nl,
  334    increment_branch_point_counter(-1),
  335    extend_unexpanded([NotB], Workedoff, Unexpanded, NewUnexpanded, 
  336                X, ['box-test-RIGHT',not(dia(test(A),B))]), 
  337    reduce_local(NewUnexpanded, X, [not(dia(test(A),B))|Workedoff], 
  338            NewWorkedoff, Universal, Existential, Eventualities).
  339
  340reduce_local([not(dia(R,A))|Unexpanded], X, Workedoff, NewWorkedoff, 
  341        [not(dia(R,A))|Universal], Existential, Eventualities) :- !,
  342    atom(R),  % important
  343    reduce_local(Unexpanded, X, [not(dia(R,A))|Workedoff], 
  344            NewWorkedoff, Universal, Existential, Eventualities).
  345
  346reduce_local([Literal|Unexpanded], X, Workedoff, NewWorkedoff,
  347        Universal, Existential, Eventualities) :- !,
  348    reduce_local(Unexpanded, X, [Literal|Workedoff], 
  349            NewWorkedoff, Universal, Existential, Eventualities)