Dynamic Predicates: ltl_formula_cache/2 ltl_counter_examples_cache/4

820 Lines

74 Predicates

Imported Modules: lists ordsets tools translate debug error_manager ltlc/ltlc

19 Exports

37 specified Imports

Imports	Exports
Name: get_texpr_expr/2 Module: bsyntaxtree Name: get_texpr_pos/2 Module: bsyntaxtree Name: predicate_identifiers/2 Module: bsyntaxtree Name: b_definition_prefixed/5 Module: bmachine Name: b_get_typed_definition/3 Module: bmachine Name: b_top_level_operation/1 Module: bmachine Name: filter_formulas_from_pragmas/3 Module: haskell_csp Name: print_error/1 Module: tools_printing Name: get_preference/2 Module: preferences Name: animation_mode/1 Module: specfile Name: set_max_nr_of_new_impl_trans_nodes/1 Module: state_space Name: current_state_id/1 Module: state_space Name: visited_expression/2 Module: state_space Name: visited_expression_id/1 Module: state_space Name: transition/4 Module: state_space Name: impl_trans_term_all/2 Module: state_space Name: state_space_reset/0 Module: state_space Name: execute_id_trace_from_current/3 Module: state_space Name: set_context_state/1 Module: state_space Name: clear_context_state/0 Module: state_space Name: state_space_initialise/0 Module: state_space Name: find_trace_to_initial_state/2 Module: state_space Name: find_initialised_states/1 Module: state_space Name: not_all_transitions_added/1 Module: state_space Name: reset_counterexample/0 Module: state_space Name: add_counterexample_node/1 Module: state_space Name: add_counterexample_op/1 Module: state_space Name: depth_breadth_first_mode/1 Module: state_space_exploration_modes Name: set_depth_breadth_first_mode/1 Module: state_space_exploration_modes 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: module_info/2 Module: module_information Name: get_preference/2 Module: preferences Name: minimize_lasso/4 Module: tools Name: register_event_listener/3 Module: eventhandling Name: catch_interrupt_assertion_call/1 Module: user_interrupts Name: user_interruptable_call_det/2 Module: user_signal/user_signal	Name: ltl_model_check/4 Name: ltl_model_check2/4 Name: ltl_model_check_ast/5 Name: ltl_check_assertions/2 Name: parse_ltlfile/2 Name: ltl_model_check_with_ce/4 Name: ltl_model_check_with_ce1/5 Name: parse_and_pp_ltl_formula/2 Name: ltl_formula_structure/3 Name: pp_ltl_formula/2 Name: preprocess_formula/2 Name: find_atomic_property_formula/2 Name: executetrace/1 Name: set_trace_to_init/1 Name: parse_and_preprocess_formula/3 Name: is_fairness_implication/1 Name: tcltk_play_ltl_counterexample/2 Name: get_ltl_formula_strings/2 Name: get_ltl_formulas/3

Imports

Exports

Name: get_texpr_expr/2

Module: bsyntaxtree

Name: get_texpr_pos/2

Module: bsyntaxtree

Name: predicate_identifiers/2

Module: bsyntaxtree

Name: b_definition_prefixed/5

Module: bmachine

Name: b_get_typed_definition/3

Module: bmachine

Name: b_top_level_operation/1

Module: bmachine

Name: filter_formulas_from_pragmas/3

Module: haskell_csp

Name: print_error/1

Module: tools_printing

Name: get_preference/2

Module: preferences

Name: animation_mode/1

Module: specfile

Name: set_max_nr_of_new_impl_trans_nodes/1

Module: state_space

Name: current_state_id/1

Module: state_space

Name: visited_expression/2

Module: state_space

Name: visited_expression_id/1

Module: state_space

Name: transition/4

Module: state_space

Name: impl_trans_term_all/2

Module: state_space

Name: state_space_reset/0

Module: state_space

Name: execute_id_trace_from_current/3

Module: state_space

Name: set_context_state/1

Module: state_space

Name: clear_context_state/0

Module: state_space

Name: state_space_initialise/0

Module: state_space

Name: find_trace_to_initial_state/2

Module: state_space

Name: find_initialised_states/1

Module: state_space

Name: not_all_transitions_added/1

Module: state_space

Name: reset_counterexample/0

Module: state_space

Name: add_counterexample_node/1

Module: state_space

Name: add_counterexample_op/1

Module: state_space

Name: depth_breadth_first_mode/1

Module: state_space_exploration_modes

Name: set_depth_breadth_first_mode/1

Module: state_space_exploration_modes

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: module_info/2

Module: module_information

Name: get_preference/2

Module: preferences

Name: minimize_lasso/4

Module: tools

Name: register_event_listener/3

Module: eventhandling

Name: catch_interrupt_assertion_call/1

Module: user_interrupts

Name: user_interruptable_call_det/2

Module: user_signal/user_signal

Name: ltl_model_check/4

Name: ltl_model_check2/4

Name: ltl_model_check_ast/5

Name: ltl_check_assertions/2

Name: parse_ltlfile/2

Name: ltl_model_check_with_ce/4

Name: ltl_model_check_with_ce1/5

Name: parse_and_pp_ltl_formula/2

Name: ltl_formula_structure/3

Name: pp_ltl_formula/2

Name: preprocess_formula/2

Name: find_atomic_property_formula/2

Name: executetrace/1

Name: set_trace_to_init/1

Name: parse_and_preprocess_formula/3

Name: is_fairness_implication/1

Name: tcltk_play_ltl_counterexample/2

Name: get_ltl_formula_strings/2

Name: get_ltl_formulas/3

Predicates

Predicates:

assert_all_visible_stutter_actions/2

assert_stutter_action/1

assert_visible_action/1

call_c_initialisation/0

call_ltl_fairness_verification/3

call_ltl_fairness_verification1/4

call_ltl_fairness_verification2/5

call_ltl_fairness_verification3/5

call_ltl_verification/2

call_ltl_verification2/3

cltl_callback_reexplore/5

convert_atom_to_statetransition/2

convert_counterexample/3

convert_counterexample_to_action_trace/5

convert_result/3

executetrace/1

extract_expectations/2

find_atomic_property_formula/2

find_operation_ids/3

get_actions_modifying_variables/3

get_all_already_explored_transitions/2

get_ltl_def_formula_strings/2

get_ltl_formula_string/2

get_ltl_formula_strings/2

get_ltl_formulas/3

get_operation_name/2

get_stutter_visible_actions/4

impl_trans_term_all1/2

impl_trans_term_rest/2

interruptable_ltl_model_check_ast/4

is_fairness_implication/1

look_up_for_visible_actions/4

look_up_for_visible_actions1/4

look_up_for_visible_actions_args/5

ltl_check_assertions/2

ltl_check_assertions2/6

ltl_formula_structure/3

ltl_model_check_ast/5

ltl_model_check_core/5

ltl_model_check_with_ce/4

ltl_model_check_with_ce1/5

ltl_model_check_with_ce2/5

minmize_model_lasso/2

parse_and_preprocess_formula/3

perform_static_analyses_if_necessary/1

perform_static_analyses_if_necessary2/1

pp_ltl_counterexample/3

prepare_ltl_model_checker_for_por/1

reset_ltl/0

safety_mc_not_possible/2

select_ltl_mode/4

set_trace_to_init/1

tcltk_play_ltl_counterexample/2

translate_ctrace/4

translate_ctrace2/5

translate_trace/4

variable_modified_by_action/3

assert_all_visible_stutter_actions/2

assert_stutter_action/1

assert_visible_action/1

call_c_initialisation/0

call_ltl_fairness_verification/3

call_ltl_fairness_verification1/4

call_ltl_fairness_verification2/5

call_ltl_fairness_verification3/5

call_ltl_verification/2

call_ltl_verification2/3

cltl_callback_reexplore/5

convert_atom_to_statetransition/2

convert_counterexample/3

convert_counterexample_to_action_trace/5

convert_result/3

executetrace/1

Description:
unparsed_ap(ap(P),ap(P)) --> !.
unparsed_ap(action(unparsed_b(OpName/Arity/Types,Exprs)),action(b(OpName/Arity,Es))) --> !,
add_unparsed_exprs(Exprs,Types,Es).
unparsed_ap(action(b(OpName/Arity/_Types)),action(b(OpName/Arity))) --> !.
unparsed_ap(action(Op),action(Op)) --> !.
unparsed_ap(unparsed(Unparsed),ap(P)) --> !,[pred(Unparsed,P)].
unparsed_ap(F,N) --> {F =..[Functor|Args]},unparsed_ap_l(Args,NArgs),{N=..[Functor|NArgs]}.
unparsed_ap_l([],[]) --> [].
unparsed_ap_l([F|Rest],[N|NRest]) --> unparsed_ap(F,N), unparsed_ap_l(Rest,NRest).
add_unparsed_exprs([],[],[]) --> [].
add_unparsed_exprs([expr(P,U)|UR],[T|TR],[expr(P,E)|ER]) -->
[expr(U,T,E)], add_unparsed_exprs(UR,TR,ER).

extract_expectations/2

find_atomic_property_formula/2

find_operation_ids/3

get_actions_modifying_variables/3

get_all_already_explored_transitions/2

get_ltl_def_formula_strings/2

get_ltl_formula_string/2

get_ltl_formula_strings/2

get_ltl_formulas/3

get_operation_name/2

get_stutter_visible_actions/4

impl_trans_term_all1/2

impl_trans_term_rest/2

interruptable_ltl_model_check_ast/4

is_fairness_implication/1

look_up_for_visible_actions/4

look_up_for_visible_actions1/4

Description:
in case of [evt], 'evt' will be recognised as visible

look_up_for_visible_actions_args/5

ltl_check_assertions/2

ltl_check_assertions2/6

ltl_formula_structure/3

ltl_model_check_ast/5

ltl_model_check_core/5

ltl_model_check_with_ce/4

ltl_model_check_with_ce1/5

ltl_model_check_with_ce2/5

minmize_model_lasso/2

parse_and_preprocess_formula/3

Description:
reset_ltl/0,

perform_static_analyses_if_necessary/1

perform_static_analyses_if_necessary2/1

pp_ltl_counterexample/3

prepare_ltl_model_checker_for_por/1

Description:
Predicates for determining which actions are visible and which are stutter in regard to the given LTL formula.
An operation Op in a B machine should be identified as visible for a given LTL formula f, if Op writes variables used
in the predicates in f or writes variables read in guard of operations inside the e(-) atoms in f.
In case the respective LTL formula f contains a X (next) operator then M_{POR} |= f and M |= f are not equivalent.
It is not clear how to handle LTL formulae containing transition propositions ([-]). (investigate e.g. LTL formulae of the form: ([Op] => g))

reset_ltl/0

safety_mc_not_possible/2

select_ltl_mode/4

set_trace_to_init/1

tcltk_play_ltl_counterexample/2

translate_ctrace/4

translate_ctrace2/5

translate_trace/4

variable_modified_by_action/3

Determinacy Checker

Determinacy Checker:

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

Name: fail
Name: add_error/2	Module: foo_error
Name: !
Name: ltlc_init	Module: foo_error

Name: call_ltl_fairness_verification1/4	Module: ltl
Name: maplist/3	Module: foo_error
Name: !

Name: add_error/3	Module: foo_error
Name: nl
Name: print/1
Name: true
Name: =/2
Name: ->/3
Name: call_ltl_fairness_verification2/5	Module: ltl
Name: RECURSIVE_CALL/4	Module: ltl
Name: get_fairness_specification/3	Module: foo_error
Name: !

Name: =/2
Name: ->/2
Name: ->/3
Name: RECURSIVE_CALL/5	Module: ltl
Name: call_ltl_fairness_verification3/5	Module: ltl

Name: add_error_fail/3	Module: foo_error
Name: =/2
Name: ->/3
Name: RECURSIVE_CALL/5	Module: ltl
Name: evaluate_ltl_fairness/6	Module: foo_error

Name: ce_result_initpath/2	Module: ltl
Name: convert_result/3	Module: ltl
Name: tcltk_play_ltl_counterexample/2	Module: ltl

Name: find_operation_ids/3	Module: ltl
Name: find_trace_to_initial_state/2	Module: state_space
Name: ce_get_first_state/2	Module: ltl

Name: RECURSIVE_CALL/3	Module: ltl
Name: =/2
Name: !
Name: check_ap/2	Module: foo_error
Name: ->/3

Name: cltl_callback/5	Module: ltl
Name: cltl_callback_reexplore/5	Module: ltl

Name: RECURSIVE_CALL/4	Module: ltl
Name: check_tps2/5	Module: ltl

Name: check_tps/4	Module: ltl
Name: impl_trans_term_all1/2	Module: ltl
Name: check_aps/3	Module: ltl

Name: debug_println/2	Module: foo_error
Name: check_tps/4	Module: ltl
Name: impl_trans_term_rest/2	Module: ltl
Name: check_aps/3	Module: ltl

Name: fail
Name: add_internal_error/2	Module: foo_error
Name: execute_id_trace_from_current/3	Module: state_space
Name: true
Name: set_trace_to_init/1	Module: ltl
Name: =/2
Name: ->/3
Name: ce_get_first_state/2	Module: ltl
Name: translate_ctrace/4	Module: ltl
Name: !

Name: convert_counterexample_to_action_trace/5	Module: ltl
Name: ltl_model_check2/4	Module: ltl

Name: ctl_model_check2/4	Module: ctl
Name: tcltk_play_ctl_counterexample/2	Module: ctl
Name: set_trace_to_init/1	Module: ltl

Name: RECURSIVE_CALL/2	Module: ltl
Name: =/2
Name: append/3
Name: atom_codes/2
Name: atom/1
Name: ->/3

Name: check_atomic_property_formula/2	Module: foo_error
Name: visited_expression_id/1	Module: state_space
Name: parse_and_preprocess_formula/3	Module: ltl

Name: append/2	Module: foo_error
Name: maplist/3	Module: foo_error

Name: fail
Name: add_all_perrors/1	Module: foo_error
Name: get_texpr_pos/2	Module: bsyntaxtree
Name: ->/2
Name: true
Name: get_texpr_expr/2	Module: bsyntaxtree
Name: ->/3
Name: b_get_typed_definition/3	Module: bmachine
Name: b_definition_prefixed/5	Module: bmachine

Name: assertz/1
Name: temporal_parser_l/3	Module: foo_error
Name: retractall/1
Name: true
Name: ltl_formula_cache/2	dynamic predicate
Name: ->/3
Name: get_ltl_formula_strings/2	Module: ltl

Name: add_error_fail/3	Module: foo_error
Name: translate_event/2	Module: foo_error
Name: transition/4	Module: state_space
Name: ->/3
Name: =/2

Name: ord_subtract/3	Module: foo_error
Name: list_to_ord_set/2	Module: foo_error
Name: look_up_for_visible_actions/4	Module: ltl
Name: findall/3

Name: findall/3
Name: compute_transitions_if_necessary_saved/1	Module: state_space
Name: get_all_already_explored_transitions/2	Module: ltl

Name: =/2
Name: ->/3
Name: look_up_for_visible_actions1/4	Module: ltl

Name: append/2	Module: foo_error
Name: look_up_for_visible_actions_args/5	Module: ltl
Name: functor/3
Name: !
Name: compound/1
Name: atomic/1
Name: RECURSIVE_CALL/4	Module: ltl
Name: get_actions_modifying_variables/3	Module: ltl
Name: list_to_ord_set/2	Module: foo_error
Name: b_get_operation_read_guard_vars/4	Module: b_read_write_info
Name: predicate_identifiers/2	Module: bsyntaxtree

prob_prolog/src/ltl/ltl.pl

Modules

Predicates of ltl

Module Information

Dynamic Predicates: ltl_formula_cache/2 ltl_counter_examples_cache/4

820 Lines

74 Predicates

Imported Modules: lists ordsets tools translate debug error_manager ltlc/ltlc

19 Exports

37 specified Imports

Predicates:

Determinacy Checker:

Name: RECURSIVE_CALL/5	Module: ltl
Name: is/2
Name: =/2
Name: look_up_for_visible_actions1/4	Module: ltl
Name: arg/3
Name: !
Name: >/2

Name: merge_outcomes/2	Module: ltl
Name: ltl_check_assertions2/6	Module: ltl
Name: extract_expectations/2	Module: ltl
Name: get_ltl_formulas/3	Module: ltl

Name: RECURSIVE_CALL/6	Module: ltl
Name: =/2
Name: add_error/3	Module: foo_error
Name: add_error/2	Module: foo_error
Name: ->/3
Name: print/1
Name: catch/3
Name: flush_output/1
Name: nl

Name: ltl_structure/3	Module: ltl
Name: pp_formulas/2	Module: foo_error
Name: c_ltl_aptp/2	Module: foo_error

Name: ltl_mc_safety_property/3	Module: foo_error
Name: =/2
Name: debug_println/2	Module: foo_error
Name: ltl_model_check5/5	Module: ltl
Name: call_c_initialisation/0	Module: ltl
Name: safety_mc_not_possible/2	Module: ltl
Name: ->/3

Name: ltl_model_check_core/5	Module: ltl
Name: print_message/1	Module: foo_error
Name: set_depth_breadth_first_mode/1	Module: state_space_exploration_modes
Name: format/2
Name: debug_println/2	Module: foo_error
Name: is/2
Name: statistics/2
Name: explore_state_space/5	Module: foo_error
Name: depth_breadth_first_mode/1	Module: state_space_exploration_modes
Name: !
Name: get_preference/2	Module: preferences

Name: debug_println/2	Module: foo_error
Name: minmize_model_lasso/2	Module: ltl
Name: call_ltl_fairness_verification/3	Module: ltl
Name: call_ltl_verification/2	Module: ltl
Name: ltl_model_check4/7	Module: ltl
Name: preprocess_formula/2	Module: foo_error
Name: select_ltl_mode/4	Module: ltl
Name: initialise_fairness_assumptions/4	Module: foo_error
Name: set_max_nr_of_new_impl_trans_nodes/1	Module: state_space
Name: perform_static_analyses_if_necessary/1	Module: ltl

Name: c_ltl_modelcheck/4	Module: foo_error
Name: c_ltl_modelcheck/9	Module: foo_error
Name: fairness_check_on/2	Module: foo_error
Name: ->/3

Name: ce_result/4	Module: ltl
Name: ltl_model_check_ast/5	Module: ltl

Name: ltl_model_check_with_ce2/5	Module: ltl
Name: debug_println/2	Module: foo_error
Name: add_error_fail/3	Module: foo_error
Name: true
Name: temporal_parser/3	Module: foo_error
Name: ->/3