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)