Dynamic Predicates: disables/2 enables/2 keeps/2 enabling_relations/6 pge_predicates_computed/0 disabled_operations/3 nr_skipped_guard_evaluations/1

476 Lines

41 Predicates

Imported Modules: ordsets lists debug module_information

8 Exports

38 specified Imports

Imports	Exports
Name: b_top_level_operation/1 Module: bmachine Name: b_machine_has_constants_or_properties/0 Module: bmachine Name: get_guard/2 Module: b_state_model_check Name: get_negated_guard/3 Module: b_state_model_check Name: clear_context_state/0 Module: state_space Name: conjunct_predicates/2 Module: bsyntaxtree Name: create_negation/2 Module: bsyntaxtree Name: b_get_read_write/3 Module: b_read_write_info Name: b_get_operation_read_guard_vars/4 Module: b_read_write_info Name: register_event_listener/3 Module: eventhandling Name: specfile_possible_trans_name_for_successors/2 Module: specfile Name: prepare_state_for_specfile_trans/3 Module: specfile Name: animation_mode/1 Module: specfile Name: assert_time_out_for_node/3 Module: state_space Name: use_no_timeout/1 Module: state_space Name: assert_max_reached_for_node/1 Module: state_space Name: save_constants/1 Module: value_persistance Name: add_new_transitions_to_cache/1 Module: value_persistance Name: reset_max_reached/0 Module: succeed_max Name: max_reached/0 Module: succeed_max Name: get_preference/2 Module: preferences Name: enter_new_error_scope/1 Module: error_manager Name: exit_error_scope/3 Module: error_manager Name: specific_event_occurred_at_level/2 Module: error_manager Name: clear_all_errors_in_error_scope/1 Module: error_manager Name: is_time_out_result/1 Module: error_manager Name: set_error_context/1 Module: error_manager Name: clear_error_context/0 Module: error_manager Name: time_out_with_enum_warning_for_findall/3 Module: error_manager Name: add_warning/3 Module: error_manager Name: add_error_fail/3 Module: error_manager Name: cputime/1 Module: tools Name: print_message/1 Module: tools Name: find_initialised_states/1 Module: state_space Name: add_transition/4 Module: tcltk_interface Name: catch_clpfd_overflow_call_for_state/4 Module: tcltk_interface Name: temporary_set_preference/3 Module: preferences Name: reset_temporary_preference/2 Module: preferences	Name: tcltk_disabling_analysis/1 Name: compute_transitions_pge/2 Name: disabled_operations_stats/1 Name: is_pge_opt_on/0 Name: is_pge_opt_on/1 Name: compute_and_update_disabled_enabled_operations/3 Name: compute_operation_relations_for_pge/1 Name: compute_operation_relations_for_pge_if_necessary/2

Imports

Exports

Name: b_top_level_operation/1

Module: bmachine

Name: b_machine_has_constants_or_properties/0

Module: bmachine

Name: get_guard/2

Module: b_state_model_check

Name: get_negated_guard/3

Module: b_state_model_check

Name: clear_context_state/0

Module: state_space

Name: conjunct_predicates/2

Module: bsyntaxtree

Name: create_negation/2

Module: bsyntaxtree

Name: b_get_read_write/3

Module: b_read_write_info

Name: b_get_operation_read_guard_vars/4

Module: b_read_write_info

Name: register_event_listener/3

Module: eventhandling

Name: specfile_possible_trans_name_for_successors/2

Module: specfile

Name: prepare_state_for_specfile_trans/3

Module: specfile

Name: animation_mode/1

Module: specfile

Name: assert_time_out_for_node/3

Module: state_space

Name: use_no_timeout/1

Module: state_space

Name: assert_max_reached_for_node/1

Module: state_space

Name: save_constants/1

Module: value_persistance

Name: add_new_transitions_to_cache/1

Module: value_persistance

Name: reset_max_reached/0

Module: succeed_max

Name: max_reached/0

Module: succeed_max

Name: get_preference/2

Module: preferences

Name: enter_new_error_scope/1

Module: error_manager

Name: exit_error_scope/3

Module: error_manager

Name: specific_event_occurred_at_level/2

Module: error_manager

Name: clear_all_errors_in_error_scope/1

Module: error_manager

Name: is_time_out_result/1

Module: error_manager

Name: set_error_context/1

Module: error_manager

Name: clear_error_context/0

Module: error_manager

Name: time_out_with_enum_warning_for_findall/3

Module: error_manager

Name: add_warning/3

Module: error_manager

Name: add_error_fail/3

Module: error_manager

Name: cputime/1

Module: tools

Name: print_message/1

Module: tools

Name: find_initialised_states/1

Module: state_space

Name: add_transition/4

Module: tcltk_interface

Name: catch_clpfd_overflow_call_for_state/4

Module: tcltk_interface

Name: temporary_set_preference/3

Module: preferences

Name: reset_temporary_preference/2

Module: preferences

Name: tcltk_disabling_analysis/1

Name: compute_transitions_pge/2

Name: disabled_operations_stats/1

Name: is_pge_opt_on/0

Name: is_pge_opt_on/1

Name: compute_and_update_disabled_enabled_operations/3

Name: compute_operation_relations_for_pge/1

Name: compute_operation_relations_for_pge_if_necessary/2

Predicates

Predicates:

add_transition_timeout/5

add_transitions_pge/3

assert_disabled_ops_to_init_states_if_necessary/0

check_only_disabled/1

check_only_enabled/1

check_timeout_result/4

clear_dynamic_predicates_for_pge/0

compute_and_update_disabled_enabled_operations/3

compute_cbc_enabling_relation_and_assert/5

compute_disabled_operations/4

compute_disabled_operations_after_state/5

compute_enabled_operations/4

compute_enabled_operations_after_state/5

compute_enabling_relations/3

compute_impossible_keep_guaranteed/3

compute_operation_relations_for_pge/1

compute_operation_relations_for_pge_if_necessary/2

compute_transitions_pge/2

compute_transitions_pge2/2

disabled_operations_stats/1

disables/4

enables/4

explore_current_state_pge/7

explore_current_state_pge1/9

get_disabled_action_by_keep/3

get_enabled_action_by_keep/3

get_first_argument/2

get_goal_predicate/4

get_possible_enabled_trans_names/5

get_possible_enabled_trans_names_aux/4

get_start_predicate/3

is_pge_opt_on/0

is_pge_opt_on/1

my_exit_error_scope/1

not_a_member_of_disabled/2

prove_and_assert_enabling_relation/6

setup_constants_state/1

setup_constants_state1/1

tcltk_disabling_analysis/1

update_disabled_enabled_operations/3

update_disabled_enabled_operations_l/3

add_transition_timeout/5

add_transitions_pge/3

assert_disabled_ops_to_init_states_if_necessary/0

check_only_disabled/1

check_only_enabled/1

check_timeout_result/4

clear_dynamic_predicates_for_pge/0

Description:
Static Analysis Predicates %%%%
Model Checker predicates %%%%
INFO %%%%
:- use_module(library(timeout)).
Dynamic predicates used for: saving the enabling relations, number of skipped guard evaluations,
and sets of enabled and disabled events at the various states. %%%%%
enabling_relations(Op1,Op2,Enable,KeepEnabled,Disable,KeepDisabled)

compute_and_update_disabled_enabled_operations/3

compute_cbc_enabling_relation_and_assert/5

compute_cbc_enabling_relation_and_assert(OpName1,OpName2,FindInvViolations,Timeout,Pref) :-
    b_get_read_write(OpName1,_Reads1_,Writes1),
    get_negated_guard(OpName2,PosGuard2,NegGuard2),
    enabling_analysis: partition_predicate(PosGuard2,Writes1,FilteredPosGuard2,StaticPosGuard2),
    create_negation(FilteredPosGuard2,FilteredNegGuard2),
    (OpName1==OpName2 ->
    KeepDisabled=false, Enable=false,
    (Pref=enabled2 ->
    test_path_non_failing(PosGuard2,[OpName1],FilteredNegGuard2,FindInvViolations,Timeout,Disable),
    KeepEnabled = unknown
    ;Pref=disabled2 ->
    translate: print_bexpr(PosGuard2),
    translate: print_bexpr(FilteredPosGuard2),
    test_path_non_failing(PosGuard2,[OpName1],FilteredPosGuard2,FindInvViolations,Timeout,KeepEnabled),
    Disable = unknown
    ;
    test_path_non_failing(PosGuard2,[OpName1],FilteredNegGuard2,FindInvViolations,Timeout,Disable),
    test_path_non_failing(PosGuard2,[OpName1],FilteredPosGuard2,FindInvViolations,Timeout,KeepEnabled)
    )
    ;
    conjunct_predicates([StaticPosGuard2,FilteredNegGuard2],NegEnableGuard2),
    (Pref=enabled2 -> % need to known just Disable and KeepDisabled
    Enable = unknown, KeepEnabled = unknown,
    test_path_non_failing(PosGuard2,[OpName1],FilteredNegGuard2,FindInvViolations,Timeout,Disable),
    test_path_non_failing(NegGuard2,[OpName1],NegGuard2,FindInvViolations,Timeout,KeepDisabled)
    ;Pref=disabled2 -> % need to known just Enable and KeepEnabled
    test_path_non_failing(NegEnableGuard2,[OpName1],FilteredPosGuard2,FindInvViolations,Timeout,Enable),
    test_path_non_failing(PosGuard2,[OpName1],FilteredPosGuard2,FindInvViolations,Timeout,KeepEnabled),
    Disable = unknown, KeepDisabled = unknown
    ; % we have full2
    test_path_non_failing(NegEnableGuard2,[OpName1],FilteredPosGuard2,FindInvViolations,Timeout,Enable),
    test_path_non_failing(PosGuard2,[OpName1],FilteredPosGuard2,FindInvViolations,Timeout,KeepEnabled),
    test_path_non_failing(PosGuard2,[OpName1],FilteredNegGuard2,FindInvViolations,Timeout,Disable),
    test_path_non_failing(NegGuard2,[OpName1],NegGuard2,FindInvViolations,Timeout,KeepDisabled)
    )
    ),
    prove_and_assert_enabling_relation(OpName1,OpName2,Enable,KeepEnabled,Disable,KeepDisabled),
    debug_println(9,enabling_relations(OpName1,OpName2,Enable,KeepEnabled,Disable,KeepDisabled)).

compute_disabled_operations/4

compute_disabled_operations_after_state/5

compute_enabled_operations/4

compute_enabled_operations_after_state/5

compute_enabling_relations/3

Description:
Analysis for the enabling relations: ER(e1,e2) (in case 'pge' is set to 'enabled2', 'disabled2', or 'full2') %%%%%%%%%%

compute_impossible_keep_guaranteed/3

Description:
Analysis for the enabling relations: keep, guaranteed, and impossible (in case 'pge' is set to 'enabled', 'disabled', or 'full') %%%%%%%%%%

compute_operation_relations_for_pge/1

compute_operation_relations_for_pge_if_necessary/2

Description:
PGE Analysis %%%%%%%%%%%%%%%%%

compute_transitions_pge/2

Description:
State Exploration by means of PGE %%%%%%%%%%%%%%%%%%%%%%%

compute_transitions_pge2/2

disabled_operations_stats/1

disables/4

enables/4

explore_current_state_pge/7

explore_current_state_pge1/9

get_disabled_action_by_keep/3

get_enabled_action_by_keep/3

get_first_argument/2

get_goal_predicate/4

get_possible_enabled_trans_names/5

get_possible_enabled_trans_names_aux/4

get_start_predicate/3

is_pge_opt_on/0

is_pge_opt_on/1

my_exit_error_scope/1

not_a_member_of_disabled/2

prove_and_assert_enabling_relation/6

setup_constants_state/1

setup_constants_state1/1

tcltk_disabling_analysis/1

update_disabled_enabled_operations/3

update_disabled_enabled_operations_l/3

Determinacy Checker

Determinacy Checker:

! Existence error in argument 1 of absolute_file_name/3
! file probsrc(bmachine) does not exist
! goal: absolute_file_name(probsrc(bmachine),_261,[access(exist),file_type(source),relative_to('/builds/stups/prob/prolog_doc_gen/prolog-Doc/prob_prolog/src/pge/pge_algo.pl')])

Name: compute_and_update_disabled_enabled_operations/3	Module: pge_algo
Name: list_to_ord_set/2	Module: foo_error
Name: maplist/3	Module: foo_error
Name: ord_union/3	Module: foo_error
Name: explore_current_state_pge/7	Module: pge_algo
Name: get_possible_enabled_trans_names/5	Module: pge_algo

Name: fail
Name: assertz/1
Name: member/2
Name: find_initialised_states/1	Module: state_space
Name: findall/3
Name: b_machine_has_constants_or_properties/0	Module: bmachine
Name: not/1

Name: specfile_trans_timeout/7	Module: ample_sets
Name: add_transition_timeout/5	Module: pge_algo

Name: RECURSIVE_CALL/3	Module: pge_algo
Name: update_disabled_enabled_operations_l/3	Module: pge_algo
Name: compute_enabled_operations/4	Module: pge_algo
Name: compute_disabled_operations/4	Module: pge_algo

Name: debug_println/2	Module: foo_error
Name: prove_and_assert_enabling_relation/6	Module: pge_algo
Name: test_path_non_failing/6	Module: foo_error
Name: =/2
Name: ->/3
Name: conjunct_predicates/2	Module: bsyntaxtree
Name: print_bexpr/1	Module: translate
Name: ==/2
Name: create_negation/2	Module: bsyntaxtree
Name: partition_predicate/4	Module: enabling_analysis
Name: get_negated_guard/3	Module: b_state_model_check
Name: b_get_read_write/3	Module: b_read_write_info

Name: add_transition/4	Module: tcltk_interface
Name: check_timeout_result/4	Module: pge_algo
Name: time_out_with_enum_warning_for_findall/3	Module: error_manager
Name: >/2
Name: ->/3
Name: set_error_context/1	Module: error_manager

Name: true
Name: assert_time_out_for_node/3	Module: state_space
Name: var/1
Name: ->/3
Name: print_message/1	Module: tools
Name: =/2
Name: is_time_out_result/1	Module: error_manager

Name: compute_disabled_operations_after_state/5	Module: pge_algo
Name: =/2
Name: check_only_enabled/1	Module: pge_algo
Name: ->/3
Name: get_preference/2	Module: preferences

Name: list_to_ord_set/2	Module: foo_error
Name: findall/4
Name: findall/3
Name: !
Name: =/2

Name: compute_enabled_operations_after_state/5	Module: pge_algo
Name: =/2
Name: check_only_disabled/1	Module: pge_algo
Name: ->/3
Name: get_preference/2	Module: preferences

Name: fail
Name: compute_cbc_enabling_relation_and_assert/5	Module: pge_algo
Name: debug_println/2	Module: foo_error
Name: assertz/1
Name: ord_intersect/2	Module: foo_error
Name: not/1
Name: ->/3
Name: true
Name: =/2
Name: b_get_operation_read_guard_vars/4	Module: b_read_write_info
Name: b_get_read_write/3	Module: b_read_write_info
Name: b_top_level_operation/1	Module: bmachine
Name: init_or_op/1	Module: foo_error

Name: !
Name: assertz/1
Name: formatsilent/2	Module: foo_error
Name: is/2
Name: debug_println/2	Module: foo_error
Name: cputime/1	Module: tools
Name: assert_disabled_ops_to_init_states_if_necessary/0	Module: pge_algo
Name: add_warning/3	Module: error_manager
Name: call_cleanup/2
Name: member/2
Name: ->/3
Name: get_preference/2	Module: preferences
Name: enter_new_error_scope/1	Module: error_manager
Name: true
Name: pge_predicates_computed	dynamic predicate

Name: compute_operation_relations_for_pge_if_necessary/2	Module: pge_algo
Name: perform_static_analyses_if_necessary2/1	Module: ltl

Name: =/2
Name: nr_skipped_guard_evaluations/1	dynamic predicate
Name: !
Name: animation_mode/1	Module: specfile
Name: is_pge_opt_on/0	Module: pge_algo

Name: true
Name: fail
Name: catch_and_ignore_well_definedness_error/2	Module: foo_error
Name: ->/3
Name: get_goal_predicate/4	Module: pge_algo
Name: get_start_predicate/3	Module: pge_algo

Name: RECURSIVE_CALL/9	Module: pge_algo
Name: reset_temporary_preference/2	Module: preferences
Name: =/2
Name: ->/3
Name: findall/3
Name: temporary_set_preference/3	Module: preferences
Name: debug_println/2	Module: foo_error
Name: assertz/1
Name: is/2
Name: nr_skipped_guard_evaluations/1	dynamic predicate
Name: retract/1
Name: ord_member/2	Module: foo_error

Name: keeps/2	dynamic predicate
Name: member/2
Name: !
Name: animation_mode/1	Module: specfile

Name: get_conj_inv_predicate/3	Module: foo_error
Name: =/2
Name: ->/3
Name: get_negated_guard/3	Module: b_state_model_check

Name: enables/4	Module: pge_algo
Name: disables/4	Module: pge_algo

Name: get_possible_enabled_trans_names_aux/4	Module: pge_algo
Name: =/2
Name: true
Name: disabled_operations/3	dynamic predicate
Name: ->/3

Name: get_specfile_possible_trans_names/5	Module: ample_sets
Name: add_transitions_pge/3	Module: pge_algo

Name: print_enable_table/1	Module: foo_error
Name: findall/3
Name: get_preference/2	Module: preferences

Name: assertz/1
Name: retractall/1
Name: ord_union/3	Module: foo_error
Name: disabled_operations/3	dynamic predicate
Name: ->/3

prob_prolog/src/pge/pge_algo.pl

Modules

Predicates of pge_algo

Module Information

Dynamic Predicates: disables/2 enables/2 keeps/2 enabling_relations/6 pge_predicates_computed/0 disabled_operations/3 nr_skipped_guard_evaluations/1

476 Lines

41 Predicates

Imported Modules: ordsets lists debug module_information

8 Exports

38 specified Imports

Predicates:

Determinacy Checker: