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