400 Lines

34 Predicates

Imported Modules: module_information heaps avl ordsets lists

1 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_get_machine_operation/4 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: state_space_reset/0 Module: state_space Name: find_successor_state/4 Module: b_trace_checking	Name: ctigar_symbolic_model_check/1

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_get_machine_operation/4

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: state_space_reset/0

Module: state_space

Name: find_successor_state/4

Module: b_trace_checking

Name: ctigar_symbolic_model_check/1

check_convergence/1

check_convergence_aux/1

ctigar_symbolic_model_check/1

extend/4

generalize_and_add/12

generate_clause/5

generate_clause_aux/5

handle_counter_example/2

inductive_clause/2

inductively_generalize/7

inductively_generalize_aux/6

propagate_clauses_aux/4

propagate_clauses_on_level/3

push_generalization/6

push_generalization_aux/11

replay_aux/2

replay_counter_example/1

strengthen/6

strengthen_aux/8

strengthen_aux1/7

strengthen_get_property/4

strengthen_loop/7

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('Checking: ~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('Checking: ~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),
    get_abstract_domain(Domain),
    catch(symbolic_model_check_fx(K,Frames,Domain,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/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),_3299,[access(exist),file_type(source),relative_to('/builds/stups/prob/prolog_doc_gen/prolog-Doc/prob_prolog/src/symbolic_model_checker/ctigar.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/ctigar.pl')])

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

Name: RECURSIVE_CALL/1	Module: ctigar
Name: ord_symdiff/3	Module: foo_error
Name: =/2

Name: format/2
Name: get_counter/2	Module: counter/counter
Name: is/2
Name: statistics/2
Name: catch/3

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

Name: RECURSIVE_CALL/12	Module: ctigar
Name: true
Name: trace
Name: nl
Name: write/1
Name: =/2
Name: ->/3
Name: length/2
Name: ord_union/3	Module: foo_error
Name: list_to_ord_set/2	Module: foo_error
Name: conjunction_to_list/2	Module: bsyntaxtree
Name: conjunct_predicates/2	Module: bsyntaxtree
Name: findall/3
Name: add_to_heap/4	Module: foo_error
Name: is/2
Name: unsat_core_with_fixed_conjuncts/3	Module: foo_error
Name: !
Name: solve/2	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: concrete_state_to_abstract_state/3	Module: foo_error

Name: strengthen_aux/8	Module: ctigar
Name: push_generalization_aux/11	Module: ctigar

Name: generate_clause_aux/5	Module: ctigar
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: ctigar

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

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

Name: inductively_generalize_aux/6	Module: ctigar
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: ctigar
Name: >/2
Name: RECURSIVE_CALL/6	Module: ctigar
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: ctigar
Name: down/4	Module: foo_error

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

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

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

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

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/2	Module: ctigar
Name: find_successor_state/4	Module: b_trace_checking

Name: replay_aux/2	Module: ctigar
Name: state_space_reset/0	Module: state_space

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

Name: symbolic_model_check_fx/6	Module: ctigar
Name: strengthen_aux/8	Module: ctigar

Name: strengthen/6	Module: ctigar
Name: push_generalization/6	Module: ctigar
Name: generalize_and_add/12	Module: ctigar
Name: empty_heap/1	Module: foo_error
Name: is/2
Name: !
Name: inductively_generalize/7	Module: ctigar
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/7	Module: ctigar
Name: strengthen_loop/7	Module: ctigar

Name: catch/3
Name: get_abstract_domain/1	Module: foo_error
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: ctigar
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: ctigar
Name: create_state_predicate/2	Module: foo_error

prob_prolog/src/symbolic_model_checker/ctigar.pl

Modules

Predicates of ctigar

Module Information

400 Lines

34 Predicates

Imported Modules: module_information heaps avl ordsets lists

1 Exports

18 specified Imports

Predicates:

Determinacy Checker: