Line data Source code
1 : // Author(s): Muck van Weerdenburg, Jan Friso Groote
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 :
10 : /** \file
11 : *
12 : * \brief Algorithms for LTS, such as equivalence reductions, determinisation, etc.
13 : * \details This contains the main algorithms useful to manipulate with
14 : * labelled transition systems. Typically, it contains algorithms for bisimulation
15 : * reduction, removal of tau loops, making an lts deterministic etc.
16 : * \author Jan Friso Groote, Bas Ploeger, Muck van Weerdenburg
17 : */
18 :
19 : #ifndef MCRL2_LTS_LTS_ALGORITHM_H
20 : #define MCRL2_LTS_LTS_ALGORITHM_H
21 :
22 : #include "mcrl2/lts/detail/liblts_bisim.h"
23 : #include "mcrl2/lts/detail/liblts_bisim_minimal_depth.h"
24 : #include "mcrl2/lts/detail/liblts_bisim_gjkw.h"
25 : #include "mcrl2/lts/detail/liblts_branching_bisim_minimal_depth.h"
26 : #include "mcrl2/lts/detail/liblts_weak_bisim.h"
27 : #include "mcrl2/lts/detail/liblts_add_an_action_loop.h"
28 : #include "mcrl2/lts/detail/liblts_ready_sim.h"
29 : #include "mcrl2/lts/detail/liblts_failures_refinement.h"
30 : #include "mcrl2/lts/detail/liblts_coupledsim.h"
31 : #include "mcrl2/lts/detail/tree_set.h"
32 : #include "mcrl2/lts/lts_equivalence.h"
33 : #include "mcrl2/lts/lts_preorder.h"
34 : #include "mcrl2/lts/sigref.h"
35 :
36 : namespace mcrl2
37 : {
38 : namespace lts
39 : {
40 :
41 : /** \brief Applies a reduction algorithm to this LTS.
42 : * \param[in] l A labelled transition system that must be reduced.
43 : * \param[in] eq The equivalence with respect to which the LTS will be
44 : * reduced.
45 : **/
46 : template <class LTS_TYPE>
47 : void reduce(LTS_TYPE& l, lts_equivalence eq);
48 :
49 : /** \brief Checks whether this LTS is equivalent to another LTS.
50 : * \param[in] l1 The first LTS that will be compared.
51 : * \param[in] l2 The second LTS that will be compared.
52 : * \param[in] eq The equivalence with respect to which the LTSs will be
53 : * compared.
54 : * \param[in] generate_counter_examples Whether to generate a counter example
55 : * \param[in] counter_example_file The file to store the counter example in
56 : * \retval true if the LTSs are found to be equivalent.
57 : * \retval false otherwise.
58 : * \warning This function alters the internal data structure of
59 : * both LTSs for efficiency reasons. After comparison, this LTS is
60 : * equivalent to the original LTS by equivalence \a eq, and
61 : * similarly for the LTS \a l.
62 : */
63 : template <class LTS_TYPE>
64 55 : bool destructive_compare(LTS_TYPE& l1,
65 : LTS_TYPE& l2,
66 : const lts_equivalence eq,
67 : const bool generate_counter_examples = false,
68 : const std::string& counter_example_file = std::string(),
69 : const bool structured_output = false)
70 : {
71 : // Merge this LTS and l and store the result in this LTS.
72 : // In the resulting LTS, the initial state i of l will have the
73 : // state number i + N where N is the number of states in this
74 : // LTS (before the merge).
75 :
76 55 : switch (eq)
77 : {
78 0 : case lts_eq_none:
79 0 : return false;
80 17 : case lts_eq_bisim:
81 : {
82 17 : if (generate_counter_examples)
83 : {
84 1 : mCRL2log(mcrl2::log::warning) << "A slower partition refinement algorithm is used to generate minimal-depth counter examples.\n";
85 1 : return detail::destructive_bisimulation_compare_minimal_depth(l1, l2, counter_example_file);
86 : }
87 16 : return detail::destructive_bisimulation_compare_dnj(l1,l2, false,false,generate_counter_examples,counter_example_file,structured_output);
88 : }
89 2 : case lts_eq_bisim_gv:
90 : {
91 2 : return detail::destructive_bisimulation_compare(l1,l2, false,false,generate_counter_examples,counter_example_file,structured_output);
92 : }
93 2 : case lts_eq_bisim_gjkw:
94 : {
95 2 : return detail::destructive_bisimulation_compare_gjkw(l1,l2, false,false,generate_counter_examples,counter_example_file,structured_output);
96 : }
97 2 : case lts_eq_branching_bisim:
98 : {
99 2 : if (generate_counter_examples)
100 : {
101 2 : mCRL2log(mcrl2::log::warning) << "The default branching bisimulation comparison algorithm cannot generate counter examples. A slower partition refinement algorithm (Martens/Groote 2024) is used instead.\n";
102 2 : return detail::destructive_branching_bisimulation_compare_minimal_depth(l1, l2, counter_example_file);
103 : }
104 0 : return detail::destructive_bisimulation_compare_dnj(l1,l2, true,false,generate_counter_examples,counter_example_file,structured_output);
105 : }
106 0 : case lts_eq_branching_bisim_gv:
107 : {
108 0 : return detail::destructive_bisimulation_compare(l1,l2, true,false,generate_counter_examples,counter_example_file,structured_output);
109 : }
110 0 : case lts_eq_branching_bisim_gjkw:
111 : {
112 0 : return detail::destructive_bisimulation_compare_gjkw(l1,l2, true,false,generate_counter_examples,counter_example_file,structured_output);
113 : }
114 0 : case lts_eq_divergence_preserving_branching_bisim:
115 : {
116 0 : if (generate_counter_examples)
117 : {
118 0 : mCRL2log(mcrl2::log::warning) << "The default divergence-preserving branching bisimulation comparison algorithm cannot generate counter examples. Therefore the slower gv algorithm is used instead.\n";
119 0 : return detail::destructive_bisimulation_compare(l1,l2, true,true,generate_counter_examples,counter_example_file,structured_output);
120 : }
121 0 : return detail::destructive_bisimulation_compare_dnj(l1,l2, true,true,generate_counter_examples,counter_example_file,structured_output);
122 : }
123 0 : case lts_eq_divergence_preserving_branching_bisim_gv:
124 : {
125 0 : return detail::destructive_bisimulation_compare(l1,l2, true,true,generate_counter_examples,counter_example_file,structured_output);
126 : }
127 0 : case lts_eq_divergence_preserving_branching_bisim_gjkw:
128 : {
129 0 : return detail::destructive_bisimulation_compare_gjkw(l1,l2, true,true,generate_counter_examples,counter_example_file,structured_output);
130 : }
131 0 : case lts_eq_weak_bisim:
132 : {
133 0 : if (generate_counter_examples)
134 : {
135 0 : mCRL2log(log::warning) << "Cannot generate counter examples for weak bisimulation\n";
136 : }
137 0 : return detail::destructive_weak_bisimulation_compare(l1,l2,false);
138 : }
139 0 : case lts_eq_divergence_preserving_weak_bisim:
140 : {
141 0 : if (generate_counter_examples)
142 : {
143 0 : mCRL2log(log::warning) << "Cannot generate counter examples for divergence-preserving weak bisimulation\n";
144 : }
145 0 : return detail::destructive_weak_bisimulation_compare(l1,l2, true);
146 : }
147 9 : case lts_eq_sim:
148 : {
149 9 : if (generate_counter_examples)
150 : {
151 0 : mCRL2log(log::warning) << "Cannot generate counter examples for simulation equivalence\n";
152 : }
153 : // Run the partitioning algorithm on this merged LTS
154 9 : std::size_t init_l2 = l2.initial_state() + l1.num_states();
155 9 : detail::merge(l1,l2);
156 9 : l2.clear(); // l2 is not needed anymore.
157 9 : detail::sim_partitioner<LTS_TYPE> sp(l1);
158 9 : sp.partitioning_algorithm();
159 :
160 9 : return sp.in_same_class(l1.initial_state(),init_l2);
161 9 : }
162 7 : case lts_eq_ready_sim:
163 : {
164 7 : if (generate_counter_examples)
165 : {
166 0 : mCRL2log(log::warning) << "Cannot generate counter examples for ready-simulation equivalence\n";
167 : }
168 : // Run the partitioning algorithm on this merged LTS
169 7 : std::size_t init_l2 = l2.initial_state() + l1.num_states();
170 7 : detail::merge(l1,l2);
171 7 : l2.clear(); // l2 is not needed anymore.
172 7 : detail::ready_sim_partitioner<LTS_TYPE> rsp(l1);
173 7 : rsp.partitioning_algorithm();
174 :
175 7 : return rsp.in_same_class(l1.initial_state(),init_l2);
176 7 : }
177 9 : case lts_eq_trace:
178 : {
179 : // Determinise first LTS
180 9 : detail::bisimulation_reduce_dnj(l1, false);
181 9 : determinise(l1);
182 :
183 : // Determinise second LTS
184 9 : detail::bisimulation_reduce_dnj(l2, false);
185 9 : determinise(l2);
186 :
187 : // Trace equivalence now corresponds to bisimilarity
188 9 : if (generate_counter_examples)
189 : {
190 0 : return detail::destructive_bisimulation_compare_minimal_depth(l1, l2, counter_example_file);
191 : }
192 9 : return detail::destructive_bisimulation_compare(l1, l2, false, false, generate_counter_examples, counter_example_file, structured_output);
193 : }
194 6 : case lts_eq_weak_trace:
195 : {
196 6 : if (generate_counter_examples)
197 : {
198 0 : mCRL2log(log::warning) << "Cannot generate counter examples for weak trace equivalence\n";
199 : }
200 :
201 : // Eliminate silent steps and determinise first LTS
202 6 : detail::bisimulation_reduce_dnj(l1,true,false);
203 6 : detail::tau_star_reduce(l1);
204 6 : detail::bisimulation_reduce_dnj(l1,false);
205 6 : determinise(l1);
206 :
207 : // Eliminate silent steps and determinise second LTS
208 6 : detail::bisimulation_reduce_dnj(l2,true,false);
209 6 : detail::tau_star_reduce(l2);
210 6 : detail::bisimulation_reduce_dnj(l2,false);
211 6 : determinise(l2);
212 :
213 : // Weak trace equivalence now corresponds to bisimilarity
214 6 : return detail::destructive_bisimulation_compare(l1,l2,false,false,false,counter_example_file,structured_output);
215 : }
216 1 : case lts_eq_coupled_sim:
217 : {
218 1 : return detail::coupled_simulation_compare(l1,l2);
219 : }
220 0 : default:
221 0 : throw mcrl2::runtime_error("Comparison for this equivalence is not available");
222 : return false;
223 : }
224 : }
225 :
226 : /** \brief Checks whether this LTS is equivalent to another LTS.
227 : * \details The input labelled transition systems are duplicated in memory to carry
228 : * out the comparison. When space efficiency is a concern, one can consider
229 : * to use destructive_compare.
230 : * \param[in] l1 The first LTS to compare.
231 : * \param[in] l2 The second LTS to compare.
232 : * \param[in] eq The equivalence with respect to which the LTSs will be
233 : * compared.
234 : * \param[in] generate_counter_examples Whether to generate a counter example
235 : * \param[in] counter_example_file The file to store the counter example in
236 : * \retval true if the LTSs are found to be equivalent.
237 : * \retval false otherwise.
238 : */
239 : template <class LTS_TYPE>
240 : bool compare(const LTS_TYPE& l1,
241 : const LTS_TYPE& l2,
242 : const lts_equivalence eq,
243 : const bool generate_counter_examples = false,
244 : const std::string& counter_example_file = "",
245 : const bool structured_output = false);
246 :
247 : /** \brief Checks whether this LTS is smaller than another LTS according
248 : * to a preorder.
249 : * \param[in] l1 The first LTS to be compared.
250 : * \param[in] l2 The second LTS to be compared.
251 : * \param[in] pre The preorder with respect to which the LTSs will be
252 : * compared.
253 : * \param[in] generate_counter_examples Whether to generate a counter example
254 : * \param[in] counter_example_file The file to store the counter example in
255 : * \param[in] strategy Choose breadth-first or depth-first for exploration strategy
256 : * of the antichain algorithms.
257 : * \param[in] preprocess Whether to allow preprocessing of the given LTSs.
258 : * \retval true if LTS \a l1 is smaller than LTS \a l2 according to
259 : * preorder \a pre.
260 : * \retval false otherwise.
261 : * \warning This function alters the internal data structure of
262 : * both LTSs for efficiency reasons. After comparison, this LTS is
263 : * equivalent to the original LTS by equivalence \a eq, and
264 : * similarly for the LTS \a l, where \a eq is the equivalence
265 : * induced by the preorder \a pre (i.e. \f$eq = pre \cap
266 : * pre^{-1}\f$).
267 : */
268 : template <class LTS_TYPE >
269 : bool destructive_compare(LTS_TYPE& l1,
270 : LTS_TYPE& l2,
271 : const lts_preorder pre,
272 : const bool generate_counter_example,
273 : const std::string& counter_example_file = "",
274 : const bool structured_output = false,
275 : const lps::exploration_strategy strategy = lps::es_breadth,
276 : const bool preprocess = true);
277 :
278 : /** \brief Checks whether this LTS is smaller than another LTS according
279 : * to a preorder.
280 : * \param[in] l1 The first LTS to be compared.
281 : * \param[in] l2 The second LTS to be compared.
282 : * \param[in] pre The preorder with respect to which the LTSs will be compared.
283 : * \param[in] generate_counter_examples Whether to generate a counter example
284 : * \param[in] counter_example_file The file to store the counter example in
285 : * \param[in] strategy Choose breadth-first or depth-first for exploration strategy
286 : * of the antichain algorithms.
287 : * \param[in] preprocess Whether to allow preprocessing of the given LTSs.
288 : * \retval true if this LTS is smaller than LTS \a l according to
289 : * preorder \a pre.
290 : * \retval false otherwise.
291 : */
292 : template <class LTS_TYPE >
293 : bool compare(const LTS_TYPE& l1,
294 : const LTS_TYPE& l2,
295 : const lts_preorder pre,
296 : const bool generate_counter_example,
297 : const std::string& counter_example_file = "",
298 : const bool structured_output = false,
299 : const lps::exploration_strategy strategy = lps::es_breadth,
300 : const bool preprocess = true);
301 :
302 : /** \brief Determinises this LTS. */
303 : template <class LTS_TYPE>
304 : void determinise(LTS_TYPE& l);
305 :
306 :
307 : /** \brief Checks whether all states in this LTS are reachable
308 : * from the initial state and remove unreachable states if required.
309 : * \details Runs in O(num_states * num_transitions) time.
310 : * \param[in] l The LTS on which reachability is checked.
311 : * \param[in] remove_unreachable Indicates whether all unreachable states
312 : * should be removed from the LTS. This option does not
313 : * influence the return value; the return value is with
314 : * respect to the original LTS.
315 : * \retval true if all states are reachable from the initial state;
316 : * \retval false otherwise. */
317 : template <class SL, class AL, class BASE>
318 39 : bool reachability_check(lts < SL, AL, BASE>& l, bool remove_unreachable = false)
319 : {
320 : // First calculate which states can be reached, and store this in the array visited.
321 39 : const outgoing_transitions_per_state_t out_trans(l.get_transitions(),l.num_states(),true);
322 :
323 39 : std::vector < bool > visited(l.num_states(),false);
324 39 : std::stack<std::size_t> todo;
325 :
326 39 : visited[l.initial_state()]=true;
327 39 : todo.push(l.initial_state());
328 :
329 214 : while (!todo.empty())
330 : {
331 175 : std::size_t state_to_consider=todo.top();
332 175 : todo.pop();
333 : // for (const outgoing_pair_t& p: out_trans[state_to_consider])
334 398 : for (detail::state_type i=out_trans.lowerbound(state_to_consider); i<out_trans.upperbound(state_to_consider); ++i)
335 : {
336 223 : const outgoing_pair_t& p=out_trans.get_transitions()[i];
337 223 : assert(visited[state_to_consider] && state_to_consider<l.num_states() && to(p)<l.num_states());
338 223 : if (!visited[to(p)])
339 : {
340 136 : visited[to(p)]=true;
341 136 : todo.push(to(p));
342 : }
343 : }
344 : }
345 :
346 : // Property: in_visited(s) == true: state s is reachable from the initial state
347 :
348 : // check to see if all states are reachable from the initial state, i.e.
349 : // whether all bits are set.
350 39 : bool all_reachable = find(visited.begin(),visited.end(),false)==visited.end();
351 :
352 39 : if (!all_reachable && remove_unreachable)
353 : {
354 : // Remove all unreachable states, transitions from such states and labels
355 : // that are only used in these transitions.
356 :
357 7 : std::vector < detail::state_type > state_map(l.num_states());
358 7 : std::vector < detail::state_type > label_map(l.num_action_labels());
359 :
360 7 : lts < SL, AL, BASE> new_lts=l; // In this way set data specification and action declarations in the new lts.
361 7 : new_lts.clear();
362 :
363 7 : std::size_t new_nstates = 0;
364 56 : for (std::size_t i=0; i<l.num_states(); i++)
365 : {
366 49 : if (visited[i])
367 : {
368 34 : state_map[i] = new_nstates;
369 34 : if (l.has_state_info())
370 : {
371 30 : new_lts.add_state(l.state_label(i));
372 : }
373 : else
374 : {
375 4 : new_lts.add_state();
376 : }
377 34 : new_nstates++;
378 : }
379 : }
380 :
381 83 : for (const transition& t: l.get_transitions())
382 : {
383 76 : if (visited[t.from()])
384 : {
385 58 : label_map[t.label()] = 1;
386 : }
387 : }
388 :
389 7 : label_map[0]=1; // Declare the tau action explicitly present.
390 7 : std::size_t new_nlabels = 0;
391 41 : for (std::size_t i=0; i<l.num_action_labels(); i++)
392 : {
393 34 : if (label_map[i]>0) // Label i is used.
394 : {
395 33 : label_map[i] = new_nlabels;
396 33 : new_lts.add_action(l.action_label(i));
397 33 : new_nlabels++;
398 : }
399 : }
400 :
401 83 : for (const transition& t: l.get_transitions())
402 : {
403 76 : if (visited[t.from()])
404 : {
405 58 : new_lts.add_transition(transition(state_map[t.from()],label_map[t.label()],state_map[t.to()]));
406 : }
407 : }
408 :
409 7 : new_lts.set_initial_state(state_map.at(l.initial_state()));
410 7 : l.swap(new_lts);
411 7 : }
412 :
413 39 : return all_reachable;
414 39 : }
415 :
416 : /** \brief Checks whether all states in a probabilistic LTS are reachable
417 : * from the initial state and remove unreachable states if required.
418 : * \details Runs in O(num_states * num_transitions) time.
419 : * \param[in] l The LTS on which reachability is checked.
420 : * \param[in] remove_unreachable Indicates whether all unreachable states
421 : * should be removed from the LTS. This option does not
422 : * influence the return value; the return value is with
423 : * respect to the original LTS.
424 : * \retval true if all states are reachable from the initial state;
425 : * \retval false otherwise. */
426 : template <class SL, class AL, class PROBABILISTIC_STATE, class BASE>
427 : bool reachability_check(probabilistic_lts < SL, AL, PROBABILISTIC_STATE, BASE>& l, bool remove_unreachable = false)
428 : {
429 : // First calculate which states can be reached, and store this in the array visited.
430 : const outgoing_transitions_per_state_t out_trans(l.get_transitions(),l.num_states(),true);
431 :
432 : std::vector < bool > visited(l.num_states(),false);
433 : std::stack<std::size_t> todo;
434 :
435 : if (l.initial_probabilistic_state().size()>1) // Target states are in a probabilistic vector.
436 : {
437 : for(const typename PROBABILISTIC_STATE::state_probability_pair& s: l.initial_probabilistic_state())
438 : {
439 : visited[s.state()]=true;
440 : todo.push(s.state());
441 : }
442 : }
443 : else // it is a singular state;
444 : {
445 : const typename PROBABILISTIC_STATE::state_t sn=l.initial_probabilistic_state().get();
446 : visited[sn]=true;
447 : todo.push(sn);
448 : }
449 :
450 : while (!todo.empty())
451 : {
452 : std::size_t state_to_consider=todo.top();
453 : todo.pop();
454 : // for (const outgoing_pair_t& p: out_trans[state_to_consider])
455 : for (detail::state_type i=out_trans.lowerbound(state_to_consider); i<out_trans.upperbound(state_to_consider); ++i)
456 : {
457 : const outgoing_pair_t& p=out_trans.get_transitions()[i];
458 : assert(visited[state_to_consider] && state_to_consider<l.num_states() && to(p)<l.num_probabilistic_states());
459 : // Walk through the the states in this probabilistic state.
460 : if (l.probabilistic_state(to(p)).size()>1) // Target states are in a probabilistic vector.
461 : {
462 : for(const typename PROBABILISTIC_STATE::state_probability_pair& pr: l.probabilistic_state(to(p)))
463 : {
464 : if (!visited[pr.state()])
465 : {
466 : visited[pr.state()]=true;
467 : todo.push(pr.state());
468 : }
469 : }
470 : }
471 : else // it is a singular state;
472 : {
473 : const typename PROBABILISTIC_STATE::state_t sn=l.probabilistic_state(to(p)).get();
474 : if (!visited[sn])
475 : {
476 : visited[sn]=true;
477 : todo.push(sn);
478 : }
479 : }
480 : }
481 : }
482 :
483 : // Property: in_visited(s) == true: state s is reachable from the initial state
484 :
485 : // check to see if all states are reachable from the initial state, i.e.
486 : // whether all bits are set.
487 : bool all_reachable = find(visited.begin(),visited.end(),false)==visited.end();
488 :
489 : if (!all_reachable && remove_unreachable)
490 : {
491 : // Remove all unreachable states, transitions from such states and labels
492 : // that are only used in these transitions.
493 :
494 : std::vector < detail::state_type > state_map(l.num_states());
495 : std::vector < detail::state_type > label_map(l.num_action_labels());
496 :
497 : probabilistic_lts < SL, AL, PROBABILISTIC_STATE, BASE> new_lts=l; // In this way set data specification and action declarations in the new lts.
498 : new_lts.clear();
499 :
500 : std::size_t new_nstates = 0;
501 : for (std::size_t i=0; i<l.num_states(); i++)
502 : {
503 : if (visited[i])
504 : {
505 : state_map[i] = new_nstates;
506 : if (l.has_state_info())
507 : {
508 : new_lts.add_state(l.state_label(i));
509 : }
510 : else
511 : {
512 : new_lts.add_state();
513 : }
514 : new_nstates++;
515 : }
516 : }
517 :
518 : for (const transition& t: l.get_transitions())
519 : {
520 : if (visited[t.from()])
521 : {
522 : label_map[t.label()] = 1;
523 : }
524 : }
525 :
526 : label_map[0]=1; // Declare the tau action explicitly present.
527 : std::size_t new_nlabels = 0;
528 : for (std::size_t i=0; i<l.num_action_labels(); i++)
529 : {
530 : if (label_map[i]>0) // Label i is used.
531 : {
532 : label_map[i] = new_nlabels;
533 : new_lts.add_action(l.action_label(i));
534 : new_nlabels++;
535 : }
536 : }
537 :
538 : for (const transition& t: l.get_transitions())
539 : {
540 : if (visited[t.from()])
541 : {
542 : new_lts.add_transition(transition(state_map[t.from()],label_map[t.label()],t.to()));
543 : }
544 : }
545 :
546 : PROBABILISTIC_STATE new_initial_state;
547 : for (std::size_t i=0; i<l.num_probabilistic_states(); ++i)
548 : {
549 : new_initial_state.clear();
550 : if (l.probabilistic_state(i).size()==0)
551 : {
552 : new_initial_state.set(state_map[l.probabilistic_state(i).get()]);
553 : }
554 : else
555 : {
556 : for(const typename PROBABILISTIC_STATE::state_probability_pair& s: l.probabilistic_state(i))
557 : {
558 : new_initial_state.add(state_map[s.state()], s.probability());
559 : }
560 : }
561 : new_lts.add_probabilistic_state(new_initial_state);
562 : }
563 :
564 : new_initial_state.clear();
565 : if (l.initial_probabilistic_state().size()==0)
566 : {
567 : new_initial_state.set(state_map[l.initial_probabilistic_state().get()]);
568 : }
569 : else
570 : {
571 : for(const typename PROBABILISTIC_STATE::state_probability_pair& s: l.initial_probabilistic_state())
572 : {
573 : new_initial_state.add(state_map[s.state()], s.probability());
574 : }
575 : }
576 : new_lts.set_initial_probabilistic_state(new_initial_state);
577 : l.swap(new_lts);
578 : }
579 :
580 : return all_reachable;
581 : }
582 :
583 : /** \brief Checks whether this LTS is deterministic.
584 : * \retval true if this LTS is deterministic;
585 : * \retval false otherwise. */
586 : template <class LTS_TYPE>
587 : bool is_deterministic(const LTS_TYPE& l);
588 :
589 : /** \brief Merge the second lts into the first lts.
590 : \param[in,out] l1 The transition system in which l2 is merged.
591 : \param[in] l2 The second transition system, which remains unchanged
592 : */
593 : template <class LTS_TYPE>
594 : void merge(LTS_TYPE& l1, const LTS_TYPE& l2)
595 : {
596 : detail::merge(l1,l2);
597 : }
598 :
599 :
600 : /* Here the implementations of the declared functions above are given.
601 : Originally these were in a .cpp file, before lts's were templated */
602 :
603 :
604 :
605 : template <class LTS_TYPE>
606 292 : void reduce(LTS_TYPE& l,lts_equivalence eq)
607 : {
608 :
609 292 : switch (eq)
610 : {
611 5 : case lts_eq_none:
612 5 : return;
613 23 : case lts_eq_bisim:
614 : {
615 23 : detail::bisimulation_reduce_dnj(l,false,false);
616 23 : return;
617 : }
618 21 : case lts_eq_bisim_gv:
619 : {
620 21 : detail::bisimulation_reduce(l,false,false);
621 21 : return;
622 : }
623 21 : case lts_eq_bisim_gjkw:
624 : {
625 21 : detail::bisimulation_reduce_gjkw(l,false,false);
626 21 : return;
627 : }
628 21 : case lts_eq_bisim_sigref:
629 : {
630 21 : sigref<LTS_TYPE, signature_bisim<LTS_TYPE> > s(l);
631 21 : s.run();
632 21 : return;
633 21 : }
634 23 : case lts_eq_branching_bisim:
635 : {
636 23 : detail::bisimulation_reduce_dnj(l,true,false);
637 23 : return;
638 : }
639 21 : case lts_eq_branching_bisim_gv:
640 : {
641 21 : detail::bisimulation_reduce(l,true,false);
642 21 : return;
643 : }
644 21 : case lts_eq_branching_bisim_gjkw:
645 : {
646 21 : detail::bisimulation_reduce_gjkw(l,true,false);
647 21 : return;
648 : }
649 21 : case lts_eq_branching_bisim_sigref:
650 : {
651 21 : sigref<LTS_TYPE, signature_branching_bisim<LTS_TYPE> > s(l);
652 21 : s.run();
653 21 : return;
654 21 : }
655 15 : case lts_eq_divergence_preserving_branching_bisim:
656 : {
657 15 : detail::bisimulation_reduce_dnj(l,true,true);
658 15 : return;
659 : }
660 15 : case lts_eq_divergence_preserving_branching_bisim_gv:
661 : {
662 15 : detail::bisimulation_reduce(l,true,true);
663 15 : return;
664 : }
665 15 : case lts_eq_divergence_preserving_branching_bisim_gjkw:
666 : {
667 15 : detail::bisimulation_reduce_gjkw(l,true,true);
668 15 : return;
669 : }
670 15 : case lts_eq_divergence_preserving_branching_bisim_sigref:
671 : {
672 15 : sigref<LTS_TYPE, signature_divergence_preserving_branching_bisim<LTS_TYPE> > s(l);
673 15 : s.run();
674 15 : return;
675 15 : }
676 19 : case lts_eq_weak_bisim:
677 : {
678 19 : detail::weak_bisimulation_reduce(l,false);
679 19 : return;
680 : }
681 : /*
682 : case lts_eq_weak_bisim_sigref:
683 : {
684 : {
685 : sigref<LTS_TYPE, signature_branching_bisim<LTS_TYPE> > s1(l);
686 : s1.run();
687 : }
688 : detail::reflexive_transitive_tau_closure(l);
689 : {
690 : sigref<LTS_TYPE, signature_bisim<LTS_TYPE> > s2(l);
691 : s2.run();
692 : }
693 : scc_reduce(l); // Remove tau loops
694 : return;
695 : }
696 : */
697 14 : case lts_eq_divergence_preserving_weak_bisim:
698 : {
699 14 : detail::weak_bisimulation_reduce(l,true);
700 14 : return;
701 : }
702 : /*
703 : case lts_eq_divergence_preserving_weak_bisim_sigref:
704 : {
705 : {
706 : sigref<LTS_TYPE, signature_divergence_preserving_branching_bisim<LTS_TYPE> > s1(l);
707 : s1.run();
708 : }
709 : std::size_t divergence_label=detail::mark_explicit_divergence_transitions(l);
710 : detail::reflexive_transitive_tau_closure(l);
711 : {
712 : sigref<LTS_TYPE, signature_bisim<LTS_TYPE> > s2(l);
713 : s2.run();
714 : }
715 : scc_reduce(l); // Remove tau loops
716 : detail::unmark_explicit_divergence_transitions(l,divergence_label);
717 : return;
718 : }
719 : */
720 5 : case lts_eq_sim:
721 : {
722 : // Run the partitioning algorithm on this LTS
723 5 : detail::sim_partitioner<LTS_TYPE> sp(l);
724 5 : sp.partitioning_algorithm();
725 :
726 : // Clear this LTS, but keep the labels
727 : // l.clear_type();
728 5 : l.clear_state_labels();
729 5 : l.clear_transitions();
730 :
731 : // Assign the reduced LTS
732 5 : l.set_num_states(sp.num_eq_classes());
733 5 : l.set_initial_state(sp.get_eq_class(l.initial_state()));
734 :
735 5 : const std::vector <transition> trans=sp.get_transitions();
736 5 : l.clear_transitions();
737 88 : for (std::vector <transition>::const_iterator i=trans.begin(); i!=trans.end(); ++i)
738 : {
739 83 : l.add_transition(*i);
740 : }
741 : // Remove unreachable parts
742 :
743 5 : reachability_check(l,true);
744 :
745 5 : return;
746 5 : }
747 0 : case lts_eq_ready_sim:
748 : {
749 : // Run the partitioning algorithm on this LTS
750 0 : detail::ready_sim_partitioner<LTS_TYPE> rsp(l);
751 0 : rsp.partitioning_algorithm();
752 :
753 : // Clear this LTS, but keep the labels
754 : // l.clear_type();
755 0 : l.clear_state_labels();
756 0 : l.clear_transitions();
757 :
758 : // Assign the reduced LTS
759 0 : l.set_num_states(rsp.num_eq_classes());
760 0 : l.set_initial_state(rsp.get_eq_class(l.initial_state()));
761 :
762 0 : const std::vector <transition> trans=rsp.get_transitions();
763 0 : l.clear_transitions();
764 0 : for (std::vector <transition>::const_iterator i=trans.begin(); i!=trans.end(); ++i)
765 : {
766 0 : l.add_transition(*i);
767 : }
768 : // Remove unreachable parts
769 :
770 0 : reachability_check(l,true);
771 :
772 0 : return;
773 0 : }
774 5 : case lts_eq_trace:
775 5 : detail::bisimulation_reduce_dnj(l,false);
776 5 : determinise(l);
777 5 : detail::bisimulation_reduce_dnj(l,false);
778 5 : return;
779 5 : case lts_eq_weak_trace:
780 : {
781 5 : detail::bisimulation_reduce_dnj(l,true,false);
782 5 : detail::tau_star_reduce(l);
783 5 : detail::bisimulation_reduce_dnj(l,false);
784 5 : determinise(l);
785 5 : detail::bisimulation_reduce_dnj(l,false);
786 5 : return;
787 : }
788 2 : case lts_red_tau_star:
789 : {
790 2 : detail::bisimulation_reduce_dnj(l,true,false);
791 2 : detail::tau_star_reduce(l);
792 2 : detail::bisimulation_reduce_dnj(l,false);
793 2 : return;
794 : }
795 5 : case lts_red_determinisation:
796 : {
797 5 : determinise(l);
798 5 : return;
799 : }
800 0 : default:
801 0 : throw mcrl2::runtime_error("Unknown reduction method.");
802 : }
803 : }
804 :
805 : template <class LTS_TYPE>
806 55 : bool compare(const LTS_TYPE& l1, const LTS_TYPE& l2, const lts_equivalence eq, const bool generate_counter_examples, const std::string& counter_example_file, const bool structured_output)
807 : {
808 55 : switch (eq)
809 : {
810 0 : case lts_eq_none:
811 0 : return false;
812 55 : default:
813 55 : LTS_TYPE l1_copy(l1);
814 55 : LTS_TYPE l2_copy(l2);
815 55 : return destructive_compare(l1_copy, l2_copy, eq ,generate_counter_examples, counter_example_file, structured_output);
816 55 : }
817 : return false;
818 : }
819 :
820 : template <class LTS_TYPE>
821 89 : bool compare(const LTS_TYPE& l1, const LTS_TYPE& l2, const lts_preorder pre, const bool generate_counter_example, const std::string& counter_example_file, const bool structured_output, const lps::exploration_strategy strategy, const bool preprocess)
822 : {
823 89 : LTS_TYPE l1_copy(l1);
824 89 : LTS_TYPE l2_copy(l2);
825 178 : return destructive_compare(l1_copy, l2_copy, pre, generate_counter_example, counter_example_file, structured_output, strategy, preprocess);
826 89 : }
827 :
828 : template <class LTS_TYPE>
829 110 : bool destructive_compare(LTS_TYPE& l1, LTS_TYPE& l2, const lts_preorder pre, const bool generate_counter_example, const std::string& counter_example_file, const bool structured_output, const lps::exploration_strategy strategy, const bool preprocess)
830 : {
831 110 : switch (pre)
832 : {
833 24 : case lts_pre_sim:
834 : {
835 : // Merge this LTS and l and store the result in this LTS.
836 : // In the resulting LTS, the initial state i of l will have the
837 : // state number i + N where N is the number of states in this
838 : // LTS (before the merge).
839 24 : const std::size_t init_l2 = l2.initial_state() + l1.num_states();
840 24 : detail::merge(l1,l2);
841 :
842 : // We no longer need l, so clear it to save memory
843 24 : l2.clear();
844 :
845 : // Run the partitioning algorithm on this merged LTS
846 24 : detail::sim_partitioner<LTS_TYPE> sp(l1);
847 24 : sp.partitioning_algorithm();
848 :
849 24 : return sp.in_preorder(l1.initial_state(),init_l2);
850 24 : }
851 9 : case lts_pre_ready_sim:
852 : {
853 : // Merge this LTS and l and store the result in this LTS.
854 : // In the resulting LTS, the initial state i of l will have the
855 : // state number i + N where N is the number of states in this
856 : // LTS (before the merge).
857 9 : const std::size_t init_l2 = l2.initial_state() + l1.num_states();
858 9 : detail::merge(l1,l2);
859 :
860 : // We no longer need l, so clear it to save memory
861 9 : l2.clear();
862 :
863 : // Run the partitioning algorithm on this prepropcessed LTS
864 9 : detail::ready_sim_partitioner<LTS_TYPE> rsp(l1);
865 9 : rsp.partitioning_algorithm();
866 :
867 9 : return rsp.in_preorder(l1.initial_state(),init_l2);
868 9 : }
869 15 : case lts_pre_trace:
870 : {
871 : // Preprocessing: reduce modulo strong bisimulation equivalence.
872 : // This is not strictly necessary, but may reduce time/memory
873 : // needed for determinisation.
874 15 : detail::bisimulation_reduce_dnj(l1,false);
875 15 : detail::bisimulation_reduce_dnj(l2,false);
876 :
877 : // Determinise both LTSes. As postprocessing, reduce modulo
878 : // strong bisimulation equivalence. This is not strictly
879 : // necessary, but may reduce time/memory needed for simulation
880 : // preorder checking.
881 15 : determinise(l1);
882 15 : detail::bisimulation_reduce_dnj(l1,false);
883 :
884 15 : determinise(l2);
885 15 : detail::bisimulation_reduce_dnj(l2,false);
886 :
887 : // Trace preorder now corresponds to simulation preorder
888 15 : return destructive_compare(l1, l2, lts_pre_sim, generate_counter_example, counter_example_file, structured_output, strategy);
889 : }
890 6 : case lts_pre_weak_trace:
891 : {
892 : // Eliminate silent steps of first LTS
893 6 : detail::bisimulation_reduce_dnj(l1,true,false);
894 6 : detail::tau_star_reduce(l1);
895 :
896 : // Eliminate silent steps of second LTS
897 6 : detail::bisimulation_reduce_dnj(l2,true,false);
898 6 : detail::tau_star_reduce(l2);
899 :
900 : // Weak trace preorder now corresponds to strong trace preorder
901 6 : return destructive_compare(l1, l2, lts_pre_trace, generate_counter_example, counter_example_file, structured_output, strategy);
902 : }
903 10 : case lts_pre_trace_anti_chain:
904 : {
905 10 : if (generate_counter_example)
906 : {
907 0 : detail::counter_example_constructor cec("counter_example_trace_preorder", counter_example_file, structured_output);
908 0 : return destructive_refinement_checker(l1, l2, refinement_type::trace, false, strategy, preprocess, cec);
909 0 : }
910 10 : return destructive_refinement_checker(l1, l2, refinement_type::trace, false, strategy, preprocess);
911 : }
912 8 : case lts_pre_weak_trace_anti_chain:
913 : {
914 8 : if (generate_counter_example)
915 : {
916 0 : detail::counter_example_constructor cec("counter_example_weak_trace_preorder", counter_example_file, structured_output);
917 0 : return destructive_refinement_checker(l1, l2, refinement_type::trace, true, strategy, preprocess, cec);
918 0 : }
919 8 : return destructive_refinement_checker(l1, l2, refinement_type::trace, true, strategy, preprocess);
920 : }
921 17 : case lts_pre_failures_refinement:
922 : {
923 17 : if (generate_counter_example)
924 : {
925 0 : detail::counter_example_constructor cec("counter_example_failures_refinement", counter_example_file, structured_output);
926 0 : return destructive_refinement_checker(l1, l2, refinement_type::failures, false, strategy, preprocess, cec);
927 0 : }
928 17 : return destructive_refinement_checker(l1, l2, refinement_type::failures, false, strategy, preprocess);
929 : }
930 8 : case lts_pre_weak_failures_refinement:
931 : {
932 8 : if (generate_counter_example)
933 : {
934 0 : detail::counter_example_constructor cec("counter_example_weak_failures_refinement", counter_example_file, structured_output);
935 0 : return destructive_refinement_checker(l1, l2, refinement_type::failures, true, strategy, preprocess, cec);
936 0 : }
937 8 : return destructive_refinement_checker(l1, l2, refinement_type::failures, true, strategy, preprocess);
938 : }
939 13 : case lts_pre_failures_divergence_refinement:
940 : {
941 13 : if (generate_counter_example)
942 : {
943 0 : detail::counter_example_constructor cec("counter_example_failures_divergence_refinement", counter_example_file, structured_output);
944 0 : return destructive_refinement_checker(l1, l2, refinement_type::failures_divergence, true, strategy, preprocess, cec);
945 0 : }
946 13 : return destructive_refinement_checker(l1, l2, refinement_type::failures_divergence, true, strategy, preprocess);
947 : }
948 0 : default:
949 0 : mCRL2log(log::error) << "Comparison for this preorder is not available\n";
950 0 : return false;
951 : }
952 : }
953 :
954 :
955 : template <class LTS_TYPE>
956 87 : bool is_deterministic(const LTS_TYPE& l)
957 : {
958 87 : if (l.num_transitions() == 0)
959 : {
960 0 : return true;
961 : }
962 :
963 87 : std::vector<transition> temporary_copy_of_transitions = l.get_transitions();
964 87 : sort_transitions(temporary_copy_of_transitions, l.hidden_label_set(), src_lbl_tgt);
965 :
966 : // Traverse the ordered transitions, and search for two consecutive pairs <s,l,t> and <s,l,t'> with t!=t'.
967 : // Such a pair exists iff l is not deterministic.
968 87 : transition& previous_t=temporary_copy_of_transitions[0];
969 87 : bool previous_t_is_valid=false;
970 717 : for(const transition& t: temporary_copy_of_transitions)
971 : {
972 633 : if (previous_t_is_valid)
973 : {
974 743 : if (previous_t.from()==t.from() &&
975 743 : previous_t.label()==t.label() &&
976 4 : previous_t.to()!=t.to())
977 : {
978 3 : return false;
979 : }
980 : }
981 630 : previous_t=t;
982 630 : previous_t_is_valid=true;
983 : }
984 84 : return true;
985 87 : }
986 :
987 :
988 : namespace detail
989 : {
990 :
991 : template <class LTS_TYPE>
992 558 : void get_trans(const outgoing_transitions_per_state_t& begin,
993 : tree_set_store& tss,
994 : std::size_t d,
995 : std::vector<transition>& d_trans,
996 : LTS_TYPE& aut)
997 : {
998 558 : if (!tss.is_set_empty(d))
999 : {
1000 558 : if (tss.is_set_empty(tss.get_set_child_right(d)))
1001 : {
1002 : // for (outgoing_transitions_per_state_t:: const_iterator
1003 : // j=begin.lower_bound(tss.get_set_child_left(d)); j!=begin.upper_bound(tss.get_set_child_left(d)); ++j)
1004 465 : const state_type from=tss.get_set_child_left(d);
1005 : // for(const outgoing_pair_t& p: begin[from])
1006 1084 : for (detail::state_type i=begin.lowerbound(from); i<begin.upperbound(from); ++i)
1007 : {
1008 619 : const outgoing_pair_t& p=begin.get_transitions()[i];
1009 619 : d_trans.push_back(transition(from, aut.apply_hidden_label_map(label(p)), to(p)));
1010 : }
1011 : }
1012 : else
1013 : {
1014 93 : get_trans(begin,tss,tss.get_set_child_left(d),d_trans,aut);
1015 93 : get_trans(begin,tss,tss.get_set_child_right(d),d_trans,aut);
1016 : }
1017 : }
1018 558 : }
1019 : } // namespace detail
1020 :
1021 :
1022 : template <class LTS_TYPE>
1023 75 : void determinise(LTS_TYPE& l)
1024 : {
1025 75 : tree_set_store tss;
1026 :
1027 75 : std::vector<transition> d_transs;
1028 75 : std::vector<std::ptrdiff_t> d_states;
1029 :
1030 : // create the initial state of the DLTS
1031 75 : d_states.push_back(l.initial_state());
1032 75 : std::ptrdiff_t d_id = tss.set_set_tag(tss.create_set(d_states));
1033 75 : d_states.clear();
1034 :
1035 75 : const outgoing_transitions_per_state_t begin(l.get_transitions(),l.num_states(),true);
1036 :
1037 75 : l.clear_transitions();
1038 75 : l.clear_state_labels();
1039 75 : std::size_t d_ntransitions = 0;
1040 75 : std::vector < transition > d_transitions;
1041 :
1042 : std::size_t s;
1043 : std::size_t i,to,lbl,n_t;
1044 :
1045 447 : while (d_id < tss.get_next_tag())
1046 : {
1047 : // collect the outgoing transitions of every state of DLTS state d_id in
1048 : // the vector d_transs
1049 372 : detail::get_trans(begin,tss,tss.get_set(d_id),d_transs,l);
1050 :
1051 : // sort d_transs by label and (if labels are equal) by destination
1052 372 : const detail::compare_transitions_lts compare(l.hidden_label_set());
1053 372 : sort(d_transs.begin(),d_transs.end(),compare);
1054 :
1055 372 : n_t = d_transs.size();
1056 372 : i = 0;
1057 2263 : for (lbl = 0; lbl < l.num_action_labels(); ++lbl)
1058 : {
1059 : // compute the destination of the transition with label lbl
1060 1891 : while (i < n_t && l.apply_hidden_label_map(d_transs[i].label()) < lbl)
1061 : {
1062 0 : ++i;
1063 : }
1064 2463 : while (i < n_t && l.apply_hidden_label_map(d_transs[i].label()) == lbl)
1065 : {
1066 572 : to = d_transs[i].to();
1067 572 : d_states.push_back(to);
1068 1912 : while (i < n_t && l.apply_hidden_label_map(d_transs[i].label()) == lbl &&
1069 721 : d_transs[i].to() == to)
1070 : {
1071 619 : ++i;
1072 : }
1073 : }
1074 1891 : s = tss.create_set(d_states);
1075 :
1076 : // generate the transitions to each of the next states
1077 1891 : if (!tss.is_set_empty(s))
1078 : {
1079 470 : d_transitions.push_back(transition(d_id,lbl,tss.set_set_tag(s)));
1080 :
1081 470 : if (d_ntransitions%10000 == 0)
1082 : {
1083 470 : mCRL2log(log::debug) <<
1084 0 : "generated " << tss.get_next_tag() << " states and " << d_ntransitions
1085 0 : << " transitions; explored " << d_id << " states" << std::endl;
1086 : }
1087 : }
1088 1891 : d_states.clear();
1089 : }
1090 372 : d_transs.clear();
1091 372 : ++d_id;
1092 : }
1093 :
1094 :
1095 75 : l.set_num_states(d_id,false); // remove the state values, and reset the number of states.
1096 75 : l.set_initial_state(0);
1097 :
1098 545 : for (const transition& t: d_transitions)
1099 : {
1100 470 : l.add_transition(t);
1101 : }
1102 75 : assert(is_deterministic(l));
1103 75 : }
1104 :
1105 : } // namespace lts
1106 : } // namespace mcrl2
1107 :
1108 : #endif // MCRL2_LTS_LTS_ALGORITHM_H
1109 :
1110 :
1111 :
|
