flow

add_init_edges :- events(L), add_init_edges(L).

add_init_edges([]).

add_init_edges(['INITIALISATION'|T]) :- !, add_init_edges(T).

add_init_edges([H|T]) :- H\='INITIALISATION',(wp('INITIALISATION',H,_)->true;add_wp('INITIALISATION',H,[])),add_init_edges(T).

add_wp(S,D,TypedPred) :-
    assertz( wp_typed(S,D,TypedPred) ).

assert_guards([],_).

assert_guards([H|T],E) :- get_texpr_expr(H,truth),!, assert_guards(T,E).

assert_guards([H|T],E) :- get_texpr_expr(H,HR),
    HR =.. [Op,X,Y],!, (keep(Op) -> assert_pred_guard(Op,X,Y);true), assert_guards(T,E).

assert_guards([H|_],_) :- add_error(flow,'Cannot normalize: ',H),fail.

assert_pred(Op,X,Y) :- %print(try(Op,X,Y)),nl,
    pred(Op,X,Y) -> true
    ; (assertz(pred_grd(X,Op,Y)), %print(pred_grd(Op,X,Y)),nl,
    assertz(pred_new(X,Op,Y)),
    (change -> true ; assertz(change)),
   
    %nl,print(check_inconsistent(Op,X,Y)),nl,
   
    (inconsistent_fact(Op,X,Y) -> (assertz(inconsistent), print('INCONSISTENT'), nl) ; true),
    ((sym(Op),X\=Y)
    -> assertz(pred_grd(Y,Op,X)), assertz(pred_new(X,Op,Y)) ; true)).

assert_pred_guard(Op,Y,Z) :-
    pred_guard(Y,Op,Z) -> true
    ; assertz(pred_guard(Y,Op,Z)),
    ((sym(Op),Z\=Y) -> assertz(pred_guard(Z,Op,Y)) ; true).

assert_pred_inv(Op,Y,Z) :-
    pred_inv(Y,Op,Z) -> true
    ; assertz(pred_inv(Y,Op,Z)),
    ((sym(Op),Z\=Y) -> assertz(pred_inv(Z,Op,Y)) ; true).

backward_analysis(Event) :- build_enable_graph,
    print_flow_automaton(Event).

build_base_guide :- findall((S,D,P),wp(S,D,P),L), build_base_guide(L).

build_base_guide([]).

build_base_guide([(S,D,P)|T]) :- (false_predicate(P) -> true; assertz(guide_wp(S,D,P))), build_base_guide(T).

build_enable_graph :- (done_flow(enable_graph) -> true;
    ((print('Computing enable_graph'),nl,
    enumerate_events,
    prepare_input,
    find_contradictions,
    add_init_edges,
    law_of_motion,
    build_base_guide,
    print('Done'),nl)
    -> assertz(done_flow(enable_graph))
    ; add_error(flow,'Could not build enable_graph'),fail)).

build_guide(E,RV) :- guide_dfs([E],RV), retractall(event_wp(_,_,_)),filter_from_guide(RV).

calculate_flow_automaton([],A,A).

calculate_flow_automaton([H|T],A,R) :- findall((S,P),(wp(S,H,P), \+false_predicate(P)),L), append(L,A,NA), calculate_flow_automaton(T,NA,R).

combine(equal,X,X).

combine(less_equal,less,less).

combine(less_equal,less_equal,less_equal).

combine(less,less,less).

combine(greater,greater,greater).

combine(greater_equal,greater,greater).

combine(greater_equal,greater_equal,greater_equal).

combine(subset_strict,subset_strict,subset_strict).

create_enable_graph(X):- build_enable_graph,
    print_single_enable_graph(X,wp).

create_enable_graphs(X):- build_enable_graph,
    print_multiple_enable_graphs(X).

dot_edge([]).

dot_edge([(S,D,P)|T]) :- eventnumber(S,SN), eventnumber(D,DN), format_edge(SN,DN,P), dot_edge(T).

dot_footer :- print('}').

dot_header(Name) :- print('digraph '), print(Name),print(' {'),nl.

dot_node([]).

dot_node([S|T]) :- eventnumber(S,C), format_node(C,S), dot_node(T).

enumerate_events :- reset_count, events(L), enumerate_events(L).

enumerate_events([]).

enumerate_events([S|T]) :- count(C), assertz(eventnumber(S,C)), inc, enumerate_events(T).

events(['INITIALISATION'|L]) :- findall(OperationName, b_top_level_operation(OperationName), L).

false_predicate([b(boolean_false,boolean,[nodeid(none)])]).

filter_from_guide(V) :- guide_wp(S,D,P), member(S,V), member(D,V), assertz(event_wp(S,D,P)), fail.

filter_from_guide(_).

find_contradictions :- findall((S,D,P), wp(S,D,P), L), clear_wp, find_contradictions(L).

find_contradictions([]).

find_contradictions([(S,D,P)|T]) :- retractall(inconsistent),
    retractall(pred_grd(_,_,_)),
    retractall(pred_new(_,_,_)),
    retractall(pred_guard(_,_,_)),
    normalize_guards(S),
    find_contradictions2(P),
    (inconsistent -> false_predicate(F), add_wp(S,D,F)
    ; (simplify(P,PR), add_wp(S,D,PR))),
    find_contradictions(T).

find_contradictions2([]).

find_contradictions2([H|_]) :- get_texpr_expr(H,boolean_false), !, assertz(inconsistent).

find_contradictions2([H|T]) :- get_texpr_expr(H,HR), (HR =.. [Op,X,Y] -> assert_pred(Op,X,Y); true), (\+inconsistent -> huelle, find_contradictions2(T);true).

format_edge(FromNumber,ToNumber,[]) :- format_edge2(FromNumber,ToNumber, green).

format_edge(FromNumber,ToNumber,F) :- false_predicate(F),!,format_edge2(FromNumber,ToNumber, red).

format_edge(FromNumber, ToNumber, LP) :- conjunct_predicates(LP,P),translate_bexpression(P,Label), print(FromNumber), print('->'), print(ToNumber), print(' '), print('[label="'), print(Label), print('"]') ,nl.

format_edge2(FromNumber, ToNumber, green) :- print(FromNumber), print('->'), print(ToNumber), print(' '), print('[color="forestgreen" label=true]') ,nl.

format_edge2(FromNumber, ToNumber, red) :- print(FromNumber), print('->'), print(ToNumber), print(' '), print('[color="crimson" label=false]') ,nl.

format_node(Number,Text) :- print(Number), print(' '), print('[label="'), print(Text), print('"]'),nl.

guide_dfs(Stack, Visited) :- guide_dfs(Stack,[],Visited).

guide_dfs([],SeenSoFar,SeenSoFar).

guide_dfs([Event|Tail],SeenSoFar,Visited) :- member(Event,SeenSoFar),!, guide_dfs(Tail,SeenSoFar,Visited). % ignore!

guide_dfs([Event|Tail],SeenSoFar,Visited) :- findall(S,guide_wp(S,Event,_),L), append(L,Tail,Todo), guide_dfs(Todo,[Event|SeenSoFar],Visited).

huelle :- pred(Op,X,Y),pred(Op2,Y,Z), combine(Op,Op2,Op3),
    assert_pred(Op3,X,Z),fail.

huelle :- (retract(change) -> huelle2 ; true).

huelle2 :- retract(pred_new(X,Op,Y)), huelle2(X,Op,Y).

huelle2 :- (retract(change) -> huelle2 ; true).

huelle2(X,Op,Y) :- pred(Op2,Y,Z), combine(Op,Op2,Op3), assert_pred(Op3,X,Z),fail.

huelle2(Y,Op,Z) :- pred(Op2,X,Y), combine(Op2,Op,Op3), assert_pred(Op3,X,Z),fail.

inc :- count(X), retract(count(_)), X1 is X+1, assertz(count(X1)).

inconsistent_fact(not_equal,X,X).

inconsistent_fact(less,X,X).

inconsistent_fact(greater,X,X).

inconsistent_fact(equal,X,Y) :- value(X), value(Y), X \= Y.

inconsistent_fact(subset_strict,X,X).

inconsistent_fact(member,_,empty_set).

keep(boolean_false).

keep(boolean_true).

keep(equal).

keep(not_equal).

keep(member).

keep(not_member).

keep(less).

keep(greater).

keep(less_equal).

keep(greater_equal).

law_of_motion :- events(L), law_of_motion(L).

law_of_motion([]).

law_of_motion(['INITIALISATION'|T]) :- !, law_of_motion(T).

law_of_motion([H|T]) :- H\='INITIALISATION',(wp(H,H,_)->true;add_wp(H,H,[])),law_of_motion(T).

neg(boolean_true,boolean_false).

neg(boolean_false,boolean_true).

neg(equal(X,Y),not_equal(X,Y)).

neg(not_equal(X,Y),equal(X,Y)).

neg(equal(X,Y),not_equal(X,Y)).

neg(member(X,Y),not_member(X,Y)).

neg(not_member(X,Y),member(X,Y)).

neg(less(X,Y),greater_equal(X,Y)).

neg(less_equal(X,Y),greater(X,Y)).

neg(greater_equal(X,Y),less(X,Y)).

neg(greater(X,Y),less_equal(X,Y)).

neg(subset_strict(X,Y),not_subset_strict(X,Y)).

neg(not_subset_strict(X,Y),subset_strict(X,Y)).

neg(subset(X,Y),not_subset(X,Y)).

neg(not_subset(X,Y),subset(X,Y)).

negate_boolean_expression(A,B) :-
    if(neg(A,B),true, add_error_fail(flow,'Unknown operator in negate: ',neg(A,B))).

normalize(TExpr,TNExpr) :- remove_bt(TExpr,Expr,NExpr,TNExpr), normalize2(Expr,NExpr).

normalize2(not_equal(X,boolean_true),equal(X,boolean_false)) :- !.

normalize2(not_equal(X,boolean_false),equal(X,boolean_true)) :- !.

normalize2(negation(TExpr),R) :- !,
    remove_bt(TExpr,Expr,NExpr,_), negate_boolean_expression(Expr,NExpr), normalize2(NExpr,R).

normalize2(TExpr, R) :-
    syntaxtransformation(TExpr,TSubExpr,_,TNSubExpr,R),!, normalize_list(TSubExpr, TNSubExpr).

normalize2(TExpr,_) :- add_error(flow,'Unknown expression in normalize2: ',TExpr),fail.

normalize_guards(E) :- findall((E,X),nonchanging_guard(E,X), L),
    print(mormalizing_grd(E,L)),nl,
    normalize_guards2(L).

normalize_guards2([]).

normalize_guards2([(E,P)|T]) :- normalize_list(P,R), assert_guards(R,E), normalize_guards2(T).

normalize_inv :- b_get_invariant_from_machine(Invariant),
    conjunction_to_list(Invariant,L),
    normalize_invs(L).

normalize_invs([]).

normalize_invs([H|T]) :- translate_bexpression(H,HP),
    print(normalizing_inv(HP)),nl, normalize(H,HX), get_texpr_expr(HX,HR),
    ((HR =.. [Op,X,Y] ,keep(Op)) -> assert_pred_inv(X,Op,Y);true),
    normalize_invs(T).

normalize_list([],R) :- !,R=[].

normalize_list([H|T],[HR|TR]) :- !, normalize(H,HR),normalize_list(T,TR).

normalize_list(A,B) :- add_error(flow,'Illegal arguments in normalize_list: ',(A,B)),fail.

normalize_wp :- findall((S,D,P), wp(S,D,P), L), clear_wp, normalize_wps(L).

normalize_wps([]).

normalize_wps([(S,D,P)|T]) :- conjunct_predicates(P,P3),conjunction_to_list(P3,P2),normalize_list(P2,R), add_wp(S,D,R), normalize_wps(T).

pred(Op,Y,Z) :- pred_grd(Y,Op,Z).

pred(Op,Y,Z) :- pred_inv(Y,Op,Z).

pred(Op,Y,Z) :- pred_guard(Y,Op,Z).

prepare_input :- statistics(runtime,_),
    normalize_inv,
    normalize_wp,
    statistics(runtime,[_,T2]), print(normalizing(T2)),nl.

print_base_guide(X) :- build_enable_graph,
    print_single_enable_graph(X,guide_wp).

print_edges([]).

print_edges([(S,D,P)|T]) :- print_node(S,D,C,X), format_edge(C,X,P), print_edges(T).

print_event_guide(X,E) :- build_enable_graph,
    retractall(event_wp(_,_,_)),
    build_guide(E,N),
    print_single_enable_graph(X,event_wp,N).

print_flow_automaton(E) :- calculate_flow_automaton([E],[],X), print(X), nl.

print_multiple_enable_graphs(File) :-
    print(writing_to_dot_file(File)),nl,
    tell(File),
    dot_header('EnableGraphs'), print('rankdir=LR'),nl, events(L), dot_node(L), print_subgraph(L),
    dot_footer, told,
    print(closing(File)),nl.

print_node(S,D,C,X) :- eventnumber(S,C), count(X), inc, format_node(X,D).

print_single_enable_graph(File,NameEdges) :- events(Nodes), print_single_enable_graph(File,NameEdges,Nodes).

print_single_enable_graph(File,NameEdges,Nodes) :-
    print(writing_to_dot_file(File)),nl,
    tell(File),
    dot_header('EnableGraph'),
    dot_node(Nodes),
    findall((S,D,P), call(NameEdges,S,D,P),WL),
    dot_edge(WL),
    dot_footer,
    told,
    print(closing(File)),nl.

print_subgraph([]).

print_subgraph([H|T]) :- findall((H,D,P), wp(H,D,P),WL),
    print_edges(WL),
    print_subgraph(T).

reset_count :- retractall(count(_)), assertz(count(0)).

reset_flow :- retractall(done_flow(_)), retractall(guide_wp(_,_,_)).

simplify([],[]).

simplify([H|T],R) :- (member(H,T) -> R=RT; %remove duplicates
    (tautology(H) -> R=RT; %remove tautologies
    R=[H|RT])),
    simplify(T,RT).

sym(equal).

sym(not_equal).

tautology(X) :- get_texpr_expr(X,Y), tautology2(Y).

tautology2(boolean_true).

tautology2(equal(A,A)).

tautology2(subset(A,A)).

tautology2(less_equal(A,A)).

tautology2(greater_equal(A,A)).

update_typed_wp :-
    retract( wp_untyped(S,D,P) ),
    bmachine:typecheck_predicates(P,TypedPred,S,D),
    add_wp(S,D,TypedPred),
    fail.

update_typed_wp.

value(X) :- get_texpr_expr(X,Y), value2(Y).

value2(X) :- number(X).

value2(boolean_false).

value2(boolean_true).

value2(integer(_,_)).

wp(S,D,TypedPred) :-
    update_typed_wp,
    wp_typed(S,D,TypedPred).