Line data Source code
1 : // Author(s): Luc Engelen
2 : // Copyright: see the accompanying file COPYING or copy at
3 : // https://github.com/mCRL2org/mCRL2/blob/master/COPYING
4 : //
5 : // Distributed under the Boost Software License, Version 1.0.
6 : // (See accompanying file LICENSE_1_0.txt or copy at
7 : // http://www.boost.org/LICENSE_1_0.txt)
8 : //
9 : /// \file mcrl2/invariant_checker.h
10 : /// \brief Add your file description here.
11 :
12 : // Interface to class Invariant_Checker
13 :
14 : #ifndef MCRL2_LPS_INVARIANT_CHECKER_H
15 : #define MCRL2_LPS_INVARIANT_CHECKER_H
16 :
17 : #include "mcrl2/data/detail/prover/bdd_prover.h"
18 : #include "mcrl2/data/detail/prover/bdd2dot.h"
19 : #include "mcrl2/lps/stochastic_specification.h"
20 :
21 : /// The class Invariant_Checker is initialized with an LPS using the constructor Invariant_Checker::Invariant_Checker.
22 : /// After initialization, the function Invariant_Checker::check_invariant can be called any number of times to check
23 : /// whether an expression of sort Bool passed as argument a_invariant is an invariant of this LPS. A new instance of the
24 : /// class Invariant_Checker has to be created for each new LPS that has to be checked.
25 : ///
26 : /// The class Invariant_Checker uses an instance of the class BDD_Prover to check whether a formula is a valid invariant
27 : /// of an mCRL2 LPS. The constructor Invariant_Checker::Invariant_Checker initializes the BDD based prover with the
28 : /// parameters a_rewrite_strategy, a_time_limit, a_path_eliminator, a_solver_type and the data specification of the LPS
29 : /// passed as parameter a_lps. The parameter a_rewrite_strategy specifies which rewrite strategy is used by the prover's
30 : /// rewriter. It can be set to either GS_REWR_JITTY or GS_REWR_JITTYC. The parameter
31 : /// a_time_limit specifies the maximum amount of time in seconds to be spent by the prover on proving a single expression.
32 : /// If a_time_limit is set to 0, no time limit will be enforced. The parameter a_path_eliminator specifies whether or not
33 : /// path elimination is applied. When path elimination is applied, the prover uses an SMT solver to remove inconsistent
34 : /// paths from BDDs. The parameter a_solver_type specifies which SMT solver is used for path elimination. Either the SMT
35 : /// solver ario (http://www.eecs.umich.edu/~ario/) or cvc-lite (http://www.cs.nyu.edu/acsys/cvcl/) can be used. To use one
36 : /// of these solvers, the directory containing the corresponding executable must be in the path. If the parameter
37 : /// a_path_eliminator is set to false, the parameter a_solver_type is ignored. The parameter a_apply_induction indicates
38 : /// whether or not induction on list will be applied.
39 : ///
40 : /// The parameter a_dot_file_name specifies whether a file in dot format of the resulting BDD is saved each time the
41 : /// prover cannot determine whether an expression is a contradiction or a tautology. If the parameter is set to 0, no .dot
42 : /// files are saved. If a string is passed as parameter a_dot_file_name, this string will be used as the prefix of the
43 : /// filenames. An instance of the class BDD2Dot is used to save these files in dot format.
44 : ///
45 : /// If the parameter a_counter_example is set to true, a so called counter example will be printed to stderr each time a
46 : /// summand is encountered that violates the invariant. A counter example is a valuation for which the expression to be
47 : /// proven does not hold. If the parameter a_all_violations is set to true, the invariant checker will not stop as soon as
48 : /// a violation of the invariant is found, but will report all violations instead.
49 : ///
50 : /// Given an LPS,
51 : ///
52 : /// P(d: D) = ...
53 : /// + sum ei: Ei. ci(d, ei) -> ai(fi(d, ei)) . P(gi(d, ei))
54 : /// + ...;
55 : ///
56 : /// an instance of the class Invariant_Checker will generate a formula of the form
57 : ///
58 : /// inv(d) /\ ci(d, ei) => inv(gi(d, ei))
59 : ///
60 : /// for each of the summands, where inv() is the expression passed as parameter a_invariant. If this expression passed as
61 : /// parameter a_invariant holds for the initial state and all the generated formulas are tautologies according to the
62 : /// prover, it is an invariant.
63 :
64 : namespace mcrl2
65 : {
66 : namespace lps
67 : {
68 : namespace detail
69 : {
70 :
71 : template <typename Specification>
72 : class Invariant_Checker
73 : {
74 : typedef typename Specification::process_type process_type;
75 : typedef typename process_type::action_summand_type action_summand_type;
76 : typedef std::vector<action_summand_type> action_summand_vector_type;
77 :
78 : private:
79 : const Specification& f_spec;
80 : data::detail::BDD_Prover f_bdd_prover;
81 : data::detail::BDD2Dot f_bdd2dot;
82 : process_initializer f_init;
83 : action_summand_vector_type f_summands;
84 : bool f_counter_example;
85 : bool f_all_violations;
86 : std::string f_dot_file_name;
87 : void print_counter_example();
88 : void save_dot_file(std::size_t a_summand_number);
89 : bool check_init(const data::data_expression& a_invariant);
90 : bool check_summand(const data::data_expression& a_invariant, const action_summand_type& a_summand, const std::size_t a_summand_number);
91 : bool check_summands(const data::data_expression& a_invariant);
92 : public:
93 :
94 : /// precondition: the argument passed as parameter a_lps is a valid mCRL2 LPS
95 : /// precondition: the argument passed as parameter a_time_limit is greater than or equal to 0. If the argument is equal
96 : /// to 0, no time limit will be enforced
97 : Invariant_Checker(
98 : const Specification& a_lps,
99 : data::rewriter::strategy a_rewrite_strategy = data::jitty,
100 : int a_time_limit = 0,
101 : bool a_path_eliminator = false,
102 : data::detail::smt_solver_type a_solver_type = data::detail::solver_type_cvc,
103 : bool a_apply_induction = false,
104 : bool a_counter_example = false,
105 : bool a_all_violations = false,
106 : const std::string& a_dot_file_name = std::string()
107 : );
108 :
109 : /// precondition: the argument passed as parameter a_invariant is a valid expression in internal mCRL2 format
110 : bool check_invariant(const data::data_expression& a_invariant);
111 : };
112 :
113 : // Class Invariant_Checker ------------------------------------------------------------------------
114 : // Class Invariant_Checker - Functions declared private -----------------------------------------
115 :
116 : template <typename Specification>
117 0 : void Invariant_Checker<Specification>::print_counter_example()
118 : {
119 0 : if (f_counter_example)
120 : {
121 0 : data::data_expression v_counter_example(f_bdd_prover.get_counter_example());
122 0 : assert(v_counter_example.defined());
123 0 : mCRL2log(log::info) << " Counter example: " << data::pp(v_counter_example) << "\n";
124 0 : }
125 0 : }
126 :
127 : // --------------------------------------------------------------------------------------------
128 :
129 : template <typename Specification>
130 0 : void Invariant_Checker<Specification>::save_dot_file(std::size_t a_summand_number)
131 : {
132 0 : if (!f_dot_file_name.empty())
133 : {
134 0 : std::string v_file_name=f_dot_file_name;
135 :
136 0 : if (a_summand_number == (std::size_t)-1) // Dangerous
137 : {
138 0 : v_file_name += "-init.dot";
139 : }
140 : else
141 : {
142 0 : v_file_name += "-" + std::to_string(a_summand_number) + ".dot";
143 : }
144 0 : f_bdd2dot.output_bdd(f_bdd_prover.get_bdd(), v_file_name);
145 0 : }
146 0 : }
147 :
148 : // --------------------------------------------------------------------------------------------
149 :
150 : template <typename Specification>
151 4 : bool Invariant_Checker<Specification>::check_init(const data::data_expression& a_invariant)
152 : {
153 4 : data::mutable_map_substitution<> v_substitutions;
154 4 : const data::variable_list& d = f_spec.process().process_parameters();
155 4 : const data::data_expression_list& e = f_init.expressions();
156 4 : auto di = d.begin();
157 4 : auto ei = e.begin();
158 21 : for (; di != d.end(); ++di, ++ei)
159 : {
160 17 : v_substitutions[*di] = *ei;
161 : }
162 :
163 4 : data::data_expression b_invariant = data::replace_variables_capture_avoiding(a_invariant, v_substitutions);
164 4 : f_bdd_prover.set_formula(b_invariant);
165 4 : if (f_bdd_prover.is_tautology() == data::detail::answer_yes)
166 : {
167 4 : return true;
168 : }
169 : else
170 : {
171 0 : if (f_bdd_prover.is_contradiction() != data::detail::answer_yes)
172 : {
173 0 : print_counter_example();
174 0 : save_dot_file((std::size_t)(-1));
175 : }
176 0 : return false;
177 : }
178 4 : }
179 :
180 : // --------------------------------------------------------------------------------------------
181 :
182 : template <typename Specification>
183 22 : bool Invariant_Checker<Specification>::check_summand(
184 : const data::data_expression& a_invariant,
185 : const action_summand_type& a_summand,
186 : const std::size_t a_summand_number)
187 : {
188 : using namespace data::sort_bool;
189 22 : const data::data_expression& v_condition = a_summand.condition();
190 :
191 22 : data::mutable_map_substitution<> v_substitutions;
192 :
193 104 : for (const data::assignment& a: a_summand.assignments())
194 : {
195 60 : v_substitutions[a.lhs()] = a.rhs();
196 : }
197 :
198 22 : const data::data_expression v_subst_invariant = data::replace_variables_capture_avoiding(a_invariant, v_substitutions);
199 :
200 44 : const data::data_expression v_formula = implies(and_(a_invariant, v_condition), v_subst_invariant);
201 22 : f_bdd_prover.set_formula(v_formula);
202 22 : if (f_bdd_prover.is_tautology() == data::detail::answer_yes)
203 : {
204 22 : mCRL2log(log::verbose) << "The invariant holds for summand " << a_summand_number << "." << std::endl;
205 22 : return true;
206 : }
207 : else
208 : {
209 0 : mCRL2log(log::info) << "The invariant does not hold for summand " << a_summand_number << std::endl;
210 0 : if (f_bdd_prover.is_contradiction() != data::detail::answer_yes)
211 : {
212 0 : print_counter_example();
213 0 : save_dot_file(a_summand_number);
214 : }
215 0 : return false;
216 : }
217 22 : }
218 :
219 : // --------------------------------------------------------------------------------------------
220 :
221 : template <typename Specification>
222 4 : bool Invariant_Checker<Specification>::check_summands(const data::data_expression& a_invariant)
223 : {
224 4 : bool v_result = true;
225 4 : std::size_t v_summand_number = 1;
226 :
227 26 : for (auto i = f_summands.begin(); i != f_summands.end() && (f_all_violations || v_result); ++i)
228 : {
229 22 : v_result = check_summand(a_invariant, *i, v_summand_number) && v_result;
230 22 : v_summand_number++;
231 : }
232 4 : return v_result;
233 : }
234 :
235 : // Class Invariant_Checker<Specification> - Functions declared public --------------------------------------------
236 :
237 : template <typename Specification>
238 9 : Invariant_Checker<Specification>::Invariant_Checker(
239 : const Specification& a_lps,
240 : data::rewriter::strategy a_rewrite_strategy, int a_time_limit, bool a_path_eliminator, data::detail::smt_solver_type a_solver_type,
241 : bool a_apply_induction, bool a_counter_example, bool a_all_violations, std::string const& a_dot_file_name
242 : ):
243 9 : f_spec(a_lps),
244 9 : f_bdd_prover(a_lps.data(), data::used_data_equation_selector(a_lps.data()), a_rewrite_strategy, a_time_limit, a_path_eliminator, a_solver_type, a_apply_induction)
245 : {
246 9 : f_init = a_lps.initial_process();
247 9 : f_summands = a_lps.process().action_summands();
248 9 : f_counter_example = a_counter_example;
249 9 : f_all_violations = a_all_violations;
250 9 : f_dot_file_name = a_dot_file_name;
251 9 : }
252 :
253 : // --------------------------------------------------------------------------------------------
254 :
255 : template <typename Specification>
256 4 : bool Invariant_Checker<Specification>::check_invariant(const data::data_expression& a_invariant)
257 : {
258 4 : bool v_result = true;
259 :
260 4 : if (check_init(a_invariant))
261 : {
262 4 : mCRL2log(log::verbose) << "The invariant holds for the initial state." << std::endl;
263 : }
264 : else
265 : {
266 0 : mCRL2log(log::info) << "The invariant does not hold for the initial state." << std::endl;
267 0 : v_result = false;
268 : }
269 4 : if ((f_all_violations || v_result))
270 : {
271 4 : if (check_summands(a_invariant))
272 : {
273 4 : mCRL2log(log::verbose) << "The invariant holds for all summands." << std::endl;
274 : }
275 : else
276 : {
277 0 : mCRL2log(log::info) << "The invariant does not hold for all summands." << std::endl;
278 0 : v_result = false;
279 : }
280 : }
281 4 : if (v_result)
282 : {
283 4 : mCRL2log(log::info) << "The invariant holds for this LPS." << std::endl;
284 : }
285 : else
286 : {
287 0 : mCRL2log(log::info) << "The invariant does not hold for this LPS." << std::endl;
288 : }
289 :
290 4 : return v_result;
291 : }
292 :
293 : } // namespace detail
294 : } // namespace lps
295 : } // namespace mcrl2
296 :
297 : #endif
|
