% BIOCHAM system http://contraintes.inria.fr/BIOCHAM/
% Copyright 2004-2006, INRIA, Projet Contraintes
%
% This program is free software; you can redistribute it and/or
% modify it under the terms of the GNU General Public License
% as published by the Free Software Foundation; either version 2
% of the License, or (at your option) any later version.
% 
% This program is distributed in the hope that it will be useful,
% but WITHOUT ANY WARRANTY; without even the implied warranty of
% MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
% GNU General Public License for more details.
% 
% You should have received a copy of the GNU General Public License
% along with this program; if not, write to the Free Software
% Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA  02111-1307, USA.
%
% GNU prolog file ctl.pl by François Fages

%%% A CTL model checker for state transition systems in Prolog
% Can be used on systems generated from BIOCHAM by export_prolog
% currently restricted to flat CTL formula without X
% plus some ad hoc CTL* treatment of oscillation properties

% assumes the following facts and clauses :
% dimension(N).
% state(name1,...,nameN).
% initial(state(v1,...,vN)).
% transition(state(v1,...,vN),state(w1,...,wN)).
% ctl_spec(formula).

% the values of a variable in a state can be
% 0 absent
% 1 present
% a absent or present as wished
% c absent or present unknown

% evaluates CTL queries by computing a frontier of forward and backward states 
% where a state S is given with its instance SI obtained by replacing variables by constant a
% fw(S,SI)
% bw(S,SI)

:- dynamic(initial/1). % initial state
:- dynamic(fw/2). % forward reachable states
:- dynamic(bw/2). % backward reachable states
:- dynamic(fm/1). % forward mask
:- dynamic(bm/1). % backward mask

%%% TODO
% boolean constraints on states
% imbrication ? normal forms ?
% algo for CTL* ?

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Checking of a complete CTL specification given with facts ctl(F)

check_all:-
    ctl(F),
    (ctl_check(F)
     ->
     write(F),write(' is true.'),nl,fail
     ;
     write(F),write(' is false.'),nl
     ).

ctl_init:-
    retractall(fm(_)),
    retractall(bm(_)),
    retractall(fw(_,_)),
    retractall(bw(_,_)).

% Forward analysis : compute the reachable states from S

forward_reachable:-
    initial(S),
    forward_reachable(S).

forward_reachable(S):-
    ctl_init,
    state_instance(S,SI),
    asserta(fw(S,SI)),
    asserta(fm(_)),
    fwEU.
forward_reachable(_):-
    retractall(fw(stop,stop)),
    fw(_,S),
    write(S),nl,
    fail.

% Backward analysis : compute the predecessor states of S

backward_reachable:-
    initial(S),
    backward_reachable(S).

backward_reachable(S):-
    ctl_init,
    state_instance(S,SI),
    asserta(bw(S,SI)),
    asserta(bm(_)),
    bwEU.
backward_reachable(_):-
    retractall(bw(stop,stop)),
    bw(_,S),
    write(S),nl,
    fail.

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% replaces the variables in a state by constant a

state_instance(S,SI):-
    S=..[O|L],
    findall(X,state_instanciated(L,X),LI),
    SI=..[O|LI].

state_instanciated([X|_],X):-
    ((X=a)
     ->
     true
     ;
     true).
state_instanciated([_|L],Y):-
    state_instanciated(L,Y).
    
% relaces the variables in a state by C (used for Ai)
state_instance(S,SI,C):-
    S=..[O|L],
    findall(X,state_instanciated(L,X,C),LI),
    SI=..[O|LI].

state_instanciated([X|_],X,C):-
    ((X=C)
     ->
     true
     ;
     true).
state_instanciated([_|L],Y,C):-
    state_instanciated(L,Y,C).
    
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% CTL model-checking with Ei (for some initial state) and Ai (for all)

ctl_check('Ei'(F)):- !,
    ctl_init,
    initial(S),
    state_instance(S,SI),
    asserta(fw(S,SI)),
    ctl_form(F).

ctl_check('Ai'(F)):- !,
    ctl_init,
    initial(S),
    state_instance(S,SI,c), % Skolem constant c (could be 0 for monotonic transition systems)
    asserta(fw(SI,SI)),
    ctl_form(F).

ctl_check(F):-
    write('Warning : no prefix, "for some initial state" assumed '),write('Ei'(F)),nl,
    ctl_check('Ei'(F)).

% copy operation on bw -> bw2

copy_bw:-
	retractall(bw2(_,_)),
	bw(X,Y),
	assertz(bw2(X,Y)),
	fail.
copy_bw:-
        retractall(bw(_,_)).

% CTL* formulas
% Oscillation property approximated in CTL as AG(!P->EF(P) & P->EF(!P)
% expressed here in CTL* as EG(F(!P)&F(P))
% by a forward EG computation with mask F(alternation on P) computed backward

%ctl_form('AG'('&'('->'(F,'EF'('!'(F))),'->'('!'(F),'EF'(F))))):- !,
%    ctl_form(oscil(F)).

ctl_form(oscil(F)):- !,
   ctl_form(loop(F,'!'(F))).

%ctl_form(oscil(F)):- !, 
%    ctl_state(F,S),
%    ctl_state('!'(F),T),
%    forall(transition(S,T),add_checkbw(S)), % alternation F -> !F
%    forall(transition(T,S),add_checkbw(T)), % alternation !F -> F
% FAUX !!!! prendre le et des F( alternation) pas le ou
%    fw(A,B),
%    retractall(fw(_,_)), % hack the initial state not to use it as mask in bwEU
%    asserta(bm(_)),
%    (bwEU;true), % complete set of states leading to one alternation of F
%    retractall(bw(stop,stop)),
%    asserta((fm(X):-bw(X,_),!)), % backward states used as mask
%    retractall(fw(_,_)),
%    asserta(fw(A,B)), % restores the initial state
%    fwEG.

% Loop property between two states X and Y
% approximated in CTL as AG(X->EF(Y) & Y-> EF(X))
% expresseded here in CTL* as EG(F X & F Y)

ctl_form(loop(F,G)):- !,
    %ctl_form('AG'('&'('->'(F,'EF'(G)),'->'(G,'EF'(F))))).
    ctl_state(F,S),
    ctl_state(G,T),
    fw(A,B),
    retractall(fw(_,_)), % hack the initial state not to use it as mask in bwEU
    add_checkbw(S),
    asserta(bm(_)),
    (bwEU;true), % complete set of states leading to F
    retractall(bw(stop,stop)),
    copy_bw, 
    add_checkbw(T),
    asserta(bm(_)),
    (bwEU;true), % complete set of states leading to G
    retractall(bw(stop,stop)),
    asserta((fm(X):-bw(X,_),bw2(X,_),!)), % conjunction of backward states used as mask
    retractall(fw(_,_)),
    asserta(fw(A,B)), % restores the initial state
    fwEG.% FAUX car je peux rester sur un chemin qui *peut* conduire a F et G sans le faire

ctl_form(reachable(F)):- !,
    ctl_form('EF'(F)).

ctl_form(stable(F)):- !,
    ctl_form('AG'(F)).

ctl_form(steady(F)):- !,
    ctl_form('EG'(F)).

ctl_form('AG'('->'('!'(Y),checkpoint(X,Y)))):- !,
    write('Warning : formula AG(!Y -> checkpoint(X,Y)) treated as checkpoint(X,Y)'),nl,
    ctl_form(checkpoint(X,Y)).

ctl_form(checkpoint(X,Y)):- !,
    \+ ctl_form('E'('U'('!'(X),Y))).

ctl_form('EF'(F)):- !,
    ctl_form('E'('U'(true,F))).
%    ctl_state(F,S),
%    state_instance(S,SI),
%    asserta(bw(S,SI)),
%    fwbwEF. % better than fwEF

ctl_form('EG'(F)):- !,
%    ctl_form('E'('W'('!'(F),false))).
    ctl_state(F,S),
    asserta(fm(S)),
    fwEG.

ctl_form('E'('U'(F,G))):- !,
     ctl_state(G,T),
     state_instance(T,TI),
    (ctl_state(F,S)  % not false
     ->
     asserta(fm(S)), % forward mask
     asserta(bm(S)), % backward mask as forward mask !
     asserta(bw(T,TI)), 
     fwbwEU
     ;
     fw(TI,_)). % G true in the initial state

ctl_form('E'('W'(F,G))):- !,
    ctl_state(F,S), % failure if false
    asserta(fm(S)), % forward mask
    (ctl_state(G,T)
     ->
     state_instance(T,TI),
     asserta(bw(T,TI)),
     S=T,            % backward mask as the conjunction of fw bw masks
     asserta(bm(S)),
     fwEW            % should better use fwbwEW.
     ;
     fwEG).

ctl_form('AF'(F)):- !,
    \+ ctl_form('EG'('!'(F))).

ctl_form('AG'(F)):- !,
    \+ ctl_form('EF'('!'(F))).

% 'X' and imbricated formulas not implemented yet
ctl_form(F):-
    ctl_state(F,S),
    fw(S,_). % success if true in initial state


% Boolean formula over states

ctl_state('&'(A,B),S):- !,
    ctl_state(A,S),
    ctl_state(B,S).

ctl_state('!'(A),S):- !,
    ctl_state(A,T),
    xor_state(T,S).

ctl_state(true,S):- !,
    dimension(N),
    functor(S,state,N).

% ctl_state(false,_):- !, fail.
ctl_state(false,false):- !. % NOT SURE WHAT TO DO

ctl_state(I,S):- integer(I), !,
    dimension(N),
    functor(S,state,N),
    arg(I,S,1).

ctl_state(F,_):-
    write('Warning : formula not implemented '),write(F),nl,
    fail.

% exchange 0 and 1 leaving variables in states

xor_state(S,T):-
    S=..[A|L],
    xor_list(L,K),
    T=..[A|K].

xor_list([],[]).
xor_list([V|L],[U|K]):-
    ctl_xor(V,U),
    xor_list(L,K).

ctl_xor(V,U):-
    var(V),var(U),!,
    V=U.
ctl_xor(0,1).
ctl_xor(1,0).
ctl_xor(a,c). % not sure !
ctl_xor(c,a).

% forall X satisfying P do Q for side effects

forall(P,Q):- P, Q, fail.
forall(_,_).


%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%% Computation of fw and bw frontiers

% add R to forward states
add_fw(R):-
    state_instance(R,RI),
    add_fw(R,RI).

add_fw(R,RI):-
    elim_fw(R),
    asserta(fw(R,RI)).  % new states in front

% add R to forward states checking not already in
add_checkfw(R):-
    state_instance(R,RI),
    (fw(RI,_)
     ->
     true
     ;
     add_fw(R,RI)).

% eliminate the forward states subsumed by R
elim_fw(R):-
    fw(S,R), % then R subsumes S
    retractall(fw(S,_)),
    fail.
elim_fw(_).

% add R to backward states
add_bw(R):-
    state_instance(R,RI),
    add_bw(R,RI).

add_bw(R,RI):-
    elim_bw(R),
    asserta(bw(R,RI)).  % new states in front

% add R to backward states checking not already in
add_checkbw(R):-
    state_instance(R,RI),
    (bw(RI,_)
     ->
     true
     ;
     add_bw(R,RI)).

% eliminate the backward states subsumed by R
elim_bw(R):-
    bw(S,R), % then R subsumes S
    retractall(bw(S,_)),
    fail.
elim_bw(_).

% is R in backward states ?
is_bw(R):-
    state_instance(R,RI),
    bw(RI,_).

% is R in forward states ?
is_fw(R):-
    state_instance(R,RI),
    fw(RI,_).

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Forward saturation with fm mask until reaching a bw state

fwEU:-
    fw(S,_),
    fm(S),   % initial failure if S does not unify with the mask
    fwEUa.

fwEUa:-
    fw(S,_),
    bw(S,_). % initial success if S unifies with a backward state
fwEUa:-
    fwEUb.

fwEUb:-fwEUc.
fwEUb:-
    fw(S,_),
    !,
    ((S=stop) -> fail ; fwEUb).

% assert does not impact the current goals
% hence the complication with first and stop markers...
fwEUc:-
    asserta(fw(first,first)),
    fw(S,_),
    ((S=stop)
     ->
     !, fail
     ;
     ((S=first)
      ->
      retractall(fw(first,_)),
      asserta(fw(stop,stop)),
      fail
      ;
      transition(S,R),
      fm(R),
      (bw(R,_)  % success if R unifies with a backward state
       ->
       !,
       asserta(fw(stop,stop)),
       asserta(bw(stop,stop))
       ;
       add_checkfw(R),
       fail
       )
      )
     ).

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Backward saturation with bm mask until reaching a fw state
% simply exchange fw with bw in fwEU code plus transition(R,S)

bwEU:-
    bw(S,_),
    bm(S),   % initial failure if S does not unify with the mask
    bwEUa.

bwEUa:-
    bw(S,_),
    fw(S,_). % initial success if S unifies with a forward state
bwEUa:-
    bwEUb.

bwEUb:-bwEUc.
bwEUb:-
    bw(S,_),
    !,
    ((S=stop) -> fail ; bwEUb).

bwEUc:-
    asserta(bw(first,first)),
    bw(S,_),
    ((S=stop)
     ->
     !, fail
     ;
     ((S=first)
      ->
      retractall(bw(first,_)),
      asserta(bw(stop,stop)),
      fail
      ;
      transition(R,S),
      bm(R),
      (fw(R,_)  % success if R unifies with a backward state
       ->
       !,
       asserta(fw(stop,stop)),
       asserta(bw(stop,stop))
       ;
       add_checkbw(R),
       fail
       )
      )
     ).

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Forward-backward saturation with fm and bm masks
% until reaching a common state

fwbwEU:-
    fw(S,_),
    fm(S),
    bw(T,_),
    bm(T),
    fwbwEUa.

fwbwEUa:-
    fw(S,_),
    bw(S,_). % initial success if S unifies with a backward state
fwbwEUa:-
    fwbwEUb.

fwbwEUb:-fwEUc.
fwbwEUb:-bwEUc.
fwbwEUb:-
    fw(S,_),
    bw(R,_),
    !,
    (S=stop
     ->
     (R=stop
      ->
      fail
      ;
      bwEUb)
     ;
     (R=stop
      ->
      fwEUb
      ;
      fwbwEUb)).

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% fwEG computes a fw set with fm mask until looping in the set

fwEG:-
    fw(S,_),
    fm(S), % initial failure if the initial state does not satisfy the mask
    fwEGb.

fwEGb:-fwEGc.
fwEGb:-
    fw(S,_),
    !,
    ((S=stop) -> fail ; fwEGb).

fwEGc:-
    asserta(fw(first,first)),
    fw(S,_),
    ((S=stop)
     ->
     !, fail % no loop
     ;
     ((S=first)
      ->
      retractall(fw(first,_)),
      asserta(fw(stop,stop)),
      fail
      ;
      transition(S,R),
      fm(R),  % R needs satisfy the formula
      (fw(R,_)  % success if R creates a loop
       ->
       !, true
       ;
       add_checkfw(R), 
       fail
       )
      )
     ).

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% fwEW computes a fw set satisfying fm until looping or reaching bw
% (simply replace EG by EW in previous code and add success check on bw)
% fwbwEW would be more efficient

fwEW:-
    fw(S,_),
    fm(S), % initial failure if the initial state does not satisfy the mask
    fwEWb.

fwEWb:-fwEWc.
fwEWb:-
    fw(S,_),
    !,
    ((S=stop) -> fail ; fwEWb).

fwEWc:-
    asserta(fw(first,first)),
    fw(S,_),
    ((S=stop)
     ->
     !, fail % no loop
     ;
     ((S=first)
      ->
      retractall(fw(first,_)),
      asserta(fw(stop,stop)),
      fail
      ;
      transition(S,R),
      fm(R),  % R needs satisfy the formula
      ((fw(R,_);bw(R,_))  % success if R creates a loop or reaches bw
       ->
       !, true
       ;
       add_checkfw(R), 
       fail
       )
      )
     ).

    



