Dynamic Predicates: max_nr_replayed/1

1016 Lines

84 Predicates

Imported Modules: lists tools error_manager debug junit_tests translate_keywords avl debug

11 Exports

70 specified Imports

Imports	Exports
Name: module_info/2 Module: module_information Name: get_texpr_type/2 Module: bsyntaxtree Name: conjunct_predicates/2 Module: bsyntaxtree Name: b_machine_name/1 Module: bmachine Name: b_is_operation_name/1 Module: bmachine Name: b_get_machine_operation_typed_parameters/2 Module: bmachine Name: lookup_global_constant/2 Module: b_global_sets Name: get_preference/2 Module: preferences Name: preference/2 Module: preferences Name: temporary_set_preference/3 Module: preferences Name: reset_temporary_preference/2 Module: preferences Name: get_prob_application_type/1 Module: preferences Name: b_or_z_mode/0 Module: specfile Name: csp_mode/0 Module: specfile Name: get_operation_name/2 Module: specfile Name: get_operation_return_values_and_arguments/3 Module: specfile Name: translate_event/2 Module: translate Name: current_options/1 Module: state_space Name: current_state_id/1 Module: state_space Name: current_expression/2 Module: state_space Name: max_reached_for_node/1 Module: state_space Name: not_all_transitions_added/1 Module: state_space Name: time_out_for_node/3 Module: state_space Name: print_red/1 Module: tools_printing Name: print_green/1 Module: tools_printing Name: format_with_colour_nl/4 Module: tools_printing Name: read_file_codes/2 Module: tools_files Name: lookup_value_for_existing_id/3 Module: store Name: tcltk_reset/0 Module: tcltk_interface Name: tcltk_add_user_executed_operation_typed/4 Module: tcltk_interface Name: tcltk_get_options/1 Module: tcltk_interface Name: profile_single_call/3 Module: runtime_profiler Name: start_ms_timer/1 Module: tools Name: stop_ms_timer_with_msg/2 Module: tools Name: def_get_texpr_ids/2 Module: bsyntaxtree Name: def_get_texpr_id/2 Module: bsyntaxtree Name: b_parse_wo_type_machine_predicate_from_codes_to_raw_expr/2 Module: bmachine Name: b_type_check_raw_expr/4 Module: bmachine Name: add_prob_deferred_set_elements_to_store/3 Module: b_global_sets Name: expand_const_and_vars_to_full_store/2 Module: specfile Name: visited_expression/2 Module: state_space Name: max_reached_for_node/1 Module: state_space Name: max_reached_or_timeout_for_node/1 Module: state_space Name: time_out_for_node/1 Module: state_space Name: format_to_codes/3 Module: codesio Name: announce_event/1 Module: eventhandling Name: b_machine_has_constants_or_properties/0 Module: bmachine Name: print_error/1 Module: tools_printing Name: get_modulename_filename/2 Module: tools Name: b_machine_has_constants_or_properties/0 Module: bmachine Name: current_state_id/1 Module: state_space Name: current_expression/2 Module: state_space Name: visited_expression_id/1 Module: state_space Name: get_action_trace/1 Module: state_space Name: transition/4 Module: state_space Name: op_trace_ids/1 Module: state_space Name: version_str/1 Module: version Name: revision/1 Module: version Name: datime/1 Module: system Name: environ/2 Module: system Name: currently_opened_file/1 Module: specfile Name: number_codes_min_length/3 Module: tools_strings Name: get_member_option/3 Module: tools_lists Name: get_operation_internal_name/2 Module: specfile Name: get_operation_return_values_and_arguments/3 Module: specfile Name: get_operation_description_for_transition/4 Module: specfile Name: get_possible_language_specific_top_level_event/3 Module: specfile Name: translate_bvalue/2 Module: translate Name: translate_bvalue_to_parseable_classicalb/2 Module: translate Name: is_memoization_closure/4 Module: memoization	Name: tcltk_check_state_sequence_from_file/1 Name: tcltk_check_state_sequence_from_file_state_id/3 Name: tcltk_check_sequence_from_file/3 Name: check_default_trace_for_specfile/1 Name: get_default_trace_file/2 Name: get_default_trace_file/3 Name: print_trace_as_fdr_check/0 Name: tcltk_save_history_as_trace_file/2 Name: tcltk_save_history_as_trace_file/3 Name: perform_initialisation/0 Name: find_successor_state/4

Imports

Exports

Name: module_info/2

Module: module_information

Name: get_texpr_type/2

Module: bsyntaxtree

Name: conjunct_predicates/2

Module: bsyntaxtree

Name: b_machine_name/1

Module: bmachine

Name: b_is_operation_name/1

Module: bmachine

Name: b_get_machine_operation_typed_parameters/2

Module: bmachine

Name: lookup_global_constant/2

Module: b_global_sets

Name: get_preference/2

Module: preferences

Name: preference/2

Module: preferences

Name: temporary_set_preference/3

Module: preferences

Name: reset_temporary_preference/2

Module: preferences

Name: get_prob_application_type/1

Module: preferences

Name: b_or_z_mode/0

Module: specfile

Name: csp_mode/0

Module: specfile

Name: get_operation_name/2

Module: specfile

Name: get_operation_return_values_and_arguments/3

Module: specfile

Name: translate_event/2

Module: translate

Name: current_options/1

Module: state_space

Name: current_state_id/1

Module: state_space

Name: current_expression/2

Module: state_space

Name: max_reached_for_node/1

Module: state_space

Name: not_all_transitions_added/1

Module: state_space

Name: time_out_for_node/3

Module: state_space

Name: print_red/1

Module: tools_printing

Name: print_green/1

Module: tools_printing

Name: format_with_colour_nl/4

Module: tools_printing

Name: read_file_codes/2

Module: tools_files

Name: lookup_value_for_existing_id/3

Module: store

Name: tcltk_reset/0

Module: tcltk_interface

Name: tcltk_add_user_executed_operation_typed/4

Module: tcltk_interface

Name: tcltk_get_options/1

Module: tcltk_interface

Name: profile_single_call/3

Module: runtime_profiler

Name: start_ms_timer/1

Module: tools

Name: stop_ms_timer_with_msg/2

Module: tools

Name: def_get_texpr_ids/2

Module: bsyntaxtree

Name: def_get_texpr_id/2

Module: bsyntaxtree

Name: b_parse_wo_type_machine_predicate_from_codes_to_raw_expr/2

Module: bmachine

Name: b_type_check_raw_expr/4

Module: bmachine

Name: add_prob_deferred_set_elements_to_store/3

Module: b_global_sets

Name: expand_const_and_vars_to_full_store/2

Module: specfile

Name: visited_expression/2

Module: state_space

Name: max_reached_for_node/1

Module: state_space

Name: max_reached_or_timeout_for_node/1

Module: state_space

Name: time_out_for_node/1

Module: state_space

Name: format_to_codes/3

Module: codesio

Name: announce_event/1

Module: eventhandling

Name: b_machine_has_constants_or_properties/0

Module: bmachine

Name: print_error/1

Module: tools_printing

Name: get_modulename_filename/2

Module: tools

Name: b_machine_has_constants_or_properties/0

Module: bmachine

Name: current_state_id/1

Module: state_space

Name: current_expression/2

Module: state_space

Name: visited_expression_id/1

Module: state_space

Name: get_action_trace/1

Module: state_space

Name: transition/4

Module: state_space

Name: op_trace_ids/1

Module: state_space

Name: version_str/1

Module: version

Name: revision/1

Module: version

Name: datime/1

Module: system

Name: environ/2

Module: system

Name: currently_opened_file/1

Module: specfile

Name: number_codes_min_length/3

Module: tools_strings

Name: get_member_option/3

Module: tools_lists

Name: get_operation_internal_name/2

Module: specfile

Name: get_operation_return_values_and_arguments/3

Module: specfile

Name: get_operation_description_for_transition/4

Module: specfile

Name: get_possible_language_specific_top_level_event/3

Module: specfile

Name: translate_bvalue/2

Module: translate

Name: translate_bvalue_to_parseable_classicalb/2

Module: translate

Name: is_memoization_closure/4

Module: memoization

Name: tcltk_check_state_sequence_from_file/1

Name: tcltk_check_state_sequence_from_file_state_id/3

Name: tcltk_check_sequence_from_file/3

Name: check_default_trace_for_specfile/1

Name: get_default_trace_file/2

Name: get_default_trace_file/3

Name: print_trace_as_fdr_check/0

Name: tcltk_save_history_as_trace_file/2

Name: tcltk_save_history_as_trace_file/3

Name: perform_initialisation/0

Name: find_successor_state/4

Predicates

Predicates:

changed_binding/3

check_default_trace_for_specfile/1

expand_explicit_set/2

filter_json_paras/4

find_action_in_options/6

find_successor_state/4

format_current_iso_time/1

generate_predicate/3

get_change_list/4

get_default_trace_file/2

get_default_trace_file/3

get_id_binding/2

get_mode_value/3

get_op_name_for_state/2

is_a_reset_operation/1

is_a_set/1

l_convert_term/2

l_generate_predicate/4

l_unify/2

my_perform_action_as_string/3

perform_action_tclk/4

perform_alternative_op_with_same_functor/7

perform_custom_operation_retry/2

perform_initialisation/0

perform_one_operation_in_sequence/2

perform_sequence_of_operations/1

perform_sequence_of_operations2/2

perform_single_operation/2

perform_single_operation_retry/4

perform_single_operation_retry/5

print_fdr/1

print_json_list/3

print_json_names/2

print_json_names_aux/2

print_json_opid/4

print_json_paras/3

print_json_paras_aux/4

print_trace_as_fdr_check/0

print_trace_for_replay/3

print_trace_for_replay/4

print_transition_list_json/3

print_transition_list_prolog/2

process_line/6

read_trace_file/4

replace_result_by_variable/2

safe_read/1

single_operation_skip/2

strip_dots/2

tcltk_check_sequence_from_file/3

tcltk_check_sequence_from_file2/2

tcltk_check_state_sequence_from_file/1

tcltk_check_state_sequence_from_file_aux/5

tcltk_check_state_sequence_from_file_state_id/3

tcltk_save_history_as_trace_file/2

tcltk_save_history_as_trace_file/3

translate_b2p/2

translate_b2p/3

translate_json_operation/2

translate_json_para/2

translate_json_term/2

translate_para/2

translate_substition_to_trace/2

unchanged_binding/3

unify/2

unify_action_as_term/3

unify_explicit_sets/2

unify_functor/3

update_max_nr_replayed/1

changed_binding/3

check_default_trace_for_specfile/1

expand_explicit_set/2

filter_json_paras/4

find_action_in_options/6

find_successor_state/4

find_successor_state(ID,Pred,NewID,_) :-
    % transition(ID,ActionOpAsTerm,OpID,SuccID),
    tcltk_get_options(_),
    current_options(Options), % print(Options),nl,
    member( (_,Action,ActionOpAsTerm,NewID), Options),
    state_space:visited_expression(NewID,State),
    expand_const_and_vars_to_full_store(State,EState),
    % print(try(NewID,State)),nl,
    add_prob_deferred_set_elements_to_store(EState,DEState,all),
    announce_event(start_solving),
    b_interpreter:b_test_boolean_expression_cs(Pred,[],DEState,'find successor state',ID), % deferred
    announce_event(end_solving),
    debug_println(19,successor_found(NewID)),
    print(' --> '),my_print_event(ActionOpAsTerm,_),nl,nl,
    my_perform_action_as_string(Action,ActionOpAsTerm,NewID),
    !.

find_successor_state(ID,Pred,NewID,_LineNr) :-
    max_reached_or_timeout_for_node(ID), % we have not computed all options
    get_op_name_for_state(ID,OpName), print(try_providing_custom_predicate(OpName)),nl,
    tcltk_add_user_executed_operation_typed(OpName,_,Pred,NewID), % The Pred can only talk about parameters and the state before; thus this only works for setup_constants and initialise_machine
    (silent_mode(on) -> true
    ; print_green(successor_found(NewID)),nl,
    print(' --> '),print(OpName),nl),
    !.

find_successor_state(ID,Pred,_,LineNr) :-
    % we could try and execute operation by predicate here; in case max_reached_for_node(ID) or time_out_for_node(ID)
    format('State ID = ~w; line number = ~w~n',[ID,LineNr]),
    (max_reached_for_node(ID)
    -> format_to_codes('Try increasing the MAX_OPERATIONS preference. No successor found satisfying predicate at step ~w of replay: ',[LineNr],Codes)
    ; time_out_for_node(ID) -> format_to_codes('TIME-OUT occurred. No successor found satisfying predicate at step ~w of replay: ',[LineNr],Codes)
    ; format_to_codes('No successor found satisfying predicate at step ~w of replay: ',[LineNr],Codes)
    ),
    atom_codes(Msg,Codes),
    translate:translate_bexpression(Pred,TP),
    add_error(tcltk_check_state_sequence_from_file,Msg,TP),
    fail.

format_current_iso_time/1

generate_predicate/3

get_change_list/4

get_default_trace_file/2

get_default_trace_file/3

get_id_binding/2

get_mode_value/3

get_op_name_for_state/2

is_a_reset_operation/1

is_a_set/1

l_convert_term/2

l_generate_predicate/4

l_unify/2

my_perform_action_as_string/3

perform_action_tclk/4

perform_alternative_op_with_same_functor/7

perform_custom_operation_retry/2

perform_custom_operation_retry(OpName,NewID) :-
    (OpName = '$initialise_machine' ; OpName = '$setup_constants'),
    !,
    state_space:current_state_id(CurID),
    (max_reached_for_node(CurID) ; not_all_transitions_added(CurID)),
    preferences:get_preference(maxNrOfInitialisations,0),
    tcltk_add_user_executed_operation_typed(OpName,_,b(truth,pred,[]),NewID),
    (get_preference(deterministic_trace_replay,true) -> ! ; true),
    print_green(init_found(NewID)),nl.

perform_custom_operation_retry(ActionAsTerm,NewID) :-
    (ActionAsTerm = '-->'(_,_) % for operations with return types we cannot provide a predicate to solve yet
    -> preferences:get_preference(maxNrOfEnablingsPerOperation,0)
    ; true),
    state_space:current_state_id(CurID),
    get_operation_name(ActionAsTerm,OpName),
    (max_reached_for_node(CurID) ; time_out_for_node(CurID,OpName,_) ; not_all_transitions_added(CurID)),
    debug_println(9,try_custom(CurID,ActionAsTerm)), % Execute operation by predicate
    % (state_space:transition(CurID,AA,BB,CC),format('Successor of ~w: ~w --~w--> ~w~n',[CurID,AA,BB,CC]),fail ; true),
    get_operation_return_values_and_arguments(ActionAsTerm,ExpectedResults,OpArgs),
    % TO DO: optionally check return values
    (OpArgs = [] -> Pred = b(truth,pred,[])
    ; \+ b_is_operation_name(OpName)
    -> add_error(trace_checking_fails,'Operation does not exist in loaded specification:',OpName),fail
    ; b_get_machine_operation_typed_parameters(OpName,TArgParas),
    l_generate_predicate(OpArgs,TArgParas,OpName,Conjuncts),
    conjunct_predicates(Conjuncts,Pred)
    ),
    !,
    %print('PRED: '),translate:print_bexpr(Pred),nl,
    start_ms_timer(Timer),
    profile_single_call(OpName,CurID,
    tcltk_interface:tcltk_add_user_executed_operation_typed(OpName,OpTerm,Pred,NewID) % The Pred can only talk about parameters and the state before; thus this only works for setup_constants and initialise_machine
    ),
    (get_preference(deterministic_trace_replay,true) -> ! ; true), % by preventing backtracking we can reduce memory consumption
    print_green(successor_found(NewID, OpName)),nl,
    get_operation_return_values_and_arguments(OpTerm,ActualResults,_),
    (l_unify(ExpectedResults,ActualResults) -> true
    ; ajoin(['Result values for ',OpName,' do not match for transition from ',CurID,' to ',NewID,':'],Msg),
    translate_bvalue(ExpectedResults,ER),
    translate_bvalue(ActualResults,AR),
    add_warning(b_trace_checking,Msg,[expected(ER),actual(AR)])
    ),
    (debug_mode(on) -> stop_ms_timer_with_msg(Timer,'Custom: ') ; true),
    garbage_collect, % important to keep memory consumption down for long traces e.g. for Innotrans VBF traces
    (debug_mode(on) -> print_memory_used_wo_gc,nl ; true),
    tcltk_get_options(_).

perform_initialisation/0

perform_one_operation_in_sequence/2

perform_one_operation_in_sequence('$non_det_modified_vars'(ActionAsTerm,NonDetVars),Ident) :- !,
    current_expression(_CurID,State),
    current_options(Options),
    member( (_Id,Action,ActionOpAsTerm,NewID), Options),
    unify_action_as_term(ActionAsTerm,ActionOpAsTerm,State),
    %ident(Ident), format('checking non_det_modified_vars for ~w in ~w~n',[ActionAsTerm,NewID]),nl,
    check_non_det_vars(NewID,NonDetVars),
    !,
    perform_action_tclk(Action,ActionOpAsTerm,NewID,Ident).

perform_one_operation_in_sequence('$non_det_modified_vars'(Op,_),Ident) :- !,
    ident(Ident), format('ignoring non_det_modified_vars for ~w~n',[Op]), % TO DO: use constraint-based finding of successor
    perform_one_operation_in_sequence(Op,Ident).

perform_one_operation_in_sequence('$check_value'(ID,VAL),Ident) :- !,
    ident(Ident), format('checking value of ~w ',[ID]),
    state_space:current_expression(_,State),
    expand_const_and_vars_to_full_store(State,EState),
    lookup_value_for_existing_id(ID,EState,StoredVal),
    translate:print_bvalue(StoredVal),
    (unify(StoredVal,VAL) -> print_green(' ok'),nl
    ; print_red(' failed'),nl, %print(StoredVal),nl, print(VAL),nl,
    fail).

perform_one_operation_in_sequence(Op,Ident) :-
    (silent_mode(on) -> true
    ; ident(Ident),print('<- '),print(Ident), print(': '), my_print_event(Op,OpStr),
    print(' :: '),
    state_space:current_state_id(CurID), print(CurID),nl
    ),
    (is_a_reset_operation(Op)
    -> tcltk_reset, %tcltk_goto_state(reset,root), % reset animation history
    tcltk_get_options(_)
    ; true),
    convert_action(Op,COp),
    if(perform_single_operation(COp,Ident),true,
    (silent_mode(off),
    ident(Ident), print_red(' **** FAIL ****'),nl,
    fail)),
    (get_preference(deterministic_trace_replay,true) -> ! ; true),
    (silent_mode(on) -> true
    ; ident(Ident), print(' | '), print(Ident), print(': '), print(OpStr),
    %functor(Op,OpName,_), print(OpName),
    %((OpName = '-->', arg(1,Op,A1), functor(A1,RealOpName,_)) -> print(RealOpName) ; true),
    print_green(' success -->'),
    state_space:current_state_id(NewCurID),
    statistics(walltime,[Tot,Delta]),
    format('~w [~w (Delta ~w) ms]~n',[NewCurID,Tot,Delta])
).

perform_sequence_of_operations/1

perform_sequence_of_operations2/2

perform_single_operation/2

Description:
user:current_expression(CurID,State),

perform_single_operation('$jump'(TO,FROM),Ident) :- !,
    current_state_id(ID),
    print_red('Warning: trace file contains JUMP!'),nl,
    (ID=FROM -> true ; ident(Ident),format('Cannot perform jump from ~w (to ~w)~n',[FROM,TO])),
    (visited_expression_id(TO) -> tcltk_interface:tcltk_goto_state(jump,TO)
    ; add_error(trace_checking_fails,'State ID does not exist for jump:',TO),fail
).

perform_single_operation(ActionAsTerm,Ident) :-
    % tools_printing:print_term_summary(perform_single_op(ActionAsTerm)),
    current_expression(_CurID,State),
    current_options(Options),
    ( if( find_action_in_options(ActionAsTerm,Options,State, Action,ActionOpAsTerm,NewID),
    perform_action_tclk(Action,ActionOpAsTerm,NewID,Ident),
    if(perform_single_operation_retry(Options,ActionAsTerm,Action,NewID,State),
    perform_action_tclk(Action,_AlternateActionOpAsTerm,NewID,Ident),
    if(perform_custom_operation_retry(ActionAsTerm,_NewID),true,
    (replace_result_by_variable(ActionAsTerm,A2),
    find_action_in_options(A2,Options,State, Action,_,NewID),
    (silent_mode(on) -> true ; format_with_colour_nl(user_output,[red],'Result of operation call in trace does not match, e.g., ~w leading to state ~w',[Action,NewID])),
    fail
    )
    )
    )

    )
    ;
    single_operation_skip(ActionAsTerm,Ident)
    ),
    (get_preference(deterministic_trace_replay,true) -> ! ; true).

perform_single_operation(ActionAsTerm,Ident) :-
    current_options(Options),
    member( (_Id,PActionS,'*permute*',NewID), Options), /* permute action from symmetry reduction */
    perform_action_tclk(PActionS,'*permute*',NewID,Ident), !,
    (silent_mode(on) -> true
    ; ident(Ident), print(' | ** PERMUTING **'),nl),
    perform_single_operation(ActionAsTerm,Ident).

perform_single_operation(ActionAsTerm,Ident) :-
    %%user:current_expression(CurID,State),
    \+ functor(ActionAsTerm,tau,1),
    current_options(Options), %print(options(Options)),nl,
    member( (_Id,AX,tau(X),NewID), Options),
    (silent_mode(on) -> true
    ; ident(Ident), print(' | ** SKIPPING ADDITIONAL TAU in SPEC. **'),nl),
    perform_action_tclk(AX,tau(X),NewID,Ident),
    perform_single_operation(ActionAsTerm,Ident).

perform_single_operation_retry/4

perform_single_operation_retry(Options,ActionAsTerm,Action,NewID) :-
    functor(ActionAsTerm,'$setup_constants',_), !,
    (get_prob_application_type(tcltk) -> OTHER = ['$partial_setup_constants'] ; OTHER = []),
    perform_alternative_op_with_same_functor(Options, ['$setup_constants' | OTHER],
    'set up constants', 'initialisation of constants',
    ActionAsTerm, Action, NewID),
    %visited_expression(NewID,concrete_constants(C)), ActionAsTerm =.. [_|Args],
    % check that state NewID corresponds to parameters provided for setup_constants in trace file
    %print(check_args),nl, check_initialised_args(Args,C), print('argsok'),nl. % TO DO: try and enable this for all tests
    true.

perform_single_operation_retry(Options,ActionAsTerm,Action,NewID) :-
    functor(ActionAsTerm,'$initialise_machine',_),!,
    perform_alternative_op_with_same_functor(Options, ['$initialise_machine'],
    'initialise', 'initialisation',
    ActionAsTerm, Action, NewID),
    true. %visited_expression(NewID,S), (S=const_and_vars(_,VS) -> true ; VS=S), ActionAsTerm =.. [_|Args],

perform_single_operation_retry(Options,ActionAsTerm,Action,NewID) :-
    functor(ActionAsTerm,tau,_), arg(1,ActionAsTerm,Arg), nonvar(Arg),!,
    perform_alternative_op_with_same_functor(Options, [tau],
    tau, tau,
    ActionAsTerm, Action, NewID).

perform_single_operation_retry(Options,ActionAsTerm,Action,NewID) :-
    functor(ActionAsTerm,F,0), preference(show_eventb_any_arguments,true),
    /* then allow also the same operation name but with more arguments */
    member( (_Id,Action,ActionAsTerm2,NewID), Options),
    functor(ActionAsTerm2,F,FArity), FArity>0,
    formatsilent('% Allowing extra Event-B style ANY arguments.~n',[]).

perform_single_operation_retry(Options,ActionAsTerm,Action,NewID) :-
    functor(ActionAsTerm,F,N),N>0, preference(show_eventb_any_arguments,false),
    /* then allow also the same operation name but with more arguments */
    member( (_Id,Action,F,NewID), Options),
    formatsilent('% Allowing operation without Event-B style ANY arguments.~n',[]).

perform_single_operation_retry/5

print_fdr/1

print_json_list/3

print_json_names/2

print_json_names_aux/2

print_json_opid/4

print_json_opid(OpId,Json,PrevId,SuccId) :-
    (transition(PrevId,Op,OpId,SuccId) -> PrevId1=PrevId
    ; add_warning(print_json_list,'Cannot find operation id from given source id: ',OpId:from(PrevId):to(SuccId)),
    transition(PrevId1,Op,OpId,SuccId)
    ),
    get_operation_internal_name(Op,OpName), % TO DO: currently this is INITIALISATION instead of $initialise_machine
    (get_possible_language_specific_top_level_event(OpName,ResultNames,ParaNames) -> true
    ; ResultNames=unknown, ParaNames=unknown),
    get_operation_return_values_and_arguments(Op,ReturnValues,Paras),
    % TO DO: extract variables and constants for $initialise_machine, $setup_constants
    Json = json([name=string(OpName)|T1]),
    (get_operation_description_for_transition(PrevId,Op,SuccId,Desc)
    -> T1=[description=string(Desc)|T2]
    ; T2=T1),
    (Paras = []
    -> T3=T2 % do not print Paras to reduce memory in JSON file
    ; (get_preference(show_eventb_any_arguments,true),
    \+ same_length(Paras,ParaNames)
    -> % we cannot easily use the parameters during replay; ANY parameters are currently only added when there are no other parameters
    add_warning(json_export,'Parameter mismatch: ',OpName:ParaNames,Paras),
    T3=T2
    ; print_json_paras(Paras,ParaNames,JsonParams),
    T2=[params=JsonParams|T3]
    )
    ),
    (ReturnValues = []
    -> T4=T3 % do not print results to reduce memory in JSON file
    ; print_json_paras(ReturnValues,ResultNames,JsonResults),
    T3=[results=JsonResults|T4]
    ),
    get_change_list(PrevId1,SuccId,ChangedVarNames,ChangedValues),
    (ChangedVarNames = []
    -> T5=T4
    ; print_json_paras(ChangedValues,ChangedVarNames,JsonDestState),
    T4=[destState=JsonDestState|T5]
    ),
    get_unchanged_list(PrevId1,SuccId,UnChangedVarNames),
    (UnChangedVarNames = []
    -> T6=T5
    ; print_json_names(UnChangedVarNames,JsonDestStateNotChanged),
    T5=[destStateNotChanged=JsonDestStateNotChanged|T6]
    ),
    T6=[].

print_json_paras/3

print_json_paras_aux/4

print_trace_as_fdr_check/0

print_trace_for_replay/3

print_trace_for_replay/4

print_transition_list_json/3

print_transition_list_prolog/2

process_line/6

read_trace_file/4

replace_result_by_variable/2

safe_read/1

single_operation_skip/2

strip_dots/2

tcltk_check_sequence_from_file/3

tcltk_check_sequence_from_file2/2

Description:
,throw(trace_checking_failed(MachineName)) % comment in if you want to stop immediately upon such an error

tcltk_check_state_sequence_from_file/1

tcltk_check_state_sequence_from_file_aux/5

tcltk_check_state_sequence_from_file_state_id/3

tcltk_save_history_as_trace_file/2

tcltk_save_history_as_trace_file/3

translate_b2p/2

translate_b2p/3

translate_json_operation/2

translate_json_para/2

translate_json_term/2

translate_para/2

translate_substition_to_trace/2

unchanged_binding/3

unify/2

unify_action_as_term/3

unify_explicit_sets/2

unify_functor/3

update_max_nr_replayed/1

Determinacy Checker

Determinacy Checker:

! Existence error in user:environ/2
! procedure user:environ/2 does not exist
! goal: user:environ(prob_release,true)
! Existence error in user:environ/2
! procedure user:environ/2 does not exist
! goal: user:environ(prob_avl_custom,true)
! Existence error in user:environ/2
! procedure user:environ/2 does not exist
! goal: user:environ(prob_core_only,true)
! Existence error in user:environ/2
! procedure user:environ/2 does not exist
! goal: user:environ(no_terminal_colors,true)
! Existence error in user:environ/2
! procedure user:environ/2 does not exist
! goal: user:environ(prob_enter_debugger_upon_error,true)
! Existence error in user:environ/2
! procedure user:environ/2 does not exist
! goal: user:environ(prob_use_timer,true)
! Existence error in user:environ/2
! procedure user:environ/2 does not exist
! goal: user:environ(prob_profile,true)
! Existence error in user:environ/2
! procedure user:environ/2 does not exist
! goal: user:environ(prob_src_profile,true)
! Existence error in user:environ/2
! procedure user:environ/2 does not exist
! goal: user:environ(prob_safe_mode,true)
! Existence error in user:environ/2
! procedure user:environ/2 does not exist
! goal: user:environ(prob_core_only,true)
! Existence error in user:environ/2
! procedure user:environ/2 does not exist
! goal: user:environ(prob_myheap,false)
! Existence error in user:environ/2
! procedure user:environ/2 does not exist
! goal: user:environ(disable_chr,true)
! Existence error in argument 1 of absolute_file_name/3
! file probsrc(tools_strings) does not exist
! goal: absolute_file_name(probsrc(tools_strings),_57883,[access(exist),file_type(source),relative_to('/builds/stups/prob/prolog_doc_gen/prolog-Doc/prob_prolog/src/pathes_lib.pl')])
! Existence error in argument 1 of absolute_file_name/3
! file extension('counter/counter') does not exist
! goal: absolute_file_name(extension('counter/counter'),_27041,[access(exist),file_type(source),relative_to('/builds/stups/prob/prolog_doc_gen/prolog-Doc/prob_prolog/src/error_manager.pl')])
! Existence error in user:environ/2
! procedure user:environ/2 does not exist
! goal: user:environ(prob_debug_flag,true)
! Existence error in user:environ/2
! procedure user:environ/2 does not exist
! goal: user:environ(plspec_patch_libraries,true)
! Existence error in user:environ/2
! procedure user:environ/2 does not exist
! goal: user:environ(prob_debug_flag,true)
! Existence error in user:environ/2
! procedure user:environ/2 does not exist
! goal: user:environ(prob_release,true)
! Existence error in argument 1 of absolute_file_name/3
! file probsrc(error_manager) does not exist
! goal: absolute_file_name(probsrc(error_manager),_37245,[access(exist),file_type(source),relative_to('/builds/stups/prob/prolog_doc_gen/prolog-Doc/prob_prolog/src/xml_prob.pl')])
! Existence error in argument 1 of absolute_file_name/3
! file probsrc(debug) does not exist
! goal: absolute_file_name(probsrc(debug),_35581,[access(exist),file_type(source),relative_to('/builds/stups/prob/prolog_doc_gen/prolog-Doc/prob_prolog/src/xml_prob.pl')])
! Existence error in argument 1 of absolute_file_name/3
! file extrasrc(json_parser) does not exist
! goal: absolute_file_name(extrasrc(json_parser),_36711,[access(exist),file_type(source),relative_to('/builds/stups/prob/prolog_doc_gen/prolog-Doc/prob_prolog/src/translate.pl')])
! Existence error in argument 1 of absolute_file_name/3
! file probsrc(tools) does not exist
! goal: absolute_file_name(probsrc(tools),_125551,[access(exist),file_type(source),relative_to('/builds/stups/prob/prolog_doc_gen/prolog-Doc/prob_prolog/src/kernel_records.pl')])
! Existence error in argument 1 of absolute_file_name/3
! file covsrc(coverage_tools_annotations) does not exist
! goal: absolute_file_name(covsrc(coverage_tools_annotations),_154113,[access(exist),file_type(source),relative_to('/builds/stups/prob/prolog_doc_gen/prolog-Doc/prob_prolog/src/kernel_waitflags.pl')])
! Existence error in user:environ/2
! procedure user:environ/2 does not exist
! goal: user:environ(prob_safe_mode,true)
! Existence error in argument 1 of absolute_file_name/3
! file probsrc(tools_lists) does not exist
! goal: absolute_file_name(probsrc(tools_lists),_154113,[access(exist),file_type(source),relative_to('/builds/stups/prob/prolog_doc_gen/prolog-Doc/prob_prolog/src/kernel_tools.pl')])
! Existence error in user:environ/2
! procedure user:environ/2 does not exist
! goal: user:environ(prob_debug_watch_flag,true)
! Existence error in user:environ/2
! procedure user:environ/2 does not exist
! goal: user:environ(prob_safe_mode,true)
! Existence error in argument 1 of absolute_file_name/3
! file probsrc(kernel_waitflags) does not exist
! goal: absolute_file_name(probsrc(kernel_waitflags),_156257,[access(exist),file_type(source),relative_to('/builds/stups/prob/prolog_doc_gen/prolog-Doc/prob_prolog/src/runtime_profiler.pl')])
! Existence error in argument 1 of absolute_file_name/3
! file probsrc(closures) does not exist
! goal: absolute_file_name(probsrc(closures),_162377,[access(exist),file_type(source),relative_to('/builds/stups/prob/prolog_doc_gen/prolog-Doc/prob_prolog/src/memoization.pl')])
! Existence error in argument 1 of absolute_file_name/3
! file extension('counter/counter') does not exist
! goal: absolute_file_name(extension('counter/counter'),_167787,[access(exist),file_type(source),relative_to('/builds/stups/prob/prolog_doc_gen/prolog-Doc/prob_prolog/src/state_space.pl')])
! Existence error in argument 1 of absolute_file_name/3
! file extrasrc(external_functions_reals) does not exist
! goal: absolute_file_name(extrasrc(external_functions_reals),_167023,[access(exist),file_type(source),relative_to('/builds/stups/prob/prolog_doc_gen/prolog-Doc/prob_prolog/src/external_functions.pl')])
! Existence error in argument 1 of absolute_file_name/3
! file extrasrc(external_functions_svg) does not exist
! goal: absolute_file_name(extrasrc(external_functions_svg),_167023,[access(exist),file_type(source),relative_to('/builds/stups/prob/prolog_doc_gen/prolog-Doc/prob_prolog/src/external_functions.pl')])
! Existence error in user:check_arithmetic_function/1
! procedure user:check_arithmetic_function/1 does not exist
! goal: user:check_arithmetic_function(log(2,4))
! Existence error in argument 1 of absolute_file_name/3
! file chrsrc(chr_integer_inequality) does not exist
! goal: absolute_file_name(chrsrc(chr_integer_inequality),_168319,[access(exist),file_type(source),relative_to('/builds/stups/prob/prolog_doc_gen/prolog-Doc/prob_prolog/src/clpfd_interface.pl')])
! Existence error in argument 1 of absolute_file_name/3
! file probsrc(preferences) does not exist
! goal: absolute_file_name(probsrc(preferences),_167645,[access(exist),file_type(source),relative_to('/builds/stups/prob/prolog_doc_gen/prolog-Doc/prob_prolog/src/kernel_z.pl')])
! Existence error in user:exists_source/1
! procedure user:exists_source/1 does not exist
! goal: user:exists_source(library(atts))
! Existence error in argument 1 of absolute_file_name/3
! file probsrc(tools_strings) does not exist
! goal: absolute_file_name(probsrc(tools_strings),_168639,[access(exist),file_type(source),relative_to('/builds/stups/prob/prolog_doc_gen/prolog-Doc/prob_prolog/src/kernel_strings.pl')])
! Existence error in argument 1 of absolute_file_name/3
! file probsrc(kernel_freetypes) does not exist
! goal: absolute_file_name(probsrc(kernel_freetypes),_162377,[access(exist),file_type(source),relative_to('/builds/stups/prob/prolog_doc_gen/prolog-Doc/prob_prolog/src/external_functions.pl')])
! Existence error in user:environ/2
! procedure user:environ/2 does not exist
! goal: user:environ(prob_use_timer,true)
! Existence error in user:environ/2
! procedure user:environ/2 does not exist
! goal: user:environ(prob_debug_watch_flag,true)
! Existence error in argument 1 of absolute_file_name/3
! file probsrc(kernel_reals) does not exist
! goal: absolute_file_name(probsrc(kernel_reals),_185405,[access(exist),file_type(source),relative_to('/builds/stups/prob/prolog_doc_gen/prolog-Doc/prob_prolog/src/b_interpreter_check.pl')])
! Existence error in argument 1 of absolute_file_name/3
! file probsrc(clpfd_interface) does not exist
! goal: absolute_file_name(probsrc(clpfd_interface),_179711,[access(exist),file_type(source),relative_to('/builds/stups/prob/prolog_doc_gen/prolog-Doc/prob_prolog/src/kernel_equality.pl')])
! Existence error in user:environ/2
! procedure user:environ/2 does not exist
! goal: user:environ(no_wd_checking,true)
! Existence error in user:exists_source/1
! procedure user:exists_source/1 does not exist
! goal: user:exists_source(library(atts))
! Existence error in user:exists_source/1
! procedure user:exists_source/1 does not exist
! goal: user:exists_source(library(atts))
! Existence error in argument 1 of absolute_file_name/3
! file probsrc(avl_tools) does not exist
! goal: absolute_file_name(probsrc(avl_tools),_162799,[access(exist),file_type(source),relative_to('/builds/stups/prob/prolog_doc_gen/prolog-Doc/prob_prolog/src/bsets_clp.pl')])
! Existence error in argument 1 of absolute_file_name/3
! file extension('counter/counter') does not exist
! goal: absolute_file_name(extension('counter/counter'),_175313,[access(exist),file_type(source),relative_to('/builds/stups/prob/prolog_doc_gen/prolog-Doc/prob_prolog/src/succeed_max.pl')])
! Existence error in user:exists_source/1
! procedure user:exists_source/1 does not exist
! goal: user:exists_source(library(logarr))
! Existence error in argument 1 of absolute_file_name/3
! file probcspsrc(haskell_csp) does not exist
! goal: absolute_file_name(probcspsrc(haskell_csp),_175167,[access(exist),file_type(source),relative_to('/builds/stups/prob/prolog_doc_gen/prolog-Doc/prob_prolog/src/xtl_interface.pl')])
! Existence error in argument 1 of absolute_file_name/3
! file extension('probhash/probhash') does not exist
! goal: absolute_file_name(extension('probhash/probhash'),_178447,[access(exist),file_type(source),relative_to('/builds/stups/prob/prolog_doc_gen/prolog-Doc/prob_prolog/src/b_machine_hierarchy.pl')])
! Existence error in argument 1 of absolute_file_name/3
! file extension('probhash/probhash') does not exist
! goal: absolute_file_name(extension('probhash/probhash'),_175313,[access(exist),file_type(source),relative_to('/builds/stups/prob/prolog_doc_gen/prolog-Doc/prob_prolog/src/value_persistance.pl')])
! Existence error in argument 1 of absolute_file_name/3
! file probsrc(avl_tools) does not exist
! goal: absolute_file_name(probsrc(avl_tools),_175455,[access(exist),file_type(source),relative_to('/builds/stups/prob/prolog_doc_gen/prolog-Doc/prob_prolog/src/state_packing.pl')])
! Existence error in argument 1 of absolute_file_name/3
! file probsrc(btypechecker) does not exist
! goal: absolute_file_name(probsrc(btypechecker),_163087,[access(exist),file_type(source),relative_to('/builds/stups/prob/prolog_doc_gen/prolog-Doc/prob_prolog/src/specfile.pl')])
! Existence error in argument 1 of absolute_file_name/3
! file extension('counter/counter') does not exist
! goal: absolute_file_name(extension('counter/counter'),_162799,[access(exist),file_type(source),relative_to('/builds/stups/prob/prolog_doc_gen/prolog-Doc/prob_prolog/src/kernel_reals.pl')])
! Existence error in argument 1 of absolute_file_name/3
! file kodkodsrc(kodkod) does not exist
! goal: absolute_file_name(kodkodsrc(kodkod),_156257,[access(exist),file_type(source),relative_to('/builds/stups/prob/prolog_doc_gen/prolog-Doc/prob_prolog/src/b_interpreter.pl')])
! Existence error in argument 1 of absolute_file_name/3
! file probsrc(kernel_waitflags) does not exist
! goal: absolute_file_name(probsrc(kernel_waitflags),_154113,[access(exist),file_type(source),relative_to('/builds/stups/prob/prolog_doc_gen/prolog-Doc/prob_prolog/src/delay.pl')])
! Existence error in argument 1 of absolute_file_name/3
! file probsrc(performance_messages) does not exist
! goal: absolute_file_name(probsrc(performance_messages),_154113,[access(exist),file_type(source),relative_to('/builds/stups/prob/prolog_doc_gen/prolog-Doc/prob_prolog/src/b_compiler.pl')])
! Existence error in user:environ/2
! procedure user:environ/2 does not exist
! goal: user:environ(prob_safe_mode,true)
! Existence error in user:environ/2
! procedure user:environ/2 does not exist
! goal: user:environ(prob_safe_mode,true)
! Existence error in user:environ/2
! procedure user:environ/2 does not exist
! goal: user:environ(no_wd_checking,true)
! Existence error in user:environ/2
! procedure user:environ/2 does not exist
! goal: user:environ(prob_data_validation_mode,xxxtrue)
! Existence error in user:environ/2
! procedure user:environ/2 does not exist
! goal: user:environ(prob_data_validation_mode,true)
! Existence error in argument 1 of absolute_file_name/3
! file probsrc(bsyntaxtree) does not exist
! goal: absolute_file_name(probsrc(bsyntaxtree),_128827,[access(exist),file_type(source),relative_to('/builds/stups/prob/prolog_doc_gen/prolog-Doc/prob_prolog/src/custom_explicit_sets.pl')])
! Existence error in argument 1 of absolute_file_name/3
! file prob_rewrite_rules(b_ast_cleanup_rewrite_rules) does not exist
! goal: absolute_file_name(prob_rewrite_rules(b_ast_cleanup_rewrite_rules),_125263,[access(exist),file_type(source),relative_to('/builds/stups/prob/prolog_doc_gen/prolog-Doc/prob_prolog/src/b_ast_cleanup.pl')])
! Existence error in argument 1 of absolute_file_name/3
! file probsrc(tools_strings) does not exist
! goal: absolute_file_name(probsrc(tools_strings),_125551,[access(exist),file_type(source),relative_to('/builds/stups/prob/prolog_doc_gen/prolog-Doc/prob_prolog/src/input_syntax_tree.pl')])
! Existence error in argument 1 of absolute_file_name/3
! file probsrc(b_state_model_check) does not exist
! goal: absolute_file_name(probsrc(b_state_model_check),_125409,[access(exist),file_type(source),relative_to('/builds/stups/prob/prolog_doc_gen/prolog-Doc/prob_prolog/src/b_read_write_info.pl')])
! Existence error in argument 1 of absolute_file_name/3
! file probsrc(eventhandling) does not exist
! goal: absolute_file_name(probsrc(eventhandling),_125409,[access(exist),file_type(source),relative_to('/builds/stups/prob/prolog_doc_gen/prolog-Doc/prob_prolog/src/parsercall.pl')])
! Existence error in argument 1 of absolute_file_name/3
! file probsrc(bmachine_eventb) does not exist
! goal: absolute_file_name(probsrc(bmachine_eventb),_118011,[access(exist),file_type(source),relative_to('/builds/stups/prob/prolog_doc_gen/prolog-Doc/prob_prolog/src/btypechecker.pl')])
! Existence error in argument 1 of absolute_file_name/3
! file probsrc(eventhandling) does not exist
! goal: absolute_file_name(probsrc(eventhandling),_118011,[access(exist),file_type(source),relative_to('/builds/stups/prob/prolog_doc_gen/prolog-Doc/prob_prolog/src/pragmas.pl')])
! Existence error in argument 1 of absolute_file_name/3
! file probsrc(module_information) does not exist
! goal: absolute_file_name(probsrc(module_information),_119817,[access(exist),file_type(source),relative_to('/builds/stups/prob/prolog_doc_gen/prolog-Doc/prob_prolog/src/bmachine_static_checks.pl')])
! Existence error in argument 1 of absolute_file_name/3
! file probsrc(error_manager) does not exist
! goal: absolute_file_name(probsrc(error_manager),_118011,[access(exist),file_type(source),relative_to('/builds/stups/prob/prolog_doc_gen/prolog-Doc/prob_prolog/src/bmachine_static_checks.pl')])
! Existence error in user:environ/2
! procedure user:environ/2 does not exist
! goal: user:environ(prob_safe_mode,true)
! Existence error in argument 1 of absolute_file_name/3
! file probsrc(bsyntaxtree) does not exist
! goal: absolute_file_name(probsrc(bsyntaxtree),_114877,[access(exist),file_type(source),relative_to('/builds/stups/prob/prolog_doc_gen/prolog-Doc/prob_prolog/src/bmachine_eventb.pl')])
! Existence error in argument 1 of absolute_file_name/3
! file kodkodsrc(kodkod) does not exist
! goal: absolute_file_name(kodkodsrc(kodkod),_83481,[access(exist),file_type(source),relative_to('/builds/stups/prob/prolog_doc_gen/prolog-Doc/prob_prolog/src/bmachine.pl')])
! Existence error in argument 1 of absolute_file_name/3
! file extension('random_permutations/random_permutations') does not exist
! goal: absolute_file_name(extension('random_permutations/random_permutations'),_84205,[access(exist),file_type(source),relative_to('/builds/stups/prob/prolog_doc_gen/prolog-Doc/prob_prolog/src/fd_utils_clpfd.pl')])
! Existence error in argument 1 of absolute_file_name/3
! file probsrc(error_manager) does not exist
! goal: absolute_file_name(probsrc(error_manager),_82203,[access(exist),file_type(source),relative_to('/builds/stups/prob/prolog_doc_gen/prolog-Doc/prob_prolog/src/partition_detection.pl')])
! Existence error in argument 1 of absolute_file_name/3
! file extension('counter/counter') does not exist
! goal: absolute_file_name(extension('counter/counter'),_45969,[access(exist),file_type(source),relative_to('/builds/stups/prob/prolog_doc_gen/prolog-Doc/prob_prolog/src/kernel_objects.pl')])
! Existence error in argument 1 of absolute_file_name/3
! file probsrc(eventhandling) does not exist
! goal: absolute_file_name(probsrc(eventhandling),_40275,[access(exist),file_type(source),relative_to('/builds/stups/prob/prolog_doc_gen/prolog-Doc/prob_prolog/src/kernel_freetypes.pl')])
! Existence error in argument 1 of absolute_file_name/3
! file probsrc(clpfd_interface) does not exist
! goal: absolute_file_name(probsrc(clpfd_interface),_36711,[access(exist),file_type(source),relative_to('/builds/stups/prob/prolog_doc_gen/prolog-Doc/prob_prolog/src/typing_tools.pl')])
! Existence error in argument 1 of absolute_file_name/3
! file probsrc(custom_explicit_sets) does not exist
! goal: absolute_file_name(probsrc(custom_explicit_sets),_7445,[access(exist),file_type(source),relative_to('/builds/stups/prob/prolog_doc_gen/prolog-Doc/prob_prolog/src/bsyntaxtree.pl')])
! Existence error in argument 1 of absolute_file_name/3
! file probsrc(preferences) does not exist
! goal: absolute_file_name(probsrc(preferences),_45497,[access(exist),file_type(source),relative_to('/builds/stups/prob/prolog_doc_gen/prolog-Doc/prob_prolog/src/tcltk_interface.pl')])
! Existence error in argument 1 of absolute_file_name/3
! file probsrc(debug) does not exist
! goal: absolute_file_name(probsrc(debug),_45497,[access(exist),file_type(source),relative_to('/builds/stups/prob/prolog_doc_gen/prolog-Doc/prob_prolog/src/tcltk_interface.pl')])
! Existence error in argument 1 of absolute_file_name/3
! file probsrc(tools) does not exist
! goal: absolute_file_name(probsrc(tools),_45497,[access(exist),file_type(source),relative_to('/builds/stups/prob/prolog_doc_gen/prolog-Doc/prob_prolog/src/tcltk_interface.pl')])
! Existence error in argument 1 of absolute_file_name/3
! file probsrc(specfile) does not exist
! goal: absolute_file_name(probsrc(specfile),_45497,[access(exist),file_type(source),relative_to('/builds/stups/prob/prolog_doc_gen/prolog-Doc/prob_prolog/src/tcltk_interface.pl')])
! Existence error in argument 1 of absolute_file_name/3
! file probsrc(state_space_exploration_modes) does not exist
! goal: absolute_file_name(probsrc(state_space_exploration_modes),_45497,[access(exist),file_type(source),relative_to('/builds/stups/prob/prolog_doc_gen/prolog-Doc/prob_prolog/src/tcltk_interface.pl')])
! Existence error in argument 1 of absolute_file_name/3
! file probsrc(translate) does not exist
! goal: absolute_file_name(probsrc(translate),_45497,[access(exist),file_type(source),relative_to('/builds/stups/prob/prolog_doc_gen/prolog-Doc/prob_prolog/src/tcltk_interface.pl')])
! Existence error in argument 1 of absolute_file_name/3
! file probsrc(b_state_model_check) does not exist
! goal: absolute_file_name(probsrc(b_state_model_check),_45497,[access(exist),file_type(source),relative_to('/builds/stups/prob/prolog_doc_gen/prolog-Doc/prob_prolog/src/tcltk_interface.pl')])
! Existence error in argument 1 of absolute_file_name/3
! file probsrc(bmachine) does not exist
! goal: absolute_file_name(probsrc(bmachine),_45497,[access(exist),file_type(source),relative_to('/builds/stups/prob/prolog_doc_gen/prolog-Doc/prob_prolog/src/tcltk_interface.pl')])
! Existence error in argument 1 of absolute_file_name/3
! file probsrc(b_interpreter) does not exist
! goal: absolute_file_name(probsrc(b_interpreter),_45497,[access(exist),file_type(source),relative_to('/builds/stups/prob/prolog_doc_gen/prolog-Doc/prob_prolog/src/tcltk_interface.pl')])
! Existence error in argument 1 of absolute_file_name/3
! file probsrc(b_trace_checking) does not exist
! goal: absolute_file_name(probsrc(b_trace_checking),_45497,[access(exist),file_type(source),relative_to('/builds/stups/prob/prolog_doc_gen/prolog-Doc/prob_prolog/src/tcltk_interface.pl')])
! Existence error in argument 1 of absolute_file_name/3
! file probsrc(bsyntaxtree) does not exist
! goal: absolute_file_name(probsrc(bsyntaxtree),_45497,[access(exist),file_type(source),relative_to('/builds/stups/prob/prolog_doc_gen/prolog-Doc/prob_prolog/src/tcltk_interface.pl')])
! Existence error in argument 1 of absolute_file_name/3
! file probsrc(state_space) does not exist
! goal: absolute_file_name(probsrc(state_space),_45497,[access(exist),file_type(source),relative_to('/builds/stups/prob/prolog_doc_gen/prolog-Doc/prob_prolog/src/tcltk_interface.pl')])
! Existence error in argument 1 of absolute_file_name/3
! file extension('plspec/plspec/plspec_core') does not exist
! goal: absolute_file_name(extension('plspec/plspec/plspec_core'),_16143,[access(exist),file_type(source),relative_to('/builds/stups/prob/prolog_doc_gen/prolog-Doc/prob_prolog/src/tcltk_interface.pl')])
* Non-determinate: b_trace_checking:get_mode_value/3 (clause 1)
* Indexing cannot distinguish this from clause 3.
* Non-determinate: b_trace_checking:get_mode_value/3 (clause 2)
* Indexing cannot distinguish this from clause 3.
! Existence error in argument 1 of absolute_file_name/3
! file extrasrc(json_parser) does not exist
! goal: absolute_file_name(extrasrc(json_parser),_261,[access(exist),file_type(source),relative_to('/builds/stups/prob/prolog_doc_gen/prolog-Doc/prob_prolog/src/b_trace_checking.pl')])

Name: get_id_binding/2	Module: b_trace_checking
Name: not/1
Name: visited_expression/2	Module: state_space

Name: maplist/2	Module: foo_error
Name: get_state/2	Module: b_trace_checking
Name: visited_expression/2	Module: state_space

Name: =../2
Name: l_convert_term/2	Module: b_trace_checking
Name: !
Name: nonvar/1
Name: =/2
Name: strip_dots/2	Module: b_trace_checking
Name: var/1

Name: =../2
Name: l_convert_term/2	Module: b_trace_checking
Name: !
Name: nonvar/1
Name: lookup_global_constant/2	Module: b_global_sets
Name: atomic/1
Name: =/2
Name: var/1

Name: on_enumeration_warning/2	Module: foo_error
Name: convert_to_avl/2	Module: custom_explicit_sets
Name: !

Name: add_message/3	Module: foo_error
Name: is_memoization_closure/4	Module: memoization

Name: =/2
Name: add_error/3	Module: foo_error
Name: RECURSIVE_CALL/4	Module: b_trace_checking
Name: do_not_print_value/2	Module: b_trace_checking
Name: ->/3
Name: true

Name: unify_action_as_term/3	Module: b_trace_checking
Name: member/2

Name: fail
Name: add_error/3	Module: foo_error
Name: translate_bexpression/2	Module: translate
Name: atom_codes/2
Name: format_to_codes/3	Module: codesio
Name: time_out_for_node/1	Module: state_space
Name: ->/3
Name: max_reached_for_node/1	Module: state_space
Name: format/2
Name: !
Name: nl
Name: print/1
Name: print_green/1	Module: tools_printing
Name: true
Name: silent_mode/1	Module: foo_error
Name: tcltk_add_user_executed_operation_typed/4	Module: tcltk_interface
Name: get_op_name_for_state/2	Module: b_trace_checking
Name: max_reached_or_timeout_for_node/1	Module: state_space
Name: my_perform_action_as_string/3	Module: b_trace_checking
Name: my_print_event/2	Module: b_trace_checking
Name: debug_println/2	Module: foo_error
Name: announce_event/1	Module: eventhandling
Name: b_test_boolean_expression_cs/5	Module: b_interpreter
Name: add_prob_deferred_set_elements_to_store/3	Module: b_global_sets
Name: expand_const_and_vars_to_full_store/2	Module: specfile
Name: visited_expression/2	Module: state_space
Name: member/2
Name: current_options/1	Module: state_space
Name: tcltk_get_options/1	Module: tcltk_interface

Name: replay_aux/2	Module: ce_replay
Name: replay_aux/2	Module: ctigar
Name: replay_aux2/3	Module: ce_replay
Name: replay_aux/3	Module: ic3
Name: process_line/6	Module: b_trace_checking

Name: additional_testcase_file/4	Module: test_runner
Name: check_default_trace_for_specfile/1	Module: b_trace_checking

Name: string_concatenate/3	Module: foo_error
Name: split_filename/3	Module: foo_error

Name: unchanged_binding/3	Module: b_trace_checking
Name: changed_binding/3	Module: b_trace_checking

Name: RECURSIVE_CALL/1	Module: b_trace_checking
Name: is/2
Name: print/1
Name: >/2
Name: !

Name: perform_sequence_of_operations2/2	Module: b_trace_checking
Name: perform_one_operation_in_sequence/2	Module: b_trace_checking
Name: perform_single_operation/2	Module: b_trace_checking
Name: perform_action_tclk/4	Module: b_trace_checking
Name: single_operation_skip/2	Module: b_trace_checking

Name: RECURSIVE_CALL/3	Module: b_trace_checking
Name: is/2
Name: !
Name: =</2

Name: RECURSIVE_CALL/2	Module: b_trace_checking
Name: convert_term/2	Module: b_trace_checking

Name: convert_action/2	Module: b_trace_checking
Name: convert_term/2	Module: b_trace_checking

Name: RECURSIVE_CALL/4	Module: b_trace_checking
Name: generate_predicate/3	Module: b_trace_checking
Name: add_warning/3	Module: foo_error
Name: !

Name: RECURSIVE_CALL/2	Module: b_trace_checking
Name: unify/2	Module: b_trace_checking

Name: unify_action_as_term/3	Module: b_trace_checking
Name: perform_custom_operation_retry/2	Module: b_trace_checking

Name: write/1
Name: reset_temporary_preference/2	Module: preferences
Name: truncate_atom/3	Module: foo_error
Name: translate_event/2	Module: translate
Name: temporary_set_preference/3	Module: preferences

Name: perform_sequence_of_operations/1	Module: b_trace_checking
Name: !
Name: b_machine_has_constants_or_properties/0	Module: bmachine
Name: b_or_z_mode/0	Module: specfile

Name: format/2
Name: statistics/2
Name: current_state_id/1	Module: state_space
Name: print_green/1	Module: tools_printing
Name: print/1
Name: ident/1	Module: b_trace_checking
Name: true
Name: silent_mode/1	Module: foo_error
Name: ->/3
Name: !
Name: get_preference/2	Module: preferences
Name: fail
Name: nl
Name: print_red/1	Module: tools_printing
Name: perform_single_operation/2	Module: b_trace_checking
Name: if/3
Name: convert_action/2	Module: b_trace_checking
Name: tcltk_get_options/1	Module: tcltk_interface
Name: tcltk_reset/0	Module: tcltk_interface
Name: is_a_reset_operation/1	Module: b_trace_checking
Name: my_print_event/2	Module: b_trace_checking
Name: unify/2	Module: b_trace_checking
Name: print_bvalue/1	Module: translate
Name: lookup_value_for_existing_id/3	Module: store
Name: expand_const_and_vars_to_full_store/2	Module: specfile
Name: current_expression/2	Module: state_space
Name: RECURSIVE_CALL/2	Module: b_trace_checking
Name: perform_action_tclk/4	Module: b_trace_checking
Name: check_non_det_vars/2	Module: b_trace_checking
Name: unify_action_as_term/3	Module: b_trace_checking
Name: member/2
Name: current_options/1	Module: state_space

Name: perform_sequence_of_operations2/2	Module: b_trace_checking
Name: assertz/1
Name: retractall/1

prob_prolog/src/b_trace_checking.pl

Modules

Predicates of b_trace_checking

Module Information

Dynamic Predicates: max_nr_replayed/1

1016 Lines

84 Predicates

Imported Modules: lists tools error_manager debug junit_tests translate_keywords avl debug

11 Exports

70 specified Imports

Predicates:

Determinacy Checker:

Name: tcltk_check_sequence_from_file2/2	Module: b_trace_checking
Name: perform_initialisation/0	Module: b_trace_checking

Name: formatsilent/2	Module: foo_error
Name: member/2
Name: preference/2	Module: preferences
Name: >/2
Name: functor/3
Name: perform_alternative_op_with_same_functor/7	Module: b_trace_checking
Name: !
Name: nonvar/1
Name: arg/3
Name: true
Name: =/2
Name: get_prob_application_type/1	Module: preferences
Name: ->/3

Name: perform_single_operation_retry/4	Module: b_trace_checking
Name: =../2
Name: nl
Name: print/1
Name: !
Name: functor/3
Name: =/2

Name: =/2
Name: print_json_names/2	Module: b_trace_checking
Name: ->/3
Name: get_unchanged_list/3	Module: b_trace_checking
Name: print_json_paras/3	Module: b_trace_checking
Name: get_change_list/4	Module: b_trace_checking
Name: add_warning/4	Module: foo_error
Name: same_length/2	Module: foo_error
Name: not/1
Name: get_preference/2	Module: preferences
Name: get_operation_description_for_transition/4	Module: specfile
Name: get_operation_return_values_and_arguments/3	Module: specfile
Name: true
Name: get_possible_language_specific_top_level_event/3	Module: specfile
Name: get_operation_internal_name/2	Module: specfile
Name: transition/4	Module: state_space
Name: add_warning/3	Module: foo_error

Name: print_json_paras_aux/4	Module: b_trace_checking
Name: filter_json_paras/4	Module: b_trace_checking

Name: add_internal_error/2	Module: foo_error
Name: RECURSIVE_CALL/4	Module: b_trace_checking
Name: =/2
Name: mytranslate/2	Module: b_trace_checking
Name: is/2
Name: !

Name: nl
Name: print/1
Name: print_fdr/1	Module: b_trace_checking
Name: reverse/2	Module: foo_error
Name: get_action_trace/1	Module: state_space
Name: !
Name: silent_mode/1	Module: foo_error

Name: print_trace_for_replay/4	Module: b_trace_checking
Name: reverse/2	Module: foo_error
Name: op_trace_ids/1	Module: state_space

Name: add_internal_error/2	Module: foo_error
Name: print_transition_list_json/3	Module: b_trace_checking
Name: !
Name: print_transition_list_prolog/2	Module: b_trace_checking

Name: fail
Name: add_error/2	Module: foo_error
Name: true
Name: json_write_stream/3	Module: foo_error
Name: ->/3
Name: =/2
Name: get_modulename_filename/2	Module: tools
Name: b_machine_name/1	Module: bmachine
Name: b_or_z_mode/0	Module: specfile
Name: currently_opened_file/1	Module: specfile
Name: revision/1	Module: version
Name: version_str/1	Module: version
Name: ajoin/2	Module: foo_error
Name: environ/2	Module: system
Name: format_current_iso_time/1	Module: b_trace_checking
Name: call_cleanup/2
Name: temporary_set_preference/3	Module: preferences
Name: get_member_option/3	Module: tools_lists
Name: get_prob_application_type/1	Module: preferences