state_space_reduction

add_line_numbers(T,LT,Total) :- add_line_numbers_aux(T,0,LT,Total).

add_line_numbers_aux([],Nr,[],Nr) :- format('Found ~w different values.~n',[Nr]).

add_line_numbers_aux([list(H)|T],Nr,[list([N1|H])|LT],Total) :-
    N1 is Nr+1,
    add_line_numbers_aux(T,N1,LT,Total).

add_ltl_ap_guard('',Pred,Res) :- !,Res=Pred.

add_ltl_ap_guard(LTLAP,Pred,guard_reduce(check_ltl_ap(PF),Pred)) :-
    temporal_parser(LTLAP,ltl,Result),
    preprocess_formula(Result,PF).

add_new_abstract_node(ID,_State,AbsState,AssertEquivClass,EquivClassID) :-
    % TO DO: use hashing to improve lookup ! hashing:my_term_hash
    my_term_hash(AbsState,Hash),
    (retract(reduced_node(Hash,AbsState,Count,Witness,EquivClassID))
    -> C1 is Count+1,
    assertz(reduced_node(Hash,AbsState,C1,Witness,EquivClassID))
    ; inc_counter(equiv_class_id,EquivClassID),
    (print_progress(EquivClassID,ID)
    -> formatsilent('% Number of equivalence classes: ~w. Treated ~w states so far.~n',[EquivClassID,ID])
    ; true),
    assertz(reduced_node(Hash,AbsState,1,ID,EquivClassID))
    ),
    (AssertEquivClass==false % we compute ohter stuff; e.g., just coverage,....
    -> true
    ; assertz(equivalence_class(ID,EquivClassID)),
    (current_expression(ID,_) -> assertz(equivalence_class_contains_current_node(EquivClassID)) ; true),
    ((not_all_transitions_added(ID), \+equivalence_class_contains_open_node(EquivClassID))
    -> assertz(equivalence_class_contains_open_node(EquivClassID)) ; true)
).

add_new_abstract_transition(EquivClassID,DestEquivClassID,_ID,_Action,_TransId,_Destination,AbsAction) :-
    (reduced_trans(EquivClassID,AbsAction,_Count,DestEquivClassID,_TransitionID)
    -> true
    ; inc_counter(transition_id,TransitionID),
    assertz(reduced_trans(EquivClassID,AbsAction,1,DestEquivClassID,TransitionID))
).

all_states(_).

check_ltl_ap(AtomicLTLProperty,ID,_State) :-
    check_atomic_property_formula(AtomicLTLProperty,ID).

compute_covered_values_for_expression(ExprToEvaluate,MaxTypeCard,TotalNrOfValuesFound,Res) :-
    LTLGuard='',
    compute_covered_values_for_expression(ExprToEvaluate,LTLGuard,MaxTypeCard,TotalNrOfValuesFound,Res).

compute_covered_values_for_expression(ExprToEvaluate,LTLGuard,MaxTypeCard,TotalNrOfValuesFound,
    list([list(['Nr'|AllColHeaders])|LResult])) :-
    parse_expression_raw_or_atom_with_prob_ids(ExprToEvaluate,TypedExpr),
    translate:translate_bexpression_with_limit(TypedExpr,100,Str),
    get_bexpression_column_template(TypedExpr,Values,ColHeaders,Columns),
    append(ColHeaders,['Occurences', 'Witness ID'],AllColHeaders),
    get_texpr_type(TypedExpr,ExprType),
    (max_cardinality(ExprType,MaxTypeCard) -> true ; MaxTypeCard='??'),
    state_space:get_state_space_stats(NrNodes,_,_),
    format('Computing all values in initialised states (of ~w states in total) for expression: ~w [Max.Card=~w]~n',[NrNodes,Str,MaxTypeCard]),
    construct_projection_pred_for_typed_expr(TypedExpr,ProjPred),
    add_ltl_ap_guard(LTLGuard,ProjPred,FullProjPred),
    reduce_states(FullProjPred,false),
    format('Collecting values~n',[]),
    findall(list(StrVals),covered_values(StrVals,Values,Columns),Result),
    sort(Result,SResult),
    add_line_numbers(SResult,LResult,TotalNrOfValuesFound).

compute_set_of_covered_values_for_typed_expression(TypedExpr,SetOfValues) :-
    construct_projection_pred_for_typed_expr(TypedExpr,ProjPred),
    %add_ltl_ap_guard(LTLGuard,ProjPred,FullProjPred),
    reduce_states(ProjPred,false),
    state_space:get_state_space_stats(NrNodes,_,_),
    format('Collecting (Count, WitnessID, Value) triples for all ~w states in state space~n',[NrNodes]),
    findall( ((int(Count),int(Witness)),Val),
    (get_reduced_node(Val,Count,Witness,_EquivClassID),Witness\=root),SetOfValues).

compute_signature_merge :-
    % we could provide options: not consider invariant, ignore certain transitions, ...
    reduce_state_space(signature_and_inv,transition_name).

compute_transition_diagram(Expr) :-
    reduce_state_space(state_value_for_expr_and_inv(Expr),transition_name).

construct_projection_pred_for_typed_expr(TypedExpr,Predicate) :-
    get_texpr_id(TypedExpr,ID),
    bmachine:b_is_variable(ID),!,
    % use optimized, faster state_value_for_variable predicate
    Predicate = state_value_for_variable(ID).

construct_projection_pred_for_typed_expr(TypedExpr,Predicate) :-
    Predicate = state_value_for_expr(TypedExpr).

covered_values(AllColumns,Values,Columns) :-
    get_reduced_node(AbsState,Count,Witness,_EquivClassID),
    Witness \= root,
    Witness \= concrete_constants(_),
    AbsState \= undefined,
    % TO DO: maybe add further info: card for sets, dom, ran for relations ?
    translate_abs_value(AbsState,Values,Columns,StrVals),
    append(StrVals,[Count,Witness],AllColumns).

gen_label(expr(Expr),[Str]) :- !,
    get_preference(dot_projection_label_limit,Lim), L2 is Lim*2,
    translate:translate_bexpression_with_limit(Expr,L2,Str).

gen_label(Value,[Str]) :-
    get_preference(dot_projection_label_limit,Lim),
    (translate:translate_bvalue_with_limit(Value,Lim,Str)
    -> true; Str = 'fail').

generate_node_color(EquivClassNodeID,_Witness,AbsState,Count,Color) :-
    (AbsState=['NOT YET EXPLORED'] -> Color=orange
    ; AbsState = [invariant_violated|_] -> Color=red
    ; AbsState = ['DEADLOCK'] -> Color=red
    ; equivalence_class_contains_open_node(EquivClassNodeID) -> Color=orange
    ; Count>1 -> Color=blue
    ; Color=green).

generate_node_labels(GenLabels,AbsState,Labels) :-
    (AbsState = [invariant_violated|Signature]
    -> Labels = ['INVARIANT VIOLATED'|CL]
    ; Labels = CL, Signature = AbsState
    ),
    call(GenLabels,Signature,CL).

generate_transition_color_and_style(ShowSelfLoops,NodeID,AbsAction,SuccID,Color,Style) :-
    %format(user_output,'~w~n',[p(ShowSelfLoops,NodeID,AbsAction,SuccID)]),
    (reduced_trans(NodeID,AbsAction,_,Other,_),
    Other \= SuccID
    -> % there exists another transition of the same abstract action leading to another equivalence class
    % Note: here we always show self-loops
    get_preference(dot_projection_non_det_edge_colour,Color),
    get_transition_style(NodeID,AbsAction,SuccID,Style)
    ; self_loop_check(NodeID,SuccID,ShowSelfLoops), % here we only show self-loops if requested by user
    get_preference(dot_projection_det_edge_colour,Color),
    get_transition_style(NodeID,AbsAction,SuccID,Style)
).

generate_transition_label(AbsAction,Count,Label) :-
    (Count>1
    -> ajoin([AbsAction,' : ',Count],Label)
    ; Label=AbsAction
).

get_and_add_abstract_transition(ID,AbstractAndFilterTransitions,EquivClassID,AbsAction,DestEquivClassID) :-
    transition(ID,Action,TransId,Destination),
    equivalence_class(Destination,DestEquivClassID),
    call(AbstractAndFilterTransitions,ID,Action,TransId,Destination,AbsAction),
    %print(trans(EquivClassID,DestEquivClassID,AbsAction)),nl,
    add_new_abstract_transition(EquivClassID,DestEquivClassID,ID,Action,TransId,Destination,AbsAction).

get_constant_value(VariableID,_,concrete_constants(S),Value) :- !, member(bind(VariableID,Value),S).

get_reduced_node(AbsState,Count,Witness,EquivClassID) :-
    reduced_node(_Hash,AbsState,Count,Witness,EquivClassID).

get_transition_style(NodeID,AbsAction,SuccID,Style) :-
    non_definite_edge(NodeID,AbsAction,SuccID),
    !, % the edge is not always possible
    get_preference(dot_projection_non_definite_edge_style,Style).

get_transition_style(_,_,_,Style) :-
    get_preference(dot_projection_definite_edge_style,Style).

get_variable_value(const_and_vars(_ID,S),Variable,Value) :- !, member(bind(Variable,Value),S).

get_variable_value(csp_and_b(_CSP,BState),Variable,Value) :- !,
    get_variable_value(BState,Variable,Value).

get_variable_value(S,Variable,Value) :- !, member(bind(Variable,Value),S).

guard_reduce(GuardPredicate,AbstractAndFilterStates,ID,State,Value) :-
    call(GuardPredicate,ID,State),
    call(AbstractAndFilterStates,ID,State,Value).

initialised_b_state_exists :-
    visited_expression(_,S),
    state_corresponds_to_initialised_b_machine(S).

insert_commas(L,R) :- insert_commas(L,0,R).

insert_commas([],_,[]).

insert_commas([H],_,R) :- !, R=[H].

insert_commas([H|T],N,[H,Sep|IT]) :-
    (N>5 -> N1=0, Sep=',\\n' ; N1 is N+1, Sep=', '),
    insert_commas(T,N1,IT).

insert_newlines([],_,_,[]).

insert_newlines([H|T],CurCodes,Limit,Res) :-
    atom_length(H,Len),
    C1 is CurCodes+Len,
    ((C1 > Limit, CurCodes>0)
    -> Res = ['\\n',H|TR], insert_newlines(T,Len,Limit,TR)
    ; Res = [H|TR], insert_newlines(T,C1,Limit,TR)).

mytranslate(Value,StrVal) :-
    translate:translate_bvalue_with_limit(Value,100,StrVal).

myundefined(_,undefined).

non_definite_edge(NodeID,AbsAction,SuccID) :-
    abs_signature(NodeID,AlwaysEnabled),
    nonmember(AbsAction/SuccID,AlwaysEnabled).

number_of_values_for_constant(ID,Count) :-
    bmachine:b_is_constant(ID),
    reduce_selected_states(is_concrete_constants_state_id,get_constant_value(ID),false),
    get_counter(equiv_class_id,Count),
    format('~w : ~w~n',[ID,Count]).

number_of_values_for_variable(ID,Count) :-
    bmachine:b_is_variable(ID),
    reduce_states(state_value_for_variable(ID),false),
    get_counter(equiv_class_id,Count),
    format('~w : ~w~n',[ID,Count]).

print_progress(EquivClassID,_ID) :- EquivClassID mod 10 =:= 0 ;EquivClassID = 5.

reduce_selected_states(SelectionPred,AbstractAndFilterStatesPred,AssertEquivClass) :-
    reset,
    call(SelectionPred,ID),
    % compute equivalence class for every state selected by SelectionPred
    visited_expression(ID,State),
    call(AbstractAndFilterStatesPred,ID,State,AbsState),
    % should succeed if state to be shown
    %print(state(ID,AbsState)),nl,
    add_new_abstract_node(ID,State,AbsState,AssertEquivClass,_EquivClassID),
    fail.

reduce_selected_states(_,_,_).

reduce_state_space(AbstracAndFilterStates,
    AbstractAndFilterTransitions) :-
    retractall(abs_signature(_,_)),
    % first compute equivalence class for every state
    statistics(walltime,[W1,_]),
    reduce_states(AbstracAndFilterStates,true),
    statistics(walltime,[W2,_]),
    (debug_mode(on)
    -> W12 is W2-W1, format('Time to abstract and filter states: ~w ms~n',[W12]) ; true),
    %set_prolog_flag(profiling,on),
    % now inspect every transition for every node (that has been retained)
    equivalence_class(ID,EquivClassID), %print(id_class(ID,EquivClassID)),nl,
    findall(AbsAction/DestEquivClassID,
    get_and_add_abstract_transition(ID,AbstractAndFilterTransitions,EquivClassID,
    AbsAction,DestEquivClassID),
    UnsortedSignature),
    sort(UnsortedSignature,Signature), %print(sig(Signature)),nl,
    update_signature(EquivClassID,Signature),
    fail.

reduce_state_space(_,_). % :- set_prolog_flag(profiling,off),print_profile.

reduce_states(AbstractAndFilterStates,AssertEquivClass) :-
    reduce_selected_states(all_states,AbstractAndFilterStates,AssertEquivClass).

reset :- retractall(reduced_node(_,_,_,_,_)), retractall(equivalence_class(_,_)),
    retractall(equivalence_class_contains_current_node(_)),
    retractall(equivalence_class_contains_open_node(_)),
    retractall(reduced_trans(_,_,_,_,_)),
    counter_init,
    new_counter(transition_id), new_counter(equiv_class_id).

reset_ignored_events :- %print(reseting_ignore_event),nl,
    retractall(ignore_event(_)).

self_loop_check(NodeID,SuccID,ShowSelfLoops) :-
    (NodeID==SuccID -> ShowSelfLoops=true % if we have a single self-loop then only show it if preference set
    ; true).

set_ignored_events([]).

set_ignored_events([H|T]) :- assertz(ignore_event(H)),
    format('Ignoring: ~w~n',[H]),
    set_ignored_events(T).

signature(ID,_,AbsState) :-
    findall(Name,(transition(ID,Action,_,_),specfile:get_operation_name(Action,Name),
    \+ ignore_event(Name)), L),
    (L=[] ->
    (not_all_transitions_added(ID) -> AbsState = ['NOT YET EXPLORED']
    ; transition(ID,_,_,_) -> AbsState = ['NO SELECTED EVENTS']
    ; AbsState = ['DEADLOCK'])
    ; sort(L,AbsState)
).

signature_and_inv(ID,S,AbsState) :-
    (invariant_violated(ID) -> AbsState = [invariant_violated|Sig] ; AbsState = Sig),
    signature(ID,S,Sig).

simple_list(List,List).

sm_node_pred(GenLabels,EqNodeID,SubGraph,NodeDesc,Shape,Style,Color) :- SubGraph=none,
    Shape=record,
    get_reduced_node(AbsState,C1,Witness,EqNodeID),
    (equivalence_class_contains_current_node(EqNodeID) -> Style = bold % bold, diagonals, rounded
    % we could optionally turn this off in case the UI wants to do this itself and update when the animator changes state
    ; Style = none), % or rounded
    %insert_commas(AbsState,0,CL),
    (AbsState = [invariant_violated|Signature]
    -> Labels = ['INVARIANT VIOLATED\\n|'|EscCL]
    ; Labels = EscCL, Signature = AbsState
    ),
    call(GenLabels,Signature,CL),
    maplist(string_escape,CL,EscCL),
    %maplist : tools:wrap_and_truncate_atom(EscCL,30,121,EscCLW),
    insert_newlines(Labels,0,100,LabelsNL),
    append(['|{' | LabelsNL],['\\n|# states: ',C1,'}|'],Atoms),
    ajoin(Atoms,NodeDesc),
    generate_node_color(EqNodeID,Witness,AbsState,C1,Color).

sm_trans_predicate(ShowSelfLoops,NodeID,Label,SuccID,Color,Style) :-
    reduced_trans(NodeID,AbsAction,Count,SuccID,_TID),
    % TO DO: maybe merge all AbsAction with the same Origin & Destination into single transition
    generate_transition_label(AbsAction,Count,Label),
    generate_transition_color_and_style(ShowSelfLoops,NodeID,AbsAction,SuccID,Color,Style).

state_value_for_expr(Expr,_ID,root,AbsState) :- !, AbsState=expr(Expr).

state_value_for_expr(_Expr,ID,_State,AbsState) :-
    get_preference(dot_projection_process_only_explored,true),
    (invariant_still_to_be_checked(ID) -> A=not_yet_explored
    ; not_interesting(ID) -> A=not_interesting), % SCOPE predicate false
    !, AbsState=A.

state_value_for_expr(Expr,ID,State,AbsState) :-
    state_corresponds_to_initialised_b_machine(State,BState),
    b_compute_expression_nowf(Expr,[],BState,Val,'state space reduction',ID),!,
    Expand=false,
    normalise_value_for_var(Expr,Expand,Val,AbsState). % not necessary if Expr is a simple ID, but then we use state_value_for_variable

state_value_for_expr(_Expr,_ID,_State,undefined).

state_value_for_expr_and_inv(Expr,ID,State,ResAbsState) :-
    state_value_for_expr(Expr,ID,State,AbsState),
    (invariant_violated(ID) -> ResAbsState = [invariant_violated|AbsState]
    % TO DO: also look if invariant_not_yet_checked ?, ... not_all_transitions_added ?
    ; ResAbsState = AbsState).

state_value_for_variable(Variable,_ID,State,Value) :- get_variable_value(State,Variable,Value).

tcltk_compute_nr_covered_values_for_all_constants(list([list(['Constant', 'Number of Values'])|VL])) :-
    state_space:get_state_space_stats(NrNodes,_,_),
    format('Computing all values in ~w states for all constants~n',[NrNodes]),
    findall(list([ID,Count]),number_of_values_for_constant(ID,Count),VL),
    format('Finished computing all values for all constants~n',[]).

tcltk_compute_nr_covered_values_for_all_variables(list([list(['Variable', 'Number of Values'])|VL])) :-
    state_space:get_state_space_stats(NrNodes,_,_),
    format('Computing all values in ~w states for all variables~n',[NrNodes]),
    findall(list([ID,Count]),number_of_values_for_variable(ID,Count),VL),
    format('Finished computing all values for all variables~n',[]).

tcltk_write_signature_merge_to_dotfile(IgnoredEventNrs,File) :-
    tcl_convert_event_numbers_to_names(list(IgnoredEventNrs),list(IgnoredEvents)),
    %print(tcl_convert_event_numbers_to_names(list(IgnoredEventNrs),list(IgnoredEvents))),nl,
    write_signature_merge_to_dotfile(IgnoredEvents,File).

transition_name(_,Action,_,_,Name) :- specfile:get_operation_name(Action,Name),
    \+ ignore_event(Name).

translate_abs_value(AbsState,Values,Columns,StrVals) :-
    AbsState=Values, !,
    maplist(mytranslate,Columns,StrVals).

translate_abs_value(undefined,_Values,Columns,StrVals) :- !,
    maplist(myundefined,Columns,StrVals).

translate_abs_value(AbsState,_Values,_Columns,[StrVal]) :-
    mytranslate(AbsState,StrVal).

update_signature(EquivClassID,Signature) :-
    (abs_signature(EquivClassID,OldSignature)
    -> (Signature=OldSignature -> true
    % ; OldSignature = [] -> true % already minimal
    ; ord_intersection(OldSignature,Signature,NewSignature),
    %print(updated_signature(NewSignature)),nl,
    (NewSignature=OldSignature -> true
    ; retract(abs_signature(EquivClassID,OldSignature)),
    assertz(abs_signature(EquivClassID,NewSignature))
    )
    )
    ; assertz(abs_signature(EquivClassID,Signature))).

write_covered_values_for_expression_to_csvfile(VorE,File) :-
    print('Parsing and type checking'),nl,
    parse_expression_raw_or_atom_with_prob_ids(VorE,TypedExpr),
    translate:translate_bexpression_with_limit(TypedExpr,100,Str),
    format('Computing all values for expression: ~w~n',[Str]),
    reduce_states(state_value_for_expr(TypedExpr),false),
    format('Writing values to CSV file: ~w~n',[File]),
    open(File,write,Stream,[encoding(utf8)]),
    format(Stream,'"~w",~w,~w,~n',[Str,'Occurences','WitnessStateID']),
    call_cleanup(write_covered_values_for_expression_to_csvfile_aux(Stream), close(Stream)),
    format('Finished writing values to CSV file: ~w~n',[File]).

write_covered_values_for_expression_to_csvfile(_VorECodes,File) :-
    add_error(state_space_reduction,'Computing Value Coverage Failed',File).

write_covered_values_for_expression_to_csvfile_aux(S) :-
    get_reduced_node(AbsState,Count,Witness,_EquivClassID),
    (Witness=root -> StrVal = '?'
    ; translate:translate_bvalue_with_limit(AbsState,100,StrVal)),
    format(S,'"~w",~w,~w~n',[StrVal,Count,Witness]),
    fail.

write_covered_values_for_expression_to_csvfile_aux(_).

write_signature_merge_to_dotfile(File) :-
    write_signature_merge_to_dotfile([],File).

write_signature_merge_to_dotfile(IgnoredEvents,File) :-
    reset_ignored_events,
    set_ignored_events(IgnoredEvents),
    time(state_space_reduction:compute_signature_merge), % from debug module
    gen_dot_graph(File,sm_node_pred(insert_commas),sm_trans_predicate(true)),
    reset_ignored_events.

write_transition_diagram_for_expr_to_dotfile(VorE,File) :-
    %print(expr(VorE)),
    parse_expression_raw_or_atom_with_prob_ids(VorE,TypedExpr),
    statistics(walltime,[W1,_]),
    compute_transition_diagram(TypedExpr),
    statistics(walltime,[W2,_]),
    (get_preference(dot_use_unicode,true) -> translate:set_unicode_mode ; true),
    get_preference(dot_print_self_loops,SELF),
    call_cleanup(
    gen_dot_graph(File,[deals_with_pref/dot_print_self_loops, merge_transitions/true],
    sm_node_pred(gen_label),sm_trans_predicate(SELF),dot_no_same_rank,dot_no_subgraph),
    (get_preference(dot_use_unicode,true) -> translate:unset_unicode_mode ; true)),
    statistics(walltime,[W3,_]),
    (debug_mode(on)
    -> W is W3-W1, W12 is W2-W1,
    format('Time to compute transition diagram projection and write to file: ~w ms (~w ms for projection)~n',[W,W12])
    ; true).