enable_graph

add_edges(EnableGraph,[],EnableGraph).

add_edges(EnableGraph,[From-Predicate-To|Edges],NewEnableGraph) :-
    add_neighbour(EnableGraph,From,Predicate,To,EnableGraph1),
    add_edges(EnableGraph1,Edges,NewEnableGraph).

add_neighbour([],From,Predicate,To,[From-[To-Predicate]]).

add_neighbour([V-Neighbours|Rest],From,Predicate,To,[V-NewNeighbours|Rest]) :-
    From==V,!,
    (member(To-Predicate,Neighbours) ->
    NewNeighbours = Neighbours
    ; sort([To-Predicate|Neighbours],NewNeighbours)
).

add_neighbour([V-Neighbours|Rest],From,Predicate,To,[From-[To-Predicate],V-Neighbours|Rest]) :-
    V @> From,!.

add_neighbour([V-Neighbours|Rest],From,Predicate,To,[V-Neighbours|S]) :-
    add_neighbour(Rest,From,Predicate,To,S).

add_vertex([],V,[V-[]]).

add_vertex([V-NB|Rest],V,[V-NB|Rest]) :- !.

add_vertex([W-NB|Rest],V,[V-[],W-NB|Rest]) :-
    W @> V,!.

add_vertex([W-NB|Rest],V,[W-NB|S]) :-
    add_vertex(Rest,V,S).

add_vertices(EnableGraph,[],EnableGraph).

add_vertices(EnableGraph,[V|Vs],NewEnableGraph) :-
    add_vertex(EnableGraph,V,EnableGraph1),
    add_vertices(EnableGraph1,Vs,NewEnableGraph).

decrease_evaluation_depth(EvaluationDepth,NewEvaluationDepth) :-
    (EvaluationDepth>0 ->
    NewEvaluationDepth is EvaluationDepth -1
    ; NewEvaluationDepth=EvaluationDepth
).

dot_eop_node_predicate(NodeID,SubGraph,NodeDesc,Shape,Style,Color):-
    eop_node_predicate(NodeID,SubGraph,NodeDesc,Shape,Style,Color).

edge(EnableGraph,V1,V2,Predicate) :-
    member(V1-NB,EnableGraph),
    member(V2-Predicate,NB).

edge_labels(EnableGraph,Labels) :-
    edge_labels(EnableGraph,[],Labels).

edge_labels([],Labels,Labels).

edge_labels([_V-NB|Rest],LabelsSoFar,Labels) :-
    maplist(get_vertex_label,NB,Ls),
    append(LabelsSoFar,Ls,LabelsSoFar1),
    edge_labels(Rest,LabelsSoFar1,Labels).

enable_trans_predicate(NodeID,Label,SuccID,Color,Style) :-
    b_top_level_operation(OpName1),
    b_top_level_operation(OpName2),
    asserted_enable_graph(EnableGraph),
    edge(EnableGraph,OpName1,OpName2,Predicate),
    translate_bexpression(Predicate,Res),
    translate_enable_res(Res,NodeID,SuccID,Label,Color,Style).

evaluate_enabling_predicate_for_por(State,DoNotVisit,P,EvaluatePredicate,OpName1,OpName2,NewPredicate) :-
    nonmember(OpName2,DoNotVisit),
    empty_state(LocalState),
    (EvaluatePredicate,State\=[] ->
    % V2 is enabled after V1, we need to execute V1 in oder to generate the next state
    % TODO: maybe we should set a sort of time-out to decrease the overhead in some cases
    !,
    b_test_boolean_expression_cs(P,LocalState,State,'POR enabling',OpName1:OpName2),
    % the success of the predicate should guarantee that no well-definedness-errors occur
    % when OpName1 is executed
    execute_operation(OpName1,LocalState,State,NextState) % TODO: handle case for non-deterministic operations
    ; % just checking whether there is an edge between V1 and V2
    NextState=[] % TODO: what should we give as next state
    ),
    NewPredicate = evaluate_enabling_predicate_for_por(NextState,DoNotVisit).

execute_expression(_OpName,precondition(_Condition,Body),LocalState,State,Updates) :- !,
    b_interpreter: b_execute_inner_statement(Body,LocalState,State,Updates,_WF,_IPath,_OR).

execute_expression(OpName,Stmt,_LocalState,State,Updates) :-
    functor(Stmt,rlevent,11),!,
    % Stmt = rlevent(Name,Section,_Status,_Params,Guard,_Theorems,_Actions,_VWitnesses,_PWitnesses,_Unmod,_AbstractEvents)
    temporary_set_preference(ltsmin_do_not_evaluate_top_level_guards,full,CHNG),
    %bsyntaxtree:safe_create_texpr(Stmt,event,Event),
    %b_interpreter_eventb:b_execute_event(OpName,Event,[],[],State,OutputState,_Path),
    %b_interpreter_eventb:b_event_with_change_set(Event,[],[],State,_ChangeSet,Updates,_Path),
    b_interpreter:b_execute_top_level_operation_update(OpName,_Operation,State,Updates,_PathInfo),
    reset_temporary_preference(ltsmin_do_not_evaluate_top_level_guards,CHNG).

execute_expression(_OpName,Stmt,LocalState,State,Updates) :-
    b_interpreter: b_execute_statement(Stmt,LocalState,State,Updates,_WF,_Path).

execute_operation(OpName,LocalState,State,NewState) :-
    %% (OpName = 'T3writebus' -> trace; true),
    b_get_machine_operation(OpName,_Res,Par,Body),
    %% print(expr(Body)),nl,
    get_texpr_expr(Body,Expr),
    (Par = [] ->
    execute_expression(OpName,Expr,LocalState,State,Updates)
    ; b_interpreter: b_execute_top_level_operation_update(OpName,_FullOp,State,Updates,_Path)
    %b_interpreter: b_execute_operation_with_parameters(OpName,State,Par,Updates,Res,_Path,_WF,output_required)
    ),
    %print(executed_operation(OpName)),nl,
    % guarantee that Updates is not a variable here
    %% print(states(Updates,State)),nl,
    store_updates_and_normalise(Updates,State,NewState).

get_vertex_label(_Dst-P,P).

path_set(EnableGraph,Src,Goals,Module,Predicate,EvaluationDepth,[Src|Path],Length) :-
    path_set1(EnableGraph,Src,Goals,Module,Predicate,EvaluationDepth,[],Path,0,Length).

path_set1(_EnableGraph,Goal,Goals,_Module,_Predicate,_EvaluationDepth,_CurPath,[],Length,Length) :-
    member(Goal,Goals).

path_set1(EnableGraph,Src,Goals,Module,Predicate,EvaluationDepth,CurPath,Path,CurLength,Length) :-
    nonmember(Src,Goals),
    (EvaluationDepth==0 -> EvaluatePredicate=fail; EvaluatePredicate=true),
    predicate_edge(EnableGraph,Src,Next,CurPath,Module,Predicate,EvaluatePredicate,NewPredicate),
    NewLength is CurLength +1,
    decrease_evaluation_depth(EvaluationDepth,NewEvaluationDepth),
    Path = [Next|PathTail],
    path_set1(EnableGraph,Next,Goals,Module,NewPredicate,NewEvaluationDepth,[Next|CurPath],PathTail,NewLength,Length).

predicate_edge(EnableGraph,V1,V2,CurPath,Module,Predicate,EvaluatePredicate,NewPredicate) :-
    edge(EnableGraph,V1,V2,P),
    nonmember(V2,CurPath),
    call(Module:Predicate,P,EvaluatePredicate,V1,V2,NewPredicate).

print_enable_graph_dot(EnableGraph,File) :-
    assertz(asserted_enable_graph(EnableGraph)),
    gen_dot_graph(File,dot_eop_node_predicate,enable_trans_predicate),
    retractall(asserted_enable_graph(_)).

vertices_edges_predicates_to_egraph(Vertices,Edges,EnableGraph) :-
    add_vertices([],Vertices,EnableGraph1),
    add_edges(EnableGraph1,Edges,EnableGraph).