1 | % (c) 2015-2022 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), [maplist/3]). | |
14 | ||
15 | :- use_module(extension('counter/counter'),[counter_init/0, | |
16 | new_counter/1]). | |
17 | ||
18 | :- use_module(extrasrc(before_after_predicates), [before_after_predicate_list_disjunct_with_equalities/3, | |
19 | before_after_predicate_for_operation/2]). | |
20 | :- use_module(probsrc(bmachine),[b_get_invariant_from_machine/1, | |
21 | b_get_machine_operation/4, | |
22 | b_get_machine_constants/1, | |
23 | b_get_machine_variables/1, | |
24 | b_specialized_invariant_for_op/2, | |
25 | get_proven_invariant/2]). | |
26 | :- use_module(probsrc(preferences),[get_preference/2]). | |
27 | :- use_module(probsrc(bsyntaxtree), [conjunct_predicates/2, | |
28 | disjunct_predicates/2, | |
29 | create_negation/2]). | |
30 | :- use_module(symbolic_model_checker(predicate_handling), [get_initial_state_predicate/1, | |
31 | prime_predicate/2, | |
32 | prime_n_times/3]). | |
33 | :- use_module(symbolic_model_checker(solver_handling), [solve/2]). | |
34 | :- use_module(symbolic_model_checker(ce_replay), [replay_counter_example/1]). | |
35 | ||
36 | bmc_symbolic_model_check(Res) :- | |
37 | counter_init, new_counter(ic3solvercalls), | |
38 | bmc_symbolic_model_check(0,Res). | |
39 | ||
40 | bmc_symbolic_model_check(25,limit_reached) :- !. | |
41 | bmc_symbolic_model_check(K,Res) :- | |
42 | format('K = ~w~n', [K]), | |
43 | get_constraint(K,Constraint), | |
44 | %translate:nested_print_bexpr(Constraint),nl, | |
45 | catch(solve(Constraint,Result),solver_and_provers_too_weak,Result=solver_and_provers_too_weak), | |
46 | bmc_symbolic_model_check_aux(Result,K,Res). | |
47 | ||
48 | bmc_symbolic_model_check_aux(solution(Sol),_K,Res) :- !, | |
49 | Res = counterexample_found, | |
50 | replay_counter_example(Sol). | |
51 | bmc_symbolic_model_check_aux(contradiction_found(_),K,Res) :- !, | |
52 | K2 is K + 1, | |
53 | bmc_symbolic_model_check(K2,Res). | |
54 | bmc_symbolic_model_check_aux(_,_K,solver_and_provers_too_weak). | |
55 | ||
56 | get_constraint(K,Base) :- | |
57 | get_preference(use_po,false), !, | |
58 | get_initial_state_predicate(I), | |
59 | b_get_invariant_from_machine(P), | |
60 | K2 is K - 1, | |
61 | constraint_transitions(K2,Transitions), | |
62 | constraint_property(K,P,Property), | |
63 | conjunct_predicates([I,Transitions,Property],Base). | |
64 | get_constraint(K,Base) :- | |
65 | %use_po true; we use proof info | |
66 | proof_supported_transition_predicate(K,Base). | |
67 | ||
68 | % with proof support we add the specialized/optimised Invariant for each operation at the end | |
69 | proof_supported_transition_predicate(0,Constraint) :- !, | |
70 | get_initial_state_predicate(I), | |
71 | b_get_invariant_from_machine(P), | |
72 | create_negation(P,NegP), | |
73 | conjunct_predicates([I,NegP],Constraint). | |
74 | proof_supported_transition_predicate(N,Constraint) :- | |
75 | N2 is N - 2, N1 is N - 1, | |
76 | get_initial_state_predicate(I), | |
77 | constraint_transitions(N2,TWoProp), | |
78 | proof_supported_transition_predicate_aux(N1,PSPred), | |
79 | conjunct_predicates([I,TWoProp,PSPred],Constraint). | |
80 | ||
81 | proof_supported_transition_predicate_aux(N,TPred) :- | |
82 | findall(op(OpName,Pred),(before_after_predicate_for_operation(OpName,Pred)),Ops), | |
83 | maplist(op_to_step_constraint,Ops,SingleSteps), | |
84 | disjunct_predicates(SingleSteps,Step), | |
85 | prime_n_times(N,Step,TPred). | |
86 | ||
87 | op_to_step_constraint(op(OpName,BaPred),StepConstraint) :- | |
88 | (b_specialized_invariant_for_op(OpName,UncheckedInvariant) | |
89 | -> true ; b_get_invariant_from_machine(UncheckedInvariant)), | |
90 | create_negation(UncheckedInvariant,NegUncheckedInvariant), | |
91 | prime_predicate(NegUncheckedInvariant,PrimedNegUncheckedInvariant), | |
92 | conjunct_predicates([BaPred,PrimedNegUncheckedInvariant],StepConstraint). | |
93 | ||
94 | constraint_transitions(K,Transitions) :- | |
95 | get_preference(use_po,false), !, | |
96 | transition_predicate(T), | |
97 | constraint_transitions(K,T,Transitions). | |
98 | constraint_transitions(K,Transitions) :- | |
99 | get_preference(use_po,true), !, | |
100 | findall(op(OpName,Pred),(before_after_predicate_for_operation(OpName,Pred)),Ops), | |
101 | maplist(op_to_transition,Ops,SingleSteps), | |
102 | disjunct_predicates(SingleSteps,Step), | |
103 | constraint_transitions(K,Step,Transitions). | |
104 | ||
105 | op_to_transition(op(OpName,BaPred),StepConstraint) :- | |
106 | (get_proven_invariant(OpName,ProvenInvariant) | |
107 | -> true ; ProvenInvariant = b(truth,pred,[])), | |
108 | prime_predicate(ProvenInvariant,PrimedProvenInvariant), | |
109 | conjunct_predicates([BaPred,PrimedProvenInvariant],StepConstraint). | |
110 | ||
111 | constraint_transitions(K,T,Transitions) :- | |
112 | constraint_transitions_aux(K,T,Conjuncts), | |
113 | conjunct_predicates(Conjuncts,Transitions). | |
114 | constraint_transitions_aux(X,_,[]) :- X < 0, !. | |
115 | constraint_transitions_aux(0,T,[T]) :- !. | |
116 | constraint_transitions_aux(N,T,[T|Rest]) :- | |
117 | prime_predicate(T,PT), | |
118 | N2 is N - 1, | |
119 | constraint_transitions_aux(N2,PT,Rest). | |
120 | ||
121 | constraint_property(K,P,Property) :- | |
122 | create_negation(P,NegP), | |
123 | constraint_property_aux(K,NegP,Disjuncts), | |
124 | disjunct_predicates(Disjuncts,Property). | |
125 | constraint_property_aux(0,P,[P]) :- !. | |
126 | constraint_property_aux(N,P,[P|Rest]) :- | |
127 | prime_predicate(P,PP), | |
128 | N2 is N - 1, | |
129 | constraint_property_aux(N2,PP,Rest). | |
130 | ||
131 | transition_predicate(TransitionPredicate) :- | |
132 | findall(Body,b_get_machine_operation(_Name,_Results,_Parameters,Body),ListOfBodies), | |
133 | b_get_machine_variables(Variables), | |
134 | %b_get_machine_constants(Constants), append(Variables,Constants,VarsAndConsts), | |
135 | before_after_predicate_list_disjunct_with_equalities(ListOfBodies,Variables,TransitionPredicate). |