Dynamic Predicates: enable_graph/1 dependent_act/4

518 Lines

29 Predicates

Imported Modules: module_information ordsets ugraphs

14 Exports

26 specified Imports

Imports	Exports
Name: b_top_level_operation/1 Module: bmachine Name: b_get_invariant_from_machine/1 Module: bmachine Name: b_get_properties_from_machine/1 Module: bmachine Name: conjunct_predicates/2 Module: bsyntaxtree Name: get_negated_guard/3 Module: b_state_model_check Name: get_guard/2 Module: b_state_model_check Name: b_get_machine_operation_for_animation/4 Module: bmachine Name: b_get_read_write/3 Module: b_read_write_info Name: b_get_read_write_vars/5 Module: b_read_write_info Name: b_get_operation_read_guard_vars/4 Module: b_read_write_info Name: get_preference/2 Module: preferences Name: real_error_occurred/0 Module: error_manager Name: call_in_fresh_error_scope_for_one_solution/1 Module: error_manager Name: add_internal_error/2 Module: error_manager Name: add_error_fail/3 Module: error_manager Name: wd_error_occured/0 Module: error_manager Name: clear_wd_errors/0 Module: error_manager Name: critical_enumeration_warning_occured_in_error_scope/0 Module: error_manager Name: clear_enumeration_warnings/0 Module: error_manager Name: debug_println/2 Module: debug Name: debug_mode/1 Module: debug Name: debug_format/3 Module: debug Name: formatsilent/2 Module: debug Name: cputime/1 Module: tools Name: silent_mode/1 Module: debug Name: set_silent_mode/1 Module: debug	Name: dependent_actions/5 Name: enable_analysis/6 Name: disable_analysis/5 Name: action_dependent_to_itself/4 Name: tcltk_enabling_analysis/2 Name: compute_dependendency_relation_of_all_events_in_the_model/3 Name: enable_graph/1 Name: dependent_act/4 Name: syntactic_independence/3 Name: get_conj_inv_predicate/3 Name: catch_and_ignore_well_definedness_error/2 Name: test_path_non_failing/6 Name: test_path/6 Name: is_timeout/1

Imports

Exports

Name: b_top_level_operation/1

Module: bmachine

Name: b_get_invariant_from_machine/1

Module: bmachine

Name: b_get_properties_from_machine/1

Module: bmachine

Name: conjunct_predicates/2

Module: bsyntaxtree

Name: get_negated_guard/3

Module: b_state_model_check

Name: get_guard/2

Module: b_state_model_check

Name: b_get_machine_operation_for_animation/4

Module: bmachine

Name: b_get_read_write/3

Module: b_read_write_info

Name: b_get_read_write_vars/5

Module: b_read_write_info

Name: b_get_operation_read_guard_vars/4

Module: b_read_write_info

Name: get_preference/2

Module: preferences

Name: real_error_occurred/0

Module: error_manager

Name: call_in_fresh_error_scope_for_one_solution/1

Module: error_manager

Name: add_internal_error/2

Module: error_manager

Name: add_error_fail/3

Module: error_manager

Name: wd_error_occured/0

Module: error_manager

Name: clear_wd_errors/0

Module: error_manager

Name: critical_enumeration_warning_occured_in_error_scope/0

Module: error_manager

Name: clear_enumeration_warnings/0

Module: error_manager

Name: debug_println/2

Module: debug

Name: debug_mode/1

Module: debug

Name: debug_format/3

Module: debug

Name: formatsilent/2

Module: debug

Name: cputime/1

Module: tools

Name: silent_mode/1

Module: debug

Name: set_silent_mode/1

Module: debug

Name: dependent_actions/5

Name: enable_analysis/6

Name: disable_analysis/5

Name: action_dependent_to_itself/4

Name: tcltk_enabling_analysis/2

Name: compute_dependendency_relation_of_all_events_in_the_model/3

Name: enable_graph/1

Name: dependent_act/4

Name: syntactic_independence/3

Name: get_conj_inv_predicate/3

Name: catch_and_ignore_well_definedness_error/2

Name: test_path_non_failing/6

Name: test_path/6

Name: is_timeout/1

action_dependent_to_itself/4

catch_and_ignore_well_definedness_error/2

Meta: catch_and_ignore_well_definedness_error(0,*)

catch_and_ignore_well_definedness_error/3

Meta: catch_and_ignore_well_definedness_error(*,0,*)

catch_enumeration_warning/2

Meta: catch_enumeration_warning(0,0)

check_if_coenabled/4

check_if_coenabled_nonfailing/5

check_result/3

cleanup_enum_and_wd/2

compute_dependendency_relation_of_all_events_in_the_model/3

Description:
suitable_for_por(EnGraph,Result) :-
(not_all_reachable(EnGraph) ->
Result=true
; Result=false
).
not_all_reachable(EnGraph) :-
ample_sets: vertices(EnGraph,Vertices),
member(V,Vertices),
\+ (ample_sets: reachable(V,EnGraph,Reachable),Reachable=Vertices).
DEPENDENCY RELATION (BEGIN)

dependent_actions/5

dependent_actions1/5

dependent_actions_coenabled/6

dependent_actions_symm/6

Description:
Act1 and Act2 are enabled in current state State,
we don't have to check if both actions are enabled in
some state

determine_dependency_enabling_relations/6

determine_dependency_enabling_relations/7

determine_dependency_enabling_relations1/7

disable_analysis/5

enable_analysis/6

get_conj_inv_predicate/3

get_dependency_enabling_predicate/9

get_dependency_status/2

get_enabling_result/6

is_timeout/1

Description:
:- use_module(library(lists)).
:- use_module(probsrc(self_check)).

may_enable/7

syntactic_independence/3

tcltk_enabling_analysis/2

Description:
compute_dependendency_relation_of_all_events_in_the_model(1,por(ample_sets,0,0,0),EnableGraph),
suitable_for_por(EnableGraph,POR),

test_enabledness_condition/9

Description:
get_conj_inv_predicate([PosGuard1,PosGuard2],FindInvViolations,GuardsConj),

test_path/6

Description:
pred(P) - adds P to invariant
typing(P) - just use typing from invariant and add P

test_path_non_failing/6

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),_6523,[access(exist),file_type(source),relative_to('/builds/stups/prob/prolog_doc_gen/prolog-Doc/prob_prolog/src/por/static_analysis.pl')])
! 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/por/static_analysis.pl')])

Name: =/2
Name: ->/3
Name: ord_intersect/2	Module: foo_error
Name: not/1
Name: >/2
Name: length/2
Name: b_get_machine_operation_for_animation/4	Module: bmachine

Name: =/2
Name: check_if_coenabled/4	Module: static_analysis
Name: ->/3

Name: get_dependency_status/2	Module: static_analysis
Name: fail
Name: ==/2
Name: ->/3
Name: RECURSIVE_CALL/5	Module: static_analysis
Name: dependent_actions1/5	Module: static_analysis

Name: =/2
Name: test_enabledness_condition/9	Module: static_analysis
Name: get_dependency_enabling_predicate/9	Module: static_analysis
Name: get_preference/2	Module: preferences
Name: ->/3
Name: ord_intersect/2	Module: foo_error
Name: not/1
Name: b_get_read_write_vars/5	Module: b_read_write_info
Name: @</2
Name: action_dependent_to_itself/4	Module: static_analysis
Name: b_top_level_operation/1	Module: bmachine

Name: dependent_actions/5	Module: static_analysis
Name: dependent_actions_coenabled/6	Module: static_analysis

Name: cleanup_enum_and_wd/2	Module: static_analysis
Name: =/2
Name: real_error_occurred/0	Module: error_manager
Name: ->/3
Name: call_cleanup/2
Name: set_silent_mode/1	Module: debug
Name: silent_mode/1	Module: debug

Name: testcase_predicate_timeout/3	Module: foo_error
Name: =/2
Name: ->/3
Name: conjunct_predicates/2	Module: bsyntaxtree
Name: get_guard/2	Module: b_state_model_check

Name: true
Name: clear_wd_errors/0	Module: error_manager
Name: formatsilent/2	Module: debug
Name: wd_error_occured/0	Module: error_manager
Name: ->/3
Name: clear_enumeration_warnings/0	Module: error_manager
Name: critical_enumeration_warning_occured_in_error_scope/0	Module: error_manager

Name: debug_println/2	Module: debug
Name: assertz/1
Name: debug_format/3	Module: debug
Name: is/2
Name: cputime/1	Module: tools
Name: call_in_fresh_error_scope_for_one_solution/1	Module: error_manager
Name: get_preference/2	Module: preferences
Name: retractall/1
Name: sort/2
Name: findall/3
Name: true
Name: enable_graph/1	dynamic predicate
Name: ->/3

Name: check_if_coenabled_nonfailing/5	Module: static_analysis
Name: get_dependency_status/2	Module: static_analysis
Name: fail
Name: ==/2
Name: ->/3
Name: RECURSIVE_CALL/6	Module: static_analysis
Name: dependent_actions1/5	Module: static_analysis

Name: vertices_edges_to_ugraph/3	Module: foo_error
Name: vertices_edges_predicates_to_egraph/3	Module: enable_graph
Name: =/2
Name: ->/3
Name: determine_dependency_enabling_relations/7	Module: static_analysis

Name: RECURSIVE_CALL/7	Module: static_analysis
Name: append/3
Name: determine_dependency_enabling_relations1/7	Module: static_analysis

Name: =/2
Name: get_enabling_result/6	Module: static_analysis
Name: test_path/6	Module: static_analysis
Name: ord_intersect/2	Module: foo_error
Name: ->/3
Name: conjunct_predicates/2	Module: bsyntaxtree
Name: get_guard/2	Module: b_state_model_check
Name: get_preference/2	Module: preferences
Name: get_negated_guard/3	Module: b_state_model_check
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: ==/2
Name: b_top_level_operation/1	Module: bmachine

Name: true
Name: nl
Name: print/1
Name: print_bexpr/1	Module: translate
Name: debug_mode/1	Module: debug
Name: =/2
Name: ->/3
Name: compute_enabling_predicate/5	Module: foo_error
Name: test_path/6	Module: static_analysis
Name: ord_intersect/2	Module: foo_error
Name: conjunct_predicates/2	Module: bsyntaxtree
Name: get_negated_guard/3	Module: b_state_model_check

Name: get_enabling_result/6	Module: static_analysis
Name: may_enable/7	Module: static_analysis
Name: disable_analysis/5	Module: static_analysis

Name: check_result/3	Module: static_analysis
Name: catch_and_ignore_well_definedness_error/3	Module: static_analysis
Name: =/2
Name: get_conj_inv_predicate/3	Module: static_analysis
Name: ->/3

prob_prolog/src/por/static_analysis.pl

Modules

Predicates of static_analysis

Module Information

Dynamic Predicates: enable_graph/1 dependent_act/4

518 Lines

29 Predicates

Imported Modules: module_information ordsets ugraphs

14 Exports

26 specified Imports

Predicates:

Determinacy Checker: