Line data Source code
1 : // Author(s): Wieger Wesselink
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/pbes/bisimulation.h
10 : /// \brief Bisimulation algorithms.
11 :
12 : #ifndef MCRL2_PBES_BISIMULATION_H
13 : #define MCRL2_PBES_BISIMULATION_H
14 :
15 : #include "mcrl2/data/merge_data_specifications.h"
16 : #include "mcrl2/lps/replace.h"
17 : #include "mcrl2/pbes/detail/lps2pbes_utility.h"
18 : #include "mcrl2/pbes/join.h"
19 :
20 : namespace mcrl2
21 : {
22 :
23 : namespace pbes_system
24 : {
25 :
26 : /// \brief Base class for bisimulation algorithms.
27 : class bisimulation_algorithm
28 : {
29 : public:
30 : /// \brief The iterator type for non-delta summands
31 : typedef lps::action_summand_vector::const_iterator my_iterator;
32 :
33 : protected:
34 : /// \brief A map type for mapping summands to strings.
35 : typedef std::map<const lps::action_summand*, std::string> name_map;
36 :
37 : /// \brief Maps summands to strings.
38 : name_map summand_names;
39 :
40 : /// \brief Store the address of the model.
41 : const lps::linear_process* model_ptr = nullptr;
42 :
43 : /// \brief Generates a name for an action_list.
44 : /// \param l A sequence of actions
45 : /// \return A string representation of the list \p l
46 288 : std::string action_list_name(const process::action_list& l) const
47 : {
48 288 : std::ostringstream out;
49 536 : for (auto i = l.begin(); i != l.end(); ++i)
50 : {
51 248 : out << (i != l.begin() ? "-" : "") << std::string(i->label().name());
52 : }
53 288 : std::string result = out.str();
54 288 : if (result.empty())
55 : {
56 40 : result = "tau";
57 : }
58 576 : return result;
59 288 : }
60 :
61 : /// \brief Returns the name of a summand
62 : /// \param i A summand iterator
63 : /// \return The name of the summand referred to by \p i
64 792 : std::string summand_name(my_iterator i) const
65 : {
66 792 : const lps::action_summand* t = &(*i);
67 792 : auto j = summand_names.find(t);
68 792 : assert(j != summand_names.end());
69 1584 : return j->second;
70 : }
71 :
72 : /// \brief Returns true if p is the linear process of the model.
73 : /// \param p A linear process
74 : /// \return True if p is the linear process of the model.
75 7904 : bool is_from_model(const lps::linear_process& p) const
76 : {
77 7904 : return &p == model_ptr;
78 : }
79 :
80 : /// \brief Returns a name of a linear process.
81 : /// \param p A linear process
82 : /// \return The name of the linear process.
83 7840 : std::string process_name(const lps::linear_process& p) const
84 : {
85 7840 : if (is_from_model(p))
86 : {
87 3920 : return "m";
88 : }
89 : else
90 : {
91 3920 : return "s";
92 : }
93 : }
94 :
95 : /// \brief Used for initializing summand names.
96 : /// \param p A linear process
97 64 : void set_summand_names(const lps::linear_process& p)
98 : {
99 64 : data::set_identifier_generator generator;
100 352 : for (const lps::action_summand& s: p.action_summands())
101 : {
102 576 : std::string name = generator(action_list_name(s.multi_action().actions()));
103 288 : summand_names[&s] = name;
104 288 : }
105 64 : }
106 :
107 : // creates the substitution v[i] := e[i]
108 : // pre: v.size() == e.size()
109 1370 : void make_substitution(const data::variable_list& v, const data::data_expression_list& e, data::mutable_map_substitution<>& result) const
110 : {
111 1370 : assert(v.size() == e.size());
112 1370 : auto vi = v.begin();
113 1370 : auto ei = e.begin();
114 12008 : for (; vi != v.end(); ++vi, ++ei)
115 : {
116 10638 : result[*vi] = *ei;
117 : }
118 1370 : }
119 :
120 : public:
121 : /// \brief Creates a name for the propositional variable Xpq
122 : /// \param p A linear process
123 : /// \param q A linear process
124 : /// \return The name for the propositional variable Xpq
125 3128 : core::identifier_string X(const lps::linear_process& p, const lps::linear_process& q) const
126 : {
127 6256 : std::string s = "X" + process_name(p) + process_name(q);
128 6256 : return core::identifier_string(s);
129 3128 : }
130 :
131 : /// \brief Creates a name for the propositional variable Ypq
132 : /// \param p A linear process
133 : /// \param q A linear process
134 : /// \return The name for the propositional variable Ypq
135 : core::identifier_string Y(const lps::linear_process& p, const lps::linear_process& q) const
136 : {
137 : std::string s = "Y" + process_name(p) + process_name(q);
138 : return core::identifier_string(s);
139 : }
140 :
141 : /// \brief Creates a name for the propositional variable Ypqi
142 : /// \pre The iterator i must be in p.action_summands().
143 : /// \param p A linear process
144 : /// \param q A linear process
145 : /// \param i A summand iterator
146 : /// \return The name for the propositional variable Ypqi
147 344 : core::identifier_string Y(const lps::linear_process& p, const lps::linear_process& q, my_iterator i) const
148 : {
149 688 : std::string s = "Y" + process_name(p) + process_name(q) + "_" + summand_name(i);
150 688 : return core::identifier_string(s);
151 344 : }
152 :
153 : /// \brief Creates a name for the propositional variable Y1pqi
154 : /// \pre The iterator i must be in p.action_summands().
155 : /// \param p A linear process
156 : /// \param q A linear process
157 : /// \param i A summand iterator
158 : /// \return The name for the propositional variable Y1pqi
159 172 : core::identifier_string Y1(const lps::linear_process& p, const lps::linear_process& q, my_iterator i) const
160 : {
161 344 : std::string s = "Y1" + process_name(p) + process_name(q) + "_" + summand_name(i);
162 344 : return core::identifier_string(s);
163 172 : }
164 :
165 : /// \brief Creates a name for the propositional variable Y2pqi
166 : /// \pre The iterator i must be in p.action_summands().
167 : /// \param p A linear process
168 : /// \param q A linear process
169 : /// \param i A summand iterator
170 : /// \return The name for the propositional variable Y2pqi
171 276 : core::identifier_string Y2(const lps::linear_process& p, const lps::linear_process& q, my_iterator i) const
172 : {
173 552 : std::string s = "Y2" + process_name(p) + process_name(q) + "_" + summand_name(i);
174 552 : return core::identifier_string(s);
175 276 : }
176 :
177 : /// \brief Creates a propositional variable.
178 : /// \param name A
179 : /// \param parameters A sequence of data variables
180 : /// \return The created propositional variable
181 392 : propositional_variable_instantiation var(const core::identifier_string& name, const data::variable_list& parameters) const
182 : {
183 392 : return propositional_variable_instantiation(name, atermpp::down_cast<data::data_expression_list>(static_cast<const atermpp::aterm&>(parameters)));
184 : }
185 :
186 : /// \brief Creates a propositional variable.
187 : /// \param name A
188 : /// \param parameters A sequence of data expressions
189 : /// \return The created propositional variable
190 3144 : propositional_variable_instantiation var(const core::identifier_string& name, const data::data_expression_list& parameters) const
191 : {
192 3144 : return propositional_variable_instantiation(name, parameters);
193 : }
194 :
195 : /// \brief Returns a pbes expression that expresses equality of the multi-actions a and b.
196 : /// \param a A sequence of actions
197 : /// \param b A sequence of actions
198 : /// \return Necessary conditions for the equality of a and b
199 2196 : pbes_expression equals(const lps::multi_action& a, const lps::multi_action& b) const
200 : {
201 2196 : return lps::equal_multi_actions(a, b);
202 : }
203 :
204 : /// \brief Returns the fixpoint symbol mu.
205 : /// \return The fixpoint symbol mu.
206 288 : fixpoint_symbol mu() const
207 : {
208 288 : return fixpoint_symbol::mu();
209 : }
210 :
211 : /// \brief Returns the fixpoint symbol nu.
212 : /// \return The fixpoint symbol nu.
213 64 : fixpoint_symbol nu() const
214 : {
215 64 : return fixpoint_symbol::nu();
216 : }
217 :
218 : /// \brief Returns a substitution of variables in q such that there are no name clashes
219 : /// between p and q.
220 : /// \param p A linear process specification
221 : /// \param q A linear process specification
222 : /// \return A substitution that should be applied to q to remove name clashes between p and q.
223 : /// \details After this substitution the following holds:
224 : /// \f[ ((param(p)\cup glob(p))\cap ((param(q)\cup glob(q))=\emptyset \f]
225 : /// where param(p) denotes p.process().process_parameters() and glob(p) denotes p.global_variables().
226 32 : data::mutable_map_substitution<> compute_process_parameter_name_clashes(const lps::specification& p, const lps::specification& q) const
227 : {
228 32 : data::mutable_map_substitution<> result;
229 :
230 : // put the names of variables appearing in p and q in an identifier generator
231 32 : std::set<data::variable> context = lps::find_all_variables(p);
232 32 : std::set<data::variable> vars = lps::find_all_variables(q);
233 32 : context.insert(vars.begin(), vars.end());
234 32 : data::set_identifier_generator generator;
235 164 : for (const data::variable& v: context)
236 : {
237 132 : generator.add_identifier(v.name());
238 : }
239 :
240 : // generate renamings for variables appearing in qvars
241 120 : for (const data::variable& w: q.process().process_parameters())
242 : {
243 176 : data::variable v(generator(w.name()), w.sort());
244 88 : if (v != w)
245 : {
246 88 : result[w] = v;
247 : }
248 88 : }
249 64 : return result;
250 32 : }
251 :
252 : /// \brief Returns a substitution of variables in q such that there are no name clashes
253 : /// between the summation variables of p and q.
254 : /// \param p A linear process specification
255 : /// \param q A linear process specification
256 : /// \return A substitution that should be applied to q to remove name clashes between p and q.
257 32 : data::mutable_map_substitution<> compute_summand_variable_name_clashes(const lps::specification& p, const lps::specification& q) const
258 : {
259 32 : data::mutable_map_substitution<> result;
260 :
261 : // put the names of variables appearing in p and q in an identifier generator
262 32 : std::set<data::variable> context = lps::find_all_variables(p);
263 32 : std::set<data::variable> vars = lps::find_all_variables(q);
264 32 : context.insert(vars.begin(), vars.end());
265 32 : data::set_identifier_generator generator;
266 244 : for (const data::variable& v: context)
267 : {
268 212 : generator.add_identifier(v.name());
269 : }
270 :
271 : // put the summation variables of q in qvars
272 32 : std::set<data::variable> qvars;
273 176 : for (const lps::action_summand& s: q.process().action_summands())
274 : {
275 144 : const data::variable_list& v = s.summation_variables();
276 144 : qvars.insert(v.begin(), v.end());
277 : }
278 52 : for (const lps::deadlock_summand& s: q.process().deadlock_summands())
279 : {
280 20 : const data::variable_list& v = s.summation_variables();
281 20 : qvars.insert(v.begin(), v.end());
282 : }
283 :
284 : // generate renamings for variables appearing in qvars
285 56 : for (const data::variable& w: qvars)
286 : {
287 48 : data::variable v(generator(w.name()), w.sort());
288 24 : if (v != w)
289 : {
290 24 : result[w] = v;
291 : }
292 24 : }
293 64 : return result;
294 32 : }
295 :
296 : /// \brief Resolves name clashes between model and spec.
297 32 : void resolve_name_clashes(const lps::specification& model, lps::specification& spec, bool include_summand_variables = false)
298 : {
299 32 : data::mutable_map_substitution<> sigma = compute_process_parameter_name_clashes(model, spec);
300 32 : lps::replace_process_parameters(spec, sigma);
301 32 : if (include_summand_variables)
302 : {
303 32 : sigma = compute_summand_variable_name_clashes(model, spec);
304 32 : lps::replace_summand_variables(spec, sigma);
305 : }
306 32 : mCRL2log(log::debug) << "bisimulation spec after resolving name clashes:\n" << lps::pp(spec) << std::endl;
307 32 : }
308 :
309 : /// \brief Initializes the name lookup table.
310 : /// \param model A linear process
311 : /// \param spec A linear process
312 : /// \pre model and spec must have the same data specification
313 32 : void init(const lps::linear_process& model, const lps::linear_process& spec)
314 : {
315 32 : summand_names.clear();
316 32 : set_summand_names(model);
317 32 : set_summand_names(spec);
318 32 : model_ptr = &model;
319 32 : assert(is_from_model(model));
320 32 : assert(!is_from_model(spec));
321 32 : }
322 :
323 : /// \brief Builds a pbes from the given equations.
324 : /// \param equations A sequence of pbes equations
325 : /// \param M A specification
326 : /// \param S A specification
327 : /// \return The constructed pbes
328 32 : pbes build_pbes(const std::vector<pbes_equation>& equations,
329 : const lps::specification& M,
330 : const lps::specification& S
331 : )
332 : {
333 32 : const lps::linear_process& m = M.process();
334 32 : const lps::linear_process& s = S.process();
335 :
336 64 : propositional_variable_instantiation init(X(m, s), M.initial_process().expressions() + S.initial_process().expressions());
337 :
338 32 : pbes result(M.data(), equations, init);
339 32 : assert(result.is_closed());
340 64 : return result;
341 32 : }
342 : };
343 :
344 : //--------------------------------------------------------------//
345 : // branching bisimulation
346 : //--------------------------------------------------------------//
347 :
348 : /// \brief Algorithm class for branching bisimulation.
349 : class branching_bisimulation_algorithm : public bisimulation_algorithm
350 : {
351 : public:
352 : /// \brief The match function.
353 : /// \param p A linear process
354 : /// \param q A linear process
355 : /// \return The function result
356 32 : pbes_expression match(const lps::linear_process& p, const lps::linear_process& q) const
357 : {
358 32 : std::vector<pbes_expression> result;
359 176 : for (auto i = p.action_summands().begin(); i != p.action_summands().end(); ++i)
360 : {
361 144 : data::data_expression ci = i->condition();
362 144 : const data::variable_list& d = p.process_parameters();
363 144 : data::variable_list e = i->summation_variables();
364 144 : const data::variable_list& d1 = q.process_parameters();
365 144 : pbes_expression expr;
366 144 : optimized_imp(expr, ci, var(Y(p, q, i), d + d1 + e));
367 144 : expr = make_forall_(e, expr);
368 144 : result.push_back(expr);
369 144 : }
370 64 : return optimized_join_and(result.begin(), result.end());
371 32 : }
372 :
373 : /// \brief The step function.
374 : /// \param p A linear process
375 : /// \param q A linear process
376 : /// \param i A summand iterator
377 : /// \return The function result
378 144 : pbes_expression step(const lps::linear_process& p, const lps::linear_process& q, my_iterator i) const
379 : {
380 144 : const data::variable_list& d1 = q.process_parameters();
381 144 : data::data_expression_list gi = i->next_state(p.process_parameters());
382 144 : if (i->is_tau())
383 : {
384 20 : std::vector<pbes_expression> v;
385 20 : pbes_expression expr;
386 76 : for (auto j = q.action_summands().begin(); j != q.action_summands().end(); ++j)
387 : {
388 56 : if (!j->is_tau())
389 : {
390 40 : continue;
391 : }
392 16 : data::data_expression cj = j->condition();
393 16 : data::variable_list e1 = j->summation_variables();
394 16 : data::data_expression_list gj = j->next_state(q.process_parameters());
395 16 : optimized_and(expr, cj, var(X(p, q), gi + gj));
396 16 : expr = make_exists_(e1, expr);
397 16 : v.push_back(expr);
398 16 : }
399 20 : optimized_or(expr, optimized_join_or(v.begin(), v.end()), var(X(p, q), gi + d1));
400 20 : return expr;
401 20 : }
402 : else
403 : {
404 124 : std::vector<pbes_expression> v;
405 1208 : for (auto j = q.action_summands().begin(); j != q.action_summands().end(); ++j)
406 : {
407 1084 : data::data_expression cj = j->condition();
408 1084 : data::variable_list e1 = j->summation_variables();
409 1084 : data::data_expression_list gj = j->next_state(q.process_parameters());
410 1084 : lps::multi_action ai = i->multi_action();
411 1084 : lps::multi_action aj = j->multi_action();
412 1084 : pbes_expression expr;
413 1084 : optimized_and(expr, cj, equals(ai, aj));
414 1084 : optimized_and(expr, expr, var(X(p, q), gi + gj));
415 1084 : expr = make_exists_(e1, expr);
416 1084 : v.push_back(expr);
417 1084 : }
418 124 : return optimized_join_or(v.begin(), v.end());
419 124 : }
420 144 : }
421 :
422 : /// \brief The close function.
423 : /// \param p A linear process
424 : /// \param q A linear process
425 : /// \param i A summand iterator
426 : /// \return The function result
427 144 : pbes_expression close(const lps::linear_process& p, const lps::linear_process& q, my_iterator i) const
428 : {
429 144 : std::vector<pbes_expression> v;
430 144 : pbes_expression expr;
431 144 : const data::variable_list& d = p.process_parameters();
432 144 : const data::variable_list& d1 = q.process_parameters();
433 144 : data::variable_list e = i->summation_variables();
434 1284 : for (auto j = q.action_summands().begin(); j != q.action_summands().end(); ++j)
435 : {
436 1140 : if (!j->is_tau())
437 : {
438 1084 : continue;
439 : }
440 56 : data::data_expression cj = j->condition();
441 56 : data::variable_list e1 = j->summation_variables();
442 56 : data::data_expression_list gj = j->next_state(q.process_parameters());
443 56 : optimized_and(expr, cj, var(Y(p, q, i),
444 56 : variable_list_to_data_expression_list(d) +
445 112 : gj +
446 56 : data::variable_list_to_data_expression_list(e)));
447 56 : expr = make_exists_(e1, expr);
448 56 : v.push_back(expr);
449 56 : }
450 :
451 144 : optimized_and(expr, var(X(p, q), d + d1), step(p, q, i));
452 144 : optimized_or(expr, optimized_join_or(v.begin(), v.end()), expr);
453 288 : return expr;
454 144 : }
455 :
456 : /// \brief Returns a pbes that expresses branching bisimulation between
457 : /// two specifications.
458 : /// \param model A linear process specification
459 : /// \param spec A linear process specification
460 : /// \return A pbes that expresses branching bisimulation between the
461 : /// two specifications.
462 8 : pbes run(const lps::specification& model, const lps::specification& spec)
463 : {
464 : // resolve name clashes, and merge the data specifications of model and spec
465 8 : data::data_specification dataspec = data::merge_data_specifications(model.data(), spec.data());
466 8 : lps::specification spec1 = spec;
467 8 : lps::specification model1 = model;
468 8 : resolve_name_clashes(model1, spec1, true);
469 8 : model1.data() = dataspec;
470 8 : spec1.data() = dataspec;
471 8 : lps::normalize_sorts(model1, model1.data());
472 8 : lps::normalize_sorts(spec1, spec1.data());
473 :
474 8 : const lps::linear_process& m = model1.process();
475 8 : const lps::linear_process& s = spec1.process();
476 8 : init(m, s);
477 :
478 8 : const data::variable_list& d = m.process_parameters();
479 8 : const data::variable_list& d1 = s.process_parameters();
480 8 : std::vector<pbes_equation> equations;
481 :
482 :
483 : // E1
484 8 : pbes_expression expr;
485 8 : optimized_and(expr, match(m, s), match(s, m));
486 8 : equations.emplace_back(nu(), propositional_variable(X(m, s), d + d1), expr);
487 8 : equations.emplace_back(nu(), propositional_variable(X(s, m), d1 + d), var(X(m, s), d + d1));
488 :
489 : // E2
490 44 : for (auto i = m.action_summands().begin(); i != m.action_summands().end(); ++i)
491 : {
492 36 : data::variable_list e = i->summation_variables();
493 72 : pbes_equation e1(mu(), propositional_variable(Y(m, s, i), d + d1 + e), close(m, s, i));
494 36 : equations.push_back(e1);
495 36 : }
496 44 : for (auto i = s.action_summands().begin(); i != s.action_summands().end(); ++i)
497 : {
498 36 : data::variable_list e = i->summation_variables();
499 72 : pbes_equation e1(mu(), propositional_variable(Y(s, m, i), d1 + d + e), close(s, m, i));
500 36 : equations.push_back(e1);
501 36 : }
502 :
503 16 : return build_pbes(equations, model1, spec1);
504 8 : }
505 : };
506 :
507 : /// \brief Returns a pbes that expresses branching bisimulation between two specifications.
508 : /// \param model A linear process specification
509 : /// \param spec A linear process specification
510 : /// \return A pbes that expresses branching bisimulation between the two specifications.
511 : inline
512 8 : pbes branching_bisimulation(const lps::specification& model, const lps::specification& spec)
513 : {
514 16 : return branching_bisimulation_algorithm().run(model, spec);
515 : }
516 :
517 : //--------------------------------------------------------------//
518 : // strong bisimulation
519 : //--------------------------------------------------------------//
520 :
521 : /// \brief Algorithm class for strong bisimulation.
522 : class strong_bisimulation_algorithm : public bisimulation_algorithm
523 : {
524 : public:
525 : /// \brief The match function.
526 : /// \param p A linear process
527 : /// \param q A linear process
528 : /// \return The function result
529 16 : pbes_expression match(const lps::linear_process& p, const lps::linear_process& q) const
530 : {
531 16 : std::vector<pbes_expression> result;
532 88 : for (auto i = p.action_summands().begin(); i != p.action_summands().end(); ++i)
533 : {
534 72 : data::data_expression ci = i->condition();
535 72 : data::variable_list e = i->summation_variables();
536 72 : pbes_expression expr;
537 72 : optimized_imp(expr, ci, step(p, q, i));
538 72 : expr = make_forall_(e, expr);
539 72 : result.push_back(expr);
540 72 : }
541 32 : return optimized_join_and(result.begin(), result.end());
542 16 : }
543 :
544 : /// \brief The step function.
545 : /// \param p A linear process
546 : /// \param q A linear process
547 : /// \param i A summand iterator
548 : /// \return The function result
549 72 : pbes_expression step(const lps::linear_process& p, const lps::linear_process& q, my_iterator i) const
550 : {
551 72 : data::data_expression_list gi = i->next_state(p.process_parameters());
552 :
553 72 : std::vector<pbes_expression> result;
554 642 : for (auto j = q.action_summands().begin(); j != q.action_summands().end(); ++j)
555 : {
556 570 : data::data_expression cj = j->condition();
557 570 : data::variable_list e1 = j->summation_variables();
558 570 : data::data_expression_list gj = j->next_state(q.process_parameters());
559 570 : lps::multi_action ai = i->multi_action();
560 570 : lps::multi_action aj = j->multi_action();
561 570 : pbes_expression expr;
562 570 : optimized_and(expr, cj, equals(ai, aj));
563 570 : optimized_and(expr, expr, var(X(p, q), gi + gj));
564 570 : expr = make_exists_(e1, expr);
565 570 : result.push_back(expr);
566 570 : }
567 144 : return optimized_join_or(result.begin(), result.end());
568 72 : }
569 :
570 : /// \brief Runs the algorithm
571 : /// \param model A linear process specification
572 : /// \param spec A linear process specification
573 : /// \return A pbes that expresses strong bisimulation between stwo specifications.
574 8 : pbes run(const lps::specification& model, const lps::specification& spec)
575 : {
576 8 : lps::specification spec1 = spec;
577 8 : resolve_name_clashes(model, spec1, true);
578 8 : const lps::linear_process& m = model.process();
579 8 : const lps::linear_process& s = spec1.process();
580 8 : init(m, s);
581 :
582 8 : const data::variable_list& d = m.process_parameters();
583 8 : const data::variable_list& d1 = s.process_parameters();
584 8 : std::vector<pbes_equation> equations;
585 :
586 :
587 : // E
588 8 : pbes_expression expr;
589 8 : optimized_and(expr, match(m, s), match(s, m));
590 8 : equations.emplace_back(nu(), propositional_variable(X(m, s), d + d1), expr);
591 8 : equations.emplace_back(nu(), propositional_variable(X(s, m), d1 + d), var(X(m, s), d + d1));
592 :
593 16 : return build_pbes(equations, model, spec1);
594 8 : }
595 : };
596 :
597 : /// \brief Returns a pbes that expresses strong bisimulation between two specifications.
598 : /// \param model A linear process specification
599 : /// \param spec A linear process specification
600 : /// \return A pbes that expresses strong bisimulation between the two specifications.
601 : inline
602 8 : pbes strong_bisimulation(const lps::specification& model, const lps::specification& spec)
603 : {
604 16 : return strong_bisimulation_algorithm().run(model, spec);
605 : }
606 :
607 : //--------------------------------------------------------------//
608 : // weak bisimulation
609 : //--------------------------------------------------------------//
610 :
611 : /// \brief Algorithm class for weak bisimulation.
612 : class weak_bisimulation_algorithm : public bisimulation_algorithm
613 : {
614 : protected:
615 : mutable data::set_identifier_generator m_generator;
616 :
617 : public:
618 : /// \brief The match function.
619 : /// \param p A linear process
620 : /// \param q A linear process
621 : /// \return The function result
622 16 : pbes_expression match(const lps::linear_process& p, const lps::linear_process& q) const
623 : {
624 16 : std::vector<pbes_expression> result;
625 88 : for (auto i = p.action_summands().begin(); i != p.action_summands().end(); ++i)
626 : {
627 72 : data::data_expression ci = i->condition();
628 72 : const data::variable_list& d = p.process_parameters();
629 72 : data::variable_list e = i->summation_variables();
630 72 : const data::variable_list& d1 = q.process_parameters();
631 72 : pbes_expression expr;
632 72 : optimized_imp(expr, ci, var(Y1(p, q, i), d + d1 + e));
633 72 : expr = make_forall_(e, expr);
634 72 : result.push_back(expr);
635 72 : }
636 32 : return optimized_join_and(result.begin(), result.end());
637 16 : }
638 :
639 : /// \brief The step function.
640 : /// \param p A linear process
641 : /// \param q A linear process
642 : /// \param i A summand iterator
643 : /// \return The function result
644 72 : pbes_expression step(const lps::linear_process& p, const lps::linear_process& q, my_iterator i) const
645 : {
646 72 : const data::variable_list& d1 = q.process_parameters();
647 72 : data::data_expression_list gi = i->next_state(p.process_parameters());
648 72 : lps::multi_action ai(i->multi_action().actions());
649 72 : if (i->is_tau())
650 : {
651 20 : return close2(p, q, i, gi, data::data_expression_list(d1.begin(), d1.end()));
652 : }
653 : else
654 : {
655 62 : std::vector<pbes_expression> v;
656 604 : for (auto j = q.action_summands().begin(); j != q.action_summands().end(); ++j)
657 : {
658 542 : data::data_expression cj = j->condition();
659 542 : data::variable_list e1 = j->summation_variables();
660 542 : data::data_expression_list gj = j->next_state(q.process_parameters());
661 542 : lps::multi_action aj(j->multi_action().actions());
662 542 : pbes_expression expr;
663 542 : optimized_and(expr, cj, equals(ai, aj)), close2(p, q, i, gi, gj);
664 542 : optimized_and(expr, expr, close2(p, q, i, gi, gj));
665 542 : expr = make_exists_(e1, expr);
666 542 : v.push_back(expr);
667 542 : }
668 62 : return optimized_join_or(v.begin(), v.end());
669 62 : }
670 72 : }
671 :
672 : /// \brief The close1 function.
673 : /// \param p A linear process
674 : /// \param q A linear process
675 : /// \param i A summand iterator
676 : /// \return The function result
677 72 : pbes_expression close1(const lps::linear_process& p, const lps::linear_process& q, my_iterator i) const
678 : {
679 72 : std::vector<pbes_expression> v;
680 72 : pbes_expression expr;
681 72 : data::variable_list e = i->summation_variables();
682 72 : const data::variable_list& d = p.process_parameters();
683 72 : const data::variable_list& d1 = q.process_parameters();
684 642 : for (auto j = q.action_summands().begin(); j != q.action_summands().end(); ++j)
685 : {
686 570 : if (!j->is_tau())
687 : {
688 542 : continue;
689 : }
690 28 : data::data_expression cj = j->condition();
691 28 : data::variable_list e1 = j->summation_variables();
692 28 : data::data_expression_list gj = j->next_state(d1);
693 28 : optimized_and(expr, cj, var(Y1(p, q, i),
694 28 : data::variable_list_to_data_expression_list(d) +
695 56 : gj +
696 28 : data::variable_list_to_data_expression_list(e)));
697 28 : expr = make_exists_(e1, expr);
698 28 : v.push_back(expr);
699 28 : }
700 72 : optimized_or(expr, optimized_join_or(v.begin(), v.end()), step(p, q, i));
701 144 : return expr;
702 72 : }
703 :
704 : /// \brief The close function.
705 : /// \param p A linear process
706 : /// \param q A linear process
707 : /// \param i A summand iterator
708 : /// \param d A sequence of data expressions
709 : /// \param d1 A sequence of data expressions
710 : /// \return The function result
711 1166 : pbes_expression close2(const lps::linear_process& p, const lps::linear_process& q, my_iterator i, const data::data_expression_list& d, const data::data_expression_list& d1) const
712 : {
713 1166 : const data::variable_list& parameters = q.process_parameters();
714 1166 : data::mutable_map_substitution<> sigma; // q.process_parameters() := d1
715 1166 : make_substitution(parameters, d1, sigma);
716 1166 : data::set_identifier_generator id_generator;
717 8868 : for (const data::variable& v: data::find_free_variables(d1))
718 : {
719 7702 : id_generator.add_identifier(v.name());
720 1166 : }
721 :
722 1166 : std::vector<pbes_expression> v;
723 1166 : pbes_expression expr;
724 :
725 15864 : for (auto j = q.action_summands().begin(); j != q.action_summands().end(); ++j)
726 : {
727 14698 : if (!j->is_tau())
728 : {
729 14494 : continue;
730 : }
731 : // d' == q.process_parameters()
732 : // e' == j->summand_variables()
733 204 : data::data_expression cj = j->condition(); // cj == cj(d',e')
734 204 : data::data_expression_list gj = j->next_state(q.process_parameters()); // gj == gj(d',e')
735 204 : data::variable_list e1 = j->summation_variables(); // e1 == e'
736 :
737 : // replace d' by d1 (if needed)
738 204 : if (d1 != data::data_expression_list(parameters.begin(), parameters.end()))
739 : {
740 168 : cj = data::replace_variables_capture_avoiding(cj, sigma, id_generator);
741 168 : gj = data::replace_variables_capture_avoiding(gj, sigma, id_generator);
742 : }
743 :
744 : // replace e' (e1) by fresh variables e'' (e11)
745 204 : std::vector<data::variable> tmp;
746 232 : for (const data::variable& w: e1)
747 : {
748 28 : tmp.emplace_back(m_generator(std::string(w.name())), w.sort());
749 : }
750 204 : data::variable_list e11(tmp.begin(), tmp.end());
751 :
752 204 : data::mutable_map_substitution<> sigma1;
753 204 : make_substitution(e1, atermpp::container_cast<data::data_expression_list>(e11), sigma1);
754 232 : for (const data::variable& w: e11)
755 : {
756 28 : id_generator.add_identifier(w.name());
757 : }
758 204 : data::data_expression cj_new = data::replace_variables_capture_avoiding(cj, sigma1, id_generator);
759 204 : data::data_expression_list gj_new = data::replace_variables_capture_avoiding(gj, sigma1, id_generator);
760 :
761 204 : optimized_and(expr, cj_new, var(Y2(p, q, i), d + gj_new));
762 204 : expr = make_exists_(e11, expr);
763 204 : v.push_back(expr);
764 204 : }
765 1166 : optimized_or(expr, var(X(p, q), d + d1), optimized_join_or(v.begin(), v.end()));
766 2332 : return expr;
767 1166 : }
768 :
769 : /// \brief Runs the algorithm
770 : /// \param model A linear process specification
771 : /// \param spec A linear process specification
772 : /// \return A pbes that expresses weak bisimulation between two specifications.
773 8 : pbes run(const lps::specification& model, const lps::specification& spec)
774 : {
775 8 : lps::specification spec1 = spec;
776 8 : resolve_name_clashes(model, spec1, true);
777 8 : const lps::linear_process& m = model.process();
778 8 : const lps::linear_process& s = spec1.process();
779 8 : init(m, s);
780 :
781 8 : m_generator.clear_context();
782 8 : m_generator.add_identifiers(data::function_and_mapping_identifiers(model.data()));
783 8 : m_generator.add_identifiers(data::function_and_mapping_identifiers(spec.data()));
784 8 : m_generator.add_identifiers(lps::find_identifiers(model));
785 8 : m_generator.add_identifiers(lps::find_identifiers(spec));
786 :
787 8 : data::variable_list const& d = m.process_parameters();
788 8 : data::variable_list const& d1 = s.process_parameters();
789 8 : std::vector<pbes_equation> equations;
790 :
791 : // E1
792 8 : pbes_expression expr;
793 8 : optimized_and(expr, match(m, s), match(s, m));
794 8 : equations.emplace_back(nu(), propositional_variable(X(m, s), d + d1), expr);
795 8 : equations.emplace_back(nu(), propositional_variable(X(s, m), d1 + d), var(X(m, s), d + d1));
796 :
797 : // E2
798 44 : for (auto i = m.action_summands().begin(); i != m.action_summands().end(); ++i)
799 : {
800 36 : data::variable_list e = i->summation_variables();
801 72 : pbes_equation e1(mu(), propositional_variable(Y1(m, s, i), d + d1 + e), close1(m, s, i));
802 72 : pbes_equation e2(mu(), propositional_variable(Y2(m, s, i), d + d1), close2(m, s, i, data::data_expression_list(d.begin(), d.end()), data::data_expression_list(d1.begin(), d1.end())));
803 36 : equations.push_back(e1);
804 36 : equations.push_back(e2);
805 36 : }
806 44 : for (auto i = s.action_summands().begin(); i != s.action_summands().end(); ++i)
807 : {
808 36 : data::variable_list e = i->summation_variables();
809 72 : pbes_equation e1(mu(), propositional_variable(Y1(s, m, i), d1 + d + e), close1(s, m, i));
810 72 : pbes_equation e2(mu(), propositional_variable(Y2(s, m, i), d1 + d), close2(s, m, i, data::data_expression_list(d1.begin(), d1.end()), data::data_expression_list(d.begin(), d.end())));
811 36 : equations.push_back(e1);
812 36 : equations.push_back(e2);
813 36 : }
814 :
815 16 : return build_pbes(equations, model, spec1);
816 8 : }
817 : };
818 :
819 : /// \brief Returns a pbes that expresses weak bisimulation between two specifications.
820 : /// \param model A linear process specification
821 : /// \param spec A linear process specification
822 : /// \return A pbes that expresses weak bisimulation between the two specifications.
823 : inline
824 8 : pbes weak_bisimulation(const lps::specification& model, const lps::specification& spec)
825 : {
826 16 : return weak_bisimulation_algorithm().run(model, spec);
827 : }
828 :
829 : //--------------------------------------------------------------//
830 : // branching simulation equivalence
831 : //--------------------------------------------------------------//
832 :
833 : /// \brief Algorithm class for branching simulation equivalence.
834 : class branching_simulation_equivalence_algorithm : public branching_bisimulation_algorithm
835 : {
836 : public:
837 : /// \brief Runs the algorithm
838 : /// \param model A linear process specification
839 : /// \param spec A linear process specification
840 : /// \return A pbes that expresses branching simulation equivalence between two specifications.
841 8 : pbes run(const lps::specification& model, const lps::specification& spec)
842 : {
843 8 : lps::specification spec1 = spec;
844 8 : resolve_name_clashes(model, spec1, true);
845 8 : const lps::linear_process& m = model.process();
846 8 : const lps::linear_process& s = spec1.process();
847 8 : init(m, s);
848 :
849 8 : data::variable_list const& d = m.process_parameters();
850 8 : data::variable_list const& d1 = s.process_parameters();
851 8 : std::vector<pbes_equation> equations;
852 :
853 :
854 : // E1
855 8 : pbes_expression expr;
856 8 : optimized_and(expr, match(m, s), match(s, m));
857 8 : equations.emplace_back(nu(), propositional_variable(X(m, s), d + d1), expr);
858 8 : equations.emplace_back(nu(), propositional_variable(X(s, m), d1 + d), var(X(m, s), d + d1));
859 :
860 : // E2
861 44 : for (auto i = m.action_summands().begin(); i != m.action_summands().end(); ++i)
862 : {
863 36 : data::variable_list e = i->summation_variables();
864 72 : pbes_equation e1(mu(), propositional_variable(Y(m, s, i), d + d1 + e), close(m, s, i));
865 36 : equations.push_back(e1);
866 36 : }
867 44 : for (auto i = s.action_summands().begin(); i != s.action_summands().end(); ++i)
868 : {
869 36 : data::variable_list e = i->summation_variables();
870 72 : pbes_equation e1(mu(), propositional_variable(Y(s, m, i), d1 + d + e), close(s, m, i));
871 36 : equations.push_back(e1);
872 36 : }
873 :
874 16 : return build_pbes(equations, model, spec1);
875 8 : }
876 : };
877 :
878 : /// \brief Returns a pbes that expresses branching simulation equivalence between two specifications.
879 : /// \param model A linear process specification
880 : /// \param spec A linear process specification
881 : /// \return A pbes that expresses branching simulation equivalence between the two specifications.
882 : inline
883 8 : pbes branching_simulation_equivalence(const lps::specification& model, const lps::specification& spec)
884 : {
885 16 : return branching_simulation_equivalence_algorithm().run(model, spec);
886 : }
887 :
888 : } // namespace pbes_system
889 :
890 : } // namespace mcrl2
891 :
892 : #endif // MCRL2_PBES_BISIMULATION_H
|
