Line data Source code
1 : // Author(s): Luc Engelen, Djurre van der Wal
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/confluence_checker.h
10 : /// \brief Add your file description here.
11 :
12 : // Interface to class Confluence_Checker
13 : // file: confluence_checker.h
14 :
15 : #ifndef MCRL2_LPS_CONFLUENCE_CHECKER_H
16 : #define MCRL2_LPS_CONFLUENCE_CHECKER_H
17 :
18 : #include "mcrl2/lps/disjointness_checker.h"
19 : #include "mcrl2/lps/invariant_checker.h"
20 : #include <iomanip>
21 :
22 :
23 : /** \brief A class that takes a linear process specification and checks all tau-summands of that LPS for confluence.
24 : \brief The tau actions of all confluent tau-summands are renamed to ctau.
25 :
26 : Given an LPS,
27 :
28 : P(d: D) = ...
29 : + sum ei: Ei. ci(d, ei) -> ai(fi(d, ei)) . P(gi(d, ei))
30 : + ...
31 : + sum ej: Ej. cj(d, ej) -> tau . P(gj(d, ej))
32 : + ...;
33 :
34 :
35 : tau-summand j is confluent with summand i if the following condition holds for all d: D, for all ei: Ei and for all
36 : ej: Ej:
37 :
38 : (inv(d) /\ ci(d, ei) /\ cj(d, ej))
39 : =>
40 : (
41 : ci(gj(d, ej), ei) /\
42 : cj(gi(d, ei), ej) /\
43 : fi(d, ei) == fi(gj(d, ej), ei) /\
44 : gi(gj(d, ej), ei) == gj(gi(d, ei), ej)
45 : )
46 :
47 : where inv() is the invariant specified using the parameter a_invariant of the function
48 : Confluence_Checker::check_confluence_and_mark. In case ai is also a tau-action, the formula above can be weakened to
49 : the following:
50 :
51 : (inv(d) /\ ci(d, ei) /\ cj(d, ej))
52 : =>
53 : (
54 : gi(d, ei) == gj(d, ej) \/
55 : (
56 : ci(gj(d, ej), ei) /\
57 : cj(gi(d, ei), ej) /\
58 : gi(gj(d, ej), ei) == gj(gi(d, ei), ej)
59 : )
60 : )
61 :
62 : The class Confluence_Checker can determine whether two summands are confluent in three ways and will indicate which
63 : of the methods was used while proving confluence. The three ways of determining confluence are as follows:
64 :
65 : If summand number 1 has been proven confluent with summand number 2, summand number 2 is obviously confluent
66 : with summand number 1. This method of checking confluence is called checking confluence by symmetry. If two summands
67 : are confluent by symmetry, the class Confluence_Checker indicates this by printing a dot ('.').
68 :
69 : Another way of checking the confluence of two summands is determining whether the two summands are
70 : syntactically disjoint. Two summands are syntactically disjoint if the following holds:
71 : - The set of variables used by one summand is disjoint from the set of variables changed by the other summand and
72 : vice versa.
73 : - The set of variables changed by one summand is disjoint from the set of variables changed by the other summand.
74 : If two summands are confluent because of syntactic disjointness, the class Confluence_Checker indicates this by
75 : printing a colon (':').
76 :
77 : The most time consuming way of checking the confluence of two summands is generating the confluence condition
78 : and then checking if this condition is a tautology using a prover for expressions of sort Bool. If two summands are
79 : proven confluent using the prover, the class Confluence_Checker indicates this by printing a plus sign ('+'). If the
80 : parameter a_generate_invariants is set to true, the class Confluence_Checker will try to prove that the reduced
81 : confluence condition is an invariant of the LPS, in case the confluence condition is not a tautology. If the reduced
82 : confluence condition is indeed an invariant, the two summands are proven confluent. The class Confluence_Checker
83 : indicates this by printing an 'i'.
84 :
85 : The class Confluence_Checker uses an instance of the class BDD_Prover, an instance of the class Disjointness_Checker
86 : and an instance of the class Invariant_Checker to determine which tau-summands of an mCRL2 LPS are confluent.
87 : Confluent tau-summands will be marked by renaming their tau-actions to ctau. The constructor
88 : Confluence_Checker::Confluence_Checker initializes the BDD based prover with the parameters a_rewrite_strategy,
89 : a_time_limit, a_path_eliminator, a_solver_type, a_apply_induction and a_lps. The parameter a_rewrite_strategy
90 : specifies which rewrite strategy is used by the prover's rewriter. It can be set to either
91 : GS_REWR_JITTY or GS_REWR_JITTYC. The parameter a_time_limit specifies the maximum amount of time in
92 : seconds to be spent by the prover on proving a single expression. If a_time_limit is set to 0, no time limit will be
93 : enforced. The parameter a_path_eliminator specifies whether or not path elimination is applied. When path
94 : elimination is applied, the prover uses an SMT solver to remove inconsistent paths from BDDs. The parameter
95 : a_solver_type specifies which SMT solver is used for path elimination. Either the SMT solver ario
96 : (http://www.eecs.umich.edu/~ario/) or cvc-lite (http://www.cs.nyu.edu/acsys/cvcl/) can be used. To use one of these
97 : solvers, the directory containing the corresponding executable must be in the path. If the parameter
98 : a_path_eliminator is set to false, the parameter a_solver_type is ignored. The parameter a_apply_induction indicates
99 : whether or not induction on list will be applied.
100 :
101 : The parameter a_dot_file_name specifies whether a file in dot format of the resulting BDD is saved each time the
102 : prover cannot determine whether an expression of sort Bool is a contradiction or a tautology. If the parameter is
103 : set to 0, no .dot files are saved. If a string is passed as parameter a_dot_file_name, this string will be used as
104 : the prefix of the filenames. An instance of the class BDD2Dot is used to save these files in dot format.
105 :
106 : If the parameter a_counter_example is set to true, a so called counter example is printed to stderr each time the
107 : prover indicates that two summands are not confluent. A counter example is a valuation for which the confluence
108 : condition to be proven does not hold.
109 :
110 : If the parameter a_check_all is set to true, the confluence of the tau-summands regarding all other summands will be
111 : checked. If the parameter is set to false, Confluence_Checker continues with the next tau-summand as soon as a
112 : summand is encountered that is not confluent with the current tau-summand.
113 :
114 : If the parameter a_generate_invariants is set, an invariant checker is used to check if the reduced confluence
115 : condition is an invariant of the LPS passed as parameter a_lps. If the reduced confluence condition is an invariant,
116 : the two summands are confluent.
117 :
118 : The function Confluence_Checker::check_confluence_and_mark returns an LPS with all tau-actions of confluent
119 : tau-summands renamed to ctau, unless the parameter a_no_marking is set to true. In case the parameter a_no_marking
120 : was set to true, the confluent tau-summands will not be marked, only the results of the confluence checking will be
121 : displayed.
122 :
123 : If there already is an action named ctau present in the LPS passed as parameter a_lps, an error will be reported. */
124 :
125 :
126 : namespace mcrl2
127 : {
128 : namespace lps
129 : {
130 : namespace detail
131 : {
132 :
133 : /**
134 : * \brief Creates an identifier for the for the ctau action
135 : **/
136 10 : inline process::action_label make_ctau_act_id()
137 : {
138 10 : static atermpp::aterm_appl ctau_act_id = atermpp::aterm_appl(core::detail::function_symbol_ActId(), atermpp::aterm_appl(atermpp::function_symbol("ctau", 0)), atermpp::aterm_list());
139 :
140 10 : assert(atermpp::detail::address(ctau_act_id));
141 :
142 10 : return process::action_label(ctau_act_id);
143 : }
144 :
145 : /**
146 : * \brief Creates the ctau action
147 : **/
148 6 : inline process::action make_ctau_action()
149 : {
150 6 : static atermpp::aterm_appl ctau_action = atermpp::aterm_appl(core::detail::function_symbol_Action(), make_ctau_act_id(), atermpp::aterm_list());
151 :
152 6 : assert(atermpp::detail::address(ctau_action));
153 :
154 6 : return process::action(ctau_action);
155 : }
156 :
157 : template <typename Specification>
158 : class Confluence_Checker
159 : {
160 : typedef typename Specification::process_type process_type;
161 : typedef typename process_type::action_summand_type action_summand_type;
162 : typedef std::vector<action_summand_type> action_summand_vector_type;
163 :
164 : private:
165 : /// \brief Class that can check if two summands are disjoint.
166 : Disjointness_Checker f_disjointness_checker;
167 :
168 : /// \brief Class that checks if an invariant holds for an LPS.
169 : Invariant_Checker<Specification> f_invariant_checker;
170 :
171 : /// \brief BDD based prover.
172 : data::detail::BDD_Prover f_bdd_prover;
173 :
174 : /// \brief Class that prints BDDs in dot format.
175 : data::detail::BDD2Dot f_bdd2dot;
176 :
177 : /// \brief A linear process specification.
178 : Specification& f_lps;
179 :
180 : /// \brief Flag indicating whether or not the tau actions of confluent tau summands are renamed to ctau.
181 : // bool f_no_marking;
182 :
183 : /// \brief Flag indicating whether or not the process of checking the confluence of a summand stops when
184 : /// \brief a summand is encountered that is not confluent with the tau summand at hand.
185 : bool f_check_all;
186 :
187 : /// \brief Do not rewrite summands with sum operators.
188 : bool f_no_sums;
189 :
190 : /// \brief Confluence types for which the tool should check.
191 : std::string f_conditions;
192 :
193 : /// \brief Flag indicating whether or not counter examples are printed.
194 : bool f_counter_example;
195 :
196 : /// \brief The prefix for the names of the files written in dot format.
197 : std::string f_dot_file_name;
198 :
199 : /// \brief Flag indicating whether or not invariants are generated and checked each time a
200 : /// \brief summand is encountered that is not confluent with the tau summand at hand.
201 : bool f_generate_invariants;
202 :
203 : /// \brief The number of summands of the current LPS.
204 : std::size_t f_number_of_summands;
205 :
206 : /// \brief An integer array, storing intermediate results per summand.
207 : std::vector <std::size_t> f_intermediate;
208 :
209 : /// \brief Identifier generator to allow variables to be uniquely renamed.
210 : data::set_identifier_generator f_set_identifier_generator;
211 :
212 : /// \brief Writes a dot file of the BDD created when checking the confluence of summands a_summand_number_1 and a_summand_number_2.
213 : void save_dot_file(std::size_t a_summand_number_1, std::size_t a_summand_number_2);
214 :
215 : /// \brief Outputs a path in the BDD corresponding to the condition at hand that leads to a node labelled false.
216 : void print_counter_example();
217 :
218 : /// \brief Checks the confluence of summand a_summand_1 and a_summand_2
219 : bool check_summands(
220 : const data::data_expression& a_invariant,
221 : const action_summand_type a_summand_1,
222 : const std::size_t a_summand_number_1,
223 : const action_summand_type a_summand_2,
224 : const std::size_t a_summand_number_2,
225 : const char a_condition_type);
226 :
227 : /// \brief Checks and updates the confluence of summand a_summand concerning all other tau-summands.
228 : void check_confluence_and_mark_summand(
229 : action_summand_type& a_summand,
230 : const std::size_t a_summand_number,
231 : const data::data_expression& a_invariant,
232 : const char a_condition_type,
233 : bool& a_is_marked);
234 :
235 : // Returns a modified instance of a summand in which summation variables are uniquely renamed.
236 : void uniquely_rename_summutation_variables(
237 : action_summand_type& summand);
238 :
239 : public:
240 : /// \brief Constructor that initializes Confluence_Checker::f_lps, Confluence_Checker::f_bdd_prover,
241 : /// \brief Confluence_Checker::f_generate_invariants and Confluence_Checker::f_dot_file_name.
242 : /// precondition: the argument passed as parameter a_lps is a valid mCRL2 LPS
243 : /// precondition: the argument passed as parameter a_time_limit is greater than or equal to 0. If the argument is equal
244 : /// to 0, no time limit will be enforced
245 : Confluence_Checker
246 : (
247 : Specification& a_lps,
248 : data::rewriter::strategy a_rewrite_strategy = data::jitty,
249 : int a_time_limit = 0,
250 : bool a_path_eliminator = false,
251 : data::detail::smt_solver_type a_solver_type = data::detail::solver_type_cvc,
252 : bool a_apply_induction = false,
253 : bool a_check_all = false,
254 : bool a_no_sums = false,
255 : std::string a_conditions = "c",
256 : bool a_counter_example = false,
257 : bool a_generate_invariants = false,
258 : std::string const& a_dot_file_name = std::string()
259 : );
260 :
261 : /// \brief Check the confluence of the LPS Confluence_Checker::f_lps.
262 : /// precondition: the argument passed as parameter a_invariant is an expression of sort Bool in internal mCRL2 format
263 : /// precondition: the argument passed as parameter a_summand_number corresponds with a summand of the LPS for which
264 : /// confluence must be checked (lowest summand has number 1). If this number is 0 confluence for all summands is checked.
265 : void check_confluence_and_mark(const data::data_expression& a_invariant, const std::size_t a_summand_number);
266 : };
267 :
268 : // Auxiliary functions ----------------------------------------------------------------------------
269 :
270 : static
271 68 : data::mutable_map_substitution<> get_substitutions_from_assignments(const data::assignment_list& a_assignments)
272 : {
273 68 : data::mutable_map_substitution<> v_substitutions;
274 :
275 287 : for (const data::assignment& a_assignment : a_assignments)
276 : {
277 219 : v_substitutions[a_assignment.lhs()]=a_assignment.rhs();
278 : }
279 68 : return v_substitutions;
280 0 : }
281 :
282 : // ----------------------------------------------------------------------------------------------
283 : static
284 34 : data::data_expression get_subst_equation_from_assignments(
285 : const data::variable_list& a_variables,
286 : data::assignment_list a_assignments_1,
287 : data::assignment_list a_assignments_2,
288 : data::mutable_map_substitution<>& a_substitutions_1,
289 : data::mutable_map_substitution<>& a_substitutions_2)
290 : {
291 34 : data::data_expression v_result = data::sort_bool::true_();
292 :
293 34 : const data::assignment_list v_assignment_1, v_assignment_2;
294 34 : data::variable v_variable_1, v_variable_2;
295 34 : data::data_expression v_expression_1, v_expression_2;
296 34 : bool v_next_1 = true, v_next_2 = true;
297 :
298 176 : for (data::variable_list::const_iterator i=a_variables.begin(); i!=a_variables.end();)
299 : {
300 142 : data::variable v_variable = *i;
301 142 : ++i;
302 :
303 142 : if (!a_assignments_1.empty() && v_next_1)
304 : {
305 124 : const data::assignment v_assignment_1 = a_assignments_1.front();
306 124 : a_assignments_1.pop_front();
307 124 : v_variable_1 = v_assignment_1.lhs();
308 124 : v_expression_1 = v_assignment_1.rhs();
309 124 : v_expression_1 = data::replace_variables_capture_avoiding(v_expression_1, a_substitutions_2);
310 124 : }
311 142 : if (!a_assignments_2.empty() && v_next_2)
312 : {
313 95 : const data::assignment v_assignment_2 = a_assignments_2.front();
314 95 : a_assignments_2.pop_front();
315 95 : v_variable_2 = v_assignment_2.lhs();
316 95 : v_expression_2 = v_assignment_2.rhs();
317 95 : v_expression_2 = data::replace_variables_capture_avoiding(v_expression_2, a_substitutions_1);
318 95 : }
319 184 : while (v_variable != v_variable_1 && v_variable != v_variable_2 && i!=a_variables.end())
320 : {
321 42 : v_variable = *i;
322 42 : ++i;
323 : }
324 142 : if (v_variable_1 == v_variable_2)
325 : {
326 87 : v_result = data::sort_bool::and_(v_result, equal_to(v_expression_1, v_expression_2));
327 87 : v_next_1 = true;
328 87 : v_next_2 = true;
329 : }
330 55 : else if (v_variable == v_variable_1)
331 : {
332 40 : data::data_expression expr = data::replace_variables_capture_avoiding(data::data_expression(v_variable_1), a_substitutions_1);
333 40 : v_result = data::sort_bool::and_(data::data_expression(v_result), equal_to(v_expression_1, expr));
334 40 : v_next_1 = true;
335 40 : v_next_2 = false;
336 40 : }
337 15 : else if (v_variable == v_variable_2)
338 : {
339 11 : data::data_expression expr = data::replace_variables_capture_avoiding(data::data_expression(v_variable_2), a_substitutions_2);
340 11 : v_result = data::sort_bool::and_(data::data_expression(v_result), equal_to(data::data_expression(v_expression_2), expr));
341 11 : v_next_1 = false;
342 11 : v_next_2 = true;
343 11 : }
344 142 : }
345 68 : return v_result;
346 34 : }
347 :
348 : // ----------------------------------------------------------------------------------------------
349 :
350 : static
351 19 : data::data_expression get_equation_from_assignments(
352 : const data::variable_list& a_variables,
353 : data::assignment_list a_assignments_1,
354 : data::assignment_list a_assignments_2)
355 : {
356 19 : data::data_expression v_result = data::sort_bool::true_();
357 :
358 128 : for (const data::variable& v_variable : a_variables)
359 : {
360 109 : if (!a_assignments_1.empty() && v_variable == a_assignments_1.front().lhs())
361 : {
362 75 : if (!a_assignments_2.empty() && v_variable == a_assignments_2.front().lhs())
363 : {
364 : // Create a condition from the assigments from both lists.
365 55 : v_result = data::sort_bool::and_(v_result, equal_to(a_assignments_1.front().rhs(), a_assignments_2.front().rhs()));
366 55 : a_assignments_2.pop_front();
367 : }
368 : else
369 : {
370 : // Create a condition from first assigment only.
371 20 : v_result = data::sort_bool::and_(v_result, equal_to(a_assignments_1.front().rhs(), v_variable));
372 : }
373 75 : a_assignments_1.pop_front();
374 : }
375 : else
376 : {
377 34 : if (!a_assignments_2.empty() && v_variable == a_assignments_2.front().lhs())
378 : {
379 : // Create a condition from the second assigments only.
380 9 : v_result = data::sort_bool::and_(v_result, equal_to(v_variable, a_assignments_2.front().rhs()));
381 9 : a_assignments_2.pop_front();
382 : }
383 : }
384 : }
385 :
386 19 : assert(a_assignments_1.empty()); // If this is not the case, the assignments do not have the
387 19 : assert(a_assignments_2.empty()); // same order as the list of variables. This means that some equations
388 : // have not been generated.
389 19 : return v_result;
390 0 : }
391 :
392 : // ----------------------------------------------------------------------------------------------
393 : inline
394 15 : data::data_expression get_subst_equation_from_actions(
395 : const process::action_list& a_actions,
396 : data::mutable_map_substitution<>& a_substitutions)
397 : {
398 15 : data::data_expression v_result = data::sort_bool::true_();
399 :
400 30 : for (const process::action& a_action: a_actions)
401 : {
402 15 : const data::data_expression_list v_expressions = a_action.arguments();
403 25 : for (const data::data_expression& v_expression : v_expressions)
404 : {
405 10 : const data::data_expression v_subst_expression = data::replace_variables_capture_avoiding(v_expression, a_substitutions);
406 10 : v_result = data::sort_bool::and_(data::data_expression(v_result), equal_to(v_expression, v_subst_expression));
407 10 : }
408 15 : }
409 15 : return v_result;
410 0 : }
411 :
412 : // ----------------------------------------------------------------------------------------------
413 :
414 0 : static data::assignment_list get_full_assignment_list(
415 : data::assignment_list a_assignment_list,
416 : const data::variable_list& a_variables)
417 : {
418 0 : data::assignment_list v_new_list;
419 :
420 0 : for (const data::variable& v_variable: a_variables)
421 : {
422 0 : bool v_assignment_added = false;
423 :
424 0 : if (!a_assignment_list.empty())
425 : {
426 0 : const data::assignment v_assignment = a_assignment_list.front();
427 0 : a_assignment_list.pop_front();
428 :
429 0 : if (v_assignment.lhs() == v_variable)
430 : {
431 0 : v_new_list.push_front(v_assignment);
432 0 : v_assignment_added = true;
433 : }
434 0 : }
435 :
436 0 : if (!v_assignment_added)
437 : {
438 0 : v_new_list.push_front(data::assignment(v_variable, v_variable));
439 : }
440 : }
441 :
442 0 : return atermpp::reverse(v_new_list);
443 0 : }
444 :
445 : // ----------------------------------------------------------------------------------------------
446 :
447 : template <typename ActionSummand>
448 34 : data::data_expression get_confluence_condition(
449 : const data::data_expression& a_invariant,
450 : const ActionSummand& a_summand_1,
451 : const ActionSummand& a_summand_2,
452 : const data::variable_list& a_variables,
453 : const char condition_type)
454 : {
455 34 : assert(a_summand_1.is_tau());
456 :
457 34 : if (condition_type == 'c' || condition_type == 'C') //Commutative confluence.
458 : {
459 34 : const data::data_expression& v_condition_1 = a_summand_1.condition();
460 34 : const data::assignment_list& v_assignments_1 = a_summand_1.assignments();
461 :
462 34 : data::mutable_map_substitution<> v_substitutions_1 = get_substitutions_from_assignments(v_assignments_1);
463 34 : const data::data_expression& v_condition_2 = a_summand_2.condition();
464 68 : const data::data_expression v_lhs = data::sort_bool::and_(data::sort_bool::and_(v_condition_1, v_condition_2), a_invariant);
465 34 : const data::assignment_list& v_assignments_2 = a_summand_2.assignments();
466 :
467 34 : data::mutable_map_substitution<> v_substitutions_2 = get_substitutions_from_assignments(v_assignments_2);
468 34 : const data::data_expression v_subst_condition_1 = data::replace_variables_capture_avoiding(v_condition_1, v_substitutions_2);
469 34 : const data::data_expression v_subst_condition_2 = data::replace_variables_capture_avoiding(v_condition_2, v_substitutions_1);
470 :
471 68 : const data::data_expression v_subst_equation = get_subst_equation_from_assignments(a_variables, v_assignments_1, v_assignments_2, v_substitutions_1, v_substitutions_2);
472 :
473 34 : const process::action_list v_actions = a_summand_2.multi_action().actions();
474 34 : data::data_expression v_rhs;
475 :
476 34 : if (v_actions.empty())
477 : {
478 : // tau-summand
479 38 : const data::data_expression v_equation = get_equation_from_assignments(a_variables, v_assignments_1, v_assignments_2);
480 19 : v_rhs = data::sort_bool::and_(v_subst_condition_1, v_subst_condition_2);
481 19 : v_rhs = data::sort_bool::and_(v_rhs, v_subst_equation);
482 19 : v_rhs = data::sort_bool::or_(v_equation, v_rhs);
483 19 : }
484 : else
485 : {
486 : // non-tau-summand
487 15 : const data::data_expression v_actions_equation = get_subst_equation_from_actions(v_actions, v_substitutions_1);
488 15 : v_rhs = data::sort_bool::and_(v_subst_condition_1, v_subst_condition_2);
489 15 : v_rhs = data::sort_bool::and_(v_rhs, v_actions_equation);
490 15 : v_rhs = data::sort_bool::and_(v_rhs, data::data_expression(v_subst_equation));
491 15 : }
492 34 : return data::sort_bool::implies(v_lhs, v_rhs);
493 34 : }
494 0 : else if (condition_type == 'T') //Triangular confluence
495 : {
496 0 : const data::data_expression& v_condition_1 = a_summand_1.condition();
497 0 : const data::data_expression& v_condition_2 = a_summand_2.condition();
498 :
499 0 : const data::assignment_list& v_assignments_1 = a_summand_1.assignments();
500 0 : const data::assignment_list v_assignments_2 = get_full_assignment_list(a_summand_2.assignments(), a_variables);
501 :
502 0 : const process::action_list v_actions = a_summand_2.multi_action().actions();
503 :
504 0 : data::mutable_map_substitution<> v_substitutions_1 = get_substitutions_from_assignments(v_assignments_1);
505 0 : data::mutable_map_substitution<> v_substitutions_2;
506 :
507 0 : const data::data_expression v_subst_condition_2 = data::replace_variables_capture_avoiding(v_condition_2, v_substitutions_1);
508 0 : const data::data_expression v_subst_equation = get_subst_equation_from_assignments(a_variables, v_assignments_2, v_assignments_2, v_substitutions_1, v_substitutions_2);
509 :
510 0 : data::data_expression v_lhs = data::sort_bool::and_(data::sort_bool::and_(v_condition_1, v_condition_2), a_invariant);
511 0 : data::data_expression v_rhs = data::sort_bool::and_(v_subst_condition_2, v_subst_equation);
512 :
513 0 : if (v_actions.empty())
514 : {
515 : // tau-summand
516 0 : const data::data_expression v_equation = get_equation_from_assignments(a_variables, v_assignments_1, v_assignments_2);
517 0 : v_rhs = data::sort_bool::or_(v_rhs, v_equation);
518 0 : }
519 : else
520 : {
521 : // non-tau-summand
522 0 : const data::data_expression v_actions_equation = get_subst_equation_from_actions(v_actions, v_substitutions_1);
523 0 : v_rhs = data::sort_bool::and_(v_rhs, v_actions_equation);
524 0 : }
525 0 : return data::sort_bool::implies(v_lhs, v_rhs);
526 0 : }
527 0 : else if (condition_type == 'Z') //Trivial confluence
528 : {
529 0 : const data::data_expression& v_condition_1 = a_summand_1.condition();
530 0 : const data::data_expression& v_condition_2 = a_summand_2.condition();
531 :
532 0 : const data::assignment_list& v_assignments_1 = a_summand_1.assignments();
533 0 : const data::assignment_list& v_assignments_2 = a_summand_2.assignments();
534 :
535 0 : data::mutable_map_substitution<> v_substitutions_1;
536 0 : data::mutable_map_substitution<> v_substitutions_2;
537 :
538 0 : const process::action_list v_actions = a_summand_2.multi_action().actions();
539 :
540 0 : const data::data_expression& v_lhs = v_condition_1;
541 0 : data::data_expression v_rhs;
542 :
543 0 : if (v_actions.empty())
544 : {
545 : // tau-summand
546 0 : data::data_expression v_subst_equation = get_subst_equation_from_assignments(a_variables, v_assignments_1, v_assignments_2, v_substitutions_1, v_substitutions_2);
547 0 : v_rhs = data::sort_bool::or_(data::sort_bool::not_(v_condition_2), v_subst_equation);
548 0 : }
549 : else
550 : {
551 : // non-tau-summand
552 0 : v_rhs = data::sort_bool::not_(v_condition_2);
553 : }
554 0 : return data::sort_bool::implies(v_lhs, v_rhs);
555 0 : }
556 :
557 0 : return data::sort_bool::false_();
558 : }
559 :
560 : // --------------------------------------------------------------------------------------------
561 :
562 : template <typename Specification>
563 7 : bool has_ctau_action(const Specification& a_lps)
564 : {
565 7 : const process::action_label_list& v_action_specification = a_lps.action_labels();
566 7 : return std::find(v_action_specification.begin(),v_action_specification.end(),make_ctau_act_id())!=v_action_specification.end();
567 : }
568 :
569 :
570 : // Class Confluence_Checker -----------------------------------------------------------------------
571 : // Class Confluence_Checker - Functions declared private ----------------------------------------
572 :
573 : template <typename Specification>
574 2 : void Confluence_Checker<Specification>::save_dot_file(std::size_t a_summand_number_1, std::size_t a_summand_number_2)
575 : {
576 2 : if (!f_dot_file_name.empty())
577 : {
578 0 : f_bdd2dot.output_bdd(f_bdd_prover.get_bdd(), f_dot_file_name + "-" + std::to_string(a_summand_number_1) + "-" + std::to_string(a_summand_number_2) + ".dot");
579 : }
580 2 : }
581 :
582 : // --------------------------------------------------------------------------------------------
583 :
584 : template <typename Specification>
585 2 : void Confluence_Checker<Specification>::print_counter_example()
586 : {
587 2 : if (f_counter_example)
588 : {
589 0 : const data::data_expression v_counter_example(f_bdd_prover.get_counter_example());
590 0 : mCRL2log(log::info) << " Counter example: " << v_counter_example << "\n";
591 0 : }
592 2 : }
593 :
594 : // --------------------------------------------------------------------------------------------
595 :
596 : template <typename Specification>
597 34 : void Confluence_Checker<Specification>::uniquely_rename_summutation_variables(
598 : action_summand_type& summand)
599 : {
600 34 : data::mutable_map_substitution<> v_substitutions;
601 34 : std::set<data::variable> v_substitution_variables;
602 :
603 34 : data::variable_list summation_variables = summand.summation_variables();
604 34 : data::assignment_list assignments = summand.assignments();
605 34 : data::data_expression condition = summand.condition();
606 34 : process::action_list actions = summand.multi_action().actions();
607 :
608 : //Compose the substitution map.
609 : //Simultaneously, create a list of the new summation variables.
610 34 : data::variable_list new_summation_variables = data::variable_list();
611 :
612 73 : for (const data::variable& summation_variable : summation_variables)
613 : {
614 5 : core::identifier_string new_name = f_set_identifier_generator(summation_variable.name());
615 : // mCRL2log(log::verbose) << "Renamed " << i->name() << " to " << new_name << std::endl;
616 :
617 5 : data::variable renamed_variable = data::variable(new_name, summation_variable.sort());
618 5 : new_summation_variables.push_front(renamed_variable);
619 5 : v_substitutions[summation_variable] = renamed_variable;
620 : }
621 :
622 34 : new_summation_variables = atermpp::reverse(new_summation_variables);
623 34 : v_substitution_variables = data::substitution_variables(v_substitutions);
624 :
625 : //Create the new condition.
626 34 : data::data_expression new_condition = data::replace_variables(summand.condition(), v_substitutions);
627 :
628 : //Create the new (multi-)action.
629 34 : process::action_list new_actions = process::action_list();
630 :
631 83 : for (const process::action& i : actions)
632 : {
633 15 : data::data_expression_list new_arguments = data::data_expression_list();
634 :
635 40 : for (const data::data_expression& argument : i.arguments())
636 : {
637 10 : new_arguments.push_front(data::replace_variables(argument, v_substitutions));
638 : }
639 :
640 15 : new_actions.push_front(process::action(i.label(), atermpp::reverse(new_arguments)));
641 : }
642 :
643 68 : multi_action new_multi_action = multi_action(atermpp::reverse(new_actions));
644 :
645 : //Create the new assignments (essentially the summand's next-state function).
646 34 : data::assignment_list new_assignments = data::assignment_list();
647 :
648 163 : for (const data::assignment& i: assignments)
649 : {
650 95 : data::data_expression rhs = data::replace_variables(i.rhs(), v_substitutions);
651 95 : new_assignments.push_front(data::assignment(i.lhs(), rhs));
652 : }
653 :
654 34 : new_assignments = atermpp::reverse(new_assignments);
655 :
656 : //Create a new summand from the components.
657 34 : summand.summation_variables() = new_summation_variables;
658 34 : summand.condition() = new_condition;
659 34 : summand.assignments() = new_assignments;
660 34 : summand.multi_action() = new_multi_action;
661 34 : }
662 :
663 : // --------------------------------------------------------------------------------------------
664 :
665 : template <typename Specification>
666 44 : bool Confluence_Checker<Specification>::check_summands(
667 : const data::data_expression& a_invariant,
668 : const action_summand_type a_summand_1,
669 : const std::size_t a_summand_number_1,
670 : const action_summand_type a_summand_2,
671 : const std::size_t a_summand_number_2,
672 : const char a_condition_type)
673 : {
674 44 : assert(a_summand_1.is_tau());
675 :
676 44 : const data::variable_list v_variables = f_lps.process().process_parameters();
677 44 : bool v_is_confluent = true;
678 :
679 44 : if ((a_condition_type == 'c' || a_condition_type == 'd') && f_disjointness_checker.disjoint(a_summand_number_1, a_summand_number_2))
680 : {
681 10 : mCRL2log(log::info) << ":";
682 : }
683 : else
684 : {
685 34 : action_summand_type tagged = a_summand_2;
686 :
687 34 : if (!f_no_sums)
688 : {
689 34 : uniquely_rename_summutation_variables(tagged);
690 : }
691 :
692 34 : const data::data_expression v_condition = get_confluence_condition(a_invariant, a_summand_1, tagged, v_variables, a_condition_type);
693 34 : f_bdd_prover.set_formula(v_condition);
694 34 : if (f_bdd_prover.is_tautology() == data::detail::answer_yes)
695 : {
696 32 : mCRL2log(log::info) << "+";
697 : }
698 : else
699 : {
700 2 : if (f_generate_invariants)
701 : {
702 0 : const data::data_expression v_new_invariant(f_bdd_prover.get_bdd());
703 0 : mCRL2log(log::verbose) << "\nChecking invariant: " << data::pp(v_new_invariant) << "\n";
704 0 : if (f_invariant_checker.check_invariant(v_new_invariant))
705 : {
706 0 : mCRL2log(log::verbose) << "Invariant holds" << std::endl;
707 0 : mCRL2log(log::info) << "i";
708 : }
709 : else
710 : {
711 0 : mCRL2log(log::verbose) << "Invariant doesn't hold" << std::endl;
712 0 : v_is_confluent = false;
713 0 : if (f_check_all)
714 : {
715 0 : mCRL2log(log::info) << "-";
716 : }
717 : else
718 : {
719 0 : mCRL2log(log::info) << "Not confluent with summand " << a_summand_number_2 << ".";
720 : }
721 0 : print_counter_example();
722 0 : save_dot_file(a_summand_number_1, a_summand_number_2);
723 : }
724 0 : }
725 : else
726 : {
727 2 : v_is_confluent = false;
728 2 : if (f_check_all)
729 : {
730 0 : mCRL2log(log::info) << "-";
731 : }
732 : else
733 : {
734 2 : mCRL2log(log::info) << "Not confluent with summand " << a_summand_number_2 << ".";
735 : }
736 2 : print_counter_example();
737 2 : save_dot_file(a_summand_number_1, a_summand_number_2);
738 : }
739 : }
740 34 : }
741 44 : return v_is_confluent;
742 44 : }
743 :
744 : // --------------------------------------------------------------------------------------------
745 :
746 : template <typename Specification>
747 9 : void Confluence_Checker<Specification>::check_confluence_and_mark_summand(
748 : action_summand_type& a_summand,
749 : const std::size_t a_summand_number,
750 : const data::data_expression& a_invariant,
751 : const char a_condition_type,
752 : bool& a_is_marked)
753 : {
754 : typedef typename Specification::process_type::action_summand_type action_summand_type;
755 9 : assert(a_summand.is_tau());
756 9 : std::vector<action_summand_type>& v_summands = f_lps.process().action_summands();
757 9 : std::size_t v_summand_number = 1;
758 9 : bool v_is_confluent = true;
759 :
760 : // Add here that the sum variables of a_summand must be empty otherwise
761 : // the confluence of the summand must be checked with respect to itself,
762 : // which requires quantification. Otherwise tau.a+tau.b will be designated
763 : // tau-confluent, if linearised with summand clustering.
764 :
765 9 : if (f_no_sums)
766 : {
767 0 : const data::variable_list a_summand_sum_variables=a_summand.summation_variables();
768 0 : if (!a_summand_sum_variables.empty())
769 : {
770 0 : v_is_confluent = false;
771 0 : mCRL2log(log::info) << "Summand " << a_summand_number << " is not proven confluent because it contains a sum operator.";
772 : }
773 0 : }
774 :
775 64 : for (typename std::vector<action_summand_type>::const_iterator i=v_summands.begin(); i!=v_summands.end() && (v_is_confluent || f_check_all); ++i)
776 : {
777 55 : const action_summand_type v_summand = *i;
778 :
779 55 : if (v_summand_number < a_summand_number)
780 : {
781 : // Check the cache
782 29 : if (f_intermediate[v_summand_number] > a_summand_number)
783 : {
784 10 : mCRL2log(log::info) << ".";
785 : }
786 : else
787 : {
788 19 : if (f_intermediate[v_summand_number] == a_summand_number)
789 : {
790 1 : if (f_check_all)
791 : {
792 0 : mCRL2log(log::info) << "-";
793 : }
794 : else
795 : {
796 1 : mCRL2log(log::info) << "Not confluent with summand " << v_summand_number << ".";
797 : }
798 1 : v_is_confluent = false;
799 : }
800 : else
801 : {
802 18 : v_is_confluent &= check_summands(a_invariant, a_summand, a_summand_number, v_summand, v_summand_number, a_condition_type);
803 : }
804 : }
805 : }
806 : else
807 : {
808 26 : v_is_confluent &= check_summands(a_invariant, a_summand, a_summand_number, v_summand, v_summand_number, a_condition_type);
809 : }
810 55 : if (v_is_confluent || f_check_all)
811 : {
812 : // Only increase number if we will continue
813 52 : v_summand_number++;
814 : }
815 : }
816 :
817 9 : if (!f_check_all)
818 : {
819 9 : f_intermediate[a_summand_number] = v_summand_number;
820 : }
821 :
822 9 : if (v_is_confluent)
823 : {
824 6 : mCRL2log(log::info) << "Confluent with all summands.";
825 6 : a_is_marked = true;
826 6 : a_summand.multi_action() = multi_action(make_ctau_action());
827 : }
828 9 : }
829 :
830 : // Class Confluence_Checker - Functions declared public -----------------------------------------
831 :
832 : template <typename Specification>
833 5 : Confluence_Checker<Specification>::Confluence_Checker(
834 : Specification& a_lps,
835 : data::rewriter::strategy a_rewrite_strategy,
836 : int a_time_limit,
837 : bool a_path_eliminator,
838 : data::detail::smt_solver_type a_solver_type,
839 : bool a_apply_induction,
840 : bool a_check_all,
841 : bool a_no_sums,
842 : std::string a_conditions,
843 : bool a_counter_example,
844 : bool a_generate_invariants,
845 : std::string const& a_dot_file_name):
846 5 : f_disjointness_checker(a_lps.process()),
847 5 : f_invariant_checker(a_lps, a_rewrite_strategy, a_time_limit, a_path_eliminator, a_solver_type, false, false, 0),
848 5 : f_bdd_prover(a_lps.data(), data::used_data_equation_selector(a_lps.data()), a_rewrite_strategy,
849 : a_time_limit, a_path_eliminator, a_solver_type, a_apply_induction),
850 5 : f_lps(a_lps),
851 5 : f_check_all(a_check_all),
852 5 : f_no_sums(a_no_sums),
853 5 : f_conditions(a_conditions),
854 5 : f_counter_example(a_counter_example),
855 5 : f_dot_file_name(a_dot_file_name),
856 10 : f_generate_invariants(a_generate_invariants)
857 : {
858 5 : if (has_ctau_action(a_lps))
859 : {
860 0 : throw mcrl2::runtime_error("An action named \'ctau\' already exists.\n");
861 : }
862 :
863 5 : std::string v_conditions = std::string(f_conditions);
864 :
865 10 : while (v_conditions.length() > 0)
866 : {
867 5 : char v_ct = v_conditions.at(0);
868 5 : v_conditions = v_conditions.substr(1);
869 :
870 5 : if (v_ct != 'c' && v_ct != 'd' && v_ct != 'C' && v_ct != 'T' && v_ct != 'Z')
871 : {
872 0 : std::string msg = std::string("Unknown confluence type: ");
873 0 : msg += v_ct;
874 0 : msg += '.';
875 :
876 0 : throw mcrl2::runtime_error(msg);
877 0 : }
878 : }
879 5 : }
880 :
881 : // --------------------------------------------------------------------------------------------
882 :
883 : template <typename Specification>
884 5 : void Confluence_Checker<Specification>::check_confluence_and_mark(const data::data_expression& a_invariant, const std::size_t a_summand_number)
885 : {
886 : typedef typename Specification::process_type::action_summand_type action_summand_type;
887 5 : typename Specification::process_type& v_process_equation = f_lps.process();
888 5 : std::vector<action_summand_type>& v_summands = v_process_equation.action_summands();
889 5 : bool v_is_marked = false;
890 :
891 5 : std::size_t v_summand_number = 1;
892 5 : std::set<std::size_t> v_unmarked_summands;
893 5 : std::set<std::size_t> v_marked_summands;
894 :
895 25 : for (const action_summand_type& s: v_summands)
896 : {
897 20 : if ((a_summand_number == v_summand_number) || (a_summand_number == 0))
898 : {
899 20 : if (s.is_tau())
900 : {
901 9 : v_unmarked_summands.insert(v_summand_number);
902 : }
903 : }
904 20 : v_summand_number++;
905 : }
906 :
907 5 : f_set_identifier_generator.clear_context();
908 5 : f_set_identifier_generator.add_identifiers(find_identifiers(f_lps));
909 5 : f_set_identifier_generator.add_identifiers(data::function_and_mapping_identifiers(f_lps.data()));
910 :
911 5 : f_number_of_summands = v_summands.size();
912 5 : std::string v_conditions = std::string(f_conditions);
913 :
914 10 : while (v_conditions.length() > 0)
915 : {
916 5 : f_intermediate = std::vector<std::size_t>(f_number_of_summands + 2, 0);
917 5 : char v_condition_type = v_conditions.at(0);
918 5 : v_conditions = v_conditions.substr(1);
919 5 : v_summand_number = 1;
920 :
921 25 : for (action_summand_type& s: v_summands)
922 : {
923 20 : std::set<std::size_t>::iterator it = v_unmarked_summands.find(v_summand_number);
924 :
925 20 : if (it != v_unmarked_summands.end())
926 : {
927 9 : bool summand_is_marked = false;
928 :
929 9 : mCRL2log(log::info) << "summand " << std::setw(3) << v_summand_number << " of " << v_summands.size() << " (condition = " << v_condition_type << "): ";
930 9 : check_confluence_and_mark_summand(s, v_summand_number, a_invariant, v_condition_type, summand_is_marked);
931 9 : mCRL2log(log::info) << std::endl;
932 :
933 9 : if (summand_is_marked)
934 : {
935 6 : v_marked_summands.insert(v_summand_number);
936 6 : v_unmarked_summands.erase(it);
937 6 : v_is_marked = true;
938 : }
939 : }
940 20 : v_summand_number++;
941 : }
942 : }
943 :
944 5 : if (v_is_marked && !has_ctau_action(f_lps))
945 : {
946 2 : f_lps.action_labels().push_front(make_ctau_act_id());
947 : }
948 :
949 10 : mCRL2log(log::info) << v_marked_summands.size() << " of " << (v_marked_summands.size() + v_unmarked_summands.size()) <<
950 5 : " tau summands were found to be confluent" << std::endl;
951 :
952 5 : f_intermediate = std::vector<std::size_t>();
953 5 : }
954 :
955 : } // namespace detail
956 : } // namespace lps
957 : } // namespace mcrl2
958 : #endif
|
