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).