Dynamic Predicates: mc_found_error/2 expired_static_analysis_time/1

388 Lines

23 Predicates

Imported Modules: module_information random state_space

10 Exports

32 specified Imports

Imports	Exports
Name: state_violates_assertions/2 Module: b_interpreter Name: enter_new_error_scope/1 Module: error_manager Name: exit_error_scope/3 Module: error_manager Name: error_occurred_in_error_scope/0 Module: error_manager Name: add_internal_error/2 Module: error_manager Name: animation_mode/1 Module: specfile Name: csp_mode/1 Module: specfile Name: visited_expression/2 Module: state_space Name: transition/3 Module: state_space Name: operation_not_yet_covered/1 Module: state_space Name: depth_breadth_first_mode/1 Module: state_space_exploration_modes Name: b_machine_has_constants/0 Module: bmachine Name: multiple_concrete_constants_exist/0 Module: state_space Name: statistics_memory_used/1 Module: tools Name: silent_mode/1 Module: debug Name: formatsilent/3 Module: debug Name: preference/2 Module: preferences Name: prepare_state_for_specfile_trans/4 Module: specfile Name: format_with_colour_nl/4 Module: tools_printing Name: get_preference/2 Module: preferences Name: b_or_z_mode/1 Module: specfile Name: get_open_node_to_check/2 Module: state_space_exploration_modes Name: get_current_breadth_first_level/1 Module: state_space_exploration_modes Name: add_warning/3 Module: error_manager Name: xtl_property/2 Module: xtl_interface Name: animation_mode/1 Module: specfile Name: b_or_z_mode/1 Module: specfile Name: csp_mode/1 Module: specfile Name: b_get_machine_goal/1 Module: bmachine Name: ajoin/2 Module: tools Name: b_machine_has_proven_invariants/0 Module: bmachine Name: b_machine_has_unproven_assertions/0 Module: bmachine	Name: is_deadlocked/1 Name: node_satisfies_goal/1 Name: open_search/12 Name: expired_static_analysis_time/1 Name: proof_info_model_checking_incomplete/5 Name: model_checking_is_incomplete/6 Name: perform_static_analyses/3 Name: compute_transitions_opt/3 Name: get_model_check_stats/6 Name: find_invariant_error/4

Imports

Exports

Name: state_violates_assertions/2

Module: b_interpreter

Name: enter_new_error_scope/1

Module: error_manager

Name: exit_error_scope/3

Module: error_manager

Name: error_occurred_in_error_scope/0

Module: error_manager

Name: add_internal_error/2

Module: error_manager

Name: animation_mode/1

Module: specfile

Name: csp_mode/1

Module: specfile

Name: visited_expression/2

Module: state_space

Name: transition/3

Module: state_space

Name: operation_not_yet_covered/1

Module: state_space

Name: depth_breadth_first_mode/1

Module: state_space_exploration_modes

Name: b_machine_has_constants/0

Module: bmachine

Name: multiple_concrete_constants_exist/0

Module: state_space

Name: statistics_memory_used/1

Module: tools

Name: silent_mode/1

Module: debug

Name: formatsilent/3

Module: debug

Name: preference/2

Module: preferences

Name: prepare_state_for_specfile_trans/4

Module: specfile

Name: format_with_colour_nl/4

Module: tools_printing

Name: get_preference/2

Module: preferences

Name: b_or_z_mode/1

Module: specfile

Name: get_open_node_to_check/2

Module: state_space_exploration_modes

Name: get_current_breadth_first_level/1

Module: state_space_exploration_modes

Name: add_warning/3

Module: error_manager

Name: xtl_property/2

Module: xtl_interface

Name: animation_mode/1

Module: specfile

Name: b_or_z_mode/1

Module: specfile

Name: csp_mode/1

Module: specfile

Name: b_get_machine_goal/1

Module: bmachine

Name: ajoin/2

Module: tools

Name: b_machine_has_proven_invariants/0

Module: bmachine

Name: b_machine_has_unproven_assertions/0

Module: bmachine

Name: is_deadlocked/1

Name: node_satisfies_goal/1

Name: open_search/12

Name: expired_static_analysis_time/1

Name: proof_info_model_checking_incomplete/5

Name: model_checking_is_incomplete/6

Name: perform_static_analyses/3

Name: compute_transitions_opt/3

Name: get_model_check_stats/6

Name: find_invariant_error/4

compute_transitions/4

compute_transitions_opt/3

Description:
Optimisation options (see first argument 'Optimisations'):

find_invariant_error/4

get_model_check_stats/6

get_next_node_to_check/4

Description:
get_next_node_to_check(1,ID,_) :- state_space:not_invariant_checked(ID). % if there is an existing node whose invariant we have not yet checked: check it now

initialise_optimisations/5

is_csp_error_state/1

is_deadlocked/1

Description:
visited_expression_id(ID),

is_xtl_error_state/3

model_checking_is_incomplete/6

model_checking_is_incomplete(FindInvViolations,FindDeadlocks,FindGoal,FindAssViolations,Msg,'') :-
    proof_info_model_checking_incomplete(FindInvViolations,FindDeadlocks,FindGoal,FindAssViolations,Msg).

model_checking_is_incomplete(_FindInv,_FindDeadlocks,_FindGoal,_FindAss,Msg,Term) :-
    (get_preference(symmetry_mode,hash),hash_model_checking_imprecise(ID,BasicType)
    -> Msg = '*** Possibly not all states computed, symmetry hashing may be imprecise, e.g., for variable ',
    translate:pretty_type(BasicType,S),
    ajoin([ID,' : ',S],Term)).

model_checking_is_incomplete(1,_FindDeadlocks,_FindGoal,_FindAss,Msg,Term) :-
    (time_out_for_invariant(ID)
    -> Msg = '*** Timeout(s) occured during invariant computation, e.g., state with id = ', Term=ID).

model_checking_is_incomplete(_FindInv,_FindDeadlocks,_FindGoal,1,Msg,Term) :-
    (time_out_for_assertions(ID)
    -> Msg = '*** Timeout(s) occured during evaluation of ASSERTIONS, e.g., state with id = ', Term=ID).

model_checking_is_incomplete(_FindInv,_FindDeadlocks,_FindGoal,_FindAss,Msg,Term) :-
    (max_reached_for_node(ID)
    -> ((ID=root ; is_concrete_constants_state_id(ID))
    -> get_preference(maxNrOfInitialisations,MI),
    ajoin(['*** Not all transitions were computed as MAX_INITIALISATIONS=',MI,' was too small, e.g., for state with id = '],Msg)
    ; get_preference(maxNrOfEnablingsPerOperation,MO),
    ajoin(['*** Not all transitions were computed as MAX_OPERATIONS=',MO,' was too small, e.g., for state with id = '],Msg)
    ),
    Term=ID).

model_checking_is_incomplete(_FindInv,_FindDeadlocks,_FindGoal,_FindAss,Msg,Term) :-
    (time_out_for_node(ID,Op,Reason) ->
    functor(Reason,Func,_), % time_out or virtual_time_out
    ajoin(['*** Not all transitions were computed due to a ', Func,', e.g., for ',Op, ' and state with id = '],Msg),
    Term=ID).

model_checking_is_incomplete(_FindInv,_FindDeadlocks,_FindGoal,_FindAss,Msg,'') :-
    get_preference(ignore_hash_collisions,true),
    Msg = '*** Possibly not all states computed due to IGNORE_HASH_COLLISIONS preference'.

no_error_found_result/1

node_satisfies_goal/1

node_satisfies_goal/2

open_search/12

open_search(LimitNr,NodesAnalysed,LimitTime,Res,FindDeadlocks,FindInvViolations,
    FindGoal,FindAssViolations,FindStateErrors,
    StopAtFullCoverage,PartialOrderReduction,PartialGuardEvaluation) :-
    animation_mode(MODE),
    retractall(mc_found_error(_,_)),
    initialise_optimisations(MODE,PartialOrderReduction,PartialGuardEvaluation,FindInvViolations,Optimisations),
    perform_static_analyses(MODE,FindInvViolations,Optimisations),
    %(error_manager:real_error_occurred -> print(error_after_perform_static_analyses),nl ; true),
    depth_breadth_first_mode(DFMODE),
    preferences:temporary_set_preference(do_invariant_checking,true,CHNG),
    statistics(walltime,[ReferenceTime,_]),
    get_model_check_stats(States,_Transitions,ProcessedTotal,Percentage,_,_),
    % MEMO: used to cache expanded concrete_constants values
    % particularly useful, e.g., for ../prob_examples/public_examples/B/PerformanceTests/LiftLargeWithLargeCst.mch
    ((\+ b_machine_has_constants ; multiple_concrete_constants_exist)
    -> MEMO = '$disabled' % it could still be useful to cache one constant setup ??
    ; true),
    enter_new_error_scope(ScopeID),
    set_context_state(root),
    open_search10(0,LimitNr,refstatus(ReferenceTime,Percentage,States,ProcessedTotal,ReferenceTime),
    NodesAnalysed,LimitTime,MCRes,FindDeadlocks,FindInvViolations,
    FindGoal,FindAssViolations,FindStateErrors,
    StopAtFullCoverage,Optimisations,MODE,DFMODE,MEMO),
    %tools_printing:print_term_summary(memo(MEMO)),nl,
    exit_error_scope(ScopeID,_,open_search),
    preferences:reset_temporary_preference(do_invariant_checking,CHNG),
    clear_context_state,
    (no_error_found_result(MCRes),
    mc_found_error(Res,ID) % stored error because of mc_continue_after_error
    -> set_counter_example_last_node(ID)
    ; Res=MCRes).

open_search10/16

open_search10(Nr,LimitNr,RefStatus,NodesAnalysed,LimitTime,Res,
    FindDeadlocks,FindInvViolations,FindGoal,FindAssViolations,FindStateErrors,
    SFC,Optimisations,MODE,DF,MEMO) :-
    %print(open_search(Nr,LimitNr,RefStatus)),nl,
    Nr < LimitNr,!,
    (\+ number(LimitTime)
    -> open_search_do_one_node(Nr,LimitNr,RefStatus,NodesAnalysed,LimitTime,Res,
    FindDeadlocks,FindInvViolations,FindGoal,FindAssViolations,FindStateErrors,
    SFC,Optimisations,MODE,DF,MEMO)
    ; statistics(walltime,[NewTime,_]),
    (Nr mod 25 =:= 24, silent_mode(off) %, Nr\=0
    -> RefStatus = refstatus(RefTime,RefPerc,PrevStates,PrevProcessed,StartTime),
    Delta is NewTime-RefTime,
    (Delta>20000 % more than 20 seconds since last progress message
    % ; random(0,20000,X), X=
    -> get_model_check_stats(States,Transitions,ProcessedTotal,Perc,Ignored,ScopePerc),
    (Ignored>0
    -> format('~n* ~w states checked (~1f% of total ~w, ~1f% wo ~w ignored), ~w transitions,',
    [ProcessedTotal,Perc,States,ScopePerc,Ignored,Transitions])
    ; get_current_breadth_first_level(Level)
    -> format('~n* ~w states checked (~1f% of total ~w), ~w transitions, bf-level ~w, ',
    [ProcessedTotal,Perc,States,Transitions,Level])
    ; format('~n* ~w states checked (~1f% of total ~w), ~w transitions,',
    [ProcessedTotal,Perc,States,Transitions])
    ),
    findall(Op,operation_not_yet_covered(Op),NotCov), length(NotCov,NrNotCov),
    (NrNotCov = 1 -> format(' 1 operation not covered,',[])
    ; NrNotCov > 0 -> format(' ~w operations not covered,',[NrNotCov]) ; true),
    statistics_memory_used(M), tools:print_mb(M),
    DeltaProcessedStates is (ProcessedTotal-PrevProcessed),
    NodesProcessedPerSec is DeltaProcessedStates*1000 / (NewTime-RefTime),
    format('~n* currently checking ~2f states/sec',[NodesProcessedPerSec]),
    DeltaStates is (States-PrevStates),
    NodesPerSec is DeltaStates*1000 / (NewTime-RefTime),
    format(', adding ~2f new states/sec~n',[NodesPerSec]),
    RefStatus1 = refstatus(NewTime,Perc,States,ProcessedTotal,StartTime),
    FullDeltaTime is NewTime - StartTime,
    FullDeltaTimeMinutes is FullDeltaTime / 60000.0,
    (Perc>RefPerc -> format('* walltime ~1f minutes~n',[FullDeltaTimeMinutes])
    ; format('* walltime ~1f minutes, percentage of checked states decreasing from ~1f%~n',[FullDeltaTimeMinutes,RefPerc]))
    ; RefStatus1 = RefStatus
    )
    ; RefStatus1 = RefStatus
    ),
    (NewTime>LimitTime, Nr>0
    -> Res = [timeout,Nr], NodesAnalysed=Nr
    ; open_search_do_one_node(Nr,LimitNr,RefStatus1,NodesAnalysed,LimitTime,Res,
    FindDeadlocks,FindInvViolations,FindGoal,FindAssViolations,FindStateErrors,
    SFC,Optimisations,MODE,DF,MEMO))
).

open_search10(N,_LimitNr,_RefStatus,N,_,no ,_,_,_,_,_,_,_,_,_,_MEMO).

open_search_check_for_error/10

open_search_do_one_node/16

open_search_do_one_node(Nr,LimitNr,RefStatus,NodesAnalysed,LimitTime,Res,
    FindDeadlocks,FindInvViolations,
    FindGoal,FindAssViolations,FindStateErrors,
    StopAtFullCoverage,Optimisations,MODE,DFMODE,MEMO) :-
    get_next_node_to_check(FindInvViolations,ID,MODE,DFMODE),!,
    update_context_state(ID), %print(treating_node(ID)),nl,

    (preference(ignore_hash_collisions,true),
    preference(forget_state_space,true)
    -> retract_visited_expression(ID,CurState) %, retractall(id_to_marker(ID,_)) not necessary
    ; visited_expression(ID,CurState)),
    (FindInvViolations=1 % compute invariant status
    -> prepare_state_for_specfile_trans(CurState,ID,MEMO,PCurState),
    tcltk_interface:compute_invariant_if_necessary(ID,PCurState,MODE)
    ; CurState=PCurState),
    %print(processed_invariant(ID)), statistics(memory_used,M), tools:print_mb(M),nl,
    !,
    compute_transitions_opt(Optimisations,ID,PCurState),
    %tools:print_message(mc(ID)),
    %print(computed_all_transitions(ID)), statistics(memory_used,M2), tools:print_mb(M2),nl,
    % !,
    (open_search_check_for_error(ID,PCurState,Res,
    FindDeadlocks,FindInvViolations,FindGoal,FindAssViolations,
    FindStateErrors,StopAtFullCoverage,MODE)
    -> print_found_error(Res,ID),
    NodesAnalysed=Nr,
    set_counter_example_last_node(ID)
    ; N1 is Nr + 1,
    open_search10(N1,LimitNr,RefStatus,NodesAnalysed,LimitTime,Res,
    FindDeadlocks,FindInvViolations,FindGoal,FindAssViolations,FindStateErrors,StopAtFullCoverage,
    Optimisations,MODE,DFMODE,MEMO)
).

open_search_do_one_node(N,_LimitNr,_RefStatus,N,_,all,_,_,_,_,_,_,_,_,_,_MEMO) :-
    formatsilent(user_output,'% Model checking finished, all open states visited~n',[]).

open_search_found_error/10

Description:
we no longer use: error_manager:real_error_occurred ; errors can happen e.g. in POR static analysis

perform_static_analyses/3

perform_static_analyses_aux/3

print_found_error/2

proof_info_model_checking_incomplete/5

set_counter_example_last_node/1

Determinacy Checker

Determinacy Checker:

! 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(no_terminal_colors,true)
! 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_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_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(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),_85937,[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'),_55663,[access(exist),file_type(source),relative_to('/builds/stups/prob/prolog_doc_gen/prolog-Doc/prob_prolog/src/error_manager.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),_48709,[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),_47045,[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 extension('counter/counter') does not exist
! goal: absolute_file_name(extension('counter/counter'),_109837,[access(exist),file_type(source),relative_to('/builds/stups/prob/prolog_doc_gen/prolog-Doc/prob_prolog/src/succeed_max.pl')])
! Existence error in argument 1 of absolute_file_name/3
! file probsrc(tools) does not exist
! goal: absolute_file_name(probsrc(tools),_157459,[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),_185879,[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),_185879,[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),_188023,[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),_194001,[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 probsrc(eventhandling) does not exist
! goal: absolute_file_name(probsrc(eventhandling),_197423,[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),_194001,[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 extension('counter/counter') does not exist
! goal: absolute_file_name(extension('counter/counter'),_199411,[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),_198647,[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),_198647,[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),_199943,[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),_199269,[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),_200263,[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),_194001,[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 probsrc(kernel_waitflags) does not exist
! goal: absolute_file_name(probsrc(kernel_waitflags),_185879,[access(exist),file_type(source),relative_to('/builds/stups/prob/prolog_doc_gen/prolog-Doc/prob_prolog/src/delay.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: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),_216749,[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),_211055,[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: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),_194143,[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 probsrc(custom_explicit_sets) does not exist
! goal: absolute_file_name(probsrc(custom_explicit_sets),_185879,[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),_160735,[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),_157171,[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(eventhandling) does not exist
! goal: absolute_file_name(probsrc(eventhandling),_160313,[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(b_state_model_check) does not exist
! goal: absolute_file_name(probsrc(b_state_model_check),_157317,[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(bmachine_eventb) does not exist
! goal: absolute_file_name(probsrc(bmachine_eventb),_150345,[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),_150345,[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),_151725,[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),_150345,[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: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),_152919,[access(exist),file_type(source),relative_to('/builds/stups/prob/prolog_doc_gen/prolog-Doc/prob_prolog/src/xtl_interface.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),_147211,[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 extension('probhash/probhash') does not exist
! goal: absolute_file_name(extension('probhash/probhash'),_146923,[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 kodkodsrc(kodkod) does not exist
! goal: absolute_file_name(kodkodsrc(kodkod),_116525,[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('probhash/probhash') does not exist
! goal: absolute_file_name(extension('probhash/probhash'),_109837,[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(btypechecker) does not exist
! goal: absolute_file_name(probsrc(btypechecker),_97611,[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 probsrc(gensym) does not exist
! goal: absolute_file_name(probsrc(gensym),_77575,[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(custom_explicit_sets) does not exist
! goal: absolute_file_name(probsrc(custom_explicit_sets),_48593,[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 extension('random_permutations/random_permutations') does not exist
! goal: absolute_file_name(extension('random_permutations/random_permutations'),_50741,[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),_48739,[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'),_38789,[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 extension('counter/counter') does not exist
! goal: absolute_file_name(extension('counter/counter'),_12647,[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 kodkodsrc(kodkod) does not exist
! goal: absolute_file_name(kodkodsrc(kodkod),_6247,[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 probporsrc(static_analysis) does not exist
! goal: absolute_file_name(probporsrc(static_analysis),_261,[access(exist),file_type(source),relative_to('/builds/stups/prob/prolog_doc_gen/prolog-Doc/prob_prolog/src/model_checker.pl')])

Name: compute_all_transitions/2	Module: tcltk_interface
Name: compute_transitions_pge/2	Module: foo_error
Name: !
Name: \=/2
Name: compute_ample_set/3	Module: tcltk_interface
Name: ==/2
Name: =/2

Name: explore_one_state/8	Module: state_space_explorer
Name: open_search_do_one_node/16	Module: model_checker

Name: is_xtl_error_state/3	Module: model_checker
Name: is_csp_error_state/1	Module: model_checker
Name: !
Name: check_invariantKO/3	Module: tcltk_interface
Name: true
Name: invariant_violated/1	Module: foo_error
Name: ->/2

Name: tcltk_print_node_for_dot/2	Module: visualize_graph
Name: open_search_found_error/10	Module: model_checker

Name: =/2
Name: is/2
Name: >/2
Name: ->/3
Name: get_state_space_stats/4	Module: foo_error

model_checker

prob_prolog/src/model_checker.pl

Modules

Predicates of model_checker

Module Information

Dynamic Predicates: mc_found_error/2 expired_static_analysis_time/1

388 Lines

23 Predicates

Imported Modules: module_information random state_space

10 Exports

32 specified Imports

Predicates:

compute_transitions/4

compute_transitions_opt/3

find_invariant_error/4

get_model_check_stats/6

get_next_node_to_check/4

initialise_optimisations/5

is_csp_error_state/1

is_deadlocked/1

is_xtl_error_state/3

model_checking_is_incomplete/6

no_error_found_result/1

node_satisfies_goal/1

node_satisfies_goal/2

open_search/12

open_search10/16

open_search_check_for_error/10

open_search_do_one_node/16

open_search_found_error/10

perform_static_analyses/3

perform_static_analyses_aux/3

print_found_error/2

proof_info_model_checking_incomplete/5

set_counter_example_last_node/1

Determinacy Checker:

Name: open_search/12	Module: model_checker
Name: open_search10/16	Module: model_checker
Name: explore_state_space/5	Module: state_space_explorer
Name: open_search/4	Module: safety_mc
Name: print_stats_and_update_refstatus/4	Module: state_space_explorer

Name: true
Name: assertz/1
Name: b_or_z_mode/1	Module: specfile
Name: ->/3
Name: get_open_node_to_check/2	Module: state_space_exploration_modes

Name: node_satisfies_goal/2	Module: model_checker
Name: animation_mode/1	Module: specfile

Name: is_goal_node/1	Module: visualize_graph
Name: accepting_state/2	Module: refinement_checker
Name: check_ap/2	Module: ltl_propositions

Name: =/2
Name: set_counter_example_last_node/1	Module: model_checker
Name: mc_found_error/2	dynamic predicate
Name: no_error_found_result/1	Module: model_checker
Name: ->/3
Name: clear_context_state	Module: foo_error
Name: reset_temporary_preference/2	Module: preferences
Name: exit_error_scope/3	Module: error_manager
Name: open_search10/16	Module: model_checker
Name: set_context_state/1	Module: foo_error
Name: enter_new_error_scope/1	Module: error_manager
Name: true
Name: multiple_concrete_constants_exist/0	Module: state_space
Name: b_machine_has_constants/0	Module: bmachine
Name: not/1
Name: get_model_check_stats/6	Module: model_checker
Name: statistics/2
Name: temporary_set_preference/3	Module: preferences
Name: depth_breadth_first_mode/1	Module: state_space_exploration_modes
Name: perform_static_analyses/3	Module: model_checker
Name: initialise_optimisations/5	Module: model_checker
Name: retractall/1
Name: animation_mode/1	Module: specfile

Name: fail
Name: assertz/1
Name: mc_found_error/2	dynamic predicate
Name: not/1
Name: print_found_error/2	Module: model_checker
Name: true
Name: get_preference/2	Module: preferences
Name: ->/3
Name: open_search_found_error/10	Module: model_checker

Name: compute_operation_relations_for_pge_if_necessary/2	Module: foo_error
Name: compute_dependendency_relation_of_all_events_in_the_model/3	Module: foo_error
Name: !
Name: ==/2
Name: =/2