1 | % (c) 2015-2016 Lehrstuhl fuer Softwaretechnik und Programmiersprachen, | |
2 | % Heinrich Heine Universitaet Duesseldorf | |
3 | % This software is licenced under EPL 1.0 (http://www.eclipse.org/org/documents/epl-v10.html) | |
4 | ||
5 | :- module(bmc,[bmc_symbolic_model_check/1, | |
6 | get_constraint/2, | |
7 | constraint_transitions/2]). | |
8 | ||
9 | :- use_module(probsrc(module_information)). | |
10 | :- module_info(group,symbolic_model_checker). | |
11 | :- module_info(description,'A finite-state symbolic model checker based on BMC.'). | |
12 | ||
13 | :- use_module(library(lists), [append/2,maplist/3]). | |
14 | ||
15 | :- use_module(extension('counter/counter'),[counter_init/0, | |
16 | new_counter/1]). | |
17 | ||
18 | :- use_module(probsrc(before_after_predicates), [before_after_predicate_list_disjunct_with_equalities/3, | |
19 | before_after_predicate_for_operation/2]). | |
20 | :- use_module(probsrc(translate), [translate_bexpression/2]). | |
21 | :- use_module(probsrc(bmachine),[b_get_invariant_from_machine/1, | |
22 | b_get_machine_operation/4, | |
23 | b_get_machine_constants/1, | |
24 | b_get_machine_variables/1, | |
25 | b_specialized_invariant_for_op/2, | |
26 | get_proven_invariant/2]). | |
27 | :- use_module(probsrc(preferences),[get_preference/2]). | |
28 | :- use_module(probsrc(bsyntaxtree), [conjunct_predicates/2, | |
29 | disjunct_predicates/2, | |
30 | create_negation/2]). | |
31 | :- use_module(symbolic_model_checker(predicate_handling), [get_initial_state_predicate/1, | |
32 | prime_predicate/2, | |
33 | prime_n_times/3]). | |
34 | :- use_module(symbolic_model_checker(solver_handling), [solve/2]). | |
35 | :- use_module(symbolic_model_checker(ce_replay), [replay_counter_example/1]). | |
36 | ||
37 | bmc_symbolic_model_check(Res) :- | |
38 | counter_init, new_counter(ic3solvercalls), | |
39 | bmc_symbolic_model_check(0,Res). | |
40 | ||
41 | bmc_symbolic_model_check(25,limit_reached) :- !. | |
42 | bmc_symbolic_model_check(K,Res) :- | |
43 | format('K = ~w~n', [K]), | |
44 | get_constraint(K,Constraint), | |
45 | % translate_bexpression(Constraint,PPConstraint), | |
46 | % format('BMC Constraint: ~w~n',[PPConstraint]), | |
47 | catch(solve(Constraint,Result),solver_and_provers_too_weak,Result=solver_and_provers_too_weak), | |
48 | bmc_symbolic_model_check_aux(Result,K,Res). | |
49 | ||
50 | bmc_symbolic_model_check_aux(solution(Sol),_K,Res) :- !, | |
51 | Res = counterexample_found, | |
52 | replay_counter_example(Sol). | |
53 | bmc_symbolic_model_check_aux(contradiction_found(_),K,Res) :- !, | |
54 | K2 is K + 1, | |
55 | bmc_symbolic_model_check(K2,Res). | |
56 | bmc_symbolic_model_check_aux(_,_K,solver_and_provers_too_weak). | |
57 | ||
58 | get_constraint(K,Base) :- | |
59 | get_preference(use_po,false), !, | |
60 | get_initial_state_predicate(I), | |
61 | b_get_invariant_from_machine(P), | |
62 | K2 is K - 1, | |
63 | constraint_transitions(K2,Transitions), | |
64 | constraint_property(K,P,Property), | |
65 | conjunct_predicates([I,Transitions,Property],Base). | |
66 | get_constraint(K,Base) :- | |
67 | get_preference(use_po,true), !, | |
68 | proof_supported_transition_predicate(K,Base). | |
69 | ||
70 | proof_supported_transition_predicate(0,Constraint) :- !, | |
71 | get_initial_state_predicate(I), | |
72 | b_get_invariant_from_machine(P), | |
73 | create_negation(P,NegP), | |
74 | conjunct_predicates([I,NegP],Constraint). | |
75 | proof_supported_transition_predicate(N,Constraint) :- | |
76 | N2 is N - 2, N1 is N - 1, | |
77 | get_initial_state_predicate(I), | |
78 | constraint_transitions(N2,TWoProp), | |
79 | proof_supported_transition_predicate_aux(N1,PSPred), | |
80 | conjunct_predicates([I,TWoProp,PSPred],Constraint). | |
81 | ||
82 | proof_supported_transition_predicate_aux(N,TPred) :- | |
83 | findall(op(OpName,Pred),(before_after_predicate_for_operation(OpName,Pred)),Ops), | |
84 | maplist(op_to_step_constraint,Ops,SingleSteps), | |
85 | disjunct_predicates(SingleSteps,Step), | |
86 | prime_n_times(N,Step,TPred). | |
87 | ||
88 | op_to_step_constraint(op(OpName,BaPred),StepConstraint) :- | |
89 | (b_specialized_invariant_for_op(OpName,UncheckedInvariant) | |
90 | -> true ; b_get_invariant_from_machine(UncheckedInvariant)), | |
91 | create_negation(UncheckedInvariant,NegUncheckedInvariant), | |
92 | prime_predicate(NegUncheckedInvariant,PrimedNegUncheckedInvariant), | |
93 | conjunct_predicates([BaPred,PrimedNegUncheckedInvariant],StepConstraint). | |
94 | ||
95 | constraint_transitions(K,Transitions) :- | |
96 | get_preference(use_po,false), !, | |
97 | transition_predicate(T), | |
98 | constraint_transitions(K,T,Transitions). | |
99 | constraint_transitions(K,Transitions) :- | |
100 | get_preference(use_po,true), !, | |
101 | findall(op(OpName,Pred),(before_after_predicate_for_operation(OpName,Pred)),Ops), | |
102 | maplist(op_to_transition,Ops,SingleSteps), | |
103 | disjunct_predicates(SingleSteps,Step), | |
104 | constraint_transitions(K,Step,Transitions). | |
105 | ||
106 | op_to_transition(op(OpName,BaPred),StepConstraint) :- | |
107 | (get_proven_invariant(OpName,ProvenInvariant) | |
108 | -> true ; ProvenInvariant = b(truth,pred,[])), | |
109 | prime_predicate(ProvenInvariant,PrimedProvenInvariant), | |
110 | conjunct_predicates([BaPred,PrimedProvenInvariant],StepConstraint). | |
111 | ||
112 | constraint_transitions(K,T,Transitions) :- | |
113 | constraint_transitions_aux(K,T,Conjuncts), | |
114 | conjunct_predicates(Conjuncts,Transitions). | |
115 | constraint_transitions_aux(X,_,[]) :- X < 0, !. | |
116 | constraint_transitions_aux(0,T,[T]) :- !. | |
117 | constraint_transitions_aux(N,T,[T|Rest]) :- | |
118 | prime_predicate(T,PT), | |
119 | N2 is N - 1, | |
120 | constraint_transitions_aux(N2,PT,Rest). | |
121 | ||
122 | constraint_property(K,P,Property) :- | |
123 | create_negation(P,NegP), | |
124 | constraint_property_aux(K,NegP,Disjuncts), | |
125 | disjunct_predicates(Disjuncts,Property). | |
126 | constraint_property_aux(0,P,[P]) :- !. | |
127 | constraint_property_aux(N,P,[P|Rest]) :- | |
128 | prime_predicate(P,PP), | |
129 | N2 is N - 1, | |
130 | constraint_property_aux(N2,PP,Rest). | |
131 | ||
132 | transition_predicate(TransitionPredicate) :- | |
133 | findall(Body,b_get_machine_operation(_Name,_Results,_Parameters,Body),ListOfBodies), | |
134 | b_get_machine_variables(Variables), | |
135 | b_get_machine_constants(Constants), | |
136 | append(Variables,Constants,VarsAndConsts), | |
137 | before_after_predicate_list_disjunct_with_equalities(ListOfBodies,VarsAndConsts,TransitionPredicate). |