Dynamic Predicates: animation_mode/1 animation_minor_mode/1 currently_opened_file_status/2

1292 Lines

145 Predicates

Imported Modules: tools module_information lists debug b_interpreter preferences self_check error_manager translate bmachine bsyntaxtree xtl_interface random debug preferences

77 Exports

46 specified Imports

Imports	Exports
Name: succeed_max_call_id/3 Module: succeed_max Name: empty_state/1 Module: store Name: load_constants/2 Module: value_persistance Name: maplist/2 Module: lists Name: b_machine_name/1 Module: bmachine Name: register_event_listener/3 Module: eventhandling Name: get_filename_extension/2 Module: tools Name: safe_absolute_file_name/3 Module: tools Name: get_parent_directory/2 Module: tools Name: b_machine_has_variables/0 Module: bmachine Name: current_expression/2 Module: state_space Name: current_state_id/1 Module: state_space Name: determine_type_of_formula/2 Module: bmachine Name: visited_expression/2 Module: state_space Name: call_residue/2 Module: tools_meta Name: pack_state/2 Module: state_packing Name: get_packed_b_state_with_uncompressed_lists/2 Module: state_packing Name: prime_atom0/2 Module: btypechecker Name: channel_type_list/2 Module: haskell_csp Name: symbol/4 Module: haskell_csp Name: b_get_machine_operation/4 Module: bmachine Name: tuple_of/3 Module: bsets_clp Name: b_is_variable/1 Module: bmachine Name: b_is_constant/1 Module: bmachine Name: b_get_machine_operation_for_animation/6 Module: bmachine Name: b_get_operation_description/2 Module: bmachine Name: b_compute_expression_nowf/6 Module: b_interpreter Name: get_operation_description_template_expr/2 Module: bmachine Name: between/3 Module: between Name: store_updates_and_normalise/3 Module: store Name: b_get_machine_operation_max/2 Module: bmachine Name: b_global_set/1 Module: b_global_sets Name: b_fd_card/2 Module: b_global_sets Name: inferred_minimum_global_set_cardinality/2 Module: b_global_sets Name: inferred_maximum_global_set_cardinality/2 Module: b_global_sets Name: unfixed_deferred_set/1 Module: b_global_sets Name: is_avl_relation/1 Module: custom_explicit_sets Name: is_avl_partial_function/1 Module: custom_explicit_sets Name: get_first_avl_elements/4 Module: custom_explicit_sets Name: avl_approximate_size/3 Module: custom_explicit_sets Name: b_is_variable/2 Module: bmachine Name: b_show_machine_representation/4 Module: bmachine Name: get_internal_csp_representation/1 Module: haskell_csp_analyzer Name: channel/2 Module: haskell_csp Name: b_top_level_operation/1 Module: bmachine Name: b_top_level_feasible_operation/1 Module: bmachine	Name: specfile_possible_trans_name/2 Name: specfile_possible_trans_name_for_successors/2 Name: specfile_trans/6 Name: prepare_state_for_specfile_trans/3 Name: prepare_state_for_specfile_trans/4 Name: extract_infos_from_prepared_state/2 Name: property/2 Name: elementary_prop/2 Name: partial_trans/4 Name: specfile_trans_or_partial_trans/7 Name: animation_mode/1 Name: set_animation_mode/1 Name: add_animation_minor_mode/1 Name: animation_minor_mode/1 Name: set_animation_minor_mode/1 Name: remove_animation_minor_mode/0 Name: unset_animation_minor_modes/1 Name: reset_animation_minor_modes/1 Name: b_mode/0 Name: z_mode/0 Name: b_or_z_mode/0 Name: b_or_z_mode/1 Name: eventb_mode/0 Name: classical_b_mode/0 Name: csp_mode/0 Name: csp_mode/1 Name: csp_with_bz_mode/0 Name: z_or_tla_minor_mode/0 Name: process_algebra_mode/0 Name: xtl_mode/0 Name: b_syntax_available_for_source/0 Name: type_check_csp_and_b/0 Name: currently_opened_file/1 Name: currently_opened_file_status/2 Name: currently_opened_specification_name/1 Name: set_currently_opened_file/1 Name: set_currently_opened_b_file/1 Name: set_failed_to_open_file/1 Name: set_minor_animation_mode_from_file/1 Name: set_currently_opening_file/1 Name: set_currently_opened_package/1 Name: spec_file_has_been_successfully_loaded/0 Name: b_absolute_file_name_relative_to_opened_file/2 Name: state_corresponds_to_initialised_b_machine/1 Name: state_corresponds_to_initialised_b_machine/2 Name: state_corresponds_to_fully_setup_b_machine/1 Name: state_corresponds_to_fully_setup_b_machine/2 Name: state_corresponds_to_set_up_constants/1 Name: state_corresponds_to_set_up_constants/2 Name: state_corresponds_to_set_up_constants_only/2 Name: extract_variables_from_state/2 Name: extract_variables_from_state_as_primed/2 Name: current_b_expression/1 Name: get_current_state_for_b_formula/2 Name: get_state_for_b_formula/3 Name: get_operation_name/2 Name: get_operation_internal_name/2 Name: translate_operation_name/2 Name: get_operation_arguments/2 Name: get_operation_return_values_and_arguments/3 Name: get_operation_description/2 Name: get_operation_description_for_transition/4 Name: build_up_b_real_operation/2 Name: expand_const_and_vars/3 Name: expand_const_and_vars_to_full_store/2 Name: expand_to_constants_and_variables/3 Name: max_operations_zero_for_operation/1 Name: compute_operation_effect_max/6 Name: create_setup_constants_operation/3 Name: get_internal_representation/1 Name: get_internal_representation/3 Name: get_possible_event/1 Name: get_feasible_event/1 Name: get_possible_language_specific_top_level_event/3 Name: get_specification_description/2 Name: get_local_states_for_operation_transition/4 Name: create_local_store_for_operation/4

Imports

Exports

Name: succeed_max_call_id/3

Module: succeed_max

Name: empty_state/1

Module: store

Name: load_constants/2

Module: value_persistance

Name: maplist/2

Module: lists

Name: b_machine_name/1

Module: bmachine

Name: register_event_listener/3

Module: eventhandling

Name: get_filename_extension/2

Module: tools

Name: safe_absolute_file_name/3

Module: tools

Name: get_parent_directory/2

Module: tools

Name: b_machine_has_variables/0

Module: bmachine

Name: current_expression/2

Module: state_space

Name: current_state_id/1

Module: state_space

Name: determine_type_of_formula/2

Module: bmachine

Name: visited_expression/2

Module: state_space

Name: call_residue/2

Module: tools_meta

Name: pack_state/2

Module: state_packing

Name: get_packed_b_state_with_uncompressed_lists/2

Module: state_packing

Name: prime_atom0/2

Module: btypechecker

Name: channel_type_list/2

Module: haskell_csp

Name: symbol/4

Module: haskell_csp

Name: b_get_machine_operation/4

Module: bmachine

Name: tuple_of/3

Module: bsets_clp

Name: b_is_variable/1

Module: bmachine

Name: b_is_constant/1

Module: bmachine

Name: b_get_machine_operation_for_animation/6

Module: bmachine

Name: b_get_operation_description/2

Module: bmachine

Name: b_compute_expression_nowf/6

Module: b_interpreter

Name: get_operation_description_template_expr/2

Module: bmachine

Name: between/3

Module: between

Name: store_updates_and_normalise/3

Module: store

Name: b_get_machine_operation_max/2

Module: bmachine

Name: b_global_set/1

Module: b_global_sets

Name: b_fd_card/2

Module: b_global_sets

Name: inferred_minimum_global_set_cardinality/2

Module: b_global_sets

Name: inferred_maximum_global_set_cardinality/2

Module: b_global_sets

Name: unfixed_deferred_set/1

Module: b_global_sets

Name: is_avl_relation/1

Module: custom_explicit_sets

Name: is_avl_partial_function/1

Module: custom_explicit_sets

Name: get_first_avl_elements/4

Module: custom_explicit_sets

Name: avl_approximate_size/3

Module: custom_explicit_sets

Name: b_is_variable/2

Module: bmachine

Name: b_show_machine_representation/4

Module: bmachine

Name: get_internal_csp_representation/1

Module: haskell_csp_analyzer

Name: channel/2

Module: haskell_csp

Name: b_top_level_operation/1

Module: bmachine

Name: b_top_level_feasible_operation/1

Module: bmachine

Name: specfile_possible_trans_name/2

Name: specfile_possible_trans_name_for_successors/2

Name: specfile_trans/6

Name: prepare_state_for_specfile_trans/3

Name: prepare_state_for_specfile_trans/4

Name: extract_infos_from_prepared_state/2

Name: property/2

Name: elementary_prop/2

Name: partial_trans/4

Name: specfile_trans_or_partial_trans/7

Name: animation_mode/1

Name: set_animation_mode/1

Name: add_animation_minor_mode/1

Name: animation_minor_mode/1

Name: set_animation_minor_mode/1

Name: remove_animation_minor_mode/0

Name: unset_animation_minor_modes/1

Name: reset_animation_minor_modes/1

Name: b_mode/0

Name: z_mode/0

Name: b_or_z_mode/0

Name: b_or_z_mode/1

Name: eventb_mode/0

Name: classical_b_mode/0

Name: csp_mode/0

Name: csp_mode/1

Name: csp_with_bz_mode/0

Name: z_or_tla_minor_mode/0

Name: process_algebra_mode/0

Name: xtl_mode/0

Name: b_syntax_available_for_source/0

Name: type_check_csp_and_b/0

Name: currently_opened_file/1

Name: currently_opened_file_status/2

Name: currently_opened_specification_name/1

Name: set_currently_opened_file/1

Name: set_currently_opened_b_file/1

Name: set_failed_to_open_file/1

Name: set_minor_animation_mode_from_file/1

Name: set_currently_opening_file/1

Name: set_currently_opened_package/1

Name: spec_file_has_been_successfully_loaded/0

Name: b_absolute_file_name_relative_to_opened_file/2

Name: state_corresponds_to_initialised_b_machine/1

Name: state_corresponds_to_initialised_b_machine/2

Name: state_corresponds_to_fully_setup_b_machine/1

Name: state_corresponds_to_fully_setup_b_machine/2

Name: state_corresponds_to_set_up_constants/1

Name: state_corresponds_to_set_up_constants/2

Name: state_corresponds_to_set_up_constants_only/2

Name: extract_variables_from_state/2

Name: extract_variables_from_state_as_primed/2

Name: current_b_expression/1

Name: get_current_state_for_b_formula/2

Name: get_state_for_b_formula/3

Name: get_operation_name/2

Name: get_operation_internal_name/2

Name: translate_operation_name/2

Name: get_operation_arguments/2

Name: get_operation_return_values_and_arguments/3

Name: get_operation_description/2

Name: get_operation_description_for_transition/4

Name: build_up_b_real_operation/2

Name: expand_const_and_vars/3

Name: expand_const_and_vars_to_full_store/2

Name: expand_to_constants_and_variables/3

Name: max_operations_zero_for_operation/1

Name: compute_operation_effect_max/6

Name: create_setup_constants_operation/3

Name: get_internal_representation/1

Name: get_internal_representation/3

Name: get_possible_event/1

Name: get_feasible_event/1

Name: get_possible_language_specific_top_level_event/3

Name: get_specification_description/2

Name: get_local_states_for_operation_transition/4

Name: create_local_store_for_operation/4

Predicates

Predicates:

add_animation_minor_mode/1

animation_mode/1

b_absolute_file_name_relative_to_opened_file/2

b_mode/0

b_or_z_mode/0

b_or_z_mode/1

b_possible_trans_name/2

b_preference_par/3

b_property/2

b_syntax_available_for_source/0

b_trans/5

b_transition_for_csp/9

build_up_b_operation_for_csp/3

build_up_b_real_operation/2

check_compatibility/3

check_rest_couple/2

check_rest_couple_els/2

check_type/3

check_type_for_id/3

choose_loaded_solution/3

classical_b_mode/0

classical_minor_mode/1

compute_constants/3

compute_operation_effect_max/6

compute_operation_on_expanded_store2/6

compute_operation_updates_on_expanded_store/6

couple_int/2

create_initialisation_operation/2

create_local_store_for_operation/4

create_setup_constants_operation/3

create_value/3

csp_and_b_transition/5

csp_b_possible_trans_name/2

csp_mode/0

csp_mode/1

csp_with_bz_mode/0

current_b_expression/1

currently_opened_file/1

currently_opened_specification_name/1

dom_range_type/3

elementary_fun_prop/3

elementary_prop/2

elementary_prop3/3

elementary_var_prop/3

eventb_mode/0

expand_const_and_vars/3

expand_const_and_vars_to_full_store/2

expand_to_constants_and_variables/3

extract_full_store/2

extract_infos_from_prepared_state/2

extract_variables_from_state/2

extract_variables_from_state_as_primed/2

file_extension_mode/3

formula_class/1

gen_para_bind/3

generate_args/6

get_alloy_description/2

get_csp_description/2

get_current_state_for_b_formula/2

get_default_description/2

get_eventb_description/2

get_feasible_event/1

get_internal_aux/4

get_internal_representation/1

get_internal_representation/3

get_local_state_for_operation_transition/3

get_local_states_for_operation_transition/4

get_max_enablings_for_init/3

get_max_enablings_per_operation/3

get_max_enablings_per_operation_aux/3

get_operation_arguments/2

get_operation_description/2

get_operation_description_for_transition/4

get_operation_internal_name/2

get_operation_name/2

get_operation_return_values_and_arguments/3

get_possible_b_top_level_event/3

get_possible_event/1

get_possible_language_specific_top_level_event/3

get_relation_element/3

get_specific_description/4

get_specification_description/2

get_state/4

get_state_for_b_formula/3

get_tla_description/2

hide_csp_event/3

i_transition/6

identifier_has_tla_type/2

is_csp_boolean_type/1

is_csp_boolean_value/1

is_csp_couple_type/3

is_csp_global_set_type/2

is_csp_integer_type/1

is_csp_list/2

is_csp_seq_type/2

is_csp_set_type/2

is_setup_constants_internal_name/1

l_check_compatibility/3

max_operations_zero_for_operation/1

my_visited_expression/2

partial_i_transition/3

partial_trans/4

prepare_infos/3

prepare_state_for_specfile_trans/4

prepare_state_for_specfile_trans/3

prime_binding/2

process_algebra_mode/0

property/2

remove_animation_minor_mode/0

remove_infos_from_prepared_state/2

reset_animation_minor_modes/1

reset_currently_opened_file/0

reset_specfile/0

set_animation_minor_mode/1

set_animation_mode/1

set_currently_opened_b_file/1

set_currently_opened_file/1

set_currently_opened_package/1

set_currently_opening_file/1

set_failed_to_open_file/1

set_minor_animation_mode_from_file/1

setup_transition_skeleton/2

show_avl_set/1

spec_file_has_been_successfully_loaded/0

specfile_possible_trans_name/2

specfile_possible_trans_name_for_successors/2

specfile_trans/6

specfile_trans_or_partial_trans/7

state_corresponds_to_fully_setup_b_machine/1

state_corresponds_to_fully_setup_b_machine/2

state_corresponds_to_initialised_b_machine/1

state_corresponds_to_initialised_b_machine/2

state_corresponds_to_set_up_constants/1

state_corresponds_to_set_up_constants/2

state_corresponds_to_set_up_constants_only/2

translate_operation_name/2

type_check_csp_and_b/0

type_ok/2

type_ok2/2

unset_animation_minor_modes/1

z_or_tla_minor_mode/0

add_animation_minor_mode/1

animation_mode/1

Description:
:- use_module(delay).

Dynamic: true

b_absolute_file_name_relative_to_opened_file/2

b_mode/0

b_or_z_mode/0

b_or_z_mode/1

b_possible_trans_name/2

b_preference_par/3

b_property/2

b_syntax_available_for_source/0

b_trans/5

b_transition_for_csp/9

Description:
print_message(trying_b_trans(Operation,ChArgs,OpArgs)), %%
, print_message(csp_btrans(Operation)), %%.
print(probing(ChOpName)),nl,

b_transition_for_csp(ChOpName,_CSPAction,ChArgs,OpArgs,BState,OpName,Operation,NewB,TransInfo) :-
    build_up_b_operation_for_csp(ChOpName,OpArgs,Operation),
    !,
    OpName = ChOpName,
    %% print_message(trying_b_trans(Operation,ChArgs,OpArgs)),
    (get_preference(try_operation_reuse,false)
    -> generate_b_operationargs_from_csp(ChArgs,OpArgs),
    b_trans(BState,OpName,Operation,NewB,TransInfo)
    ;
    % compute B transition without parameters so that we can cache
    b_trans(BState,OpName,Operation,NewB,TransInfo),
    % and unify afterwards
    generate_b_operationargs_from_csp(ChArgs,OpArgs)
).

b_transition_for_csp(ChOpName,_CSPAction,ChArgs,OpArgs,BState,OpName,Operation,NewB,TransInfo) :-
    OpName = ChOpName,
    (b_is_variable(ChOpName) ; b_is_constant(ChOpName)),
    %% print(probing(ChOpName)),nl,
    expand_const_and_vars_to_full_store(BState,FBState),
    try_lookup_value_in_store_and_global_sets(ChOpName,FBState,IdValue),
    !,
    remove_infos_from_prepared_state(BState,NewB),
    TransInfo=[],
    /* interpret as probing operation: get value of var,cst,SET */
    generate_b_operationargs_from_csp(ChArgs,OpArgs),
    (OpArgs=[SingleVal]
    -> SingleVal = IdValue, Operation='-->'(ChOpName,[IdValue])
    ; OpArgs=[Val1,Val2],
    tuple_of(Val1,Val2,IdValue), /* from bsets_clp, use exact_element_of ??? */
    OpCall =.. [ChOpName,Val1],
    Operation='-->'(OpCall,[Val2])
).

b_transition_for_csp(_ChOpName,CSPAction,_ChArgs,_OpArgs,BState,OpName,Operation,NewB,TransInfo) :-
    OpName = '$CSP', % all CSP events grouped together
    remove_infos_from_prepared_state(BState,NewB),
    TransInfo=[],
    /* no B operation of the name; could be tau or tick or extra comm channel */
    %Op1 =.. [ChOpName|OpArgs],
    Operation = CSPAction. % removed csp(.) wrapper [for LTL model checker]

build_up_b_operation_for_csp/3

build_up_b_real_operation/2

check_compatibility/3

check_rest_couple/2

check_rest_couple_els/2

check_type/3

Block: check_type(?,-,?)

check_type_for_id/3

choose_loaded_solution/3

classical_b_mode/0

classical_minor_mode/1

compute_constants/3

compute_operation_effect_max/6

Description:
print_message('FOUND_CONSTANTS'(OpName)),

compute_operation_effect_max([],OpName,Operation,NewState,PathInfo,Max) :-
    compute_operation_updates_on_expanded_store([],OpName,Operation,Updates,PathInfo,Max),
    store_updates_and_normalise(Updates,[],NewState).

compute_operation_effect_max([H|T],OpName,Operation,NewState,PathInfo,Max) :-
    compute_operation_updates_on_expanded_store([H|T],OpName,Operation,Updates,PathInfo,Max),
    store_updates_and_normalise(Updates,[H|T],NewState).

compute_operation_effect_max(const_and_vars(ConstID,Vars),OpName,Operation,ResultingStore,PathInfo,Max) :-
    prepare_state_for_specfile_trans(const_and_vars(ConstID,Vars),unknown,R),
    %print(expanded_const_and_vars(ConstID)),nl,
    compute_operation_effect_max(R,OpName,Operation,ResultingStore,PathInfo,Max).

compute_operation_effect_max(expanded_const_and_vars(ID,Vars,FullStore,Infos),OpName,Operation,NewState,PathInfo,Max) :-
    compute_operation_updates_on_expanded_store(expanded_const_and_vars(ID,Vars,FullStore,Infos),
    OpName,Operation,Updates,PathInfo,Max),
    NewState = const_and_vars(ID,NewVars),
    store_updates_and_normalise(Updates,Vars,NewVars).

compute_operation_effect_max(expanded_vars(FullStore,Infos),OpName,Operation,NewState,PathInfo,Max) :-
    compute_operation_updates_on_expanded_store(expanded_vars(FullStore,Infos),
    OpName,Operation,Updates,PathInfo,Max),
    store_updates_and_normalise(Updates,FullStore,NewState).

compute_operation_effect_max(concrete_constants(ConstantsStore),'$initialise_machine',OpInit,ResultingStore,PathInfo,Max) :-
    get_max_enablings_for_init(Max,'$initialise_machine',MaxForCall),
    succeed_max_call_id('$initialise_machine',
    b_interpreter:b_initialise_machine(ConstantsStore,InitialVars,InitialStore,PathInfo),MaxForCall),
    create_initialisation_operation(InitialVars,OpInit),
    (\+ preferences:preference(symmetry_mode,flood), /* TO DO : improve permutation to allow using const_and_vars optimisation */
    visited_expression(ConstID,concrete_constants(ConstantsStore))
    -> ResultingStore = const_and_vars(ConstID,InitialVars) /* avoid storing constant values again */
    ; ResultingStore = InitialStore).

compute_operation_effect_max(root,'$setup_constants',OpSetup,concrete_constants(FilteredConstantsStore),[],Max) :-
    b_machine_has_constants_or_properties,
    get_max_enablings_for_init(Max,'$setup_constants',MaxForCall),
    compute_constants(ConstantsStore,MaxForCall,Complete),
    create_setup_constants_operation(ConstantsStore,Complete,OpSetup),
    %%print_message('FOUND_CONSTANTS'(OpName)),
    (get_preference(filter_unused_constants,true) % possibly disable if VisB or Custom Graph Definitions exist
    -> exclude(unused_binding,ConstantsStore,FilteredConstantsStore)
    ; FilteredConstantsStore=ConstantsStore).

compute_operation_effect_max(root,'$initialise_machine',OpInit,InitialStore,PathInfo,Max) :-
    \+ b_machine_has_constants_or_properties,
    get_max_enablings_for_init(Max,'$initialise_machine',MaxForCall),
    empty_state(EmptyState),
    succeed_max_call_id('$initialise_machine',
    b_interpreter:b_initialise_machine(EmptyState,InitialVars,InitialStore,PathInfo),MaxForCall),
    create_initialisation_operation(InitialVars,OpInit).

compute_operation_on_expanded_store2/6

compute_operation_updates_on_expanded_store/6

couple_int/2

create_initialisation_operation/2

create_local_store_for_operation/4

create_setup_constants_operation/3

create_value/3

csp_and_b_transition/5

Description:
print(csp_trans(ChOpName,ChArgs)),nl, %%

csp_b_possible_trans_name/2

csp_mode/0

csp_mode/1

csp_with_bz_mode/0

current_b_expression/1

currently_opened_file/1

currently_opened_specification_name/1

dom_range_type/3

elementary_fun_prop/3

elementary_prop/2

elementary_prop3/3

elementary_var_prop/3

eventb_mode/0

expand_const_and_vars/3

Description:
This can take a while if the Constants are big !

expand_const_and_vars_to_full_store/2

expand_to_constants_and_variables/3

extract_full_store/2

extract_infos_from_prepared_state/2

extract_variables_from_state/2

extract_variables_from_state_as_primed/2

file_extension_mode/3

formula_class/1

gen_para_bind/3

generate_args/6

get_alloy_description/2

get_csp_description/2

get_current_state_for_b_formula/2

get_default_description/2

get_eventb_description/2

get_feasible_event/1

get_internal_aux/4

get_internal_representation/1

get_internal_representation/3

get_local_state_for_operation_transition/3

get_local_states_for_operation_transition/4

get_max_enablings_for_init/3

get_max_enablings_per_operation/3

get_max_enablings_per_operation_aux/3

get_operation_arguments/2

get_operation_description/2

get_operation_description_for_transition/4

get_operation_internal_name/2

get_operation_name/2

get_operation_return_values_and_arguments/3

get_possible_b_top_level_event/3

get_possible_event/1

get_possible_language_specific_top_level_event/3

get_relation_element/3

get_specific_description/4

get_specification_description/2

get_state/4

get_state_for_b_formula/3

get_tla_description/2

hide_csp_event/3

i_transition/6

identifier_has_tla_type/2

is_csp_boolean_type/1

is_csp_boolean_value/1

is_csp_couple_type/3

is_csp_global_set_type/2

is_csp_integer_type/1

is_csp_list/2

is_csp_seq_type/2

is_csp_set_type/2

is_setup_constants_internal_name/1

l_check_compatibility/3

max_operations_zero_for_operation/1

my_visited_expression/2

partial_i_transition/3

partial_trans/4

prepare_infos/3

prepare_state_for_specfile_trans/4

Description:
This can take a while if the Constants are big !

prepare_state_for_specfile_trans/3

prime_binding/2

process_algebra_mode/0

property/2

Description:
print(checking_csp_and_b(CSPState)),nl,

remove_animation_minor_mode/0

remove_infos_from_prepared_state/2

reset_animation_minor_modes/1

reset_currently_opened_file/0

reset_specfile/0

set_animation_minor_mode/1

set_animation_mode/1

set_currently_opened_b_file/1

set_currently_opened_file/1

set_currently_opened_package/1

set_currently_opening_file/1

set_failed_to_open_file/1

set_minor_animation_mode_from_file/1

setup_transition_skeleton/2

show_avl_set/1

spec_file_has_been_successfully_loaded/0

specfile_possible_trans_name/2

specfile_possible_trans_name_for_successors/2

specfile_trans/6

specfile_trans_or_partial_trans/7

state_corresponds_to_fully_setup_b_machine/1

state_corresponds_to_fully_setup_b_machine/2

state_corresponds_to_initialised_b_machine/1

state_corresponds_to_initialised_b_machine/2

state_corresponds_to_set_up_constants/1

state_corresponds_to_set_up_constants/2

state_corresponds_to_set_up_constants_only/2

translate_operation_name/2

type_check_csp_and_b/0

type_ok/2

type_ok2/2

unset_animation_minor_modes/1

z_or_tla_minor_mode/0

Determinacy Checker

Determinacy Checker:

! Existence error in user:environ/2
! procedure user:environ/2 does not exist
! goal: user:environ(prob_release,true)
! Existence error in argument 1 of absolute_file_name/3
! file extension('dll_path/dll_path') does not exist
! goal: absolute_file_name(extension('dll_path/dll_path'),_35251,[access(exist),file_type(source),relative_to('/builds/stups/prob/prolog_doc_gen/prolog-Doc/prob_prolog/src/pathes.pl')])
! Existence error in user:environ/2
! procedure user:environ/2 does not exist
! goal: user:environ(no_terminal_colors,true)
! Existence error in user:environ/2
! procedure user:environ/2 does not exist
! goal: user:environ(prob_enter_debugger_upon_error,true)
! Existence error in user:environ/2
! procedure user:environ/2 does not exist
! goal: user:environ(prob_use_timer,true)
! Existence error in user:environ/2
! procedure user:environ/2 does not exist
! goal: user:environ(prob_profile,true)
! Existence error in user:environ/2
! procedure user:environ/2 does not exist
! goal: user:environ(prob_src_profile,true)
! Existence error in user:environ/2
! procedure user:environ/2 does not exist
! goal: user:environ(prob_safe_mode,true)
! Existence error in user:environ/2
! procedure user:environ/2 does not exist
! goal: user:environ(prob_core_only,true)
! Existence error in user:environ/2
! procedure user:environ/2 does not exist
! goal: user:environ(prob_myheap,false)
! Existence error in user:environ/2
! procedure user:environ/2 does not exist
! goal: user:environ(disable_chr,true)
! Existence error in argument 1 of absolute_file_name/3
! file probsrc(tools_strings) does not exist
! goal: absolute_file_name(probsrc(tools_strings),_66093,[access(exist),file_type(source),relative_to('/builds/stups/prob/prolog_doc_gen/prolog-Doc/prob_prolog/src/pathes_lib.pl')])
! Existence error in argument 1 of absolute_file_name/3
! file extension('counter/counter') does not exist
! goal: absolute_file_name(extension('counter/counter'),_35251,[access(exist),file_type(source),relative_to('/builds/stups/prob/prolog_doc_gen/prolog-Doc/prob_prolog/src/error_manager.pl')])
! Existence error in user:environ/2
! procedure user:environ/2 does not exist
! goal: user:environ(prob_debug_flag,true)
! Existence error in user:environ/2
! procedure user:environ/2 does not exist
! goal: user:environ(plspec_patch_libraries,true)
! Existence error in user:environ/2
! procedure user:environ/2 does not exist
! goal: user:environ(prob_debug_flag,true)
! Existence error in user:environ/2
! procedure user:environ/2 does not exist
! goal: user:environ(prob_release,true)
! Existence error in argument 1 of absolute_file_name/3
! file probsrc(error_manager) does not exist
! goal: absolute_file_name(probsrc(error_manager),_45455,[access(exist),file_type(source),relative_to('/builds/stups/prob/prolog_doc_gen/prolog-Doc/prob_prolog/src/xml_prob.pl')])
! Existence error in argument 1 of absolute_file_name/3
! file probsrc(debug) does not exist
! goal: absolute_file_name(probsrc(debug),_43791,[access(exist),file_type(source),relative_to('/builds/stups/prob/prolog_doc_gen/prolog-Doc/prob_prolog/src/xml_prob.pl')])
! Existence error in argument 1 of absolute_file_name/3
! file extrasrc(json_parser) does not exist
! goal: absolute_file_name(extrasrc(json_parser),_88721,[access(exist),file_type(source),relative_to('/builds/stups/prob/prolog_doc_gen/prolog-Doc/prob_prolog/src/translate.pl')])
! Existence error in argument 1 of absolute_file_name/3
! file probsrc(eventhandling) does not exist
! goal: absolute_file_name(probsrc(eventhandling),_92285,[access(exist),file_type(source),relative_to('/builds/stups/prob/prolog_doc_gen/prolog-Doc/prob_prolog/src/kernel_freetypes.pl')])
! Existence error in argument 1 of absolute_file_name/3
! file probsrc(clpfd_interface) does not exist
! goal: absolute_file_name(probsrc(clpfd_interface),_88721,[access(exist),file_type(source),relative_to('/builds/stups/prob/prolog_doc_gen/prolog-Doc/prob_prolog/src/typing_tools.pl')])
! Existence error in argument 1 of absolute_file_name/3
! file covsrc(coverage_tools_annotations) does not exist
! goal: absolute_file_name(covsrc(coverage_tools_annotations),_114433,[access(exist),file_type(source),relative_to('/builds/stups/prob/prolog_doc_gen/prolog-Doc/prob_prolog/src/kernel_waitflags.pl')])
! Existence error in user:environ/2
! procedure user:environ/2 does not exist
! goal: user:environ(prob_safe_mode,true)
! Existence error in argument 1 of absolute_file_name/3
! file probsrc(tools_lists) does not exist
! goal: absolute_file_name(probsrc(tools_lists),_114433,[access(exist),file_type(source),relative_to('/builds/stups/prob/prolog_doc_gen/prolog-Doc/prob_prolog/src/kernel_tools.pl')])
! Existence error in user:environ/2
! procedure user:environ/2 does not exist
! goal: user:environ(prob_debug_watch_flag,true)
! Existence error in user:environ/2
! procedure user:environ/2 does not exist
! goal: user:environ(prob_safe_mode,true)
! Existence error in argument 1 of absolute_file_name/3
! file probsrc(kernel_waitflags) does not exist
! goal: absolute_file_name(probsrc(kernel_waitflags),_116577,[access(exist),file_type(source),relative_to('/builds/stups/prob/prolog_doc_gen/prolog-Doc/prob_prolog/src/runtime_profiler.pl')])
! Existence error in argument 1 of absolute_file_name/3
! file probsrc(tools) does not exist
! goal: absolute_file_name(probsrc(tools),_130237,[access(exist),file_type(source),relative_to('/builds/stups/prob/prolog_doc_gen/prolog-Doc/prob_prolog/src/kernel_records.pl')])
! Existence error in argument 1 of absolute_file_name/3
! file prob_rewrite_rules(b_ast_cleanup_rewrite_rules) does not exist
! goal: absolute_file_name(prob_rewrite_rules(b_ast_cleanup_rewrite_rules),_129949,[access(exist),file_type(source),relative_to('/builds/stups/prob/prolog_doc_gen/prolog-Doc/prob_prolog/src/b_ast_cleanup.pl')])
! Existence error in argument 1 of absolute_file_name/3
! file probsrc(tools_strings) does not exist
! goal: absolute_file_name(probsrc(tools_strings),_130237,[access(exist),file_type(source),relative_to('/builds/stups/prob/prolog_doc_gen/prolog-Doc/prob_prolog/src/input_syntax_tree.pl')])
! Existence error in argument 1 of absolute_file_name/3
! file probsrc(eventhandling) does not exist
! goal: absolute_file_name(probsrc(eventhandling),_169041,[access(exist),file_type(source),relative_to('/builds/stups/prob/prolog_doc_gen/prolog-Doc/prob_prolog/src/pragmas.pl')])
! Existence error in argument 1 of absolute_file_name/3
! file probsrc(module_information) does not exist
! goal: absolute_file_name(probsrc(module_information),_170847,[access(exist),file_type(source),relative_to('/builds/stups/prob/prolog_doc_gen/prolog-Doc/prob_prolog/src/bmachine_static_checks.pl')])
! Existence error in argument 1 of absolute_file_name/3
! file extension('counter/counter') does not exist
! goal: absolute_file_name(extension('counter/counter'),_184007,[access(exist),file_type(source),relative_to('/builds/stups/prob/prolog_doc_gen/prolog-Doc/prob_prolog/src/state_space.pl')])
! Existence error in argument 1 of absolute_file_name/3
! file extrasrc(external_functions_reals) does not exist
! goal: absolute_file_name(extrasrc(external_functions_reals),_183243,[access(exist),file_type(source),relative_to('/builds/stups/prob/prolog_doc_gen/prolog-Doc/prob_prolog/src/external_functions.pl')])
! Existence error in argument 1 of absolute_file_name/3
! file extrasrc(external_functions_svg) does not exist
! goal: absolute_file_name(extrasrc(external_functions_svg),_183243,[access(exist),file_type(source),relative_to('/builds/stups/prob/prolog_doc_gen/prolog-Doc/prob_prolog/src/external_functions.pl')])
! Existence error in user:check_arithmetic_function/1
! procedure user:check_arithmetic_function/1 does not exist
! goal: user:check_arithmetic_function(log(2,4))
! Existence error in argument 1 of absolute_file_name/3
! file chrsrc(chr_integer_inequality) does not exist
! goal: absolute_file_name(chrsrc(chr_integer_inequality),_184539,[access(exist),file_type(source),relative_to('/builds/stups/prob/prolog_doc_gen/prolog-Doc/prob_prolog/src/clpfd_interface.pl')])
! Existence error in argument 1 of absolute_file_name/3
! file probsrc(preferences) does not exist
! goal: absolute_file_name(probsrc(preferences),_183865,[access(exist),file_type(source),relative_to('/builds/stups/prob/prolog_doc_gen/prolog-Doc/prob_prolog/src/kernel_z.pl')])
! Existence error in user:exists_source/1
! procedure user:exists_source/1 does not exist
! goal: user:exists_source(library(atts))
! Existence error in argument 1 of absolute_file_name/3
! file probsrc(tools_strings) does not exist
! goal: absolute_file_name(probsrc(tools_strings),_184859,[access(exist),file_type(source),relative_to('/builds/stups/prob/prolog_doc_gen/prolog-Doc/prob_prolog/src/kernel_strings.pl')])
! Existence error in argument 1 of absolute_file_name/3
! file probsrc(kernel_freetypes) does not exist
! goal: absolute_file_name(probsrc(kernel_freetypes),_178455,[access(exist),file_type(source),relative_to('/builds/stups/prob/prolog_doc_gen/prolog-Doc/prob_prolog/src/external_functions.pl')])
! Existence error in argument 1 of absolute_file_name/3
! file probsrc(error_manager) does not exist
! goal: absolute_file_name(probsrc(error_manager),_169041,[access(exist),file_type(source),relative_to('/builds/stups/prob/prolog_doc_gen/prolog-Doc/prob_prolog/src/bmachine_static_checks.pl')])
! Existence error in user:exists_source/1
! procedure user:exists_source/1 does not exist
! goal: user:exists_source(library(logarr))
! Existence error in argument 1 of absolute_file_name/3
! file probcspsrc(haskell_csp) does not exist
! goal: absolute_file_name(probcspsrc(haskell_csp),_171615,[access(exist),file_type(source),relative_to('/builds/stups/prob/prolog_doc_gen/prolog-Doc/prob_prolog/src/xtl_interface.pl')])
! Existence error in user:environ/2
! procedure user:environ/2 does not exist
! goal: user:environ(prob_safe_mode,true)
! Existence error in argument 1 of absolute_file_name/3
! file probsrc(eventhandling) does not exist
! goal: absolute_file_name(probsrc(eventhandling),_165619,[access(exist),file_type(source),relative_to('/builds/stups/prob/prolog_doc_gen/prolog-Doc/prob_prolog/src/parsercall.pl')])
! Existence error in argument 1 of absolute_file_name/3
! file probsrc(bsyntaxtree) does not exist
! goal: absolute_file_name(probsrc(bsyntaxtree),_165907,[access(exist),file_type(source),relative_to('/builds/stups/prob/prolog_doc_gen/prolog-Doc/prob_prolog/src/bmachine_eventb.pl')])
! Existence error in argument 1 of absolute_file_name/3
! file extension('probhash/probhash') does not exist
! goal: absolute_file_name(extension('probhash/probhash'),_165619,[access(exist),file_type(source),relative_to('/builds/stups/prob/prolog_doc_gen/prolog-Doc/prob_prolog/src/b_machine_hierarchy.pl')])
! Existence error in argument 1 of absolute_file_name/3
! file kodkodsrc(kodkod) does not exist
! goal: absolute_file_name(kodkodsrc(kodkod),_134511,[access(exist),file_type(source),relative_to('/builds/stups/prob/prolog_doc_gen/prolog-Doc/prob_prolog/src/bmachine.pl')])
! Existence error in argument 1 of absolute_file_name/3
! file probsrc(b_state_model_check) does not exist
! goal: absolute_file_name(probsrc(b_state_model_check),_130095,[access(exist),file_type(source),relative_to('/builds/stups/prob/prolog_doc_gen/prolog-Doc/prob_prolog/src/b_read_write_info.pl')])
! Existence error in argument 1 of absolute_file_name/3
! file probsrc(bmachine_eventb) does not exist
! goal: absolute_file_name(probsrc(bmachine_eventb),_122697,[access(exist),file_type(source),relative_to('/builds/stups/prob/prolog_doc_gen/prolog-Doc/prob_prolog/src/btypechecker.pl')])
! Existence error in argument 1 of absolute_file_name/3
! file probsrc(closures) does not exist
! goal: absolute_file_name(probsrc(closures),_122697,[access(exist),file_type(source),relative_to('/builds/stups/prob/prolog_doc_gen/prolog-Doc/prob_prolog/src/memoization.pl')])
! Existence error in user:environ/2
! procedure user:environ/2 does not exist
! goal: user:environ(prob_use_timer,true)
! Existence error in user:environ/2
! procedure user:environ/2 does not exist
! goal: user:environ(prob_debug_watch_flag,true)
! Existence error in argument 1 of absolute_file_name/3
! file probsrc(kernel_reals) does not exist
! goal: absolute_file_name(probsrc(kernel_reals),_151845,[access(exist),file_type(source),relative_to('/builds/stups/prob/prolog_doc_gen/prolog-Doc/prob_prolog/src/b_interpreter_check.pl')])
! Existence error in argument 1 of absolute_file_name/3
! file probsrc(clpfd_interface) does not exist
! goal: absolute_file_name(probsrc(clpfd_interface),_146151,[access(exist),file_type(source),relative_to('/builds/stups/prob/prolog_doc_gen/prolog-Doc/prob_prolog/src/kernel_equality.pl')])
! Existence error in user:environ/2
! procedure user:environ/2 does not exist
! goal: user:environ(no_wd_checking,true)
! Existence error in user:exists_source/1
! procedure user:exists_source/1 does not exist
! goal: user:exists_source(library(atts))
! Existence error in user:exists_source/1
! procedure user:exists_source/1 does not exist
! goal: user:exists_source(library(atts))
! Existence error in argument 1 of absolute_file_name/3
! file probsrc(avl_tools) does not exist
! goal: absolute_file_name(probsrc(avl_tools),_129239,[access(exist),file_type(source),relative_to('/builds/stups/prob/prolog_doc_gen/prolog-Doc/prob_prolog/src/bsets_clp.pl')])
! Existence error in argument 1 of absolute_file_name/3
! file probsrc(kernel_waitflags) does not exist
! goal: absolute_file_name(probsrc(kernel_waitflags),_114433,[access(exist),file_type(source),relative_to('/builds/stups/prob/prolog_doc_gen/prolog-Doc/prob_prolog/src/delay.pl')])
! Existence error in argument 1 of absolute_file_name/3
! file probsrc(performance_messages) does not exist
! goal: absolute_file_name(probsrc(performance_messages),_114433,[access(exist),file_type(source),relative_to('/builds/stups/prob/prolog_doc_gen/prolog-Doc/prob_prolog/src/b_compiler.pl')])
! Existence error in user:environ/2
! procedure user:environ/2 does not exist
! goal: user:environ(prob_safe_mode,true)
! Existence error in user:environ/2
! procedure user:environ/2 does not exist
! goal: user:environ(prob_safe_mode,true)
! Existence error in user:environ/2
! procedure user:environ/2 does not exist
! goal: user:environ(no_wd_checking,true)
! Existence error in user:environ/2
! procedure user:environ/2 does not exist
! goal: user:environ(prob_data_validation_mode,xxxtrue)
! Existence error in user:environ/2
! procedure user:environ/2 does not exist
! goal: user:environ(prob_data_validation_mode,true)
! Existence error in argument 1 of absolute_file_name/3
! file probsrc(bsyntaxtree) does not exist
! goal: absolute_file_name(probsrc(bsyntaxtree),_88579,[access(exist),file_type(source),relative_to('/builds/stups/prob/prolog_doc_gen/prolog-Doc/prob_prolog/src/custom_explicit_sets.pl')])
! Existence error in argument 1 of absolute_file_name/3
! file probsrc(custom_explicit_sets) does not exist
! goal: absolute_file_name(probsrc(custom_explicit_sets),_59313,[access(exist),file_type(source),relative_to('/builds/stups/prob/prolog_doc_gen/prolog-Doc/prob_prolog/src/bsyntaxtree.pl')])
! Existence error in argument 1 of absolute_file_name/3
! file extension('random_permutations/random_permutations') does not exist
! goal: absolute_file_name(extension('random_permutations/random_permutations'),_61461,[access(exist),file_type(source),relative_to('/builds/stups/prob/prolog_doc_gen/prolog-Doc/prob_prolog/src/fd_utils_clpfd.pl')])
! Existence error in argument 1 of absolute_file_name/3
! file probsrc(error_manager) does not exist
! goal: absolute_file_name(probsrc(error_manager),_59459,[access(exist),file_type(source),relative_to('/builds/stups/prob/prolog_doc_gen/prolog-Doc/prob_prolog/src/partition_detection.pl')])
! Existence error in argument 1 of absolute_file_name/3
! file extension('counter/counter') does not exist
! goal: absolute_file_name(extension('counter/counter'),_49509,[access(exist),file_type(source),relative_to('/builds/stups/prob/prolog_doc_gen/prolog-Doc/prob_prolog/src/kernel_reals.pl')])
! Existence error in argument 1 of absolute_file_name/3
! file extension('counter/counter') does not exist
! goal: absolute_file_name(extension('counter/counter'),_23225,[access(exist),file_type(source),relative_to('/builds/stups/prob/prolog_doc_gen/prolog-Doc/prob_prolog/src/kernel_objects.pl')])
! Existence error in argument 1 of absolute_file_name/3
! file kodkodsrc(kodkod) does not exist
! goal: absolute_file_name(kodkodsrc(kodkod),_16683,[access(exist),file_type(source),relative_to('/builds/stups/prob/prolog_doc_gen/prolog-Doc/prob_prolog/src/b_interpreter.pl')])
! Existence error in argument 1 of absolute_file_name/3
! file extension('counter/counter') does not exist
! goal: absolute_file_name(extension('counter/counter'),_18499,[access(exist),file_type(source),relative_to('/builds/stups/prob/prolog_doc_gen/prolog-Doc/prob_prolog/src/succeed_max.pl')])
! Existence error in argument 1 of absolute_file_name/3
! file extension('probhash/probhash') does not exist
! goal: absolute_file_name(extension('probhash/probhash'),_20529,[access(exist),file_type(source),relative_to('/builds/stups/prob/prolog_doc_gen/prolog-Doc/prob_prolog/src/value_persistance.pl')])
* Non-determinate: specfile:b_mode/0 (clause 1)
* This clause contains a disjunction not forced to be deterministic.
* Non-determinate: specfile:z_mode/0 (clause 1)
* This clause contains a disjunction not forced to be deterministic.
* Non-determinate: specfile:eventb_mode/0 (clause 1)
* This clause contains a disjunction not forced to be deterministic.
* Non-determinate: specfile:csp_with_bz_mode/0 (clause 1)
* Calls nondet predicate specfile:animation_mode/1 .
* Non-determinate: specfile:z_or_tla_minor_mode/0 (clause 1)
* This clause contains a disjunction not forced to be deterministic.
* Non-determinate: specfile:csp_mode/0 (clause 1)
* Calls nondet predicate specfile:animation_mode/1 .
* Non-determinate: specfile:xtl_mode/0 (clause 1)
* Calls nondet predicate specfile:animation_mode/1 .
* Non-determinate: specfile:process_algebra_mode/0 (clause 1)
* Calls nondet predicate specfile:animation_mode/1 .
* Non-determinate: specfile:set_minor_animation_mode_from_file/1 (clause 1)
* Calls nondet predicate specfile:animation_mode/1 .
* Non-determinate: specfile:currently_opened_file/1 (clause 1)
* Calls nondet predicate specfile:currently_opened_file_status/2 .
* Non-determinate: specfile:b_absolute_file_name_relative_to_opened_file/2 (clause 1)
* Calls nondet predicate specfile:currently_opened_file_status/2 .
* Non-determinate: specfile:state_corresponds_to_set_up_constants_only/2 (clause 1)
* Calls nondet predicate specfile:animation_mode/1 .
* Non-determinate: specfile:state_corresponds_to_set_up_constants/2 (clause 6)
* Calls nondet predicate specfile:animation_mode/1 .
* Non-determinate: specfile:state_corresponds_to_set_up_constants/2 (clause 7)
* Calls nondet predicate specfile:animation_mode/1 .
* Non-determinate: specfile:specfile_trans/6 (clause 1)
* Calls nondet predicate specfile:animation_mode/1 .
! Existence error in argument 1 of absolute_file_name/3
! file probsrc(avl_tools) does not exist
! goal: absolute_file_name(probsrc(avl_tools),_111595,[access(exist),file_type(source),relative_to('/builds/stups/prob/prolog_doc_gen/prolog-Doc/prob_prolog/src/state_packing.pl')])
! Existence error in argument 1 of absolute_file_name/3
! file probsrc(btypechecker) does not exist
! goal: absolute_file_name(probsrc(btypechecker),_261,[access(exist),file_type(source),relative_to('/builds/stups/prob/prolog_doc_gen/prolog-Doc/prob_prolog/src/specfile.pl')])

Name: assertz/1
Name: true
Name: animation_minor_mode/1	dynamic predicate
Name: ->/3

Name: recursion_detection_enabled_aux/3	Module: b_ast_cleanup
Name: tcltk_analyse_assertions/3	Module: predicate_evaluator
Name: eventb_mode/0	Module: specfile
Name: tcltk_print_node_for_dot/2	Module: visualize_graph
Name: xtl_mode/0	Module: specfile
Name: perform_static_analyses_if_necessary/1	Module: ltl
Name: print_state/1	Module: translate
Name: print_overall_header/0	Module: fdr_csp_generator
Name: get_specification_description/2	Module: specfile
Name: html_info/3	Module: graphical_state_viewer_images
Name: typecheck_ap/3	Module: ltl_tools
Name: do_machine_consistency_check/0	Module: bmachine
Name: write_state/2	Module: b_show_history
Name: open_search/12	Module: model_checker
Name: b_get_set_pref_definition/4	Module: pref_definitions
Name: tcltk_can_react_to_item_right_click/2	Module: graphical_state_viewer_images
Name: specfile_possible_trans_name/2	Module: specfile
Name: specfile_possible_trans_name_for_successors/2	Module: specfile
Name: type_check_csp_and_b/0	Module: specfile
Name: b_or_z_mode/0	Module: specfile
Name: process_algebra_mode/0	Module: specfile
Name: tcltk_react_to_item_drag/2	Module: graphical_state_viewer_images
Name: node_satisfies_goal/1	Module: model_checker
Name: explore_state_space/5	Module: state_space_explorer
Name: find_trace_to_initial_state/2	Module: state_space
Name: tcltk_can_react_to_item_drag/3	Module: graphical_state_viewer_images
Name: get_animation_images/1	Module: graphical_state_viewer_images
Name: extract_op_name/2	Module: prob2_interface
Name: disabled_operations_stats/1	Module: pge_algo
Name: z_mode/0	Module: specfile
Name: convert_state_to_string/2	Module: visualize_graph
Name: filter_op/5	Module: eclipse_interface
Name: parse_preds_exprs/1	Module: ltl_tools
Name: specfile_trans/6	Module: specfile
Name: get_refused_set/2	Module: refinement_checker
Name: typecheck_tp/3	Module: ltl_tools
Name: get_tp_specification/2	Module: ltl_fairness
Name: write_tran/0	Module: fdr_csp_generator
Name: get_disabled_action_by_keep/3	Module: pge_algo
Name: get_animation_image_numbers/1	Module: graphical_state_viewer_images
Name: conversion_check/1	Module: translate
Name: b_get_definition_string_from_spec/3	Module: pref_definitions
Name: tcltk_get_image_list/6	Module: graphical_state_viewer_images
Name: set_minor_animation_mode_from_file/1	Module: specfile
Name: impl_trans_term_all1/2	Module: ltl
Name: get_internal_representation/3	Module: specfile
Name: get_language_mode/1	Module: translate
Name: react_to_item_right_click/6	Module: graphical_state_viewer_images
Name: check_ap_at_state/2	Module: safety_mc
Name: pp_any_state/4	Module: translate
Name: csp_with_bz_mode/0	Module: specfile
Name: get_animation_image_grid/6	Module: graphical_state_viewer_images
Name: html_print_animation_image_grid/3	Module: graphical_state_viewer_images
Name: b_mode/0	Module: specfile
Name: csp_mode/0	Module: specfile
Name: ref_generate_label/2	Module: refinement_checker
Name: partial_i_transition/3	Module: specfile
Name: find_initialised_states/1	Module: state_space
Name: create_action_argument/2	Module: ltl_fairness
Name: property/2	Module: specfile
Name: compute_heuristic_function_for_state_id/2	Module: state_space_exploration_modes
Name: state_corresponds_to_set_up_constants/2	Module: specfile
Name: start_mc_safety_property/3	Module: safety_mc
Name: get_reduced_refused_set/2	Module: refinement_checker
Name: extract_op_tuple/4	Module: prob2_interface
Name: get_ltl_formula_strings/2	Module: ltl
Name: state_corresponds_to_set_up_constants_only/2	Module: specfile
Name: get_react_to_item_right_click_options/4	Module: graphical_state_viewer_images
Name: pp_value/4	Module: translate

Name: classical_b_mode/0	Module: specfile
Name: translate_b_operation_call/4	Module: translate
Name: translate_event_with_target_id2/5	Module: translate

Name: =/2
Name: true
Name: ->/3
Name: animation_mode/1	Module: specfile
Name: ->/2

Name: state_corresponds_to_initialised_b_machine/1	Module: specfile
Name: is_initialised_state/1	Module: prob2_interface
Name: send_definitions/1	Module: parsercall
Name: gen_state_table/3	Module: visb_visualiser
Name: check_and_adapt_trace_step/5	Module: b_intelligent_trace_replay
Name: is_a_reset_operation/1	Module: b_trace_checking
Name: get_machine_operation_infos_typed/1	Module: prob2_interface
Name: perform_initialisation/0	Module: b_trace_checking
Name: get_ltl_lang_spec/1	Module: parsercall
Name: get_animation_expression_label_and_value/3	Module: graphical_state_viewer_images
Name: get_local_states_for_operation_transition/4	Module: specfile
Name: filter_elementary_prop/2	Module: visualize_graph
Name: max_operations_zero_for_operation/1	Module: specfile
Name: get_spec_identifiers2/1	Module: prob2_interface
Name: tcltk_check_sequence_from_file2/2	Module: b_trace_checking
Name: get_possible_event/1	Module: specfile
Name: state_corresponds_to_fully_setup_b_machine/1	Module: specfile
Name: command_unavailable/2	Module: meta_interface
Name: pad_text_frame_items/2	Module: graphical_state_viewer_images
Name: get_animation_image_source_file/2	Module: bmachine
Name: get_definitions/1	Module: parsercall
Name: get_machine_operation_names/1	Module: prob2_interface
Name: getAllOperations/1	Module: eclipse_interface
Name: print_current_state/0	Module: prob_cli
Name: visb_current_state_can_be_visualised/0	Module: visb_visualiser
Name: b_syntax_available_for_source/0	Module: specfile
Name: state_corresponds_to_initialised_b_machine/2	Module: specfile
Name: get_operation_description/2	Module: specfile
Name: state_corresponds_to_set_up_constants/2	Module: specfile
Name: heuristic_function_active/0	Module: state_space_exploration_modes
Name: state_corresponds_to_fully_setup_b_machine/2	Module: specfile
Name: b_get_operation_typed_results/2	Module: b_intelligent_trace_replay
Name: initialise_specification/0	Module: prob2_interface
Name: get_possible_language_specific_top_level_event/3	Module: specfile
Name: get_operation_description_for_transition/4	Module: specfile
Name: reset_goal_for_model_checking/0	Module: prob2_interface
Name: property/2	Module: specfile
Name: get_current_keywords/2	Module: tools_matching
Name: print_transition_list_prolog/2	Module: b_trace_checking
Name: add_visb_event/8	Module: visb_visualiser
Name: we_need_only_static_assertions/1	Module: prob_cli
Name: state_corresponds_to_set_up_constants_only/2	Module: specfile
Name: update_preferences_from_spec/0	Module: prob2_interface
Name: retract_open_node/1	Module: state_space
Name: get_transition_groups/1	Module: ltsmin
Name: perform_aux/8	Module: visb_visualiser
Name: init_enabling_degree_info/2	Module: coverage_statistics
Name: get_feasible_event/1	Module: specfile
Name: update_preferences_from_spec/1	Module: prob2_interface
Name: b_get_operation_typed_paras/2	Module: b_intelligent_trace_replay
Name: compute_operation_updates_on_expanded_store/6	Module: specfile
Name: tcltk_get_state/1	Module: tcltk_interface
Name: get_expanded_bstate/2	Module: visb_visualiser
Name: get_machine_operation_infos/1	Module: prob2_interface
Name: illegal_json_binding_type/4	Module: b_intelligent_trace_replay
Name: is_constants_set_up_state/1	Module: prob2_interface
Name: initialise_operation_not_yet_covered/0	Module: state_space
Name: treat_state_for_min_max/1	Module: coverage_statistics
Name: get_dest_store/2	Module: b_intelligent_trace_replay
Name: b_sorted_b_definition_prefixed/4	Module: bmachine
Name: get_animation_string/2	Module: graphical_state_viewer_images
Name: currently_opened_specification_name/1	Module: specfile
Name: reset_node_hit/2	Module: coverage_statistics
Name: get_animation_expression_value/2	Module: visualize_graph
Name: typecheck_tp/3	Module: ltl_tools
Name: is_var_binding/1	Module: visb_visualiser

Name: csp_b_possible_trans_name/2	Module: specfile
Name: specfile_possible_trans_name/2	Module: specfile
Name: specfile_possible_trans_name_for_successors/2	Module: specfile

Name: =/2
Name: ajoin/2	Module: foo_error
Name: unfixed_deferred_set/1	Module: b_global_sets
Name: ->/3
Name: inferred_maximum_global_set_cardinality/2	Module: b_global_sets
Name: not/1
Name: inferred_minimum_global_set_cardinality/2	Module: b_global_sets
Name: \=/2
Name: true
Name: b_fd_card/2	Module: b_global_sets
Name: b_global_set/1	Module: b_global_sets
Name: get_preference/2	Module: foo_error

Name: elementary_prop/2	Module: specfile
Name: ground/1
Name: not/1
Name: member/2
Name: debug_mode/1	Module: debug
Name: =../2
Name: b_preference_par/3	Module: specfile
Name: !

Name: b_transition_for_csp/9	Module: specfile
Name: csp_and_b_transition/5	Module: specfile
Name: re_execute_transition/3	Module: tcltk_interface
Name: i_transition/6	Module: specfile

Name: =/2
Name: remove_infos_from_prepared_state/2	Module: specfile
Name: =../2
Name: tuple_of/3	Module: bsets_clp
Name: ->/3
Name: generate_b_operationargs_from_csp/2	Module: foo_error
Name: !
Name: try_lookup_value_in_store_and_global_sets/3	Module: foo_error
Name: expand_const_and_vars_to_full_store/2	Module: specfile
Name: b_is_constant/1	Module: bmachine
Name: b_is_variable/1	Module: bmachine
Name: b_trans/5	Module: specfile
Name: get_preference/2	Module: foo_error
Name: build_up_b_operation_for_csp/3	Module: specfile

Name: =/2
Name: ->/3
Name: safe_univ/2	Module: foo_error
Name: generate_args/6	Module: specfile
Name: b_get_machine_operation/4	Module: bmachine
Name: nonvar/1

Name: add_internal_error/2	Module: foo_error
Name: !
Name: add_error/4	Module: foo_error
Name: true
Name: type_ok/2	Module: specfile
Name: ->/3

Name: RECURSIVE_CALL/2	Module: specfile
Name: type_ok/2	Module: specfile
Name: !

Name: fail
Name: add_error/3	Module: foo_error
Name: def_get_texpr_id/2	Module: foo_error
Name: RECURSIVE_CALL/3	Module: specfile
Name: !

Name: check_type/3	Module: specfile
Name: get_texpr_type/2	Module: foo_error

Name: true
Name: classical_minor_mode/1	Module: specfile
Name: animation_minor_mode/1	dynamic predicate
Name: ->/3
Name: b_mode/0	Module: specfile

Name: keyword_clash/1	Module: bmachine_static_checks
Name: check_record_construction_ok/2	Module: record_detection
Name: cache_is_applicable/0	Module: value_persistance
Name: get_current_keywords/2	Module: tools_matching
Name: minor_mode_to_check/0	Module: bmachine
Name: detect_partial_records_for_field/1	Module: visb_visualiser
Name: is_dummy_machine_name/2	Module: bmachine_static_checks

Name: succeed_max_call_id/3	Module: succeed_max
Name: choose_loaded_solution/3	Module: specfile
Name: =/2
Name: !
Name: load_constants/2	Module: value_persistance

Name: create_initialisation_operation/2	Module: specfile
Name: succeed_max_call_id/3	Module: succeed_max
Name: empty_state/1	Module: store
Name: get_max_enablings_for_init/3	Module: specfile
Name: b_machine_has_constants_or_properties	Module: foo_error
Name: not/1
Name: =/2
Name: exclude/3	Module: foo_error
Name: get_preference/2	Module: foo_error
Name: ->/3
Name: create_setup_constants_operation/3	Module: specfile
Name: compute_constants/3	Module: specfile
Name: visited_expression/2	Module: state_space
Name: preference/2	Module: preferences
Name: store_updates_and_normalise/3	Module: store
Name: compute_operation_updates_on_expanded_store/6	Module: specfile
Name: RECURSIVE_CALL/6	Module: specfile
Name: prepare_state_for_specfile_trans/3	Module: specfile

Name: b_trans/5	Module: specfile
Name: execute_custom_operation/4	Module: eclipse_interface
Name: prob2_exec_custom_aux/4	Module: prob2_interface

Name: succeed_max_call_id/3	Module: succeed_max
Name: get_max_enablings_per_operation/3	Module: specfile

Name: compute_operation_on_expanded_store2/6	Module: specfile
Name: !
Name: extract_full_store/2	Module: specfile
Name: compute_operation_on_expanded_store_cache/6	Module: foo_error
Name: get_max_enablings_per_operation/3	Module: specfile
Name: b_or_z_mode/0	Module: specfile
Name: \=/2
Name: get_preference/2	Module: foo_error

Name: get_local_states_for_operation_transition/4	Module: specfile
Name: create_sorted_store/4	Module: b_intelligent_trace_replay

Name: add_constants_to_state_space/5	Module: cbc_path_solver
Name: compute_operation_effect_max/6	Module: specfile

Name: cspm_transition/3	Module: foo_error
Name: hide_csp_event/3	Module: specfile
Name: b_transition_for_csp/9	Module: specfile
Name: length/2
Name: csp_transition_for_b/5	Module: foo_error
Name: !
Name: =/2
Name: csp_initialisation_for_b/1	Module: foo_error
Name: b_trans/5	Module: specfile
Name: ->/3

prob_prolog/src/specfile.pl

Modules

Predicates of specfile

Module Information

Dynamic Predicates: animation_mode/1 animation_minor_mode/1 currently_opened_file_status/2

1292 Lines

145 Predicates

Imported Modules: tools module_information lists debug b_interpreter preferences self_check error_manager translate bmachine bsyntaxtree xtl_interface random debug preferences

77 Exports

46 specified Imports

Predicates:

Name: b_possible_trans_name/2	Module: specfile
Name: =/2
Name: !
Name: b_machine_has_constants_or_properties	Module: foo_error
Name: ->/3

Name: get_refused_set3/3	Module: refinement_checker
Name: reset_refine_spec/0	Module: refinement_checker
Name: parse_single_csp_expression/3	Module: haskell_csp
Name: pp_csp_value/3	Module: translate
Name: generate_bound_long_state/2	Module: ltsmin
Name: tcltk_analyse_assertions/3	Module: predicate_evaluator
Name: get_operation_read_projection_infos/6	Module: b_operation_cache
Name: state_corresponds_to_initialised_b_machine/2	Module: specfile
Name: get_ltl_lang_spec/1	Module: parsercall
Name: put_may_write_matrix/2	Module: msg_interop
Name: get_init/2	Module: ltsmin
Name: state_corresponds_to_set_up_constants/2	Module: specfile
Name: print_state/1	Module: translate
Name: state_corresponds_to_initialised_b_machine/1	Module: specfile
Name: get_transition_groups/1	Module: ltsmin
Name: fdr_translate_event/2	Module: fdr_csp_generator
Name: preprocess_tp/2	Module: ltl_tools
Name: get_language_mode/1	Module: translate
Name: translate_event2/3	Module: translate
Name: state_corresponds_to_set_up_constants_only/2	Module: specfile
Name: patch_matrix/2	Module: ltsmin
Name: initialise_operation_not_yet_covered/0	Module: state_space
Name: translate_action/2	Module: ltl_translate

Name: html_print_history/2	Module: graphical_state_viewer_images
Name: print_state_from_id/1	Module: refinement_checker
Name: print_overall_header/0	Module: fdr_csp_generator
Name: nested_print_sequent_as_classicalb_aux/6	Module: translate
Name: cb_test_cases_step/5	Module: sap
Name: currently_opened_specification_name/1	Module: specfile
Name: parse_single_csp_expression/3	Module: haskell_csp
Name: write_version_info/2	Module: visb_visualiser
Name: spec_file_has_been_successfully_loaded/0	Module: specfile
Name: print_transition_list_json/3	Module: b_trace_checking

Name: get_modulename_filename/2	Module: foo_error
Name: currently_opened_file/1	Module: specfile
Name: b_machine_name/1	Module: bmachine
Name: b_or_z_mode/0	Module: specfile
Name: ->/3

Name: tcltk_save_history_as_trace_file/3	Module: b_trace_checking
Name: check_model_name/1	Module: b_intelligent_trace_replay
Name: print_transition_list_json/3	Module: b_trace_checking

Name: translate_bexpression_with_limit/3	Module: foo_error
Name: create_texpr/4	Module: foo_error
Name: create_value/3	Module: specfile
Name: get_relation_element/3	Module: specfile
Name: =/2
Name: true
Name: dom_range_type/3	Module: specfile
Name: var_cst_type/2	Module: specfile
Name: ->/3
Name: nonvar/1
Name: simple/1

Name: elementary_var_prop/3	Module: specfile
Name: elementary_fun_prop/3	Module: specfile
Name: !
Name: get_preference/2	Module: foo_error
Name: =/2
Name: show_avl_set/1	Module: specfile
Name: ->/3
Name: var/1

Name: =/2
Name: translate_bvalue_with_type_and_limit/4	Module: foo_error
Name: var_cst_type/2	Module: specfile
Name: ->/3
Name: translate_bvalue/2	Module: foo_error
Name: translate_bvalue_with_tlatype/3	Module: foo_error
Name: identifier_has_tla_type/2	Module: specfile
Name: !
Name: animation_minor_mode/1	dynamic predicate

Name: load_default_visb_file_if_necessary/0	Module: visb_visualiser
Name: int_power2/5	Module: kernel_objects
Name: always_wd/1	Module: bsyntaxtree
Name: command_unavailable/2	Module: meta_interface
Name: safe_int_power/5	Module: kernel_objects
Name: always_not_wd_top/1	Module: bsyntaxtree
Name: check_uses_implementable_integers/1	Module: b_interpreter
Name: create_top_level_wd_po/7	Module: well_def_analyser

Name: b_test_boolean_expression_for_ground_state/5	Module: b_interpreter
Name: property/2	Module: specfile
Name: find_successor_state/4	Module: b_trace_checking
Name: compute_marker_for_state/2	Module: symmetry_marker
Name: b_transition_for_csp/9	Module: specfile
Name: permute_state2/2	Module: state_permuter
Name: get_state_infos/5	Module: b_operation_cache
Name: cb_get_initialised_state/2	Module: sap
Name: get_state2/3	Module: prob2_interface
Name: get_state_for_predicate/2	Module: prob2_interface
Name: perform_one_operation_in_sequence/2	Module: b_trace_checking
Name: print_uml_actors/2	Module: uml_generator