425 Lines

24 Predicates

Imported Modules: lists

1 Exports

33 specified Imports

Imports	Exports
Name: module_info/2 Module: module_information Name: subtract/3 Module: sets Name: solve_predicate/5 Module: solver_interface Name: animation_minor_mode/1 Module: specfile Name: full_b_machine/1 Module: bmachine Name: b_get_refined_machine/1 Module: bmachine Name: b_get_machine_operation/6 Module: bmachine Name: b_get_invariant_from_machine/1 Module: bmachine Name: b_get_linking_invariant_from_machine/1 Module: bmachine Name: b_get_properties_from_machine/1 Module: bmachine Name: b_get_machine_variables/1 Module: bmachine Name: b_get_machine_constants/1 Module: bmachine Name: b_machine_name/1 Module: bmachine Name: nested_print_bexpr/1 Module: translate Name: formatsilent/2 Module: debug Name: debug_mode/1 Module: debug Name: get_texpr_expr/2 Module: bsyntaxtree Name: get_texpr_info/2 Module: bsyntaxtree Name: get_texpr_id/2 Module: bsyntaxtree Name: add_texpr_description/3 Module: bsyntaxtree Name: add_labels_to_texpr/3 Module: bsyntaxtree Name: get_rodin_name/2 Module: bsyntaxtree Name: conjunct_predicates/2 Module: bsyntaxtree Name: conjunction_to_list/2 Module: bsyntaxtree Name: create_texpr/4 Module: bsyntaxtree Name: safe_create_texpr/3 Module: bsyntaxtree Name: rename_bt/3 Module: bsyntaxtree Name: construct_optimized_exists/3 Module: b_interpreter_components Name: get_section/3 Module: bmachine_structure Name: prime_identifiers/2 Module: btypechecker Name: create_negation/2 Module: bsyntaxtree Name: get_preference/2 Module: preferences Name: ajoin/2 Module: tools_strings	Name: cbc_refinement_check/2

Imports

Exports

Name: module_info/2

Module: module_information

Name: subtract/3

Module: sets

Name: solve_predicate/5

Module: solver_interface

Name: animation_minor_mode/1

Module: specfile

Name: full_b_machine/1

Module: bmachine

Name: b_get_refined_machine/1

Module: bmachine

Name: b_get_machine_operation/6

Module: bmachine

Name: b_get_invariant_from_machine/1

Module: bmachine

Name: b_get_linking_invariant_from_machine/1

Module: bmachine

Name: b_get_properties_from_machine/1

Module: bmachine

Name: b_get_machine_variables/1

Module: bmachine

Name: b_get_machine_constants/1

Module: bmachine

Name: b_machine_name/1

Module: bmachine

Name: nested_print_bexpr/1

Module: translate

Name: formatsilent/2

Module: debug

Name: debug_mode/1

Module: debug

Name: get_texpr_expr/2

Module: bsyntaxtree

Name: get_texpr_info/2

Module: bsyntaxtree

Name: get_texpr_id/2

Module: bsyntaxtree

Name: add_texpr_description/3

Module: bsyntaxtree

Name: add_labels_to_texpr/3

Module: bsyntaxtree

Name: get_rodin_name/2

Module: bsyntaxtree

Name: conjunct_predicates/2

Module: bsyntaxtree

Name: conjunction_to_list/2

Module: bsyntaxtree

Name: create_texpr/4

Module: bsyntaxtree

Name: safe_create_texpr/3

Module: bsyntaxtree

Name: rename_bt/3

Module: bsyntaxtree

Name: construct_optimized_exists/3

Module: b_interpreter_components

Name: get_section/3

Module: bmachine_structure

Name: prime_identifiers/2

Module: btypechecker

Name: create_negation/2

Module: bsyntaxtree

Name: get_preference/2

Module: preferences

Name: ajoin/2

Module: tools_strings

Name: cbc_refinement_check/2

all_abstract_parameters/2

assign_violation_found/3

cbc_refinement_check/2

cbc_solve_predicate/3

classical_refinement_check/2

create_equals/3

eventb_refinement_check/2

extract_witness_predicate/2

get_all_operations_from_machine/2

guard_strengthening/5

guard_strengthening_aux/6

guard_strengthening_aux(_Axioms,_Invariant,_Properties,
    rlevent(_Name,_Section,_Stat,_Parameters,_Guards,_Thm,_Actions,_VWit,_PWit,_Unmod,[]),
    [],false) :- !. % nothing to check

guard_strengthening_aux(Axioms,Invariant,Properties,
    rlevent(Name,_Section,_Stat,_Parameters,Guards,_Thm,_Actions,VWit,PWit,_Unmod,[AbsEvent]),
    Results,ViolationFound) :- !,
    get_texpr_expr(AbsEvent,ABSRLEVENT),
    ABSRLEVENT = rlevent(_AbsName,_Absection,_AbsStat,_AbsParameters,AbsGrds,_AbsThm,_AbsAct,_AbsVWit,_AbsPWit,_AbsUnmod,_AbsEvents),
    conjunction_to_list(AbsGrds,AbsGrdsList),
    % map over all abstract guards
    maplist(guard_strengthening_single_event(Name,Axioms,Invariant,Properties,VWit,PWit,Guards),AbsGrdsList,Results,SubViolationFound),
    merge_violation_found(SubViolationFound,ViolationFound).

guard_strengthening_aux(Axioms,Invariant,Properties,
    rlevent(Name,_Section,_Stat,_Parameters,Guards,_Thm,Actions,VWit,PWit,_Unmod,AbsEvents),
    [Result],ViolationFound) :-
    % concrete before-after-predicate
    b_get_machine_variables(Vars),
    b_get_machine_constants(Consts),
    append(Vars,Consts,Both),
    before_after_predicate_list_conjunct_with_equalities(Actions,Both,Tau),
    % collect all abstract guards G_i and negate
    findall(AbsGrds,
    (member(Evt,AbsEvents),
    get_texpr_expr(Evt,rlevent(_AbsName,_AbsSection,_AbsStat,_AbsParams,AbsGrds,_AbsThm,_AbsAct,_AbsVWit,_AbsPWit,_AbsUnmod,_AbsAbsEvents))),
    ListOfAbstractGuards),
    maplist(create_negation,ListOfAbstractGuards,NegatedAbstractGuards),

    % build up predicate A & I & J & H & W & Tau => G_1 or ... or G_n
    maplist(extract_witness_predicate,VWit,VWitPreds),
    maplist(extract_witness_predicate,PWit,PWitPreds),

    append([Axioms,[Invariant,Properties,Guards,Tau],VWitPreds,PWitPreds,NegatedAbstractGuards],LHSPred),
    conjunct_predicates(LHSPred,Pred),
    cbc_solve_predicate(Pred,State,Res),

    assign_violation_found(Res,ViolationFound,ResTxt),

    % result string and print
    ajoin([Name,'/MRG: ','Counter-Example found: ', ResTxt],Result),
    formatsilent(' * ~w~n',[Result]),
    (debug_mode(off) -> true ; nested_print_bexpr(Pred), write(State),nl).

guard_strengthening_single_event/10

initialisation_pos/5

is_concrete_var/1

merge_violation_found/2

modifies_concrete_var/1

operations_pos/7

operations_pos([],_I,_LI,_AM,_A,[],false).

operations_pos([operation(Name,Results,_Parameters,_Body)|FurtherOps],Invariant,
    LinkingInvariant,AbsMachine,AbstractOperations,Results,ViolationFound) :-
    % there might be no abstract operation with the same name (includes, etc.)
    \+ (member(operation(Name,_AbsResults,_AbsParameters,_AbsBody),AbstractOperations)), !,
    operations_pos(FurtherOps,Invariant,LinkingInvariant,AbsMachine,AbstractOperations,Results,ViolationFound).

operations_pos([operation(Name,Results,_Parameters,Body)|FurtherOps],Invariant,
    LinkingInvariant,AbsMachine,AbstractOperations,[PreRefPoResult,RefPoResult|ListOpPos],ViolationFound) :-
    % first find the matching abstract operation
    member(operation(Name,_AbsResults,_AbsParameters,AbsBody),AbstractOperations),

    % check if we have preconditions - otherwise we assume true
    (get_texpr_expr(Body,precondition(Precondition0,RealBody)) -> true
    ; RealBody=Body, create_texpr(truth,pred,[],Precondition0)),
    add_labels_to_texpr(Precondition0,['P1 (concrete PRE)'], Precondition),
    (get_texpr_expr(AbsBody,precondition(AbsPrecondition0,AbsRealBody))
    -> true
    ; AbsRealBody=AbsBody, create_texpr(truth,pred,[],AbsPrecondition0)
    ),
    add_labels_to_texpr(AbsPrecondition0,['P (abstract PRE)'], AbsPrecondition),

    % refinement po for the preconditions
    create_negation(Precondition,NegPrecondition), % description
    conjunct_predicates([Invariant,LinkingInvariant,AbsPrecondition,NegPrecondition],PreRefPo),
    cbc_solve_predicate(PreRefPo,State,PreRefPoRes),
    assign_violation_found(PreRefPoRes,V2,RTxt2),

    % result string and print
    % This PO is in Section 14.3, page 225 of Schneider's B Book; part of obligation 4 on page 530 of Abrial's B Book
    ajoin([Name, ' Precondition Refinement I & J & P => P1: Counter-Example found: ', RTxt2],PreRefPoResult),
    formatsilent(' * ~w~n',[PreRefPoResult]),
    (debug_mode(off) -> true ; nested_print_bexpr(PreRefPo), write(State),nl),

    % for the refinement of operations, we need to rename existing output variables (i.e. prime them)
    prime_identifiers(Results,PrimedResults),
    list_renamings_to_primed_vars(Results,Renamings),
    rename_bt(RealBody,Renamings,RealBodyWithPrimedVariables),
    create_equals(Results,PrimedResults,EqualResultsPred),

    % refinement po for the operation
    % I & J & P => [S1[out'/out]] not S not (J & out'=out)
    conjunct_predicates([LinkingInvariant|EqualResultsPred],RHS),
    create_negation(RHS,NegRHS),

    set_reference_machine(AbsMachine),
    weakest_precondition(AbsRealBody,NegRHS,RHS2),
    delete_reference_machine,

    create_negation(RHS2,NegRHS2),
    weakest_precondition(RealBodyWithPrimedVariables,NegRHS2,RHS3),
    create_negation(RHS3,NegRHS3),
    conjunct_predicates([Invariant,LinkingInvariant,Precondition,NegRHS3],RefPo),

    cbc_solve_predicate(RefPo,State2,RefPoRes),
    assign_violation_found(RefPoRes,V1,RTxt),
    % result string and print
    ajoin([Name, ' Refinement I & J & P => S1 not S not J: Counter-Example found: ', RTxt],RefPoResult),
    formatsilent(' * ~w~n',[RefPoResult]),
    (debug_mode(off) -> true ; nested_print_bexpr(RefPo), write(State2),nl),

    operations_pos(FurtherOps,Invariant,LinkingInvariant,AbsMachine,AbstractOperations,ListOpPos,SubViolationFound),

    merge_violation_found([V1,V2,SubViolationFound],ViolationFound).

witness_feasibility/5

witness_feasibility_aux/6

witness_feasibility_parameters/6

Determinacy Checker

Determinacy Checker:

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

Name: append/2	Module: foo_error
Name: merge_violation_found/2	Module: cbc_refinement_checks
Name: maplist/4	Module: foo_error
Name: findall/3

Name: append/2	Module: foo_error
Name: merge_violation_found/2	Module: cbc_refinement_checks
Name: maplist/4	Module: foo_error
Name: conjunct_predicates/2	Module: bsyntaxtree
Name: maplist/3	Module: foo_error
Name: before_after_predicate_list_conjunct_with_equalities/3	Module: foo_error
Name: append/3
Name: b_get_machine_constants/1	Module: bmachine
Name: b_get_machine_variables/1	Module: bmachine

Name: merge_violation_found/2	Module: cbc_refinement_checks
Name: maplist/4	Module: foo_error
Name: get_texpr_expr/2	Module: bsyntaxtree

Name: append/3
Name: RECURSIVE_CALL/2	Module: cbc_refinement_checks
Name: get_texpr_expr/2	Module: bsyntaxtree

Name: action_simulation3/5	Module: cbc_refinement_checks
Name: witness_feasibility_parameters/6	Module: cbc_refinement_checks
Name: guard_strengthening_single_event/10	Module: cbc_refinement_checks
Name: operations_pos/7	Module: cbc_refinement_checks
Name: initialisation_pos/5	Module: cbc_refinement_checks
Name: guard_strengthening_aux/6	Module: cbc_refinement_checks

cbc_refinement_checks

prob_prolog/src/symbolic_model_checker/cbc_refinement_checks.pl

Modules

Predicates of cbc_refinement_checks

Module Information

425 Lines

24 Predicates

Imported Modules: lists

1 Exports

33 specified Imports

Predicates:

action_simulation/5

action_simulation/6

action_simulation2/5

action_simulation3/5

all_abstract_parameters/2

assign_violation_found/3

cbc_refinement_check/2

cbc_solve_predicate/3

classical_refinement_check/2

create_equals/3

eventb_refinement_check/2

extract_witness_predicate/2

get_all_operations_from_machine/2

guard_strengthening/5

guard_strengthening_aux/6

guard_strengthening_single_event/10

initialisation_pos/5

is_concrete_var/1

merge_violation_found/2

modifies_concrete_var/1

operations_pos/7

witness_feasibility/5

witness_feasibility_aux/6

witness_feasibility_parameters/6

Determinacy Checker:

Name: nl
Name: write/1
Name: nested_print_bexpr/1	Module: translate
Name: true
Name: debug_mode/1	Module: debug
Name: ->/3
Name: formatsilent/2	Module: debug
Name: ajoin/2	Module: tools_strings
Name: assign_violation_found/3	Module: cbc_refinement_checks
Name: cbc_solve_predicate/3	Module: cbc_refinement_checks
Name: conjunct_predicates/2	Module: bsyntaxtree
Name: create_negation/2	Module: bsyntaxtree
Name: before_after_predicate_with_equalities/3	Module: foo_error
Name: exclude/3	Module: foo_error
Name: b_get_machine_variables/1	Module: bmachine
Name: get_rodin_name/2	Module: bsyntaxtree
Name: !
Name: modifies_concrete_var/1	Module: cbc_refinement_checks

Name: classical_refinement_check/2	Module: cbc_refinement_checks
Name: eventb_refinement_check/2	Module: cbc_refinement_checks
Name: animation_minor_mode/1	Module: specfile
Name: ->/3

Name: =/2
Name: merge_violation_found/2	Module: cbc_refinement_checks
Name: append/2	Module: foo_error
Name: operations_pos/7	Module: cbc_refinement_checks
Name: get_all_operations_from_machine/2	Module: cbc_refinement_checks
Name: initialisation_pos/5	Module: cbc_refinement_checks
Name: add_labels_to_texpr/3	Module: bsyntaxtree
Name: b_get_linking_invariant_from_machine/1	Module: bmachine
Name: b_get_invariant_from_machine/1	Module: bmachine
Name: b_get_refined_machine/1	Module: bmachine
Name: full_b_machine/1	Module: bmachine
Name: ->/3

Name: RECURSIVE_CALL/3	Module: cbc_refinement_checks
Name: safe_create_texpr/3	Module: bsyntaxtree

Name: member/2
Name: b_machine_name/1	Module: bmachine
Name: b_get_machine_variables/1	Module: bmachine
Name: RECURSIVE_CALL/1	Module: cbc_refinement_checks
Name: !

Name: guard_strengthening/5	Module: cbc_refinement_checks
Name: witness_feasibility_aux/6	Module: cbc_refinement_checks
Name: classical_refinement_check/2	Module: cbc_refinement_checks
Name: action_simulation/6	Module: cbc_refinement_checks
Name: operations_pos/7	Module: cbc_refinement_checks
Name: guard_strengthening_aux/6	Module: cbc_refinement_checks
Name: action_simulation/5	Module: cbc_refinement_checks
Name: witness_feasibility/5	Module: cbc_refinement_checks
Name: eventb_refinement_check/2	Module: cbc_refinement_checks
Name: action_simulation2/5	Module: cbc_refinement_checks

Name: some/2	Module: foo_error
Name: member/2
Name: get_texpr_info/2	Module: bsyntaxtree

Name: merge_violation_found/2	Module: cbc_refinement_checks
Name: RECURSIVE_CALL/7	Module: cbc_refinement_checks
Name: nl
Name: write/1
Name: nested_print_bexpr/1	Module: translate
Name: true
Name: debug_mode/1	Module: debug
Name: ->/3
Name: formatsilent/2	Module: debug
Name: ajoin/2	Module: tools_strings
Name: assign_violation_found/3	Module: cbc_refinement_checks
Name: cbc_solve_predicate/3	Module: cbc_refinement_checks
Name: conjunct_predicates/2	Module: bsyntaxtree
Name: create_negation/2	Module: bsyntaxtree
Name: weakest_precondition/3	Module: foo_error
Name: delete_reference_machine	Module: foo_error
Name: set_reference_machine/1	Module: foo_error
Name: create_equals/3	Module: cbc_refinement_checks
Name: rename_bt/3	Module: bsyntaxtree
Name: list_renamings_to_primed_vars/2	Module: foo_error
Name: prime_identifiers/2	Module: btypechecker
Name: add_labels_to_texpr/3	Module: bsyntaxtree
Name: create_texpr/4	Module: bsyntaxtree
Name: =/2
Name: get_texpr_expr/2	Module: bsyntaxtree
Name: member/2
Name: !
Name: not/1