eclipse_interface

cbc_dynamic_assertion_violation_checking(Result) :-
    user_interruptable_call_det(catch_clpfd_overflow_call1(cbc_dynamic_assertions_check(State)),InterruptResult), !,
    ( InterruptResult = interrupted ->
    Result = interrupted
    ; State = time_out ->
    Result = interrupted
    ; State = no_counterexample_found ->
    Result = no_counterexample_found
    ; functor(State,no_counterexample_exists,_) -> % arity is 0
    Result = no_counterexample_exists
    ;
    State = counterexample_found(RealState),
    Result = counterexample_found(Transition,StateId),
    transition_name(dynamic,TransName),
    create_helper_transition(root,TransName,RealState,StateId,Transition)).

cbc_static_assertion_violation_checking(Result) :-
    user_interruptable_call_det(catch_clpfd_overflow_call1(cbc_static_assertions_check(State)),InterruptResult), !,
    ( InterruptResult = interrupted ->
    Result = interrupted
    ; State = time_out ->
    Result = interrupted
    ; State = no_counterexample_found ->
    Result = no_counterexample_found
    ; functor(State,no_counterexample_exists,_) -> % arity is 3
    Result = no_counterexample_exists
    ;
    State = counterexample_found(RealState),
    Result = counterexample_found(Transition,StateId),
    transition_name(static,TransName),
    create_helper_transition(root,TransName,RealState,StateId,Transition)).

clear_loaded_machines :-
    clear_loaded_machines_wo_errors,
    reset_errors,
    % now done via event-handling: reset_all_temporary_preferences,
    garbage_collect_atoms,!. % reclaim atoms if possible

clear_loaded_machines :- add_error(clear_loaded_machines,'clear_loaded_machines Failed').

clear_loaded_machines_wo_errors :-
    announce_event(reset_specification),
    announce_event(clear_specification).

computeOperationsForState(StateID, OpsAndIDs) :- /* compute the enabled operations
    (without the backtrack options) for a state ID which is not necessarily the current one */
    visited_expression_id(StateID),
    tcltk_interface:tcltk_compute_options(StateID,OpsSTAndIDs),
    %print('OpsSTAndIDs: '),print(OpsSTAndIDs),nl,
    (filter_ops_and_ids(OpsSTAndIDs,StateID,OpsAndIDs) -> true
    ; print(filter_ops_and_ids_failed(OpsSTAndIDs)),nl,fail).

convert_errors([],[]).

convert_errors([Error|InRest],[error(Event,Short,Long)|OutRest]) :-
    ( Error = eventerror(Event,EError,Trace) ->
    translate_event_error(EError,Short),
    explain_event_trace(Trace,LongStr,_Span),
    safe_atom_codes(Long,LongStr)
    ;
    (get_event_from_state_error(Error,Event) -> true
    ; Event = '*unknown*' % we don't know which event is responsible
    ),
    translate_state_error(Error,Short),
    explain_state_error(Error,_Span,LongStr),
    safe_atom_codes(Long,LongStr)
    ),
    convert_errors(InRest,OutRest).

create_helper_transition(SrcId,Op,DstState,DstId,Transition) :-
    tcltk_interface:tcltk_add_new_transition_transid(SrcId,Op,DstId,DstState,[],TransId),
    transition(SrcId,Action,TransId,DstId),!,
    create_operation_term(TransId,Action,SrcId,DstId,Transition).

create_operation_term(TransId,Op,CurID,NewID, JavaOpTerm) :-
    (filter_op(TransId,Op,CurID,NewID, JavaOpTerm) -> true
    ; add_error(eclipse_interface,'filter_op failed: ', filter_op(TransId,Op,CurID,NewID, JavaOpTerm)),fail).

deadlock_freedom_check(Result) :-
    create_texpr(truth,pred,[],Predicate),
    deadlock_freedom_check1(Predicate,Result).

deadlock_freedom_check(Predicate,Result) :-
    b_type_expression(Predicate,[variables],pred,TPredicate,Errors),
    ( Errors == [] ->
    deadlock_freedom_check1(TPredicate,Result)
    ;
    Result = errors(Errors)).

deadlock_freedom_check1(Predicate,Result) :-
    % always do a deadlock check with SMT mode enabled
    call_with_smt_mode_enabled(deadlock_freedom_check2(Predicate,Result)).

deadlock_freedom_check2(Predicate,Result) :-
    user_interruptable_call_det(clpfd_interface:catch_clpfd_overflow_call1(
    b_state_model_check:cbc_deadlock_freedom_check(State,Predicate,0)),
    InterruptResult),!,
    ( InterruptResult = interrupted ->
    Result = interrupted
    ; State = time_out ->
    Result = interrupted
    ;
    Result = deadlock(Transition,StateId),
    create_helper_transition(root,deadlock_check,State,StateId,Transition)).

deadlock_freedom_check2(_Predicate,no_deadlock_found).

do_ltl_modelcheck(Formula,Max,Mode,Atomics,Structure,Result) :-
    typecheck_temporal_formula(Formula,TypeCheckedFormula,Status),
    ( Status=ok ->
    ltl_formula_structure(TypeCheckedFormula,Atomics,Structure),
    ltl_model_check_with_ce(TypeCheckedFormula,Max,Mode,Result1),
    ltl_adapt_operations(Result1,Result)
    ;
    Atomics=[], Structure=[],
    Result=typeerror([])).

do_modelchecking(Time, Options, Result, StatsRes) :-
    MaxNumberOfStatesToCheck=100000,
    do_modelchecking(MaxNumberOfStatesToCheck, Time, Options, Result, StatsRes).

evaluate_expression(Expression,Result) :-
    current_expression(_CurID,CurState),
    b_interpreter:b_compute_expression_nowf(Expression,[],CurState,Result,'ProB1-Java',0).

evaluate_raw_expression(StateID, Raw, Val):-
    bmachine:b_type_expression(Raw, [variables], _, TExpr, Errors),
    ( var(TExpr) ->
    print(error_while_typing_raw_expression(Errors)),nl,
    flush_output,
    !,
    fail
    ;
    get_state(StateID, State),
    get_value_string_of_formula(State, [], TExpr, 400, Val) % get_value_of_expression or predicate without wd errors
).

evaluate_raw_expressions(StateID, Raws, Vals):-
    maplist(evaluate_raw_expression(StateID), Raws, Vals).

evaluation_expand_formula(Id,Label,Children) :-
    % Currently, we do not want to see the rodin information positons
    % in the expression viewer
    suppress_rodin_positions(CHNG),
    bv_expand_formula(Id,Label,Children),
    reset_suppress_rodin_positions(CHNG).

evaluation_get_top_level(Tops) :-
    % Currently, we do not want to see the rodin information positons
    % in the expression viewer
    suppress_rodin_positions(CHNG),
    bv_get_top_level(TopIds),
    findall( top(Id,Label,Children),
    ( member(Id,TopIds), bv_expand_formula(Id,Label,Children) ),
    Tops),
    reset_suppress_rodin_positions(CHNG).

evaluation_get_values(Ids,StateId,Values) :-
    bv_get_values(Ids,StateId,Values).

evaluation_insert_formula(AST,ParentId,Id) :-
    b_type_expression(AST,[variables],_,Typed,Errors),
    % this also calls ast_cleanup; we could temporarily set OPTIMIZE_AST to false
    ( Errors == [] ->
    bv_insert_formula(Typed,ParentId,Id)
    ;
    add_error_and_fail(eclipse_interface,'Could not type-check AST','')).

execute_custom_operation(CurID,OpName,Operation_op,Max) :-
    visited_expression(CurID,InState),
    specfile:compute_operation_effect_max(InState,OpName,Operation,NewState,_TransPathInfo,Max),
    % logger:writeln_log(sol(OpName,NewState)),
    tcltk_interface:add_trans_id(CurID,Operation,NewState,NewID,TransId),
    % logger:writeln_log(ids(OpName,Operation,NewID,TransId)),
    create_operation_term(TransId,Operation,CurID,NewID, Operation_op).

execute_custom_operations(CurID, OpName, ParsedPredicate, MaxNrOfSolutions, TOperations, Errors) :-
    setCurrentState(CurID),
   
    ( (OpName = '$initialise_machine';OpName = '$setup_constants' ) -> Scope = [prob_ids(visible),variables];
    b_top_level_operation(OpName),
    b_get_machine_operation(OpName,_,Parameters,_),
    Scope = [identifier(Parameters),prob_ids(visible),variables] % prob scope allows one to use identifiers for deferred set elements
    ),
    (MaxNrOfSolutions<1
    -> add_message(eclipse_interface,'execute_custom_operations MaxNrOfSolutions < 1: ',MaxNrOfSolutions)
    ; true),
    bmachine:b_type_expression(ParsedPredicate, Scope, _, TypedPred, Errors),
    inline_prob_deferred_set_elements_into_bexpr(TypedPred,CP),
    assert_temp_typed_predicate(CP),
    set_context_state(CurID,execute_custom_operations),
    findall(TO, execute_custom_operation(CurID,OpName,TO,MaxNrOfSolutions), TOperations),
    reset_temp_predicate,
    clear_context_state.

extract_args_and_return_values(Term,OpName,Arguments) :-
    ( Term='-->'(OpTerm,Results) ->
    ( result_warning_emitted -> true
    ;
    print('Warning: results of operations are currently treated like arguments'),nl,
    assertz(result_warning_emitted)),
    append(Results,Args,Arguments)
    ; Term=OpTerm,Args=Arguments
    ),
    OpTerm =.. [OpName|Args].

extract_csp_args_and_return_values(io(Args,ChName,_SPAN),ChName,Args).

extract_csp_args_and_return_values(start_cspm(Name),Name,[]).

extract_csp_args_and_return_values(start_cspm_MAIN,'start_cspm_MAIN',[]).

extract_csp_args_and_return_values(tick(_),tick,[]).

extract_csp_args_and_return_values(tau(_),tau,[]).

extract_csp_args_and_return_values(_OP,'?',[]).

filter_event_stack([],[]).

filter_event_stack([event(Name,Params)|Irest],[event(Name,Strings)|Orest]) :-
    translate_bvalue_l(Params,Strings),
    filter_event_stack(Irest,Orest).

filter_op(TransId,OpTerm,Src,Dst,JavaOpTerm) :-
    (animation_mode(cspm) ->
    filter_op_csp(TransId,OpTerm,Src,Dst,JavaOpTerm)
    ;
    filter_op1(TransId,OpTerm,Src,Dst,JavaOpTerm)).

filter_op1(TransId,OpTerm,Src,Dst,
    op(TransId,Op,Src,Dst,Arguments,ArgumentsPretty,Infos,State)) :-
    extract_args_and_return_values(OpTerm,Op,Arguments),
    get_state(Dst,BState), translate:translate_bstate(BState,State),
    prettyprint(Arguments,ArgumentsPretty),
    get_event_infos(TransId,Infos).

filter_op_csp(TransId,OpTerm,Src,Dst,op(TransId,Op,Src,Dst,Arguments,ArgumentsPretty,Infos,CSPState)) :-
    extract_csp_args_and_return_values(OpTerm,Op,Arguments),
    translate:translate_event(OpTerm,PPEvent),
    tools: split_atom(PPEvent,['.','!'],[_Op|ArgumentsPretty]),
    get_state(Dst,CSPState),
    get_event_infos(TransId,Infos).

filter_ops_and_ids([],_,[]).

filter_ops_and_ids([OpTuple|T],StateID,[FOp|FT]) :-
    ((OpTuple = (Id,OpTerm,Dst), create_operation_term(Id,OpTerm,StateID,Dst,FOp))
    -> true
    ; print(filter_op_failed(OpTuple,StateID)),nl, FOp = ('?')),
    filter_ops_and_ids(T,StateID,FT).

filter_transition_info(event(StackI),event(StackO)) :- !,
    filter_event_stack(StackI,StackO).

filter_transition_info(I,I).

filter_transition_infos([],[]).

filter_transition_infos([I|Irest],[O|Orest]) :-
    filter_transition_info(I,O),
    filter_transition_infos(Irest,Orest).

find_shortest_trace_to_current_state(TraceStrings) :-
    find_shortest_trace_to_current_state2(TraceStrings, _).

find_shortest_trace_to_current_state2(TraceStrings, StateIDs) :-
    current_state_id(ID),
    find_shortest_trace_to_node(root,ID,TraceIds,StateIDs),
    extract_term_trace_from_transition_ids(TraceIds,Trace),
    translate_events(Trace,TraceStrings).

find_state_satisfying_predicate(Predicate,Result) :-
    b_type_expression(Predicate,[variables],pred,TPredicate,Errors),
    ( Errors == [] ->
    find_state_satisfying_predicate1(TPredicate,Result)
    ;
    Result = errors(Errors)).

find_state_satisfying_predicate1(Predicate,Result) :-
    user_interruptable_call_det(clpfd_interface:catch_clpfd_overflow_call1(
    b_state_model_check:b_set_up_valid_state_with_pred(State,Predicate)),
    InterruptResult),!,
    ( InterruptResult = interrupted ->
    Result = interrupted
    ; State = time_out ->
    Result = interrupted
    ;
    Result = state_found(Transition,StateId),
    create_helper_transition(root,find_valid_state,State,StateId,Transition)).

find_state_satisfying_predicate1(_Predicate,no_valid_state_found).

getAllOperations(L) :-
    (b_or_z_mode
    -> findall(OperationName, b_top_level_operation(OperationName), L)
    ; L=[]). % FIXME: provide list for CSP-M

getCurrentStateID(CurID) :-
    current_state_id(CurID).

getErrorMessages(WarningsOnly,ListOfErrMsgs) :-
    (real_error_occurred -> WarningsOnly = false ; WarningsOnly = true),
    (get_all_errors_and_reset(ListOfErrMsgs) -> true ; ListOfErrMsgs=[]).

getOperationParameterNames(Operation,Paras) :-
    b_get_machine_operation_parameter_names(Operation,Paras).

getStateValues(CurID,VariableState) :- /* get variable values */
    get_state(CurID,CurBState),
    findall( binding(Id,nope,PPValue),
    (member(bind(Id,Value),CurBState),
    (translate_bvalue(Value,PPValue) -> true ; PPValue='**pretty-print failed**')),
    VariableState).

get_disj_lhs(implication(LHS,_),LHS).

get_disj_lhs(disjunction(LHS,_),NLHS) :- create_negation(LHS,NLHS).

get_error_event_from_context(span_context(_,Context),Event) :-
    get_error_event_from_context(Context,Event).

get_error_event_from_context(operation(Event,_State),Event).

get_event_from_state_error(abort_error(TYPE,_Msg,_ErrTerm,ErrorContext),Event) :-
    (get_error_event_from_context(ErrorContext,Event) -> true ; functor(TYPE,Event,_)).

get_event_infos(TransId,Infos) :-
    findall(Info, transition_info(TransId,Info), Infos1),
    filter_transition_infos(Infos1,Infos).

get_guard_with_one_negated(OpName,SingleGuard,FullModifiedGuard) :-
    get_operation_enabling_condition(OpName,Parameters,EnablingCondition,_BecomesSuchVars,_Precise,false,true),
    % TO DO: partition; avoid lifting becomes_such_that conditions
    % (in EventB the feasibility PO will ensure that Guard => BecomeSuchThat is ok)
    negate_one_guard(EnablingCondition,SingleGuard,ModifiedEnablingCondition),
    construct_optimized_exists(Parameters,ModifiedEnablingCondition,FullModifiedGuard).

get_machine_objects(Sections,SetElements,Constants,Variables,Operations) :-
    b_get_animated_sections(Sections),
    findall(TId,
    ( enum_global_type_limited(fd(Nr,Set),_),
    translate_bvalue(fd(Nr,Set),String),
    create_texpr(identifier(String),global(Set),[],TId)),
    SetElements),
    b_get_machine_constants(Constants),
    b_get_machine_variables(Variables),
    b_get_promoted_machine_operations(Operations1),
    maplist(remove_op,Operations1,Operations).

get_state_errors(StateId,Errors) :-
    findall(E, (state_error(StateId,_,E),E \== invariant_violated), Errs),
    convert_errors(Errs,Errors).

get_vacuous_guards(L) :-
    findall(G,vacuous_guard(_,G),L).

get_vacuous_invariants(L) :-
    findall(I,vacuous_invariant(I),L).

invariant_check(all,Result) :-
    findall(OpName,b_is_operation_name(OpName),Ops),
    invariant_check2(Ops,Result).

invariant_check(ops(Ops),Result) :-
    invariant_check2(Ops,Result).

invariant_check2(Ops,Result) :-
    call_with_smt_mode_enabled(user_interruptable_call_det(invariant_check3(Ops,Res,[]), Status)),
    (Status = interrupted -> Result = interrupted ; Result = Res).

invariant_check3([]) --> !.

invariant_check3([Op|Rest]) -->
    invariant_check_for_single_op(Op),
    invariant_check3(Rest).

invariant_check_for_single_op(OpName,In,Out) :-
    ( clpfd_interface:catch_clpfd_overflow_call1(
    b_state_model_check:state_model_check_invariant(OpName,State1,Operation,State2)) ->
    In = [counterexample(OpName,Trans1,Trans2)|Out],
    atom_concat( invariant_check_ , OpName, RootTrans),
    create_helper_transition(root, RootTrans,State1,StateId1,Trans1),
    create_helper_transition(StateId1,Operation,State2,_StateId2,Trans2)
    ;
    In = Out).

load_b_file(Filename) :- load_b_file(Filename,[]).

load_b_file(Filename,Options) :-
    clear_loaded_machines_wo_errors,
    set_animation_mode(b),
    set_currently_opening_file(Filename),
    (bmachine:b_load_machine_from_file(Filename,Options) % we can pass release_java_parser flag here
    -> set_currently_opened_b_file(Filename)
    ; set_failed_to_open_file(Filename),fail).

load_eventb_file(Filename) :-
    clear_loaded_machines_wo_errors,
    set_animation_mode(b), set_animation_minor_mode(eventb),
    set_currently_opening_file(Filename),
    (b_load_eventb_project(Filename)
    -> set_currently_opened_b_file(Filename)
    ; set_failed_to_open_file(Filename),fail
).

load_prob_file(Filename) :- load_prob_file(Filename,[]).

load_prob_file(Filename,Options) :- % one option is use_fastread
    clear_loaded_machines_wo_errors,
    set_animation_mode(b),
    set_currently_opening_file(Filename),
    (bmachine:b_load_machine_probfile(Filename,Options)
    -> set_currently_opened_b_file(Filename)
    ; set_failed_to_open_file(Filename),fail).

load_tla_file(Filename) :-
    call_tla2b_parser(Filename),
    tla2prob_filename(Filename,GeneratedProbFile),
    debug_println(10,loading_generated_prob_file(GeneratedProbFile)),
    load_prob_file(GeneratedProbFile),
    %load_b_file(GeneratedBFile),
    debug_println(10,set_animation_minor_mode(tla)),
    set_animation_minor_mode(tla). % TO DO: set before loading as parameter to load_prob_file ?

ltl_adapt_ce([],[]).

ltl_adapt_ce([atom(State,Evals,OpTuple)|Irest],[atom(State,Evals,Transition)|Orest]) :-
    ltl_adapt_ce2(OpTuple,State,Transition),
    ltl_adapt_ce(Irest,Orest).

ltl_adapt_ce2(none,_State,none).

ltl_adapt_ce2((TransId,Action,DstId),State,Transition) :-
    create_operation_term(TransId,Action,State,DstId,Transition).

ltl_adapt_operations(counterexample(CE1,LoopEntry,PathToCE1), counterexample(CE,LoopEntry,PathToCE)) :- !,
    filter_ops_and_ids(PathToCE1,root,PathToCE),
    ltl_adapt_ce(CE1,CE).

ltl_adapt_operations(Result,Result).

negate_one_guard(Conjunct,SingleGuard,ModifiedConjunct) :-
    conjunction_to_list(Conjunct,L),
    append(Rest1,[SingleGuard|Rest2],L),
    create_negation(SingleGuard,NegSingleGuard),
    append(Rest1,[NegSingleGuard|Rest2],NewGuard), % TO DO: better treatment for well-definedness !?
    conjunct_predicates(NewGuard,ModifiedConjunct).

op_tuples_to_full_operations([],[]).

op_tuples_to_full_operations([(Id,OpTerm,Src,Dst)|Trest],[Op|Orest]) :-
    create_operation_term(Id,OpTerm,Src,Dst,Op),
    op_tuples_to_full_operations(Trest,Orest).

prettyprint([],[]).

prettyprint([H|T],[P|R]) :- translate_bvalue(H,P), prettyprint(T,R).

quick_describe_unsat_properties(Res) :-
    tcltk_unsatisfiable_components_exist
    -> tcltk_quick_describe_unsat_properties(list(TRes),_Status), % sometimes this can be 'The properties were satisfiable' if tcltk_unsatisfiable_components_exist faulty
    Res = unsat_properties(TRes) % TO DO: use Status to say unsat or unknown_properties
    ; Res = no_unsat_properties_found.

refinement_check(ResultsString,Result) :-
    call_with_smt_mode_enabled(cbc_refinement_check(ResultsString,Result)).

remove_op(TId,NTId) :-
    remove_bt(TId,identifier(Id),identifier(NId),NTId),
    remove_op2(Id,NId).

remove_op2(op(Op),Op) :- !.

remove_op2(Op,Op).

sap_find_test_path(Events,EndPredicate,Timeout,Operations) :-
    type_predicate(EndPredicate,TypedPredicate),
    (create_testcase_path(init,Events,TypedPredicate,Timeout,Trace) -> true ; Trace = []),
    % Trace can be "timeout" or "interrupt", too
    (is_list(Trace) -> op_tuples_to_full_operations(Trace,Operations) ; Operations=Trace).

setCurrentState(ID) :- current_state_id(ID),!. % no need to jump

setCurrentState(ID) :- /* jumps to the given node; can be backtracked */
    visited_expression_id(ID),
    tcltk_interface:tcltk_goto_state(jump,ID).

set_application_type(T) :- % Note: can also be set as probcli option
    set_prob_application_type(T). % T can be tcltk, probcli, prob2, rodin,...

test_boolean_expression_in_node(ResID,BoolExpr) :-
    test_boolean_expression_in_node(ResID,BoolExpr,'ProB1-Java in state').

test_boolean_expression_in_node(ResID,BoolExpr,Kind) :-
    visited_expression(ResID,CurState),
    state_corresponds_to_initialised_b_machine(CurState,CurBState),
    set_context_state(ResID,test_boolean_expression_in_node), % also sets it for external functions
    call_cleanup(b_interpreter:b_test_boolean_expression_cs(BoolExpr,[],CurBState,Kind,ResID),
    clear_context_state).

transition_name(dynamic,Name) :- animation_minor_mode(eventb),!,
    Name = 'context_theorems_check'.

transition_name(dynamic,dynamic_asserion_check).

transition_name(static,Name) :- animation_minor_mode(eventb),!,
    Name = 'invariant_theorems_check'.

transition_name(static,static_asserion_check).

translate_bvalue_l([],[]).

translate_bvalue_l([V|Vrest],[S|Srest]) :-
    translate_bvalue(V,S),
    translate_bvalue_l(Vrest,Srest).

type_predicate(Predicate,TypedPredicate) :-
    b_type_expression(Predicate,[variables],pred,TypedPredicate,Errors),
    add_all_perrors(Errors,[],sap_target_predicate_type_error),
    no_real_perror_occurred(Errors).

vacuous_guard(OpName,Result) :-
    get_guard_with_one_negated(OpName,Guard,Neg),
    translate:translate_bexpression_with_limit(Guard,GuardTS),
    format('Checking vor vacuity: ~w : ~w~n',[OpName,GuardTS]),
    %translate:print_bexpr(Neg),nl,
    (test_boolean_expression_in_node(ResID,Neg,'vacuous guard')
    -> print(guard_individually_false_in(ResID)),nl,nl,
    fail
    ; print(' *** VACUOUS *** '),nl,nl,
    ajoin([OpName,' : ',GuardTS],Result)
).

vacuous_invariant(Inv) :-
    b_get_invariant_from_machine(Invariant),
    b_interpreter:member_conjunct(Inv,Invariant,_),
    get_texpr_expr(Inv,IE),get_disj_lhs(IE,LHS),
    print('Checking vor vacuity: '), translate:print_bexpr(Inv),nl,
    (test_boolean_expression_in_node(ResID,LHS,'vacuous invariant')
    -> print(rhs_triggered_in_state(ResID)),nl,nl, % Implication/disjunction trigger in at least one state
    fail
    ; print(' *** VACUOUS *** '),nl,nl
).