%
%  Symbolic module checking
%

user:file_search_path(common,'../common').
:- ensure_loaded(common(ops)).
:- ensure_loaded(common(def)).

user:file_search_path(bdd,'../bdd').
:- ensure_loaded(bdd(bdd)).
:- ensure_loaded(bdd(bddwrite)).

%
%  Databases.
%    fml_to_atom - Correspondence between TL formulas and BDD atom numbers.
%    num - Generate atom numbers.
%

:- dynamic fml_to_atom/2.
:- dynamic num/1.

symbolic_tableau(F) :-
  retractall(fml_to_atom(_,_)),
  retractall(num(_)),
  assert(num(1)),
  demorgan(F, FN),                  % Push negation inwards.
  tlatom(FN, Atoms, State),         % Create BDD with TL atoms.
  write_formula_list(Atoms), nl,
  tlform(Atoms, Fmls),
  write_formula_list(Fmls), nl,
  write_tl_bdd(State), nl,
  transitions(Fmls, Trans),
  closure(Atoms, State, Trans, Result),
  write_tl_bdd(Result), nl.

%
%  tlatom(Fml, Atoms, BDD)
%    Create temporal logic atoms as BDDs.
%    An atom is a formula which is a literal or
%      whose principal operator is temporal.
%      (1) Next formula is atom.
%      (2) Negation (assume negations are pushed inwards).
%      (3) Formula with non-next temporal operator is an atom,
%          and recurse on subformulas.
%      (4) Boolean operator: recurse to obtain subBDDs and
%          perform apply operation with the operator.
%      (5) Atom.
%
tlatom(next F,  [], BDD) :- !,
  get_atom(next F, A),
  literal(pos, A, BDD).
tlatom(neg F, [neg F], BDD) :- !,
  get_atom(F, A),
  literal(neg, A, BDD).
tlatom(F,   [F | A1], BDD) :-
  F =.. [_, F1], !,
  tlatom(F1, A1, _),
  get_atom(F, A),
  literal(pos, A, BDD).
tlatom(F, A, BDD) :-
  F =.. [Func, F1, F2], !,
  tlatom(F1, A1, BDD1),
  tlatom(F2, A2, BDD2),
  union(A1, A2, A),
  apply(BDD1, Func, BDD2, BDD).
tlatom(F, [F], BDD) :-
  get_atom(F, A),
  literal(pos, A, BDD).

%
%  tlform(Atoms, Fmls)
%    From the atom list, extract a list of non-next temporal formulas.
%
tlform([always F | Tail],  [always F | Tail1])  :- !,
  tlform(Tail, Tail1).
tlform([eventually F | Tail], [eventually F | Tail1]) :- !,
  tlform(Tail, Tail1).
tlform([_ | Tail],   Tail1) :- !,
  tlform(Tail, Tail1).
tlform([], []).

%
%  transitions(Fmls, BDD)
%    BDD is the BDD for the transition conditions on the
%    temporal Fmls.
%  trans(F, BDD)
%    The transitions are: #p <-> p ^ @#p and <>p <-> p v @<>p.
%
transitions([], bdd(leaf, t, x)).   % Start with true.
transitions([F | Tail], BDD) :-
  trans(F, BDD1),                   % Get the BDD for this transition.
  transitions(Tail, BDD2),          % Recurse on list.
  apply(BDD1, and, BDD2, BDD).      % 'and' result with this transition.

trans(always F, BDD) :- 
  get_literal(always F,   B1),
  get_literal(F,    B2),
  get_literal(next always F, B3),
  apply(B2, and, B3, B4),
  apply(B1, eqv, B4, BDD).
trans(eventually F, BDD) :-
  get_literal(eventually F,   B1),
  get_literal(F,     B2),
  get_literal(next eventually F, B3),
  apply(B2, or, B3, B4),
  apply(B1, eqv, B4, BDD).

%
%  closure(Atoms, State, Trans, Result)
%    Create next states until there is no more change.
%    Next state will have 'primed', that is, next formulas.
%    Unprime then and 'or' with current state.
%
closure(Atoms, State, Trans, Result) :-
  next_state(Atoms, State, Trans, NewPrimed), 
  write_tl_bdd(NewPrimed), 
  unprime(NewPrimed, NewNext),
  apply(State, or, NewNext, New),
  ((State = New) ->
    (Result = State) ;
    closure(Atoms, New, Trans, Result)).

%
%  next_state(Atoms, State, Trans, Result)
%    'and' the transitions with the current state.
%  next_state1(Atoms, State and Trans, Result)
%    For each atom, perform an existential quantification
%      on the BDD obtained by 'State and Trans'.
%
next_state(Atoms, State, Trans, Result) :-
  apply(State, and, Trans, ST),
  next_state1(Atoms, ST, Result).

next_state1([], Result, Result).
next_state1([neg F | Tail], State, Result) :- !,
  get_atom(F, A),
  exists(State, A, State1),
  next_state1(Tail, State1, Result).
next_state1([F | Tail], State, Result) :-
  get_atom(F, A),
  exists(State, A, State1),
  next_state1(Tail, State1, Result).

%
%  unprime(BP, BU)
%    BU is unprimed version of BDD BP.
%    After unpriming,
%      convert to formula and back to maintain ordering.
%  unprime1(BP, BU)
%    Remove 'next' from formula.
%
unprime(Primed, Unprimed) :-
  unprime1(Primed, BDD),
  to_fml(BDD, Fml),
  to_bdd(Fml, Unprimed).

unprime1(bdd(leaf, V, x), bdd(leaf, V, x)) :- !.
unprime1(bdd(N, Left, Right), bdd(N1, Left1, Right1)) :-
  get_atom(next F, N),
  get_atom(F,  N1),
  unprime1(Left,  Left1),
  unprime1(Right, Right1).

%
%  to_fml(BDD, Fml)
%    Convert a BDD to a formula Fml on atom numbers
%      (i.e. no temporal operators).
%    Use Shannon decomposition:
%      neg and left child, or, pos and right child.
%    (1-2) Two leaves is a literal.
%    (3-6) One leaf, one non-leaf.
%    (7)   Two non-leaves.
%
to_fml(bdd(F, bdd(leaf, f, x), bdd(leaf, t, x)), F)   :- !.

to_fml(bdd(F, bdd(leaf, t, x), bdd(leaf, f, x)), neg F) :- !.

to_fml(bdd(F, bdd(leaf, t, x), Right), Fml) :- !,
  to_fml(Right, FR),
  Fml = neg F or (F and FR).

to_fml(bdd(F, bdd(leaf, f, x), Right), Fml) :- !,
  to_fml(Right, FR),
  Fml = F and FR.

to_fml(bdd(F, Left, bdd(leaf, t, x)), Fml) :- !,
  to_fml(Left, FL),
  Fml = (neg F and FL) or F.

to_fml(bdd(F, Left, bdd(leaf, f, x)), Fml) :- !,
  to_fml(Left, FL),
  Fml = (neg F and FL).

to_fml(bdd(F, Left, Right), Fml) :-
  to_fml(Left, FL),
  to_fml(Right, FR),
  Fml = ((neg F) and FL) or (F and FR).

%
%  to_bdd(Fml, BDD)
%    Converse of to_fml.
%    (1) Binary operator - apply it.
%    (2) Negation of non-atom - complement.
%    (3-4) Literals.
%
to_bdd(A, B) :-
  A =.. [Func, A1, A2], !,
  to_bdd(A1, B1),
  to_bdd(A2, B2),
  apply(B1, Func, B2, B).
to_bdd(neg A, B) :-
  A =.. [_|_], !,
  to_bdd(A, B1),
  complement(B1, B).
to_bdd(neg A, B) :- !,
  literal(neg, A, B).
to_bdd(A, B)   :-
  literal(pos, A, B).

%
%  get_atom(F, A)
%    F is a formula.
%    Check if its atom is already in the fml_to_atom database.
%    Otherwise, get a new atom number and assert fml_to_atom.
%  get_liternal(F, B)
%    Get a atom for F and construct the corresponding BDD B.
%
get_atom(F, A) :-
  fml_to_atom(F, A), !.
get_atom(F, A) :-
  get_num(A),
  assert(fml_to_atom(F, A)).

get_literal(neg F, B) :- !,
  get_atom(F, A),
  literal(neg, A, B).
get_literal(F, B) :-
  get_atom(F, A),
  literal(pos, A, B).

%
%  get_num(Num) - Increment atom number counter.
%
get_num(Num) :- retract(num(Num)), Num1 is Num+1, assert(num(Num1)).

%
%  write_tl_bdd(B)
%    Write a temporal logic BDD, using write_fml.
%  write_fml(N)
%    Write the TL formula represented by BDD atom N.
%
write_tl_bdd(B) :-
  write_bdd(B, write_fml).

write_fml(N) :-
  fml_to_atom(F, N),
  to_external(F, FE),
  write_formula(FE).