Dynamic Predicates: constant_can_be_expanded/1 var_min_max/3 operation_hit/3 node_hit/2 definitely_enabled_after/2 possibly_enables/2 degree_in_id/3 max_degree/2

486 Lines

46 Predicates

Imported Modules: module_information state_space tools

12 Exports

43 specified Imports

Imports	Exports
Name: debug_println/2 Module: debug Name: debug_format/3 Module: debug Name: add_message/4 Module: error_manager Name: add_message/3 Module: error_manager Name: add_debug_message/4 Module: error_manager Name: add_debug_message/3 Module: error_manager Name: length_less/2 Module: tools_lists Name: current_state_id/1 Module: state_space Name: get_constants_state_for_id/2 Module: state_space Name: try_get_unique_constants_state/1 Module: state_space Name: samsort/3 Module: samsort Name: term_size/2 Module: terms Name: translate_bvalue_with_limit/3 Module: translate Name: debug_mode/1 Module: debug Name: b_is_variable/1 Module: bmachine Name: b_is_constant/1 Module: bmachine Name: abstract_constant/2 Module: b_machine_hierarchy Name: is_registered_function_name/2 Module: memoization Name: get_registered_function/3 Module: memoization Name: cardinality_as_int/2 Module: kernel_objects Name: is_interval_closure/3 Module: custom_explicit_sets Name: explicit_set_cardinality/2 Module: custom_explicit_sets Name: is_infinite_or_very_large_explicit_set/2 Module: custom_explicit_sets Name: try_expand_custom_set_with_catch/3 Module: custom_explicit_sets Name: is_infinite_explicit_set/1 Module: custom_explicit_sets Name: avl_size/2 Module: avl Name: time_out_with_factor_call/4 Module: tools_timeout Name: translate_bvalue_kind/2 Module: translate Name: get_nr_of_machine_variables/1 Module: bmachine Name: get_nr_of_machine_constants/1 Module: bmachine Name: get_constant_span/2 Module: bmachine Name: write_lines_to_file/2 Module: tools_files Name: abstract_constant/2 Module: b_machine_hierarchy Name: concrete_constant/2 Module: b_machine_hierarchy Name: property/2 Module: specfile Name: avl_size/2 Module: avl Name: avl_max/2 Module: avl Name: get_specification_description/2 Module: specfile Name: get_possible_event/1 Module: specfile Name: get_operation_name/2 Module: specfile Name: is_not_interesting/1 Module: state_space_exploration_modes Name: b_or_z_mode/0 Module: specfile Name: b_is_operation_name/1 Module: bmachine	Name: tcltk_compute_coverage/1 Name: tcltk_compute_coverage_and_enabling/1 Name: tcltk_compute_coverage_and_degree/1 Name: tcltk_compute_min_max/1 Name: pretty_print_min_max_coverage_to_file/1 Name: compute_the_coverage/5 Name: pretty_print_coverage_information_to_file/1 Name: operation_hit/2 Name: query_node_hit/2 Name: uncovered_operation/1 Name: tcltk_analyse_constants/2 Name: tcltk_analyse_constants/1

Imports

Exports

Name: debug_println/2

Module: debug

Name: debug_format/3

Module: debug

Name: add_message/4

Module: error_manager

Name: add_message/3

Module: error_manager

Name: add_debug_message/4

Module: error_manager

Name: add_debug_message/3

Module: error_manager

Name: length_less/2

Module: tools_lists

Name: current_state_id/1

Module: state_space

Name: get_constants_state_for_id/2

Module: state_space

Name: try_get_unique_constants_state/1

Module: state_space

Name: samsort/3

Module: samsort

Name: term_size/2

Module: terms

Name: translate_bvalue_with_limit/3

Module: translate

Name: debug_mode/1

Module: debug

Name: b_is_variable/1

Module: bmachine

Name: b_is_constant/1

Module: bmachine

Name: abstract_constant/2

Module: b_machine_hierarchy

Name: is_registered_function_name/2

Module: memoization

Name: get_registered_function/3

Module: memoization

Name: cardinality_as_int/2

Module: kernel_objects

Name: is_interval_closure/3

Module: custom_explicit_sets

Name: explicit_set_cardinality/2

Module: custom_explicit_sets

Name: is_infinite_or_very_large_explicit_set/2

Module: custom_explicit_sets

Name: try_expand_custom_set_with_catch/3

Module: custom_explicit_sets

Name: is_infinite_explicit_set/1

Module: custom_explicit_sets

Name: avl_size/2

Module: avl

Name: time_out_with_factor_call/4

Module: tools_timeout

Name: translate_bvalue_kind/2

Module: translate

Name: get_nr_of_machine_variables/1

Module: bmachine

Name: get_nr_of_machine_constants/1

Module: bmachine

Name: get_constant_span/2

Module: bmachine

Name: write_lines_to_file/2

Module: tools_files

Name: abstract_constant/2

Module: b_machine_hierarchy

Name: concrete_constant/2

Module: b_machine_hierarchy

Name: property/2

Module: specfile

Name: avl_size/2

Module: avl

Name: avl_max/2

Module: avl

Name: get_specification_description/2

Module: specfile

Name: get_possible_event/1

Module: specfile

Name: get_operation_name/2

Module: specfile

Name: is_not_interesting/1

Module: state_space_exploration_modes

Name: b_or_z_mode/0

Module: specfile

Name: b_is_operation_name/1

Module: bmachine

Name: tcltk_compute_coverage/1

Name: tcltk_compute_coverage_and_enabling/1

Name: tcltk_compute_coverage_and_degree/1

Name: tcltk_compute_min_max/1

Name: pretty_print_min_max_coverage_to_file/1

Name: compute_the_coverage/5

Name: pretty_print_coverage_information_to_file/1

Name: operation_hit/2

Name: query_node_hit/2

Name: uncovered_operation/1

Name: tcltk_analyse_constants/2

Name: tcltk_analyse_constants/1

Predicates

Predicates:

add_cov_hit/2

add_node_hit/1

compute_cardinality/3

compute_coverage/2

compute_the_coverage/5

def_enables/1

finalise_degree_info/0

init_enabling_degree_info/2

pretty_print_coverage_information_to_file/1

pretty_print_min_max_coverage_to_file/1

tcltk_analyse_constants/1

tcltk_analyse_constants/2

tcltk_compute_coverage/1

tcltk_compute_coverage_and_degree/1

tcltk_compute_coverage_and_enabling/1

tcltk_compute_min_max/1

tcltk_compute_min_max/2

total_number_of_transitions/1

translate_min_max/5

treat_state_for_min_max/1

treat_var/2

uncovered_operation/1

update_degree/2

update_degree_info/2

update_enabling_info/3

update_last_degree/0

add_cov_hit/2

add_node_hit/1

compute_cardinality/3

compute_coverage/2

compute_the_coverage/5

def_enables/1

finalise_degree_info/0

Description:
,pge_algo: disabled_operations_stats(ResPGE), % in case no disabling stats are given an empty list is returned
append(Res_,ResPGE,Res).

get_value_kind(CL,_,Res,Msg) :- is_infinite_explicit_set(CL),!,
    Res = 'INFINITE-Set',
    Msg = 'The constant is definitely infinite'.

get_value_kind(CL,_,Res,Msg) :- is_interval_closure(CL,_,_),!,
    Res = 'INTERVAL',
    Msg = 'The constant is a symbolic interval.'.

get_value_kind(SimpleValue,_ID,Res,Msg) :- SimpleValue \= closure(_,_,_),
    translate_bvalue_kind(SimpleValue,R), !,
    Res=R, Msg=''.

get_value_kind(closure(P,T,B),ID,Res,Msg) :-
    add_debug_message(constants_analysis,'Checking if symbolic closure can be expanded: ',ID,B),
    % TODO: provide flag as this can take long
    time_out_with_factor_call(
    try_expand_custom_set_with_catch(closure(P,T,B),Expansion,get_value_kind),
    min_max_time_out(10,100,15000), % Factor 10, minimum 100 ms, maximum 15 seconds
    [silent],
    (add_debug_message(constants_analysis,'TIME-OUT during expansion for: ',ID),fail)),
    %functor(Expansion,FF,NN),print(expansion(FF,NN)),nl,
    %translate:translate_bvalue_with_limit(Expansion,100000,S), write(S),nl,
    Expansion \= closure(_,_,_),
    %(length(Expansion,Len) -> print(len(Len)),nl ; true),
    time_out_with_factor_call(
    compute_cardinality(closure(P,T,B),Expansion,Size),
    min_max_time_out(10,100,15000), % Factor=10, but min. 100 ms, max 15000 ms
    [],
    (add_debug_message(constants_analysis,'TIME-OUT during computation of Size: ',ID),
    Size='?')),
    !, % Symbolic set can be expanded; user could mark it as concrete constant
    (abstract_constant(ID,_)
    -> CC = 'Abstract constant ',
    Suggestion = ' (by moving to CONCRETE_CONSTANTS or annotating with /*@desc expand */ pragma): '
    ; CC = 'Concrete constant ',
    Suggestion = ' (by annotating with /*@desc expand */ pragma) '
    ),
    ajoin([CC,'is stored symbolically but can be expanded to a finite set of size ',Size,
    Suggestion ],Msg),
    get_constant_span(ID,Span),
    (constant_can_be_expanded(ID) -> true ; assert(constant_can_be_expanded(ID))),
    add_debug_message(constants_analysis,Msg,ID,Span),
    ajoin(['FINITE-SYMBOLIC-Set:',Size],Res).

get_value_kind(CL,_,Res,Msg) :-
    is_infinite_or_very_large_explicit_set(CL,20000),!,
    Res= 'LARGE-SYMBOLIC-Set',
    Msg = 'The constant has at least 20000 elements'.

get_value_kind(closure(_P,_T,_B),_,Res,Msg) :- !,
    Res = 'SYMBOLIC-Set', Msg=''.

get_value_kind(global_set(G),_,Res,Msg) :- !,
    Res = G, Msg='The constant is a synonym for an enumerated or deferred set'.

get_value_kind(_,_,'?','').

init_enabling_degree_info/2

Dynamic: true

Dynamic: true

pretty_print_coverage_information_to_file/1

pretty_print_min_max_coverage_to_file/1

tcltk_analyse_constants/1

tcltk_analyse_constants/2

tcltk_compute_coverage/1

tcltk_compute_coverage_and_degree/1

tcltk_compute_coverage_and_enabling/1

tcltk_compute_min_max/1

tcltk_compute_min_max/2

total_number_of_transitions/1

translate_min_max/5

treat_state_for_min_max/1

treat_var/2

uncovered_operation/1

update_degree/2

update_degree_info/2

update_enabling_info/3

update_last_degree/0

Determinacy Checker

Determinacy Checker:

! Existence error in argument 1 of absolute_file_name/3
! file probsrc(module_information) does not exist
! goal: absolute_file_name(probsrc(module_information),_4861,[access(exist),file_type(source),relative_to('/builds/stups/prob/prolog_doc_gen/prolog-Doc/prob_prolog/src/extra/coverage_statistics.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),_5975,[access(exist),file_type(source),relative_to('/builds/stups/prob/prolog_doc_gen/prolog-Doc/prob_prolog/src/extra/coverage_statistics.pl')])
! Existence error in argument 1 of absolute_file_name/3
! file probsrc(tools) does not exist
! goal: absolute_file_name(probsrc(tools),_6375,[access(exist),file_type(source),relative_to('/builds/stups/prob/prolog_doc_gen/prolog-Doc/prob_prolog/src/extra/coverage_statistics.pl')])
! Existence error in argument 1 of absolute_file_name/3
! file probsrc(debug) does not exist
! goal: absolute_file_name(probsrc(debug),_261,[access(exist),file_type(source),relative_to('/builds/stups/prob/prolog_doc_gen/prolog-Doc/prob_prolog/src/extra/coverage_statistics.pl')])

Name: assertz/1
Name: is/2
Name: operation_hit/3	Module: coverage_statistics
Name: retract/1
Name: ->/3
Name: =/2

Name: assertz/1
Name: is/2
Name: node_hit/2	Module: coverage_statistics
Name: retract/1
Name: ->/3

Name: true
Name: finalise_degree_info/0	Module: coverage_statistics
Name: =/2
Name: ->/3
Name: fail
Name: update_degree_info/2	Module: coverage_statistics
Name: update_enabling_info/3	Module: coverage_statistics
Name: add_cov_hit/2	Module: coverage_statistics
Name: get_operation_name/2	Module: specfile
Name: nonvar/1
Name: transition/3	Module: foo_error
Name: add_node_hit/1	Module: coverage_statistics
Name: \=/2
Name: state_error/3	Module: foo_error
Name: invariant_not_yet_checked/1	Module: foo_error
Name: time_out_for_assertions/1	Module: foo_error
Name: time_out_for_invariant/1	Module: foo_error
Name: invariant_violated/1	Module: foo_error
Name: max_reached_or_timeout_for_node/1	Module: foo_error
Name: is_not_interesting/1	Module: state_space_exploration_modes
Name: not_all_transitions_added/1	Module: foo_error
Name: visited_expression_id/1	Module: foo_error

Name: append/3
Name: ajoin/2	Module: foo_error
Name: query_node_hit/2	Module: coverage_statistics
Name: get_op_string/3	Module: coverage_statistics
Name: =/2
Name: findall/3
Name: ->/3
Name: total_number_of_transitions/1	Module: coverage_statistics
Name: length/2
Name: sort/2
Name: compute_coverage/2	Module: coverage_statistics
Name: reset_node_hit/2	Module: coverage_statistics
Name: retractall/1

Name: string_concatenate/3	Module: foo_error
Name: definitely_enabled_after/2	dynamic predicate
Name: operation_hit/3	Module: coverage_statistics

Name: RECURSIVE_CALL/4	Module: coverage_statistics
Name: is/2
Name: =/2
Name: !
Name: >/2

Name: =/2
Name: update_last_degree/0	Module: coverage_statistics
Name: degree_in_id/3	dynamic predicate
Name: retract/1
Name: ->/3

Name: translate_min_max/5	Module: coverage_statistics
Name: =/2
Name: concrete_constant/2	Module: b_machine_hierarchy
Name: abstract_constant/2	Module: b_machine_hierarchy
Name: ->/3
Name: var_min_max/3	dynamic predicate

Name: get_value_info2/4	Module: coverage_statistics
Name: !
Name: get_registered_function/3	Module: memoization
Name: is_registered_function_name/2	Module: memoization
Name: get_id_class/2	Module: coverage_statistics

Name: @</2
Name: =/2
Name: ->/2
Name: true
Name: RECURSIVE_CALL/2	Module: coverage_statistics
Name: ->/3
Name: avl_max/2	Module: avl
Name: </2
Name: !
Name: avl_size/2	Module: avl
Name: fail
Name: \==/2

Name: pos_enables/1	Module: coverage_statistics
Name: add_cov_hit/2	Module: coverage_statistics
Name: operation_hit/2	Module: coverage_statistics
Name: uncovered_operation/1	Module: coverage_statistics
Name: def_enables/1	Module: coverage_statistics

Name: string_concatenate/3	Module: foo_error
Name: possibly_enables/2	dynamic predicate
Name: operation_hit/3	Module: coverage_statistics

Name: init_enabling_degree_info/2	Module: coverage_statistics
Name: assertz/1
Name: true
Name: b_or_z_mode/0	Module: specfile
Name: ->/3
Name: retractall/1

Name: =/2
Name: format/3
Name: true
Name: ->/3
Name: findall/3
Name: samsort/3	Module: samsort
Name: reorder_cols/2	Module: coverage_statistics
Name: retractall/1
Name: !
Name: try_get_unique_constants_state/1	Module: state_space
Name: get_constants_state_for_id/2	Module: state_space

Name: =/2
Name: translate_bvalue/2	Module: translate
Name: gen_fd_set/4	Module: coverage_statistics
Name: !

Name: fail
Name: treat_var/2	Module: coverage_statistics
Name: property/2	Module: specfile
Name: b_or_z_mode/0	Module: specfile
Name: not/1
Name: member/2
Name: !
Name: =/2
Name: RECURSIVE_CALL/1	Module: coverage_statistics

Name: assertz/1
Name: =/2
Name: is_smaller/2	Module: coverage_statistics
Name: ->/3
Name: !
Name: var_min_max/3	dynamic predicate
Name: retract/1

Name: assertz/1
Name: format/2
Name: retractall/1
Name: true
Name: >=/2
Name: max_degree/2	dynamic predicate
Name: ->/3

Name: fail
Name: assertz/1
Name: opname_possible/2	Module: coverage_statistics
Name: not/1
Name: possibly_enables/2	dynamic predicate
Name: definitely_enabled_after/2	dynamic predicate
Name: retract/1
Name: true
Name: ->/3

Name: true
Name: update_degree/2	Module: coverage_statistics
Name: degree_in_id/3	dynamic predicate
Name: retract/1
Name: ->/3

Name: get_cur_degree/3	Module: coverage_statistics
Name: finalise_degree_info/0	Module: coverage_statistics

prob_prolog/src/extra/coverage_statistics.pl

Modules

Predicates of coverage_statistics

Module Information

Dynamic Predicates: constant_can_be_expanded/1 var_min_max/3 operation_hit/3 node_hit/2 definitely_enabled_after/2 possibly_enables/2 degree_in_id/3 max_degree/2

486 Lines

46 Predicates

Imported Modules: module_information state_space tools

12 Exports

43 specified Imports

Predicates:

Determinacy Checker: