Index

Symbols

--ctl command line option --do_not_trim command line option --generate command line option --insert_only command line option --invar command line option --keep_last_stage command line option --ltl command line option --max_iter command line option --no_checks command line option --no_var_print command line option

--nuxmv_path command line option --on_sides command line option --overwrite command line option --py_tree_print command line option --record_times command line option --recursion_limit command line option --serene_print command line option --simulate command line option --use_encoding command line option

A

action_nodes (behaverify.agent_expander.ExpandedModel attribute) agent_types (behaverify.agent_expander.ExpandedModel attribute) arg_parser (in module behaverify.counter_trace) (in module behaverify.dsl_to_cpp) (in module behaverify.dsl_to_haskell) (in module behaverify.dsl_to_latex) (in module behaverify.dsl_to_nuxmv) (in module behaverify.dsl_to_python) (in module create_c_monitor) (in module create_dsl_monitor) (in module create_python_monitor)

argmax() (in module behaverify.behaverify_common)

B

behaverify module behaverify.agent_expander module behaverify.behaverify module behaverify.behaverify_common module behaverify.behaverify_to_smv module behaverify.check_grammar module behaverify.counter_trace module behaverify.dsl_to_cpp module behaverify.dsl_to_haskell module behaverify.dsl_to_latex module

behaverify.dsl_to_nuxmv module behaverify.dsl_to_python module behaverify.meta_functions module behaverify.meta_functions_neural module behaverify.model_to_dsl module behaverify.node_creator module blackboard body_text (behaverify.agent_expander.ExpandedSpec attribute) BT BT.CPP BTreeException build_meta_func() (in module behaverify.meta_functions) (in module behaverify.meta_functions_neural)

C

check_nodes (behaverify.agent_expander.ExpandedModel attribute) CHILD_TRACK_STRING (in module behaverify.behaverify_to_smv) children (behaverify.agent_expander.ExpandedTreeNode attribute) COLORS (in module behaverify.counter_trace) command line option --ctl --do_not_trim --generate --insert_only --invar --keep_last_stage --ltl --max_iter --no_checks --no_var_print --nuxmv_path --on_sides --overwrite --py_tree_print --record_times --recursion_limit --serene_print --simulate --use_encoding common_string_composite() (in module behaverify.node_creator) common_string_decorator() (in module behaverify.node_creator) condition_text (behaverify.agent_expander.ExpandedCheck attribute) configuration_text (behaverify.agent_expander.ExpandedModel attribute) constant_type() (in module behaverify.behaverify_common) constants_text (behaverify.agent_expander.ExpandedModel attribute) counter_trace() (in module behaverify.counter_trace) create_array_index() (in module create_dsl_monitor) create_assign_value() (in module create_dsl_monitor) create_blackboard() (in module behaverify.node_creator) create_blank_variable_obj() (in module create_dsl_monitor) create_c_monitor module create_composite_parallel_success_on_all_with_partial_memory() (in module behaverify.node_creator) create_composite_parallel_success_on_all_without_memory() (in module behaverify.node_creator)

create_composite_parallel_success_on_one_without_memory() (in module behaverify.node_creator) create_composite_selector_with_partial_memory() (in module behaverify.node_creator) create_composite_selector_without_memory() (in module behaverify.node_creator) create_composite_sequence_with_partial_memory() (in module behaverify.node_creator) create_composite_sequence_without_memory() (in module behaverify.node_creator) create_constant() (in module create_dsl_monitor) create_decorator_inverter() (in module behaverify.node_creator) create_decorator_one_shot() (in module behaverify.node_creator) create_decorator_repeat() (in module behaverify.node_creator) create_decorator_X_is_Y() (in module behaverify.node_creator) create_dot_from_BehaVerify_json() (in module behaverify.counter_trace) create_dsl_monitor module create_iterative_assign() (in module create_dsl_monitor) create_lambda_to_apply_function() (in module behaverify.meta_functions) (in module behaverify.meta_functions_neural) create_local_root_to_relevant_list_map() (in module behaverify.behaverify_common) create_loop_array() (in module create_dsl_monitor) create_ltl2ba_command() (in module create_c_monitor) (in module create_dsl_monitor) (in module create_python_monitor) create_names_module() (in module behaverify.node_creator) create_node_name() (in module behaverify.behaverify_common) create_node_template() (in module behaverify.behaverify_common) create_node_to_descendants_map() (in module behaverify.behaverify_common) create_node_to_local_root_map() (in module behaverify.behaverify_common) create_nodes() (in module behaverify.behaverify_to_smv) create_python_monitor module create_result() (in module create_dsl_monitor) create_resume_point() (in module behaverify.behaverify_to_smv) create_resume_structure() (in module behaverify.behaverify_to_smv) create_status_module() (in module behaverify.node_creator) create_variable_obj_p() (in module create_dsl_monitor) create_variable_obj_states() (in module create_dsl_monitor) create_variable_statement() (in module create_dsl_monitor) create_variable_statement_iterative() (in module create_dsl_monitor) create_variable_template() (in module behaverify.behaverify_common) CTL

D

domain_text (behaverify.agent_expander.ExpandedVariable attribute) dsl_to_cpp() (in module behaverify.dsl_to_cpp) dsl_to_haskell() (in module behaverify.dsl_to_haskell)

dsl_to_latex() (in module behaverify.dsl_to_latex) dsl_to_nuxmv() (in module behaverify.dsl_to_nuxmv) dsl_to_python() (in module behaverify.dsl_to_python) dummy_value() (in module behaverify.behaverify_common)

E

enumerations (behaverify.agent_expander.ExpandedModel attribute) environment_checks (behaverify.agent_expander.ExpandedModel attribute) environment_update_text (behaverify.agent_expander.ExpandedModel attribute) error_exit() (in module behaverify.behaverify) expand_agents() (in module behaverify.agent_expander) ExpandedAction (class in behaverify.agent_expander)

ExpandedCheck (class in behaverify.agent_expander) ExpandedModel (class in behaverify.agent_expander) ExpandedSpec (class in behaverify.agent_expander) ExpandedTreeNode (class in behaverify.agent_expander) ExpandedVariable (class in behaverify.agent_expander) extract_brace_content() (in module behaverify.behaverify)

F

fast-forwarding encoding fix_name() (in module behaverify.counter_trace)

format_node_type() (in module behaverify.behaverify_common) FUNCTIONS (in module behaverify.meta_functions) (in module behaverify.meta_functions_neural)

G

get_metamodel_file() (in module behaverify.behaverify) get_min_max() (in module behaverify.behaverify_common)

get_right_sibling() (in module behaverify.behaverify_common) get_root_from_BehaVerify_json() (in module behaverify.counter_trace) get_root_node() (in module behaverify.behaverify_common)

H

handle_constant_or_reference() (in module behaverify.behaverify_common) handle_constant_or_reference_meta() (in module behaverify.meta_functions) (in module behaverify.meta_functions_neural) handle_constant_or_reference_no_type() (in module behaverify.behaverify_common)

handle_files_at_location() (in module create_dsl_monitor) handle_index() (in module behaverify.meta_functions) (in module behaverify.meta_functions_neural) handle_smv() (in module behaverify.counter_trace) haskell_indent() (in module behaverify.behaverify_common)

I

indent() (in module behaverify.behaverify_common) (in module behaverify.dsl_to_latex) initial_text (behaverify.agent_expander.ExpandedVariable attribute) initial_value (behaverify.agent_expander.ExpandedVariable attribute) INVARSPEC

is_array() (in module behaverify.behaverify_common) is_blackboard() (in module behaverify.behaverify_common) is_env() (in module behaverify.behaverify_common) is_local() (in module behaverify.behaverify_common) is_neural() (in module behaverify.behaverify_common)

L

leaf node leaf_name (behaverify.agent_expander.ExpandedTreeNode attribute)

LOCAL_ROOT_TREE_STRING (in module behaverify.behaverify_to_smv) LTL

M

main() (in module behaverify.behaverify) (in module behaverify.behaverify_to_smv) map_node_name_to_number() (in module behaverify.behaverify_common) maybe_expand() (in module behaverify.agent_expander) message (behaverify.behaverify_common.BTreeException attribute) meta_case_loop() (in module behaverify.meta_functions) (in module behaverify.meta_functions_neural) meta_if() (in module behaverify.meta_functions) (in module behaverify.meta_functions_neural) meta_loop() (in module behaverify.meta_functions) (in module behaverify.meta_functions_neural) model_to_dsl() (in module behaverify.model_to_dsl) model_to_tree_text() (in module behaverify.agent_expander) module behaverify behaverify.agent_expander behaverify.behaverify behaverify.behaverify_common behaverify.behaverify_to_smv behaverify.check_grammar behaverify.counter_trace behaverify.dsl_to_cpp behaverify.dsl_to_haskell behaverify.dsl_to_latex behaverify.dsl_to_nuxmv behaverify.dsl_to_python behaverify.meta_functions behaverify.meta_functions_neural behaverify.model_to_dsl behaverify.node_creator create_c_monitor create_dsl_monitor create_python_monitor

monitor

N

name (behaverify.agent_expander.ExpandedAction attribute) (behaverify.agent_expander.ExpandedCheck attribute) (behaverify.agent_expander.ExpandedTreeNode attribute) (behaverify.agent_expander.ExpandedVariable attribute)

node_type (behaverify.agent_expander.ExpandedTreeNode attribute) nuXmv

O

ONNX ONNX_IMPORTED (in module behaverify.check_grammar), [1] (in module behaverify.dsl_to_cpp), [1] (in module behaverify.dsl_to_nuxmv), [1] (in module behaverify.dsl_to_python), [1]

order_nodes() (in module behaverify.behaverify_common)

P

parallel_policy (behaverify.agent_expander.ExpandedTreeNode attribute) PARALLEL_SKIP_STRING (in module behaverify.behaverify_to_smv) parse_ba() (in module create_c_monitor) (in module create_dsl_monitor) (in module create_python_monitor)

parse_dsl_specifications() (in module behaverify.behaverify) parse_nuxmv_results() (in module behaverify.behaverify) print_verification_summary() (in module behaverify.behaverify) prune_nodes() (in module behaverify.behaverify_common)

R

read_vars (behaverify.agent_expander.ExpandedCheck attribute) refine_invalid() (in module behaverify.behaverify_common) refine_return_types() (in module behaverify.behaverify_common) resolve_potential_reference() (in module behaverify.behaverify_common)

resolve_potential_reference_no_type() (in module behaverify.behaverify_common) reverse_thing_if_true() (in module behaverify.meta_functions) (in module behaverify.meta_functions_neural) run_nuxmv() (in module behaverify.behaverify)

S

scope (behaverify.agent_expander.ExpandedVariable attribute) SHAPES (in module behaverify.counter_trace) SHORT_TYPE (in module behaverify.counter_trace) Silly_Dictionary (class in create_dsl_monitor) spec_type (behaverify.agent_expander.ExpandedSpec attribute)

specifications (behaverify.agent_expander.ExpandedModel attribute) split_file() (in module behaverify.counter_trace) STATUS_COLORS (in module behaverify.counter_trace) str_format() (in module behaverify.behaverify_common) sub_trees_text (behaverify.agent_expander.ExpandedModel attribute)

T

tab_indent() (in module behaverify.behaverify_common) tick_prerequisite_text (behaverify.agent_expander.ExpandedModel attribute) to_tree_text() (behaverify.agent_expander.ExpandedAction method) (behaverify.agent_expander.ExpandedCheck method) (behaverify.agent_expander.ExpandedTreeNode method) (behaverify.agent_expander.ExpandedVariable method)

tree (behaverify.agent_expander.ExpandedModel attribute)

U

update_dictionary() (in module behaverify.meta_functions) (in module behaverify.meta_functions_neural)

update_text (behaverify.agent_expander.ExpandedAction attribute)

V

validate_model() (in module behaverify.check_grammar) variable_array_size() (in module behaverify.behaverify_common) variable_scope() (in module behaverify.behaverify_common) variable_type() (in module behaverify.behaverify_common)

variables (behaverify.agent_expander.ExpandedModel attribute) verify_input() (in module behaverify.behaverify) verify_location() (in module behaverify.behaverify) verify_nuxmv_path() (in module behaverify.behaverify) visualize_BehaVerify_json() (in module behaverify.counter_trace)

W

write_smv() (in module behaverify.behaverify_to_smv)

write_vars (behaverify.agent_expander.ExpandedAction attribute)