cbc_path_solver

add_constants_to_state_space(ConstantsState,TestStates,TestStates,[],root) :-
    empty_state(ConstantsState),!.

add_constants_to_state_space(ConstantsState,TestStates,ConstTestStates,[Tuple],ConstantsID) :-
    Tuple = (SetupID,Setup,root,ConstantsID),
    specfile:create_setup_constants_operation(ConstantsState,complete_properties,Setup),
    tcltk_interface:tcltk_add_new_transition_transid(root,Setup,ConstantsID,concrete_constants(ConstantsState),[],SetupID),
    remove_constants_from_state(TestStates,ConstantsState,ConstantsID,ConstTestStates).

add_operations_to_state_space([],_,[],[],[]).

add_operations_to_state_space([Operation|Orest],PrevId,[State|Srest],[TransInfo|Trest],[Tuple|Irest]) :-
    Tuple = (OpId,Operation,PrevId,NextId),
    tcltk_interface:tcltk_add_new_transition_transid(PrevId,Operation,NextId,State,TransInfo,OpId),
    add_operations_to_state_space(Orest,NextId,Srest,Trest,Irest).

catch_enumeration_warning_and_overflow(Call,Handler) :-
    % throw/1 predicate raises instantiation_error
    catch_clpfd_overflow_call3(
    catch(Call, enumeration_warning(enumerating(_),_Type,_,_,critical), call(Handler)),
    message, % could also be silent
    call(Handler)).

create_testcase_path(INIT,Events,EndPredicate,Timeout,Result) :-
    % allow user interrupts during the search, just fail if that happens
    testcase_path_timeout(INIT,Timeout,Events,EndPredicate,ConstantsState,Operations,TestStates,TransInfos,R),
    ( R==ok ->
    add_constants_to_state_space(ConstantsState,TestStates,ConstTestStates,SetupSequence,StartStateId),
    add_operations_to_state_space(Operations,StartStateId,ConstTestStates,TransInfos,OpSequence),
    append(SetupSequence,OpSequence,Result)
    ; Result = R).

create_testcase_path_nondet(INIT,Events,EndPredicate,Result) :-
    % allow user interrupts during the search, just fail if that happens
    testcase_path(INIT,Events,EndPredicate,ConstantsState,Operations,TestStates,TransInfos),
    add_constants_to_state_space(ConstantsState,TestStates,ConstTestStates,SetupSequence,StartStateId),
    add_operations_to_state_space(Operations,StartStateId,ConstTestStates,TransInfos,OpSequence),
    append(SetupSequence,OpSequence,Result).

eval_predicate(Predicate,State,WF) :-
    empty_state(EmptyState),
    b_test_boolean_expression(Predicate,EmptyState,State,WF).

get_init_option_paras(init,init,none).

get_init_option_paras(typing,typing,none).

get_init_option_paras(typing(Pred),typing,Pred). % just use typing from invariant and add P

get_init_option_paras(invariant,invariant,none).

get_init_option_paras(pred(Pred),invariant,Pred). % add P to invariant

get_init_option_paras(INITIALISE,_,_) :-
    add_internal_error('Illegal init option:',get_init_option_paras(INITIALISE)),fail.

get_precondition_from_translated_alloy_operation(b(precondition(TPrecondition,_),subst,_), Precondition) :-
    !,
    Precondition = TPrecondition.

get_precondition_from_translated_alloy_operation(_, b(truth,pred,[])).

init_opt_has_predicate(Option,Pred) :- get_init_option_paras(Option,_,Pred),!, Pred \= none.

just_typing_opt(Option) :- get_init_option_paras(Option,Typing,_), !, Typing=typing.

remove_constants_from_state([],_,_,[]).

remove_constants_from_state([InState|Irest],Constants,ConstId,[const_and_vars(ConstId,OutState)|Orest]) :-
    append(OutState,Constants,InState),!, % assume constants are at hend
    remove_constants_from_state(Irest,Constants,ConstId,Orest).

set_up_a_typed_state(ConstantState,ValidState,WF) :-
    set_up_constants_typed_state(ConstantState,WF),
    b_get_machine_variables(Variables),
    % create_target_state(Variables,Values,ConstantsState,ValidState,WF),
    set_up_typed_localstate(Variables,_Values,TypedVals,ConstantState,ValidState,positive),
    b_tighter_enumerate_all_values(TypedVals,WF).

set_up_a_valid_state(ConstantState,ValidState,WF) :-
    set_up_constants_state(ConstantState,WF),
    b_get_machine_variables(Variables),
    % create_target_state(Variables,Values,ConstantsState,ValidState,WF),
    set_up_typed_localstate(Variables,_Values,TypedVals,ConstantState,ValidState,positive),
    b_tighter_enumerate_all_values(TypedVals,WF),
    b_get_invariant_from_machine(Invariant),
    empty_state(EmptyState),
    b_test_boolean_expression(Invariant,EmptyState,ValidState,WF).

set_up_constants_state(ConstantsState,_WF) :-
    \+ not_all_transitions_added(root),
    \+ state_space:max_reached_or_timeout_for_node(root),
    % We should also check enumeration warnings : [DONE with max_reached_or_timeout_for_node]
    (state_space:transition(root,_,N) -> true),
    \+ ( state_space:transition(root,_,N2), N2\=N ),
    state_space:visited_expression(N,concrete_constants(ConstantsState)),
    !, % there is only one possible valuation of the constants
    debug_format(19,'Reusing constant values from state id ~w (only solution for PROPERTIES/axioms)~n',[N]).

set_up_constants_state(ConstantState,WF) :-
    b_get_properties_from_machine(Properties),
    b_get_machine_constants(Constants),
    empty_state(EmptyState),
    set_up_typed_localstate(Constants,_FreshVars,TypedVals,EmptyState,ConstantState,positive),
    static_symmetry_reduction_for_global_sets(ConstantState), % from b_global_sets
    b_tighter_enumerate_all_values(TypedVals,WF),
    b_test_boolean_expression(Properties,EmptyState,ConstantState,WF).

set_up_constants_typed_state(ConstantState,WF) :-
    b_get_machine_constants(Constants),
    empty_state(EmptyState),
    set_up_typed_localstate(Constants,_FreshVars,TypedVals,EmptyState,ConstantState,positive),
    b_tighter_enumerate_all_values(TypedVals,WF).

testcase_initialise(ConstantState,InitialState,Initialisation,TransInfo,WF) :-
    set_up_constants_state(ConstantState,WF),
    set_up_initialisation(ConstantState,InitialState,Initialisation,TransInfo,WF). % TO DO: here I would like to be able to set up the invariant instead, if requested by another parameter

testcase_path(INITIALISE,Events,EndPredicate,NormalisedConstantsState,OPS,StateSequence,TINFOS) :-
    init_wait_flags(WF0,[testcase_path]),
    opt_push_wait_flag_call_stack_info(WF0,using_state(cbc_path_solver,InitialState),WF),
    (INITIALISE=init
    -> OPS = [OpInit|Operations], TINFOS = [ITransInfo|OpTransInfos],
    testcase_initialise(ConstantsState,InitialState,OpInit,ITransInfo,WF)
    % TODO: push Init on WF call stack
    ; OPS = Operations, TINFOS = OpTransInfos,
    (just_typing_opt(INITIALISE)
    -> set_up_a_typed_state(ConstantsState,InitialState,WF) % only set up types
    ; set_up_a_valid_state(ConstantsState,InitialState,WF) % set up invariant
    ),
    % TO DO: project away constants and variables not needed for OPS and Predicates
    (init_opt_has_predicate(INITIALISE,InitialPredicate)
    -> eval_predicate(InitialPredicate,InitialState,WF)
    ; true)
    ),
    testcase_set_up_events(Events,InitialState,ConstantsState,Operations,States,FinalState,OpTransInfos,WF,WF2),
    eval_predicate(EndPredicate,FinalState,WF2),
    ground_wait_flags(WF2),
    normalise_states([InitialState|States],StateSequence),
    normalise_state(ConstantsState,NormalisedConstantsState).

testcase_path_interrupt(INIT,Events,EndPredicate,ConstantsState,Operations,TestStates,TransInfos,Result) :-
    catch_clpfd_overflow_call3(
    testcase_path_interrupt2(INIT,Events,EndPredicate,ConstantsState,Operations,TestStates,TransInfos,Result),
    message, % no need to create warning or error; we return clpfd_overflow as result
    Result=clpfd_overflow).

testcase_path_interrupt2(INIT,Events,EndPredicate,ConstantsState,Operations,TestStates,TransInfos,Result) :-
    user_interruptable_call_det(testcase_path(INIT,Events,EndPredicate,ConstantsState,Operations,TestStates,TransInfos),
    Interrupt),
    (Interrupt==ok -> Result=ok ; Result=interrupt).

testcase_path_timeout(INIT,0,Events,EndPredicate,ConstantsState,Operations,TestStates,TransInfos,R) :-
    !,testcase_path_interrupt(INIT,Events,EndPredicate,ConstantsState,Operations,TestStates,TransInfos,R).

testcase_path_timeout(INIT,TimeoutMs,Events,EndPredicate,ConstantsState,Operations,TestStates,TransInfos,Result) :-
    safe_time_out(testcase_path_interrupt(INIT,Events,EndPredicate,ConstantsState,Operations,TestStates,TransInfos,R),
    TimeoutMs,
    T),
    (T==success -> Result=R ; Result=timeout).

testcase_path_timeout_catch(Pred,TIMEOUT,Seq,P2,Csts,Ops,TestS,TI,Res) :-
    enter_new_error_scope(ScopeID,testcase_path_timeout_catch),
    (catch_enumeration_warning_and_overflow(
    cbc_path_solver:testcase_path_timeout(Pred,TIMEOUT,Seq,P2,Csts,Ops,TestS,TI,Res),
    Res=virtual_time_out)
    -> exit_error_scope(ScopeID,_ErrOcc,testcase_path_timeout_catch)
    ; (critical_enumeration_warning_occured_in_error_scope ->
    debug_format(19,'Enumeration warning occurred and is treated as timeout due to failure to find solution.~n',[]),
    exit_error_scope(ScopeID,_ErrOcc,testcase_path_timeout_catch),
    Res=virtual_time_out
    ; exit_error_scope(ScopeID,_ErrOcc,testcase_path_timeout_catch),
    fail
)
).

testcase_predicate(Predicate) :-
    init_wait_flags(WF,[testcase_predicate]),
    (just_typing_opt(Predicate) ->
    set_up_a_typed_state(_ConstantsState,InitialState,WF) % only set up types
    ;
    set_up_a_valid_state(_ConstantsState,InitialState,WF)),
    (init_opt_has_predicate(Predicate,Pred) ->
    eval_predicate(Pred,InitialState,WF)
    ; true),
    ground_wait_flags(WF).

testcase_predicate_timeout(Pred,Timeout,Result) :-
    catch((
    safe_time_out(testcase_predicate(Pred), Timeout, T),
    (T==success -> Result=ok ; Result=timeout)
    ), enumeration_warning(_,_,_,_,_), Result=timeout).

testcase_set_up_events([],State,_ConstState,[],[],State,[],WF,WF).

testcase_set_up_events([Event|Erest],InState,ConstantState,[Operation|Orest],
    [InterState|Srest],OutState,[TransInfo|Trest],WF,WF3) :-
    set_up_transition(Event,Operation,ConstantState,InState,InterState,TransInfo,WF),
    push_wait_flag_call_stack_info(WF,after_event(Operation),WF2),
    testcase_set_up_events(Erest,InterState,ConstantState,Orest,Srest,OutState,Trest,WF2,WF3).

validate_solver_result_for_command(RunOrCheck, Res, CmdIsValid) :-
    Res == contradiction_found,
    !,
    ( RunOrCheck == check
    -> CmdIsValid = true
    ; CmdIsValid = false
).

validate_solver_result_for_command(RunOrCheck, Res, CmdIsValid) :-
    Res = solution(_),
    ground(Res),
    !,
    ( RunOrCheck == run
    -> CmdIsValid = true
    ; CmdIsValid = false
).

validate_solver_result_for_command(_, _, unknown).

verify_alloy_command(ProvidedCmdName, Solver, CmdIsValid, IsCheckCmd, Res) :-
    (ProvidedCmdName = '_' , b_get_machine_operation(CmdName, _, _, _) -> true % _ as a wildcard for first command
    ; CmdName = ProvidedCmdName),
    if(b_get_machine_operation(CmdName, _, _, Body),
    true,
    (add_error(cbc_path_solver,'Unknown Alloy command name:',CmdName),
    findall(Other,b_get_machine_operation(Other, _, _, _),OL),
    add_message(cbc_path_solver,'Available B operations: ',OL),fail)),
    get_precondition_from_translated_alloy_operation(Body, Precondition),
    b_get_properties_from_machine(Properties),
    conjunct_predicates([Properties,Precondition], Conj),
    start_ms_timer(Timer),
    ( Solver == prob
    -> solve_predicate(Conj, _, 1, [use_smt_mode/true,use_clpfd_solver/true,use_chr_solver/false,clean_up_pred,allow_improving_wd_mode/true], Res)
    ; Solver == probkodkod
    -> solve_predicate(Conj, _, 1, [use_smt_mode/true,use_clpfd_solver/true,use_chr_solver/false,clean_up_pred,allow_improving_wd_mode/true,use_solver_on_load/kodkod], Res)
    ; Solver == probsmt
    -> cdclt_solve_predicate(Conj, _SolvedWDPred, Res)
    ; Solver == z3,
    smt_solve_predicate(z3, Conj, _, Res)
    ),
    ( atom_concat(check, _, CmdName)
    -> validate_solver_result_for_command(check, Res, CmdIsValid),
    IsCheckCmd = true
    ; validate_solver_result_for_command(run, Res, CmdIsValid),
    IsCheckCmd = false
    ),
    (silent_mode(on) -> true
    ; (Res=solution(_) -> RS=solution ; RS=Res),
    ajoin(['Checking Alloy command ',CmdName,' with ',Solver,'; result = ',RS],Msg),
    stop_ms_walltimer_with_msg(Timer,Msg)).

verify_alloy_command(ProvidedCmdName, Solver, CmdIsValid, IsCheckCmd, Res) :-
    add_internal_error('Call failed:',verify_alloy_command(ProvidedCmdName, Solver, CmdIsValid, IsCheckCmd, Res)).