Imports | Exports |
---|---|
Name: add_error_fail/3 Module: error_manager Name: add_error/3 Module: error_manager Name: add_warning/2 Module: error_manager Name: add_error_and_fail/2 Module: error_manager Name: add_error/2 Module: error_manager Name: add_warning/3 Module: error_manager Name: animation_mode/1 Module: specfile Name: debug_println/2 Module: debug Name: formatsilent/2 Module: debug Name: cputime/1 Module: tools Name: is_truth/1 Module: bsyntaxtree Name: visited_expression_id/1 Module: state_space Name: transition/4 Module: state_space Name: visited_expression/2 Module: state_space Name: not_all_transitions_added/1 Module: state_space Name: retract_open_node/1 Module: state_space Name: set_context_state/1 Module: state_space Name: clear_context_state/0 Module: state_space Name: module_info/2 Module: module_information Name: get_model_check_stats/6 Module: model_checker Name: check_enabled/2 Module: ltl_propositions | Name: start_mc_safety_property/3 |
Description:
synchronising the automaton transitions with the successor states of the model
for transition predicates (like [Event]) the ActionId will be instantiated, and the BA property relies on the Action to be taken next
if the ActionId remains a variable, then the property only depends on the state (like, {Pred} )
Description:
for getting the result from LTL Safety Model Check
Description:
getting the initial states with respect to the the safety property
Description:
CEPath = [atom(CurId,CurId,none)],
Description:
state space exploration modules
:- use_module(probsrc(state_space_open_nodes), [retract_open_node_direct/1]).
ltl modules
library modules
profiler modules
:- use_module('../../extensions/profiler/profiler.pl').
:- use_module('../../extensions/profiler/profiler_te.pl').
:- enable_profiling(add_state_at_end/3).
:- enable_profiling(pop_state_from_end/1).
:- enable_profiling(check_for_aut_transition/4).
:- enable_profiling(compute_all_product_transitions/4).
perform_static_analyses(MODE,Optimizations),