395 Lines

36 Predicates

Imported Modules: module_information heaps avl lists

2 Exports

18 specified Imports

Imports	Exports
Name: counter_init/0 Module: counter/counter Name: new_counter/1 Module: counter/counter Name: get_counter/2 Module: counter/counter Name: get_preference/2 Module: preferences Name: b_get_invariant_from_machine/1 Module: bmachine Name: b_get_properties_from_machine/1 Module: bmachine Name: b_specialized_invariant_for_op/2 Module: bmachine Name: get_proven_invariant/2 Module: bmachine Name: conjunct_predicates/2 Module: bsyntaxtree Name: disjunct_predicates/2 Module: bsyntaxtree Name: conjunction_to_list/2 Module: bsyntaxtree Name: create_implication/3 Module: bsyntaxtree Name: create_negation/2 Module: bsyntaxtree Name: translate_bexpression/2 Module: translate Name: print_bexpr/1 Module: translate Name: add_error_and_fail/2 Module: error_manager Name: state_space_reset/0 Module: state_space Name: find_successor_state/4 Module: b_trace_checking	Name: ic3_symbolic_model_check/1 Name: counter_example_can_be_replayed/0

Imports

Exports

Name: counter_init/0

Module: counter/counter

Name: new_counter/1

Module: counter/counter

Name: get_counter/2

Module: counter/counter

Name: get_preference/2

Module: preferences

Name: b_get_invariant_from_machine/1

Module: bmachine

Name: b_get_properties_from_machine/1

Module: bmachine

Name: b_specialized_invariant_for_op/2

Module: bmachine

Name: get_proven_invariant/2

Module: bmachine

Name: conjunct_predicates/2

Module: bsyntaxtree

Name: disjunct_predicates/2

Module: bsyntaxtree

Name: conjunction_to_list/2

Module: bsyntaxtree

Name: create_implication/3

Module: bsyntaxtree

Name: create_negation/2

Module: bsyntaxtree

Name: translate_bexpression/2

Module: translate

Name: print_bexpr/1

Module: translate

Name: add_error_and_fail/2

Module: error_manager

Name: state_space_reset/0

Module: state_space

Name: find_successor_state/4

Module: b_trace_checking

Name: ic3_symbolic_model_check/1

Name: counter_example_can_be_replayed/0

check_convergence/1

check_convergence_aux/1

counter_example_can_be_replayed/0

extend/4

generalize_and_add/8

generate_clause/5

generate_clause_aux/5

handle_counter_example/2

ic3_symbolic_model_check/1

inductive_clause/2

inductively_generalize/7

inductively_generalize_aux/6

propagate_clauses_aux/4

propagate_clauses_on_level/3

push_generalization/4

push_generalization_aux/8

replay_aux/3

replay_counter_example/1

strengthen/4

strengthen_aux/6

strengthen_aux1/5

strengthen_get_property/4

strengthen_loop/5

symbolic_model_check/3

symbolic_model_check(Property,Init,ResultOut) :-
    % ce of length 0? check if Init => Invariant
    create_implication(Init,Property,Predicate),
    % debug output
    translate_bexpression(Predicate,PPPredicate),
    format('~nChecking for Counter-Example of Length 0: ~w~n',[PPPredicate]),
    solve_negated(Predicate,Result),
    functor(Result,ForPrint,_),
    format('Counter-Example of Length 0 exists: ~w~n', [ForPrint]),
    Result = solution(Sol), !,
    create_state_predicate(Sol,StatePred),
    replay_counter_example([StatePred]),
    ResultOut = counterexample_found.

symbolic_model_check(Property,Init,ResultOut) :-
    % ce of length 1? check if Init & Transition => Invariant'
    prime_predicate(Property,PrimedProperty),
    get_single_transition_predicate(OpName,Transition),
    conjunct_predicates([Init,Transition],LHS),
    create_implication(LHS,PrimedProperty,Predicate),
    % debug output
    translate_bexpression(Predicate,PPPredicate),
    format('~nChecking for Counter-Example of Length 1: ~w~n',[PPPredicate]),
    solve_negated(Predicate,Result),
    functor(Result,ForPrint,_),
    format('Counter-Example of Length 1 (transition ~w) exists: ~w~n', [OpName,ForPrint]),
    Result = solution(Sol), !,
    handle_counter_example(Sol,[]),
    ResultOut = counterexample_found.

symbolic_model_check(Property,Init,Result) :-
    K = 1,
    % two initial frames:
    % F_0 holds the initial condition
    % F_1 holds the property
    % further frames will be added by extend later on
    % we store the transition in the frames as well in order to spare passing it around
    b_get_properties_from_machine(PropertiesOnConstants),
    F_0 = frame([Init,PropertiesOnConstants],[]), F_1 = frame([Property,PropertiesOnConstants],[]),
    empty_avl(E),
    avl_store(0,E,F_0,FramesT),
    avl_store(1,FramesT,F_1,Frames),
    catch(symbolic_model_check_fx(K,Frames,Property,Init,Result),
    ic3_counter_example(Solution,Succs),
    (handle_counter_example(Solution,Succs),Result=counterexample_found)).

symbolic_model_check_aux/1

symbolic_model_check_fx/5

use_generalization/1

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),_3441,[access(exist),file_type(source),relative_to('/builds/stups/prob/prolog_doc_gen/prolog-Doc/prob_prolog/src/symbolic_model_checker/ic3.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'),_261,[access(exist),file_type(source),relative_to('/builds/stups/prob/prolog_doc_gen/prolog-Doc/prob_prolog/src/symbolic_model_checker/ic3.pl')])

Name: check_convergence_aux/1	Module: ic3
Name: avl_to_list/2	Module: foo_error

Name: avl_store/4	Module: foo_error
Name: b_get_properties_from_machine/1	Module: bmachine
Name: is/2

Name: add_error_and_fail/2	Module: error_manager
Name: unsat_core_generalization/8	Module: foo_error
Name: !
Name: use_generalization/1	Module: ic3
Name: add_to_heap/4	Module: foo_error

Name: strengthen_aux/6	Module: ic3
Name: push_generalization_aux/8	Module: ic3

Name: generate_clause_aux/5	Module: ic3
Name: maplist/3	Module: foo_error
Name: conjunction_to_list/2	Module: bsyntaxtree
Name: format/2
Name: translate_bexpression/2	Module: translate
Name: mic/6	Module: ic3

Name: RECURSIVE_CALL/5	Module: ic3
Name: is/2
Name: add_clauses_to_level/4	Module: foo_error
Name: !
Name: =</2

Name: replay_counter_example/1	Module: ic3
Name: create_constants_state_predicate/2	Module: foo_error
Name: ->/3
Name: print_succs/1	Module: ic3
Name: format/2
Name: !
Name: create_succ_state_predicate/2	Module: foo_error
Name: create_state_predicate/2	Module: foo_error

Name: =/2
Name: !
Name: solve/2	Module: foo_error
Name: conjunct_predicates/2	Module: bsyntaxtree
Name: prime_predicate/2	Module: foo_error
Name: create_negation/2	Module: bsyntaxtree
Name: disjunct_predicates/2	Module: bsyntaxtree
Name: get_transition_predicate/1	Module: foo_error

Name: inductively_generalize_aux/6	Module: ic3
Name: is/2
Name: throw/1
Name: !
Name: =/2
Name: solve/2	Module: foo_error
Name: conjunct_predicates/2	Module: bsyntaxtree
Name: get_transition_predicate/1	Module: foo_error
Name: create_negation/2	Module: bsyntaxtree
Name: prime_predicate/2	Module: foo_error
Name: in_solver_on_level/3	Module: foo_error
Name: </2

Name: generate_clause/5	Module: ic3
Name: >/2
Name: RECURSIVE_CALL/6	Module: ic3
Name: is/2
Name: =/2
Name: ->/2
Name: ->/3
Name: !
Name: solve/2	Module: foo_error
Name: conjunct_predicates/2	Module: bsyntaxtree
Name: get_transition_predicate/1	Module: foo_error
Name: create_negation/2	Module: bsyntaxtree
Name: prime_predicate/2	Module: foo_error
Name: in_solver_on_level/3	Module: foo_error
Name: =</2

Name: conjunct_predicates/2	Module: bsyntaxtree
Name: ctgDown/6	Module: foo_error
Name: conjunction_to_list/2	Module: bsyntaxtree
Name: !
Name: mic_algorithm/1	Module: ic3
Name: down/4	Module: foo_error

Name: RECURSIVE_CALL/1	Module: ic3
Name: print/1
Name: nl
Name: print_bexpr/1	Module: translate
Name: disjunct_predicates/2	Module: bsyntaxtree

Name: print_frames_list/1	Module: ic3
Name: avl_to_list/2	Module: foo_error

Name: RECURSIVE_CALL/1	Module: ic3
Name: print_clauses/1	Module: ic3
Name: format/2
Name: length/2

Name: print_heap2/1	Module: ic3
Name: nl
Name: write/1
Name: heap_to_list/2	Module: foo_error

Name: print_heap2/1	Module: ic3
Name: handle_counter_example/2	Module: ic3

Name: true
Name: RECURSIVE_CALL/4	Module: ic3
Name: is/2
Name: </2
Name: ->/3
Name: propagate_clauses_on_level/3	Module: ic3

Name: add_clauses_to_level/4	Module: foo_error
Name: include/3	Module: foo_error
Name: in_solver_on_level/3	Module: foo_error
Name: clauses_on_level/4	Module: foo_error
Name: is/2

Name: RECURSIVE_CALL/3	Module: ic3
Name: is/2
Name: find_successor_state/4	Module: b_trace_checking

Name: true
Name: replay_aux/3	Module: ic3
Name: state_space_reset/0	Module: state_space
Name: counter_example_can_be_replayed/0	Module: ic3
Name: ->/3

Name: handle_counter_example/2	Module: ic3
Name: symbolic_model_check/3	Module: ic3

Name: strengthen_aux/6	Module: ic3
Name: symbolic_model_check_fx/5	Module: ic3

Name: strengthen/4	Module: ic3
Name: push_generalization/4	Module: ic3
Name: generalize_and_add/8	Module: ic3
Name: empty_heap/1	Module: foo_error
Name: is/2
Name: !
Name: inductively_generalize/7	Module: ic3
Name: create_primary_inputs_predicate/2	Module: foo_error
Name: create_succ_state_predicate/2	Module: foo_error
Name: create_state_predicate/2	Module: foo_error

Name: RECURSIVE_CALL/5	Module: ic3
Name: strengthen_loop/5	Module: ic3

Name: catch/3
Name: avl_store/4	Module: foo_error
Name: empty_avl/1	Module: foo_error
Name: =/2
Name: b_get_properties_from_machine/1	Module: bmachine
Name: handle_counter_example/2	Module: ic3
Name: !
Name: format/2
Name: functor/3
Name: solve_negated/2	Module: foo_error
Name: translate_bexpression/2	Module: translate
Name: create_implication/3	Module: bsyntaxtree
Name: conjunct_predicates/2	Module: bsyntaxtree
Name: get_single_transition_predicate/2	Module: foo_error
Name: prime_predicate/2	Module: foo_error
Name: replay_counter_example/1	Module: ic3
Name: create_state_predicate/2	Module: foo_error

prob_prolog/src/symbolic_model_checker/ic3.pl

Modules

Predicates of ic3

Module Information

395 Lines

36 Predicates

Imported Modules: module_information heaps avl lists

2 Exports

18 specified Imports

Predicates:

Determinacy Checker: