tcltk_interface.pl

add_additional_destination_infos(FromID,ActionName,ToID) :-
    preference(try_operation_reuse,true),
    ToID \= FromID,
    animation_mode(b),
    preference(symmetry_mode,MODE), (MODE=off ; MODE=flood),
    % TO DO: can we enable this trick in symmetry mode ?
    bmachine:reuse_operation_effect(ActionName,OtherAction),
    \+ reuse_operation(ToID,OtherAction,_,_),
    assert(reuse_operation(ToID,OtherAction,FromID,ActionName)),
    % print(reuse_operation(ToID,OtherAction,FromID,ActionName)),nl,
    fail.

add_additional_destination_infos(FromID,ActionName,ToID) :- %print(add_dest(FromID,ActionName,ToID)),nl,
    ( b_specialized_invariant_for_op(ActionName,_),
    \+ invariant_not_yet_checked(FromID),
    \+ invariant_violated(FromID) % if Invariant does not hold in previous state, we have no idea about invariants in the new state (proof assumes invariant holds before)
    ->
    (retract(specialized_inv(ToID,OldAVL)) -> true ; empty_avl(OldAVL)),
    avl_store(ActionName,OldAVL,nothing,NewAVL),
    % TO DO: provide a special value if an operation preserves the entire invariant ??
    %print(specialized_inv(ToID,NewAVL)),nl,
    assert(specialized_inv(ToID,NewAVL))
    ; true
).

add_cover('-->'(Action1,_),OpName) :- !,add_cover_aux(Action1,OpName).

add_cover(Action1,OpName) :- add_cover_aux(Action1,OpName).

add_cover_aux(Action1,OpName) :- functor(Action1,OpName,_),
    (retract(operation_not_yet_covered(OpName))
    -> (preferences:get_preference(provide_trace_information,true)
    -> print(cover(OpName)),nl ; true),
    (operation_not_yet_covered(_) -> true ; formatsilent('~nALL OPERATIONS COVERED~n',[]))
    ; true
).

add_csp_general_process_id(val_of(Process,_),ID) :- !,
    ( animatable_process_without_arguments(Process) % in case the called processes is one without arguments, then we don't have to parse the expression
       -> add_csp_process_id(Process,ID)
% code below not covered; loaded_main_file only defined for probcli entry point !
%; animation_mode(cspm),
% loaded_main_file(CSPFile),
% parse_and_analyze_process_expression(Process,CSPFile,Proc),
   % (transition(root,start_cspm(Proc),_TransID,ID) -> true
   % ; otherwise -> add_trans_id(root,start_cspm(Proc),Proc,[],ID,[],_)
   % )
).

add_csp_general_process_id(GenProcExpr,ID) :-
    % stripping out the source-loc info
    haskell_csp_analyzer: clear_span(GenProcExpr,GenProcExpr1),
    get_start_transition_term(GenProcExpr1,Trans),
    (transition(root,Trans,_TransID,ID)
    -> true
    ; add_trans_id(root,Trans,GenProcExpr1,[],ID,[],_)
).

add_csp_process_id(Process,NewID) :-
    add_csp_process_id1(Process,NewID,animatable_process_cli).

add_csp_process_id1(Process,NewID,Pred) :-
    (call(Pred,Process)
    -> get_start_transition_term(Process,Trans),
    (transition(root,Trans,_,DestID) -> NewID=DestID % process already set up
    ; xtl_interface:get_start_expr(Process,NewState),
    add_trans_id(root,Trans,NewState,[],NewID,[],_)
    )
    ; add_error_fail(add_csp_process_id,'Not an animatable CSP Process: ',Process)).

add_csp_process_id_normalized(Spec,Functor,CSpec,CSpecNodeID) :-
    % stripping out the src_span info
    haskell_csp_analyzer: clear_span(Spec,SpecNoSpan),
    haskell_csp_analyzer: compile_body(SpecNoSpan,Functor,[],[],CSpec),
    add_csp_general_process_id(CSpec,CSpecNodeID).

add_id_to_history(CurID) :-
    (retract(history(History))->true),
    assert(history([CurID|History])), retractall(forward_history(_)).

add_or_between_constant_predicates([],'1=1').

add_or_between_constant_predicates(L,Res) :-
    tools: ajoin_with_sep(L,' or ',Res).

add_partial_transitions(root,CurState) :-
    /* for the moment the only state where partial transitions are computed */
    \+ any_transition(root,_,_), /* adding normal transitions was not successful */
    partial_trans(CurState,Act,NewExpression,Residue),
    add_trans_id(root,Act,NewExpression,Residue,_NewID,[],_),fail.

add_partial_transitions(_CurID,_).

add_trans_id(CurID,Act,NewExpression,Residue,NewID,TransInfo,TransId) :-
    (Residue=[] -> true
    ; tools_printing:print_goal(Residue),nl,
    add_error(add_trans_id,'Residue: ',CurID:Act:Residue)),
    tcltk_add_new_transition_transid(CurID,Act,NewID,NewExpression,TransInfo,TransId).

add_transition(CurID,CurState,ActionName,PreviousSuccessorID) :-
    %(var(ActionName) -> add_error_fail(add_transition,'ActionName is a variable: ',CurID) ; true),
    nonvar(ActionName), % can happen in CSP, CSP||B, XTL, ... modes but also in B mode
    candidate_operation_for_reuse(ActionName), % can only be true when try_operation_reuse preference is true
    retract(reuse_operation(CurID,ActionName,PreviousID,_FromOp)),!,
    % we don't have to compute the operation again; simply reuse pre-computed effect
    b_get_operation_normalized_read_write_info(ActionName,_Read,WrittenVariables),
    build_up_b_real_operation(ActionName,ActionTemplate), % missing add any parameters
    % print(reusing_operation(ActionName,ActionTemplate, from(PreviousID), for(CurID),via(FromOp))),nl,
    transition(PreviousID,ActionTemplate,TransID,PreviousSuccessorID),
    findall(Info,transition_info(TransID,Info),TransInfos),
    visited_expression(PreviousSuccessorID,PreviousExpression,true),
    ~~mnf(patch_state(CurState,WrittenVariables,PreviousExpression,NewExpression)),
    % (specfile_trans(CurState,ActionName,ActionTemplate,NewExpression,_,_)
    % -> true ; add_error(add_transition,'Mismatch in operation reuse',ActionName),
    % print(CurID),nl, print(ActionName), print(' via '), print(via(PrevOp)),nl),
    ~~mnf(add_trans_id(CurID,ActionTemplate,NewExpression,[],_NewID,TransInfos,_)).

add_transition(CurID,CurState,ActionName,NewId) :-
    /* ActionName maybe pre-instantiated */
    specfile_trans(CurState,ActionName,Act,NewExpression,TransInfo,Residue),
    %% print_bt_message(specfile_trans(CurState,ActionName,Act,NewExpression,TransInfo,Residue)),
    add_trans_id(CurID,Act,NewExpression,Residue,NewId,TransInfo,_).

add_transitions__with_timeout_fail_loop(CurID,CurState,CurTO) :-
    enter_new_error_scope(Level,add_transitions__with_timeout_fail_loop),
    call_cleanup(add_transitions__with_timeout_fail_loop2(Level,CurID,CurState,CurTO),
    exit_error_scope(Level,_,add_transitions__with_timeout_fail_loop)).

add_transitions__with_timeout_fail_loop2(Level,CurID,CurState,CurTO) :- % statistics(runtime,_),
    % TO DO: prepare computing the state: expanding const and vars, unpacking, ...
    specfile_possible_trans_name_for_successors(CurState,ActionName),
    profile_failure_driven_loop(ActionName,CurID),
    % Note: we enumerate possible transition names so that we can catch the time-out per name !
    % statistics(runtime,[T1,DeltaT]), print(delta_time(ActionName,DeltaT)),nl,
    % first enumerate possible Operations/... to obtain timeout per operation/...
    % TO DO: divide CurTO by number of transitions ???
    % We could also decide to have one time-out per state, only if that one is triggered move to
    % finer-grained timeouts
    % For probcli ../prob_examples/public_examples/B/Benchmarks/Cruise_finite1.mch --model-check, there are 35360 calls to timeout/3 (one per state the model checker reached and per transition group), with -disable-timeout none
    % In SICS 4.3.5 the runtime increased from 1.480 to 2.270 seconds = 0.022 ms per timeout call
    % In SICS 4.4.1 the runtime increased from 1.494 to 3.033 seconds. = 0.044 ms per timeout call.
    %% statistics(runtime,[T1,_]), print(try(ActionName,T1)),nl,
    set_error_context(operation(ActionName,CurID)),
    time_out_with_enum_warning_for_findall_in_current_error_scope(Level,add_transition(CurID,CurState,ActionName,_NewId),CurTO,TimeOutRes),
    %% statistics(runtime,[T2,_]), TDiff is T2-T1, print(added_transition(CurID,ActionName,TDiff,TimeOutRes)),nl,
    %% add_transition(CurID,CurState,ActionName,_NewId) ,
        ((TimeOutRes==time_out ; nonvar(TimeOutRes),TimeOutRes=virtual_time_out(_), \+ max_reached(ActionName))
        % virtual time outs not relevant if we have already stopped earlier anyway; TO DO: does not seem to work for INITIALISATION
        -> (TimeOutRes=virtual_time_out(_) -> true
        ; print_message('TIME OUT: '),print_message(CurID),
        print_message(CurTO),print_message(ActionName)
        ),
            (var(ActionName)
            -> assert_time_out_for_node(CurID,'unspecified_operation',TimeOutRes)
            ; assert_time_out_for_node(CurID,ActionName,TimeOutRes)) % TO DO: assert info per ActionSkeleton ?
           ; true
        ),fail.

add_transitions__with_timeout_fail_loop2(_,_,_,_) :- clear_error_context.

add_transitions_fail_loop(CurID,CurState) :-
    specfile_possible_trans_name_for_successors(CurState,ActionName),
    %print(adding_transition_no_timeout(CurID,ActionName)),nl,
    set_error_context(operation(ActionName,CurID)),
    add_transition(CurID,CurState,ActionName,_NewId), % TO DO: transmit animation_mode value?
    fail.

add_transitions_fail_loop(_,_) :- clear_error_context.

b_compute_expression_with_prob_ids(Expr,BState,Value) :-
    add_prob_deferred_set_elements_to_store(BState,BState1,visible),
    b_interpreter:b_compute_expression_nowf(Expr,[],BState1,Value).

b_full_execute_top_level_statement_with_probids(Body,InState,Updates,NewState) :-
    add_prob_deferred_set_elements_to_store(InState,InState1,visible),
    init_wait_flags(WF,[b_full_execute_top_level_statement_with_probids]),
    b_execute_top_level_statement(Body,[],InState1,Updates,WF,_Path1,output_not_required),
    ground_wait_flags(WF),
    store:store_updates_and_normalise(Updates,InState,NewState).

b_trans_one_solution_with_pred(OpName,TypedCustomPredicate,Operation,NewID) :-
    call_cleanup(b_trans_one_solution_with_pred2(OpName,TypedCustomPredicate,Operation,NewID),
    bmachine:reset_temp_predicate).

b_trans_one_solution_with_pred2(OpName,TypedCustomPredicate,Operation,NewID) :-
    b_top_level_operation(OpName),
    !,
    current_expression(CurID,InState),
    set_context_state(CurID),
    call_cleanup(execute_operation_by_predicate_in_state(InState,OpName,TypedCustomPredicate,Operation,NewState),
    clear_context_state),
    !,
    debug_format(19,'Executed by predicate: ~w~n',[OpName]),
    %debug_format(19,'Executed ~w: ~w~nOut=~w~n',[OpName,Operation,NewState]),
    add_trans_id(CurID,Operation,NewState,[],NewID,[],_TransId),
    tcltk_goto_state(Operation,NewID).

b_trans_one_solution_with_pred2(OpName,TypedCustomPredicate,Operation,NewID) :-
    bmachine:assert_temp_typed_predicate(TypedCustomPredicate),
    current_expression(CurID,InState),
    set_context_state(CurID),
    temporary_set_preference(maxNrOfEnablingsPerOperation,1,Max),
    temporary_set_preference(maxNrOfInitialisations,1,MaxI),
    start_ms_timer(Timer),
    call_cleanup((specfile:b_trans(InState,OpName,Operation,NewState,TransInfo) -> true),
    (stop_ms_timer(Timer),
    reset_temporary_preference(maxNrOfEnablingsPerOperation,Max),
    reset_temporary_preference(maxNrOfInitialisations,MaxI),
    clear_context_state)
    ),
    debug_println(9,found_solution(NewState)),nl,
    % now add a transition to the state space:
    Residue=[],
    add_trans_id(CurID,Operation,NewState,Residue,NewID,TransInfo,_),
    tcltk_goto_state(Operation,NewID).

call_cbc_command(Command) :-
    call_in_fresh_error_scope_for_one_solution(
    (catch_clpfd_overflow_call1(Command) -> true
    ; translate_events_in_current_scope_to_warnings(cbc,'Warning: '),fail
% Maybe we should raise error when Command fails and enumeration warnings are there ?
)).

call_pred_on_expanded_state(_Pred,root,_,ColList) :- !, ColList=unknown.

call_pred_on_expanded_state(Pred,StateId,action(_,ActionTerm),ResColList) :- print(StateId),nl,
    specfile:get_operation_name(ActionTerm,OpName),
    format('Processing state ~w (reached via ~w)~n',[StateId,OpName]),
    visited_expression(StateId,State),
    (state_corresponds_to_initialised_b_machine(State,BState)
    -> call(Pred,ColList,BState,OpName), ResColList = list([OpName,StateId|ColList])
    ; ResColList = unknown ).

can_generate_dot_from_last_state_error :- last_detailed_error(span_predicate(_,_,_),_).

catch_clpfd_overflow_call_for_state(CurID, Call,ExtraCleanUpCode) :-
    catch_clpfd_overflow_call2(Call,
    ( store_state_error(CurID,'CLPFD_integer_overflow',_),
    call(ExtraCleanUpCode)) ).

cbc_constraint_find_static_assertion_violation(Result,Options) :-
    call_cbc_command(cbc_static_assertions_check(State,Options)),
    ( State = counterexample_found(CE) ->
    Result = counterexample_found,
    tcltk_add_cbc_state(CE,static_assertion_check)
    ; otherwise ->
    Result = State).

checkAssertion(Assertion,PP,Negated,Ok,ResTrace) :-
    (silent_mode(on) -> true
    ; print('CHECKING '),
    translate_csp_assertion(Assertion,PP),
    print(PP),nl
    ),
    debug_println(9,checkAssertion(Assertion)),
    reset_refinement_checker,
    (run_assertion_check(Assertion,Negated,ResTrace)
    -> debug_println(9,result(ResTrace)),
    (ResTrace=no_counter_example
    -> (Negated = 'False' -> Ok=true
    ; %add_error(check_assertRef,'Assertion FAILS (expected refinement not to hold): ',PP),
    Ok=false)
    ; (ResTrace=[interrupted|_]
    -> Ok=interrupted
    ; (Negated = 'False' -> %add_error(check_assertRef,'Assertion FAILS: ',PP),
    Ok=false ; Ok=true)
    )
    ),
    (Ok=true -> printsilent('OK'),nls
    ; Ok=interrupted -> print('*** Execution interrupted by user ***'),nl
    ; print('*** FALSE ***'),nl
    )
    ; add_error_fail(checkAssertion,'Internal Error, Assertion Checking Failed for: ',PP)
).

check_cst([],_,_,[]).

check_cst([ [bind(C,OtherVal)|T1] | TT], C, Value, [ T1 | PTT]) :-
    (Value=OtherVal -> check_cst(TT,C,Value,PTT)
    ; assert(non_det_constant(C)), peel2(TT,PTT)).

check_event_list_property(relative_deadlock_freedom,ID,TemplateList) :-
    relative_deadlock_freedom(ID,TemplateList).

check_event_list_property(valid_controller,ID,TemplateList) :-
    is_valid_controller_state(ID,TemplateList).

check_event_list_property(det_controller,ID,TemplateList) :-
    is_det_controller_state(ID,TemplateList).

check_invariantKO(ID,State) :-
    animation_mode(MODE),check_invariantKO(MODE,ID,State).

check_invariantKO(b,ID,State) :-
    check_invariantKO2(ID,State).

check_invariantKO(csp_and_b,ID,State) :-
    check_invariantKO2(ID,State).

check_invariantKO2(ID,_) :- invariant_violated(ID),!.

check_invariantKO2(ID,CurState) :-
    set_invariant_checked(ID), % only succeeds if we haven't checked invariant for ID yet
    % print(check_inv(ID)),nl,
    state_corresponds_to_initialised_b_machine(CurState,CurBState),
    ( preferences:preference(do_invariant_checking,false) -> assert(not_invariant_checked(ID))
    ; force_check_invariantKO(ID,CurBState)).

check_valid_operation(Op) :-
    (get_possible_language_specific_top_level_event(Op,_,_) -> true
    ; add_error(cbc_find_sequence,'Unknown operation/event: ',Op),fail).

check_we_are_in_b_mode(_) :- b_or_z_mode,!.

check_we_are_in_b_mode(Cmd) :- add_error(check_we_are_in_b_mode,'This command can only be performed in B,Z or TLA+ mode: ',Cmd),fail.

compute_all_inits :- is_concrete_constants_state_id(ID), compute_all_transitions_if_necessary(ID),fail.

compute_all_inits.

compute_all_transitions(CurID,CurState) :-
    catch_clpfd_overflow_call_for_state(CurID,compute_all_transitions2(CurID,CurState),clear_context_state).

compute_all_transitions2(CurID,CurState) :- /* compute all outgoing transitions for a given node */
    % set_context_state(CurID), % error_context is set for each operation below anyway.
    reset_max_reached,
    prepare_state_for_specfile_trans(CurState,PreparedCurState), % will perform unpacking of constants just once, for example
    ((time_out_preference_disabled % e.g., when using probcli -disable_time_out
    ; use_no_timeout(CurID))
    -> add_transitions_fail_loop(CurID,PreparedCurState)
    ; preferences:preference(time_out,CurTO),
    add_transitions__with_timeout_fail_loop(CurID,PreparedCurState,CurTO)
    ),
        add_partial_transitions(CurID,PreparedCurState), % also copies unsat component infos
    (max_reached -> assert_max_reached_for_node(CurID),MaxReached=true ; MaxReached=false), % TO DO: use max_reached(OpID)
    (CurID==root -> save_constants(MaxReached) ; add_new_transitions_to_cache(CurID))
. %,clear_context_state.

compute_all_transitions_if_necessary :-
    current_state_id(CurID),
    compute_all_transitions_if_necessary(CurID,false).

compute_all_transitions_if_necessary(CurID) :-
    compute_all_transitions_if_necessary(CurID,false).

compute_all_transitions_if_necessary(CurID,CheckInvariant) :-
    (retract_open_node(CurID) % will assert not_invariant_checked
    -> set_context_state(CurID),
    % first check invariant, relevant if we want to use specialized_inv proof information
    visited_expression(CurID,State),
    % TO DO: this does not expand concrete_constants: the expansion may be done twice below:
    % once for compute_invariant (corresponds_to_b...) and once for compute_all_transitions (prepare_state_for_specfile_trans)
    prepare_state_for_specfile_trans(State,PreparedState),
    (CheckInvariant==true
    -> compute_invariant_if_necessary_and_requested(CurID,PreparedState) ; true),
    compute_all_transitions(CurID,PreparedState),
    clear_context_state
    ; true).

compute_ample_set(CurID,CurState,POROptions) :-
    catch_clpfd_overflow_call_for_state(CurID,compute_ample_set2(CurID,CurState,POROptions),clear_context_state).

compute_for_dot([],_,[]).

compute_for_dot([String,TypedExpr|Tail],BState,[bind(Str,Value)|TS]) :-
    % allow user to specify labels for graphs ("lbl1", e1, "lbl2", e2, ...)
    get_texpr_expr(String,string(Str)),!,
    translate:translate_bexpression_with_limit(TypedExpr,100,EStr),
    format('Computing value for expression: ~w~n',[EStr]),
    b_compute_expression_with_prob_ids(TypedExpr,BState,Value),
    compute_for_dot(Tail,BState,TS).

compute_for_dot([TypedExpr|Tail],BState,[bind(Str,Value)|TS]) :-
    translate:translate_bexpression_with_limit(TypedExpr,100,Str),
    format('Computing value for expression: ~w~n',[Str]),
    b_compute_expression_with_prob_ids(TypedExpr,BState,Value),
    compute_for_dot(Tail,BState,TS).

compute_invariant_if_necessary(ID,State) :-
    animation_mode(MODE),compute_invariant_if_necessary(ID,State,MODE).

compute_invariant_if_necessary(ID,State,MODE) :-
    ( check_invariantKO(MODE,ID,State) -> true ; true).

compute_invariant_if_necessary_and_requested(ID,State) :-
    enter_new_error_scope(ErrScID,compute_invariant_if_necessary_and_requested), % here we setup a new error scope; see comment for force_check_invariantKO below
    compute_invariant_if_necessary(ID,State),
    exit_error_scope(ErrScID,_ErrOcc,compute_invariant_if_necessary_and_requested). % should we do something with error occured result ?

compute_state_information_if_necessary(CurID) :-
    compute_all_transitions_if_necessary(CurID,true).

convert_explain_tag(ptrue,explaintrue).

convert_explain_tag(pfalse,explainfalse).

convert_explain_tag(X,X).

convert_trace_to_list_of_strings([],[]).

convert_trace_to_list_of_strings([action(AS,_)|T],[AS|CT]) :- !,
    %truncate_atom(AS,1000,TruncatedAS), % especially SETUP_CONSTANTS, INITIALISATION can be very large; leading to performance issues
    % get_action_trace now truncates
    convert_trace_to_list_of_strings(T,CT).

convert_trace_to_list_of_strings([H|T],[H|CT]) :- convert_trace_to_list_of_strings(T,CT).

convert_typed_varlist([],[],[]).

convert_typed_varlist([b(identifier(ID),Type,_)|T],[ID|IT],[Type|TT]) :-
    %print(ID), print(' : '), print(Type),nl,
    % db : set(couple(global(Name),global(Code))) a : set(integer) boolean
    convert_typed_varlist(T,IT,TT).

convert_value_to_tcl(int(X),R) :- !, R=X.

convert_value_to_tcl(pred_true,R) :- !, R=1.

convert_value_to_tcl(pred_false,R) :- !, R=0.

convert_value_to_tcl(string(X),R) :- !, R=X.

convert_value_to_tcl(R,R) :- print(cannot_convert_to_tcl(R,R)),nl.

count_nodes :-
    refinement_checker: dvisited(_NodeID),
    nr_csp_process_state(NrNodes),
    NewNrNodes is NrNodes +1,
    retractall(nr_csp_process_state(_)),
    assert(nr_csp_process_state(NewNrNodes)),
    fail.

count_nodes.

csp_ref_style('[T=',trace). % Trace Refinement

csp_ref_style('T',trace). % Trace Refinement

csp_ref_style('[SF=',singleton_failures). % Singleton Failures Refinement

csp_ref_style('[F=',failures). % Failures Refinement

csp_ref_style('[R=',refusals). % Refusals Refinement

csp_ref_style('[RD=',refusals_div). % Refusals-Divergence Refinement

csp_ref_style('F',failures). % Failures Refinement

csp_ref_style('[FD=',X) :- csp_ref_style('FailureDivergence',X).

csp_ref_style('FD',X) :- csp_ref_style('FailureDivergence',X).

csp_ref_style('Trace',trace).

csp_ref_style('Failure',failures).

csp_ref_style('FailureDivergence',failure_divergences).

csp_ref_style('RefusalTesting',refusals).

csp_ref_style('RefusalTestingDiv',refusals_div).

csp_ref_style('RevivalTesting',revival) :- add_error(unsupported_refinement_operator,'[V= refinement not yet supported.').

csp_ref_style('RevivalTestingDiv',revival_div) :- add_error(unsupported_refinement_operator,'[VD= refinement not yet supported.').

decompose_expression_for_dot(b(couple(A,B),_,_)) --> !,
    decompose_expression_for_dot(A), decompose_expression_for_dot(B).

decompose_expression_for_dot(b(rec(Fields),_,_)) --> !,decompose_fields_for_dot(Fields).

decompose_expression_for_dot(X) --> [X].

decompose_fields_for_dot([]) --> [].

decompose_fields_for_dot([field(Name,Val)|T]) --> [b(string(Name),string,[]),Val], decompose_fields_for_dot(T).

dif_ID(ID1,ID2) :- (number(ID1),number(ID2) -> ID2>ID1 ; ID1 \= ID2).

do_model_check(_Nr,NodesAnalysed,_LimitTime,Res,FindDeadlocks,FindInvViolations,FindGoal,
    FindAssViolations,_StopFullCoverage,_PartialOrderReduction,_PartialGuardsEvaluation,ForceInspectExistingNodes) :-
    (tcltk_state_space_only_has_root_node -> true % Then also look at the root node
    ; ForceInspectExistingNodes == 1),
    search_among_existing_nodes(Res,FindDeadlocks,FindInvViolations,FindGoal,
    FindAssViolations), Res \=all, NodesAnalysed=0.

do_model_check(LimitNr,NodesAnalysed,LimitTime,Res,FindDeadlocks,FindInvViolations,FindGoal,
    FindAssViolations,StopFullCoverage,PartialOrderReduction,PartialGuardsEvaluation,_) :-
    update_ass(FindAssViolations,FindAssViolations2),
    open_search(LimitNr,NodesAnalysed,LimitTime,Res,FindDeadlocks,FindInvViolations,FindGoal,
    FindAssViolations2,StopFullCoverage,PartialOrderReduction,PartialGuardsEvaluation).

equivalent_states(S1,true,S2,true) :- \+(\+(S1=S2)). /* IMPROVE, may even

eval_string_in_cur_state(String,Typed,Value) :-
    %format('Parsing : "~w"~n',[String]),
    bmachine:parse_expression_raw_or_atom_with_prob_ids(String,Typed),
    current_state_id(CurID), prob2_interface:get_state(CurID,EState),
    %print(evaluating_in_state(CurID)),nl,
    b_compute_expression_with_prob_ids(Typed,EState,Value).

evaluate_bexpr_over_state(Stream,Expr,ValueTemplate,Columns,ResultColStrings,BState,OpName) :-
    format(Stream,'~w,',[OpName]),
    b_compute_expression_with_prob_ids(Expr,BState,Value),
    copy_term((ValueTemplate,Columns),(Value,ResultCols)),
    my_print_csv_value(ResultCols,Stream),
    maplist(translate:translate_bvalue,ResultCols,ResultColStrings),
    nl(Stream).

evaluate_expression_over_history_to_csv_file(Expr,File) :-
    parse_machine_expression(Expr,TypedExpr),
    get_bexpression_column_template(TypedExpr,ValueTemplate,ColHeaders,Columns),
    format('Writing CSV file: ~w~n',[File]),
    open(File,write,Stream),
    format(Stream,'OPERATION,',[]),
    my_print_csv_atoms(ColHeaders,Stream),
    call_cleanup(map_over_history(evaluate_bexpr_over_state(Stream,TypedExpr,ValueTemplate,Columns),_),
    close(Stream)),
    format('Finished writing CSV file: ~w~n',[File]).

extract_actions([],_,_,[],[]).

extract_actions([(_,Term,_)|T],CurID,Parameters,Srest,ET) :-
    member(no_query_operations,Parameters),
    query_op_transition(Term),
    !,
       extract_actions(T,CurID,Parameters,Srest,ET).

extract_actions([(ActionId,Term,Dst)|T],CurID,Parameters,[(ActionId,Str,Term,Dst)|Srest],[Str|ET]) :-
       time_out_call(translate_event_with_src_and_target_id(Term,CurID,Dst,Str),
                    Str='**TIMEOUT**'),
       extract_actions(T,CurID,Parameters,Srest,ET).