Dynamic Predicates: obtain_action_enabling_conditions/0 simplify_enabling_condition/1

388 Lines

27 Predicates

Imported Modules: tools bsyntaxtree debug error_manager lists ordsets

8 Exports

18 specified Imports

Imports	Exports
Name: module_info/2 Module: module_information Name: b_top_level_operation/1 Module: bmachine Name: b_get_machine_operation_for_animation/6 Module: bmachine Name: b_get_machine_operation_for_animation/4 Module: bmachine Name: b_get_machine_operation/6 Module: bmachine Name: bmachine_is_precompiled/0 Module: bmachine Name: construct_optimized_exists/3 Module: b_interpreter_components Name: construct_optimized_exists/4 Module: b_interpreter_components Name: animation_minor_mode/1 Module: specfile Name: external_subst_enabling_condition/3 Module: external_functions Name: clean_up/3 Module: b_ast_cleanup Name: create_implication/3 Module: bsyntaxtree Name: b_top_level_operation/1 Module: bmachine Name: print_bexpr/1 Module: translate Name: conjunction_to_list/2 Module: bsyntaxtree Name: find_identifier_uses/3 Module: bsyntaxtree Name: safe_create_texpr/3 Module: bsyntaxtree Name: always_well_defined/1 Module: bsyntaxtree	Name: get_quantified_operation_enabling_condition/4 Name: get_operation_enabling_condition/7 Name: get_unsimplified_operation_guard/2 Name: get_unsimplified_operation_enabling_condition/5 Name: get_simplified_operation_enabling_condition/5 Name: get_operation_propositional_guards/3 Name: get_operation_propositional_guards/6 Name: get_substitution_enabling_condition/4

Imports

Exports

Name: module_info/2

Module: module_information

Name: b_top_level_operation/1

Module: bmachine

Name: b_get_machine_operation_for_animation/6

Module: bmachine

Name: b_get_machine_operation_for_animation/4

Module: bmachine

Name: b_get_machine_operation/6

Module: bmachine

Name: bmachine_is_precompiled/0

Module: bmachine

Name: construct_optimized_exists/3

Module: b_interpreter_components

Name: construct_optimized_exists/4

Module: b_interpreter_components

Name: animation_minor_mode/1

Module: specfile

Name: external_subst_enabling_condition/3

Module: external_functions

Name: clean_up/3

Module: b_ast_cleanup

Name: create_implication/3

Module: bsyntaxtree

Name: b_top_level_operation/1

Module: bmachine

Name: print_bexpr/1

Module: translate

Name: conjunction_to_list/2

Module: bsyntaxtree

Name: find_identifier_uses/3

Module: bsyntaxtree

Name: safe_create_texpr/3

Module: bsyntaxtree

Name: always_well_defined/1

Module: bsyntaxtree

Name: get_quantified_operation_enabling_condition/4

Name: get_operation_enabling_condition/7

Name: get_unsimplified_operation_guard/2

Name: get_unsimplified_operation_enabling_condition/5

Name: get_simplified_operation_enabling_condition/5

Name: get_operation_propositional_guards/3

Name: get_operation_propositional_guards/6

Name: get_substitution_enabling_condition/4

Predicates

Predicates:

construct_select/5

definitely_not_empty/2

disjoin_ifs/4

get_disjunction_of_enabling_conditions/4

get_guards/6

get_if_condition/5

get_operation_enabling_condition/7

get_operation_enabling_condition2/4

get_operation_enabling_condition3/4

get_operation_enabling_for_event_b_actions/5

get_operation_guards_aux/5

get_operation_propositional_guards/3

get_operation_propositional_guards/6

get_parameter_independent_guards/4

get_quantified_operation_enabling_condition/4

get_simplified_operation_enabling_condition/5

get_substitution_enabling_condition/4

get_unsimplified_operation_enabling_condition/5

get_unsimplified_operation_guard/2

get_variant_pred/2

get_variant_pred_aux/2

has_no_enabling_condition/1

l_get_parameter_independent_guards/5

obtain_action_enabling_conditions/0

set_obtain_action_enabling_conditions/1

set_simplify_enabling_condition/1

simplify_enabling_condition/1

construct_select/5

definitely_not_empty/2

disjoin_ifs/4

get_disjunction_of_enabling_conditions/4

get_guards/6

get_if_condition/5

get_operation_enabling_condition/7

Description:
nonvar(OpName), %% I am not sure why this test is here ??
print(getting_enabling(OpName,GetAct)),nl,%%

get_operation_enabling_condition2/4

get_operation_enabling_condition2(precondition(PreCond,TBody),Res,BecomesSuchVars,IsPrecise) :- !, % PRE
    get_substitution_enabling_condition(TBody,RC,BecomesSuchVars,IsPrecise),
    conjunct_predicates_with_pos_info(PreCond,RC,Res).

get_operation_enabling_condition2(assertion(_PreCond,TBody),Res,BecomesSuchVars,IsPrecise) :- !, % ASSERT
    get_substitution_enabling_condition(TBody,Res,BecomesSuchVars,IsPrecise).

get_operation_enabling_condition2(witness_then(_PreCond,TBody),Res,BecomesSuchVars,IsPrecise) :- !, % WITNESS
    get_substitution_enabling_condition(TBody,Res,BecomesSuchVars,IsPrecise).

get_operation_enabling_condition2(block(TBody),Res,BecomesSuchVars,IsPrecise) :- !, % BEGIN ... END
    get_substitution_enabling_condition(TBody,Res,BecomesSuchVars,IsPrecise).

get_operation_enabling_condition2(choice(ChoiceList),Res,BecomesSuchVars,IsPrecise) :- !, % CHOICE ... OR ...
    get_disjunction_of_enabling_conditions(ChoiceList,Res,BecomesSuchVars,IsPrecise).

get_operation_enabling_condition2(var(_Parameters,TBody),Res,BecomesSuchVars,IsPrecise) :- !, % VAR
    % should the Parameters be added somewhere ? In principle the enabling condition should always be true, as we have a low-level construct
    get_substitution_enabling_condition(TBody,Res,BecomesSuchVars,IsPrecise).

get_operation_enabling_condition2(sequence([TBody1|Tail]),Res,BecomesSuchVars,IsPrecise) :- !, % ;
    get_substitution_enabling_condition(TBody1,Res,BecomesSuchVars,IsPrecise),
    (nonvar(IsPrecise) -> true
    ; maplist(has_no_enabling_condition,Tail) -> true
    ; IsPrecise = imprecise
    ),
    (debug_mode(on), nonvar(IsPrecise)
    -> print(ignoring_potential_enabling_condition_in_tail_of_sequence),nl ; true).

get_operation_enabling_condition2(lazy_let_subst(ID,ExprOrPred,TBody),Res,BecomesSuchVars,IsPrecise) :- !,
    Res = b(lazy_let_pred(ID,ExprOrPred,BodyRes),pred,[]),
    get_substitution_enabling_condition(TBody,BodyRes,BecomesSuchVars,IsPrecise).

get_operation_enabling_condition2(let(Parameters,PreCond,TBody),Res,BecomesSuchVars,IsPrecise) :- !, % LET
    % for the moment: treat like ANY, but we could avoid introducing existential quantifier ?!
    get_operation_enabling_condition2(any(Parameters,PreCond,TBody),Res,BecomesSuchVars,IsPrecise).

get_operation_enabling_condition2(any(Parameters,PreCond,TBody),Res,BecomesSuchVars,IsPrecise) :- !, % ANY
    get_substitution_enabling_condition(TBody,RC,BecomesSuchVars,IsPrecise),
    conjunct_predicates_with_pos_info(PreCond,RC,Res1),
    simplify_enabling_condition(Simplify),
    construct_optimized_exists(Parameters,Res1,Res,Simplify).

get_operation_enabling_condition2(select_when(PreCond,TBody),Res,BecomesSuchVars,IsPrecise) :- !,
    get_substitution_enabling_condition(TBody,RC,BecomesSuchVars,IsPrecise),
    conjunct_predicates_with_pos_info(PreCond,RC,Res).

get_operation_enabling_condition2(select(ListOfWhens),Res,BecomesSuchVars,IsPrecise) :- !,
    get_disjunction_of_enabling_conditions(ListOfWhens,Res,BecomesSuchVars,IsPrecise).

get_operation_enabling_condition2(select(ListOfWhens,Else),Res,BecomesSuchVars,IsPrecise) :- !,
    get_texpr_exprs(ListOfWhens,ListOfSelectWhens),
    maplist(get_operation_enabling_condition3(IsPrecise),ListOfSelectWhens,Res1,BecomesSuchVars1),
    get_substitution_enabling_condition(Else,ResElse,ElseBecomesSuchVars,IsPrecise),
    disjunct_predicates([ResElse|Res1],Res),
    append([ElseBecomesSuchVars|BecomesSuchVars1],BecomesSuchVars).

get_operation_enabling_condition2(parallel([TH|T]),Res,BecomesSuchVars,IsPrecise) :- !,
    get_substitution_enabling_condition(TH,E1,BecomesSuchVarsH,IsPrecise),
    (T=[] -> Res=E1, BecomesSuchVarsH=BecomesSuchVars
    ; get_operation_enabling_condition2(parallel(T),E2,BecomesSuchVarsT,IsPrecise),
    append(BecomesSuchVarsH,BecomesSuchVarsT,BecomesSuchVars),
    conjunct_predicates_with_pos_info(E1,E2,Res)
).

get_operation_enabling_condition2(becomes_element_of(_LHS,RHS),Res,[],_Precise) :-
    obtain_action_enabling_conditions,
    get_texpr_expr(RHS,RHSExpr),get_texpr_type(RHS,Type),!,
    (simplify_enabling_condition(true),
    definitely_not_empty(RHSExpr,Type)
    -> %print(def_not_empty(RHSExpr)),nl,
    create_texpr(truth,pred,[],Res)
    ; create_texpr(empty_set,Type,[],EmptySet),
    safe_create_texpr(not_equal(RHS,EmptySet),pred,Res2),
    %print(not_equal_empty(RHSExpr,Type)),nl,
    clean_up(Res2,[],Res)
).

get_operation_enabling_condition2(becomes_such(Vars,Condition),Res,Vars,_Precise) :- % Vars : (Condition)
    % example x: (x$0 >= 1 & x=x$0+1)
    obtain_action_enabling_conditions,!,
    simplify_enabling_condition(Simplify),
    construct_optimized_exists(Vars,Condition,Res1,Simplify),
    %translate:print_bexpr(Res1),nl,
    % e.g, for example above we have #x.(x$0 >= 1 & x=x$0+1) -> x$0 >= 1
    % now rename $0 variables to act on current state to obtain the condition:
    findall(rename(BeforeId,Id),
    (member(b(identifier(Id),_,Infos),Vars),
    member(before_substitution(_,BeforeId),Infos)),
    RenameList),
    rename_bt(Res1,RenameList,Res). % for example above: Res is x >= 1

get_operation_enabling_condition2(rlevent(_Name,_Section,_Status,_Params,Guard,_Theorems,Actions,_VWitnesses,_PWitnesses,_Unmod,_AbstractEvents),Res,BecomesSuchVars,IsPrecise) :- !,
    %print(actions(Actions)),nl,
    % TO DO: have a look at get_full_eventb_guard. Do we want to recurse through the abstractions ?
    (obtain_action_enabling_conditions
    -> get_operation_enabling_for_event_b_actions(Actions,Guard,Res,BecomesSuchVars,IsPrecise)
    ; Res=Guard,BecomesSuchVars=[]).

get_operation_enabling_condition2(case(A,_,_),Truth,[],imprecise) :- !, % CASE is now translated to LET + IF-THEN-ELSE in b_ast_cleanup
    print('Not computing enabling for CASE: '), translate:print_bexpr(A),nl,
    create_texpr(truth,pred,[],Truth).

get_operation_enabling_condition2(while(_,_,_,_),Truth,[],imprecise) :- !,
    debug_println(9,enabling_for_while_assumed_true),
    create_texpr(truth,pred,[],Truth).

get_operation_enabling_condition2(if(IfList),Res,BecomesSuchVars,IsPrecise) :- !,
    maplist5(get_if_condition(IsPrecise),IfList,Tests,Conds,BecomesSuchVars1),
    append(BecomesSuchVars1,BecomesSuchVars),
    (member(X,Conds), \+ is_truth(X)
    -> disjoin_ifs(Tests,Conds,[],L),
    conjunct_predicates_with_pos_info(L,Res)
    ; create_texpr(truth,pred,[],Res) % all branches have no enabling condition
).

get_operation_enabling_condition2(external_subst_call(Pred,Args),Res,[],_Precise) :-
    external_subst_enabling_condition(Pred,Args,Cond),!, Res=Cond.

get_operation_enabling_condition2(operation_call(Operation,_OpCallResults,OpCallParas),Res,BecomeSuchVars,IsPrecise) :-
    def_get_texpr_id(Operation,op(OperationName)), TopLevel=false,
    b_get_machine_operation_for_animation(OperationName,_OpResults,OpParameters,Body,_OType,TopLevel),
    bsyntaxtree:replace_ids_by_exprs(Body,OpParameters,OpCallParas,Body2),
    !,
    %print(get_enabling_for_opcall),nl,translate:print_subst(Body2),nl,
    get_substitution_enabling_condition(Body2,Res,BecomeSuchVars,IsPrecise).

get_operation_enabling_condition2(Subst,Truth,[],_Prcise) :- has_no_enabling_condition(Subst),!,
    create_texpr(truth,pred,[],Truth).

get_operation_enabling_condition2(X,Truth,[],imprecise) :- %print(cannot_obtain(X)),nl,
    (obtain_action_enabling_conditions
    -> functor(X,F,A),debug_println(9,cannot_obtain_enabling(F/A,X)) ; true),
    create_texpr(truth,pred,[],Truth).

get_operation_enabling_condition3/4

get_operation_enabling_for_event_b_actions/5

get_operation_guards_aux/5

get_operation_propositional_guards/3

get_operation_propositional_guards/6

get_parameter_independent_guards/4

get_quantified_operation_enabling_condition/4

get_simplified_operation_enabling_condition/5

get_substitution_enabling_condition/4

get_unsimplified_operation_enabling_condition/5

get_unsimplified_operation_guard/2

get_variant_pred/2

get_variant_pred_aux/2

has_no_enabling_condition/1

l_get_parameter_independent_guards/5

obtain_action_enabling_conditions/0

Dynamic: true

set_obtain_action_enabling_conditions/1

set_simplify_enabling_condition/1

simplify_enabling_condition/1

Dynamic: true

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 user:environ/2
! procedure user:environ/2 does not exist
! goal: user:environ(prob_avl_custom,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(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),_58323,[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'),_27481,[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),_37685,[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),_36021,[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),_35597,[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(tools) does not exist
! goal: absolute_file_name(probsrc(tools),_124437,[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 covsrc(coverage_tools_annotations) does not exist
! goal: absolute_file_name(covsrc(coverage_tools_annotations),_152999,[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),_152999,[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),_155143,[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(closures) does not exist
! goal: absolute_file_name(probsrc(closures),_161263,[access(exist),file_type(source),relative_to('/builds/stups/prob/prolog_doc_gen/prolog-Doc/prob_prolog/src/memoization.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'),_166673,[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),_165909,[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),_165909,[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),_167205,[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),_166531,[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),_167525,[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),_161263,[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: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),_184291,[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),_178597,[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),_161685,[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 extension('counter/counter') does not exist
! goal: absolute_file_name(extension('counter/counter'),_174199,[access(exist),file_type(source),relative_to('/builds/stups/prob/prolog_doc_gen/prolog-Doc/prob_prolog/src/succeed_max.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),_174053,[access(exist),file_type(source),relative_to('/builds/stups/prob/prolog_doc_gen/prolog-Doc/prob_prolog/src/xtl_interface.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'),_177333,[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 extension('probhash/probhash') does not exist
! goal: absolute_file_name(extension('probhash/probhash'),_174199,[access(exist),file_type(source),relative_to('/builds/stups/prob/prolog_doc_gen/prolog-Doc/prob_prolog/src/value_persistance.pl')])
! Existence error in argument 1 of absolute_file_name/3
! file probsrc(avl_tools) does not exist
! goal: absolute_file_name(probsrc(avl_tools),_174341,[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),_161973,[access(exist),file_type(source),relative_to('/builds/stups/prob/prolog_doc_gen/prolog-Doc/prob_prolog/src/specfile.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'),_161685,[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 kodkodsrc(kodkod) does not exist
! goal: absolute_file_name(kodkodsrc(kodkod),_155143,[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 probsrc(kernel_waitflags) does not exist
! goal: absolute_file_name(probsrc(kernel_waitflags),_152999,[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),_152999,[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),_127713,[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 prob_rewrite_rules(b_ast_cleanup_rewrite_rules) does not exist
! goal: absolute_file_name(prob_rewrite_rules(b_ast_cleanup_rewrite_rules),_124149,[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),_124437,[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(b_state_model_check) does not exist
! goal: absolute_file_name(probsrc(b_state_model_check),_124295,[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(eventhandling) does not exist
! goal: absolute_file_name(probsrc(eventhandling),_124295,[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(bmachine_eventb) does not exist
! goal: absolute_file_name(probsrc(bmachine_eventb),_116897,[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(eventhandling) does not exist
! goal: absolute_file_name(probsrc(eventhandling),_116897,[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),_118703,[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 probsrc(error_manager) does not exist
! goal: absolute_file_name(probsrc(error_manager),_116897,[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: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(bsyntaxtree) does not exist
! goal: absolute_file_name(probsrc(bsyntaxtree),_113763,[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 kodkodsrc(kodkod) does not exist
! goal: absolute_file_name(kodkodsrc(kodkod),_82367,[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 extension('random_permutations/random_permutations') does not exist
! goal: absolute_file_name(extension('random_permutations/random_permutations'),_83091,[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),_81089,[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'),_44855,[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 probsrc(eventhandling) does not exist
! goal: absolute_file_name(probsrc(eventhandling),_39161,[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),_35597,[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 probsrc(custom_explicit_sets) does not exist
! goal: absolute_file_name(probsrc(custom_explicit_sets),_6331,[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 chrsrc(chr_integer_inequality) does not exist
! goal: absolute_file_name(chrsrc(chr_integer_inequality),_8035,[access(exist),file_type(source),relative_to('/builds/stups/prob/prolog_doc_gen/prolog-Doc/prob_prolog/src/b_interpreter_components.pl')])
* Non-determinate: b_operation_guards:get_operation_enabling_condition2/4 (clause 10)
* Calls nondet predicate b_operation_guards:simplify_enabling_condition/1 .
* Non-determinate: b_operation_guards:get_operation_enabling_condition2/4 (clause 16)
* Calls nondet predicate b_operation_guards:simplify_enabling_condition/1 .
* Non-determinate: b_operation_guards:get_operation_enabling_condition2/4 (clause 19)
* Calls nondet predicate b_operation_guards:debug_println/2 .
* Non-determinate: b_operation_guards:get_operation_enabling_condition2/4 (clause 24)
* Calls nondet predicate b_operation_guards:debug_println/2 .
* Non-determinate: b_operation_guards:get_guards/6 (clause 1)
* Indexing cannot distinguish this from clause 2.
* Non-determinate: b_operation_guards:get_guards/6 (clause 2)
* Indexing cannot distinguish this from clause 3.
* Non-determinate: b_operation_guards:get_guards/6 (clause 3)
* Indexing cannot distinguish this from clause 4.

Name: RECURSIVE_CALL/4	Module: b_operation_guards
Name: append/3
Name: create_negation/2	Module: foo_error
Name: create_implication/3	Module: bsyntaxtree
Name: conjunct_predicates_with_pos_info/2	Module: foo_error

Name: append/2	Module: foo_error
Name: disjunct_predicates/2	Module: foo_error
Name: maplist/4	Module: foo_error
Name: get_texpr_exprs/2	Module: foo_error

Name: RECURSIVE_CALL/6	Module: b_operation_guards
Name: =/2
Name: b_get_machine_operation/6	Module: bmachine
Name: def_get_texpr_id/2	Module: foo_error
Name: bmachine_is_precompiled/0	Module: bmachine
Name: get_preference/2	Module: preferences

Name: =/2
Name: var/1
Name: ->/3
Name: get_substitution_enabling_condition/4	Module: b_operation_guards
Name: b_get_machine_operation_for_animation/4	Module: bmachine
Name: set_simplify_enabling_condition/1	Module: b_operation_guards
Name: set_obtain_action_enabling_conditions/1	Module: b_operation_guards

Name: get_quantified_operation_enabling_condition/4	Module: b_operation_guards
Name: b_debug_operation/1	Module: predicate_debugger
Name: get_simplified_operation_enabling_condition/5	Module: b_operation_guards
Name: get_mcdc_coverage_criterion/4	Module: mcdc_coverage
Name: get_guard_with_one_negated/3	Module: eclipse_interface
Name: get_unsimplified_operation_enabling_condition/5	Module: b_operation_guards

b_operation_guards

prob_prolog/src/b_operation_guards.pl

Modules

Predicates of b_operation_guards

Module Information

Dynamic Predicates: obtain_action_enabling_conditions/0 simplify_enabling_condition/1

388 Lines

27 Predicates

Imported Modules: tools bsyntaxtree debug error_manager lists ordsets

8 Exports

18 specified Imports

Predicates:

construct_select/5

definitely_not_empty/2

disjoin_ifs/4

get_disjunction_of_enabling_conditions/4

get_guards/6

get_if_condition/5

get_operation_enabling_condition/7

get_operation_enabling_condition2/4

get_operation_enabling_condition3/4

get_operation_enabling_for_event_b_actions/5

get_operation_guards_aux/5

get_operation_propositional_guards/3

get_operation_propositional_guards/6

get_parameter_independent_guards/4

get_quantified_operation_enabling_condition/4

get_simplified_operation_enabling_condition/5

get_substitution_enabling_condition/4

get_unsimplified_operation_enabling_condition/5

get_unsimplified_operation_guard/2

get_variant_pred/2

get_variant_pred_aux/2

has_no_enabling_condition/1

l_get_parameter_independent_guards/5

obtain_action_enabling_conditions/0

set_obtain_action_enabling_conditions/1

set_simplify_enabling_condition/1

simplify_enabling_condition/1

Determinacy Checker:

Name: create_texpr/4	Module: foo_error
Name: true
Name: debug_println/2	Module: foo_error
Name: functor/3
Name: obtain_action_enabling_conditions/0	Module: b_operation_guards
Name: ->/3
Name: !
Name: has_no_enabling_condition/1	Module: b_operation_guards
Name: get_substitution_enabling_condition/4	Module: b_operation_guards
Name: replace_ids_by_exprs/4	Module: bsyntaxtree
Name: b_get_machine_operation_for_animation/6	Module: bmachine
Name: =/2
Name: def_get_texpr_id/2	Module: foo_error
Name: external_subst_enabling_condition/3	Module: external_functions
Name: conjunct_predicates_with_pos_info/2	Module: foo_error
Name: disjoin_ifs/4	Module: b_operation_guards
Name: is_truth/1	Module: foo_error
Name: not/1
Name: member/2
Name: append/2	Module: foo_error
Name: maplist5/5	Module: foo_error
Name: nl
Name: print_bexpr/1	Module: translate
Name: print/1
Name: get_operation_enabling_for_event_b_actions/5	Module: b_operation_guards
Name: rename_bt/3	Module: foo_error
Name: findall/3
Name: construct_optimized_exists/4	Module: b_interpreter_components
Name: simplify_enabling_condition/1	Module: b_operation_guards
Name: clean_up/3	Module: b_ast_cleanup
Name: safe_create_texpr/3	Module: bsyntaxtree
Name: definitely_not_empty/2	Module: b_operation_guards
Name: get_texpr_type/2	Module: foo_error
Name: get_texpr_expr/2	Module: foo_error
Name: conjunct_predicates_with_pos_info/3	Module: foo_error
Name: append/3
Name: RECURSIVE_CALL/4	Module: b_operation_guards
Name: disjunct_predicates/2	Module: foo_error
Name: maplist/4	Module: foo_error
Name: get_texpr_exprs/2	Module: foo_error
Name: get_disjunction_of_enabling_conditions/4	Module: b_operation_guards
Name: nonvar/1
Name: debug_mode/1	Module: foo_error
Name: maplist/2	Module: foo_error

Name: get_operation_enabling_condition3/4	Module: b_operation_guards
Name: get_substitution_enabling_condition/4	Module: b_operation_guards

Name: append/3
Name: RECURSIVE_CALL/5	Module: b_operation_guards
Name: conjunct_predicates_with_pos_info/3	Module: foo_error
Name: get_substitution_enabling_condition/4	Module: b_operation_guards

Name: get_operation_propositional_guards/3	Module: b_operation_guards
Name: cleanup_post_with_path/8	Module: b_ast_cleanup

Name: nl
Name: print_subst/1	Module: translate
Name: print/1
Name: maplist/2	Module: foo_error
Name: format/2
Name: true
Name: debug_mode/1	Module: foo_error
Name: ->/3
Name: get_operation_guards_aux/5	Module: b_operation_guards
Name: sort/2
Name: append/3
Name: get_texpr_ids/2	Module: foo_error

Name: l_get_parameter_independent_guards/5	Module: b_operation_guards
Name: conjunction_to_list/2	Module: bsyntaxtree

Name: create_or_merge_exists/3	Module: foo_error
Name: get_operation_enabling_condition/7	Module: b_operation_guards

Name: generate_dot_from_operation/2	Module: tcltk_interface
Name: potentially_enabled_operation/3	Module: tcltk_interface
Name: generate_dot_from_operation_with_params/4	Module: tcltk_interface

Name: get_if_condition/5	Module: b_operation_guards
Name: get_operation_enabling_condition2/4	Module: b_operation_guards
Name: b_execute_statement2/8	Module: b_interpreter
Name: get_operation_enabling_condition/7	Module: b_operation_guards
Name: get_operation_enabling_for_event_b_actions/5	Module: b_operation_guards

Name: get_full_eventb_guard/2	Module: b_read_write_info
Name: get_operation_guards_aux/5	Module: b_operation_guards

Name: retractall/1
Name: assertz/1
Name: true
Name: obtain_action_enabling_conditions/0	Module: b_operation_guards
Name: ->/3
Name: !
Name: RECURSIVE_CALL/1	Module: b_operation_guards
Name: =/2
Name: animation_minor_mode/1	Module: specfile