Line data Source code
1 : // Author(s): 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 : /// \file lts/detail/liblts_failures_refinement.h
10 :
11 : // This file contains an implementation of
12 : // T. Wang, S. Song, J. Sun, Y. Liu, J.S. Dong, X. Wang and S. Li.
13 : // More Anti-Chain Based Refinement Checking. In proceedings ICFEM 2012, editors T. Aoki and K. Tagushi,
14 : // Lecture Notes in Computer Science no 7635, pages 364-380, 2012.
15 : //
16 : // There are six algorithms. One for trace inclusion, one for failures inclusion and one for failures-divergence inclusion.
17 : // All algorithms come in a variant with and without internal steps.
18 : // It is possible to generate a counter transition system in case the inclusion is answered by no.
19 :
20 : #ifndef LIBLTS_FAILURES_REFINEMENT_H
21 : #define LIBLTS_FAILURES_REFINEMENT_H
22 :
23 : #include "mcrl2/lts/detail/counter_example.h"
24 : #include "mcrl2/lps/exploration_strategy.h"
25 : #include "mcrl2/lts/detail/liblts_bisim_dnj.h"
26 :
27 : namespace mcrl2
28 : {
29 : namespace lts
30 : {
31 : namespace detail
32 : {
33 : typedef std::size_t state_type;
34 : typedef std::size_t label_type;
35 : typedef std::set<state_type> set_of_states;
36 : typedef std::multimap <detail::state_type,detail::set_of_states> anti_chain_type;
37 : typedef std::set < label_type > action_label_set;
38 :
39 : template < class COUNTER_EXAMPLE_CONSTRUCTOR >
40 : class state_states_counter_example_index_triple
41 : {
42 : protected:
43 : detail::state_type m_state;
44 : detail::set_of_states m_states;
45 : typename COUNTER_EXAMPLE_CONSTRUCTOR::index_type m_counter_example_index;
46 :
47 : public:
48 157 : state_states_counter_example_index_triple()
49 157 : {}
50 :
51 : /// \brief Constructor.
52 230 : state_states_counter_example_index_triple(
53 : const state_type state,
54 : const set_of_states& states,
55 : const typename COUNTER_EXAMPLE_CONSTRUCTOR::index_type& counter_example_index)
56 230 : : m_state(state),
57 230 : m_states(states),
58 0 : m_counter_example_index(counter_example_index)
59 230 : {}
60 :
61 : /// \brief Get the state.
62 1356 : state_type state() const
63 : {
64 1356 : return m_state;
65 : }
66 :
67 157 : void swap(state_states_counter_example_index_triple& other)
68 : {
69 157 : std::swap(m_state,other.m_state);
70 157 : std::swap(m_states,other.m_states);
71 157 : std::swap(m_counter_example_index,other.m_counter_example_index);
72 157 : }
73 :
74 : /// \brief Get the set of states.
75 622 : const set_of_states& states() const
76 : {
77 622 : return m_states;
78 : }
79 :
80 : /// \brief Get the counter example index.
81 203 : const typename COUNTER_EXAMPLE_CONSTRUCTOR::index_type& counter_example_index() const
82 : {
83 203 : return m_counter_example_index;
84 : }
85 : };
86 :
87 : template < class COUNTER_EXAMPLE_CONSTRUCTOR >
88 : inline bool antichain_insert(
89 : anti_chain_type& anti_chain,
90 : const state_states_counter_example_index_triple<COUNTER_EXAMPLE_CONSTRUCTOR>& impl_spec);
91 :
92 : // The class below recalls what the stable states and the states with a divergent
93 : // self loop of a transition system are, such that it does not have to be recalculated each time again.
94 : template < class LTS_TYPE >
95 : class lts_cache
96 : {
97 : protected:
98 : LTS_TYPE& m_l;
99 : std::vector<std::vector<state_type> > m_tau_reachable_states;
100 : std::vector<std::vector<transition> > m_sorted_transitions;
101 : std::vector<bool> m_divergent;
102 : std::vector<action_label_set> m_enabled_actions;
103 :
104 : private:
105 48 : void calculate_weak_property_cache(const bool weak_reduction)
106 : {
107 48 : scc_partitioner<LTS_TYPE> strongly_connected_component_partitioner(m_l);
108 480 : for(const transition& t: m_l.get_transitions())
109 : {
110 432 : assert(t.from()<m_l.num_states());
111 432 : if (m_l.is_tau(m_l.apply_hidden_label_map(t.label())) && weak_reduction)
112 : {
113 25 : m_tau_reachable_states[t.from()].push_back(t.to()); // There is an outgoing tau.
114 : }
115 432 : m_sorted_transitions[t.from()].push_back(t);
116 :
117 457 : if (weak_reduction && m_l.is_tau(m_l.apply_hidden_label_map(t.label())) &&
118 25 : strongly_connected_component_partitioner.in_same_class(t.from(),t.to()))
119 : {
120 5 : m_divergent[t.from()]=true; // There is a self loop.
121 : }
122 432 : m_enabled_actions[t.from()].insert(m_l.apply_hidden_label_map(t.label()));
123 : }
124 48 : }
125 :
126 : public:
127 :
128 48 : lts_cache(/* const */ LTS_TYPE& l, const bool weak_reduction) /* l is not changed, but the use of the scc partitioner requires l to be non const */
129 48 : : m_l(l),
130 48 : m_tau_reachable_states(l.num_states()),
131 48 : m_sorted_transitions(l.num_states()),
132 48 : m_divergent(l.num_states(),false),
133 48 : m_enabled_actions(l.num_states())
134 : {
135 48 : calculate_weak_property_cache(weak_reduction);
136 48 : }
137 :
138 219 : bool stable(const state_type s) const
139 : {
140 219 : return m_tau_reachable_states[s].size()==0;
141 : }
142 :
143 305 : const std::vector<state_type>& tau_reachable_states(const state_type s) const
144 : {
145 305 : return m_tau_reachable_states[s];
146 : }
147 :
148 435 : const std::vector<transition>& transitions(const state_type s) const
149 : {
150 435 : assert(s<m_sorted_transitions.size());
151 435 : return m_sorted_transitions[s];
152 : }
153 :
154 212 : bool diverges(const state_type s) const
155 : {
156 212 : return m_divergent[s];
157 : }
158 :
159 214 : const action_label_set& action_labels(const state_type s) const
160 : {
161 214 : return m_enabled_actions[s];
162 : }
163 : };
164 :
165 : template < class LTS_TYPE >
166 : set_of_states collect_reachable_states_via_taus(
167 : const state_type s,
168 : const lts_cache<LTS_TYPE>& weak_property_cache,
169 : const bool weak_reduction);
170 :
171 : template < class LTS_TYPE >
172 : set_of_states collect_reachable_states_via_an_action(
173 : const state_type s,
174 : const label_type e,
175 : const lts_cache<LTS_TYPE>& weak_property_cache,
176 : const bool weak_reduction,
177 : const LTS_TYPE& l);
178 :
179 : template < class LTS_TYPE >
180 : bool refusals_contained_in(
181 : const state_type impl,
182 : const set_of_states& spec,
183 : const lts_cache<LTS_TYPE>& weak_property_cache,
184 : label_type& culprit,
185 : const LTS_TYPE& l,
186 : const bool provide_a_counter_example,
187 : const bool structured_output);
188 :
189 : } // namespace detail
190 :
191 : enum class refinement_type { trace, failures, failures_divergence };
192 :
193 : template<typename T>
194 : struct refinement_statistics
195 : {
196 48 : refinement_statistics(detail::anti_chain_type& antichain, std::deque<T>& working) :
197 48 : antichain(antichain),
198 48 : working(working)
199 48 : {}
200 :
201 : detail::anti_chain_type& antichain;
202 : std::deque<T>& working;
203 : std::size_t max_working = 0; // The largest size of working.
204 : std::size_t max_antichain = 0; // The largest size of the antichain.
205 : std::size_t antichain_misses = 0; // Number of times a pair was inserted into the antichain.
206 : std::size_t antichain_inserts = 0; // Number of times antichain_insert was called.
207 : };
208 :
209 : /// \brief Print a message to debugging containing information about the given statistics.
210 : template<typename T>
211 48 : void report_statistics(refinement_statistics<T>& stats)
212 : {
213 48 : mCRL2log(log::debug) << "working (current: " << stats.working.size() << ", max: " << stats.max_working << ").\n";
214 48 : mCRL2log(log::debug) << "antichain (hits: " << stats.antichain_inserts - stats.antichain_misses
215 0 : << ", misses: " << stats.antichain_misses
216 0 : << ", size: " << stats.antichain.size()
217 0 : << ", max: " << stats.max_antichain << ")\n";
218 48 : }
219 :
220 : /// \brief Preprocess the LTS for destructive refinement checking.
221 : /// \param lts The lts to preprocess.
222 : /// \param init The initial state of the right LTS that was merged.
223 : /// \return A pair where the first element is the state number of init in the reduced
224 : /// lts and the second value indicate whether this state in equal to lts.initial_state.
225 : template<typename LTS_TYPE>
226 56 : std::pair<std::size_t, bool> reduce(LTS_TYPE& lts,
227 : const bool weak_reduction,
228 : const bool preserve_divergence,
229 : std::size_t l2_init)
230 : {
231 56 : lts.clear_state_labels();
232 56 : if (weak_reduction)
233 : {
234 : // Remove inert tau loops when requested, but preserve divergences for failures and failures-divergence.
235 29 : detail::scc_partitioner<LTS_TYPE> scc_part(lts);
236 29 : l2_init = scc_part.get_eq_class(l2_init);
237 29 : scc_part.replace_transition_system(preserve_divergence);
238 29 : }
239 :
240 56 : detail::bisim_partitioner_dnj<LTS_TYPE> bisim_part(lts, weak_reduction,
241 : preserve_divergence);
242 : // Assign the reduced LTS, and set init_l2.
243 56 : l2_init = bisim_part.get_eq_class(l2_init);
244 56 : bisim_part.finalize_minimized_LTS();
245 :
246 112 : return std::make_pair(l2_init, l2_init == lts.initial_state());
247 56 : }
248 :
249 : /// \brief This function checks using algorithms in the paper mentioned above
250 : /// whether transition system l1 is included in transition system l2, in the
251 : /// sense of trace inclusions, failures inclusion and divergence failures
252 : /// inclusion.
253 : /// \param weak_reduction Remove inert tau loops.
254 : /// \param strategy Choose between breadth and depth first.
255 : /// \param preprocess Uses (divergence preserving) branching bisimulation and tau scc reduction to reduce the input LTSs.
256 : /// \param generate_counter_example If set, a labelled transition system is generated
257 : /// that can act as a counterexample. It consists of a trace, followed by
258 : /// outgoing transitions representing a refusal set.
259 : template < class LTS_TYPE, class COUNTER_EXAMPLE_CONSTRUCTOR = detail::dummy_counter_example_constructor >
260 56 : bool destructive_refinement_checker(
261 : LTS_TYPE& l1,
262 : LTS_TYPE& l2,
263 : const refinement_type refinement,
264 : const bool weak_reduction,
265 : const lps::exploration_strategy strategy,
266 : const bool preprocess = true,
267 : COUNTER_EXAMPLE_CONSTRUCTOR generate_counter_example = detail::dummy_counter_example_constructor())
268 : {
269 56 : assert(strategy == lps::exploration_strategy::es_breadth || strategy == lps::exploration_strategy::es_depth); // Need a valid strategy.
270 :
271 : // For weak-failures and failures-divergence, the existence of tau loops make a difference.
272 : // Therefore, we apply bisimulation reduction preserving divergences.
273 : // A typical example is a.(b+c) which is not weak-failures included n a.tau*.(b+c). The lhs has failure pairs
274 : // <a,{a}>, <a,{}> while the rhs has only failure pairs <a,{}>, as the state after the a is not stable.
275 56 : const bool preserve_divergence = weak_reduction && (refinement != refinement_type::trace);
276 :
277 56 : if (!generate_counter_example.is_dummy() && preprocess)
278 : {
279 : // Counter example is requested, apply bisimulation to l2.
280 0 : reduce(l2, weak_reduction, preserve_divergence, l2.initial_state());
281 : }
282 :
283 56 : std::size_t init_l2 = l2.initial_state() + l1.num_states();
284 56 : mcrl2::lts::detail::merge(l1, l2);
285 56 : l2.clear(); // No use for l2 anymore.
286 :
287 56 : if (generate_counter_example.is_dummy() && preprocess)
288 : {
289 : // No counter example is requested. We can use bisimulation preprocessing.
290 56 : bool initial_equal = false;
291 56 : std::tie(init_l2, initial_equal) = reduce(l1, weak_reduction, preserve_divergence, init_l2);
292 :
293 56 : if (initial_equal && weak_reduction)
294 : {
295 8 : mCRL2log(log::verbose) << "The two LTSs are";
296 8 : if (preserve_divergence)
297 : {
298 4 : mCRL2log(log::verbose) << " divergence-preserving";
299 : }
300 8 : mCRL2log(log::verbose) << " branching bisimilar, so there is no need to check the refinement relation.\n";
301 8 : return true;
302 : }
303 : }
304 :
305 :
306 48 : const detail::lts_cache<LTS_TYPE> weak_property_cache(l1,weak_reduction);
307 : std::deque<detail::state_states_counter_example_index_triple<COUNTER_EXAMPLE_CONSTRUCTOR>>
308 192 : working( // let working be a stack containg the triple (init1,{s|init2-->s},root_index);
309 : { detail::state_states_counter_example_index_triple<COUNTER_EXAMPLE_CONSTRUCTOR>(
310 : l1.initial_state(),
311 : detail::collect_reachable_states_via_taus(init_l2,weak_property_cache,weak_reduction),
312 96 : generate_counter_example.root_index() ) });
313 : // let antichain := emptyset;
314 48 : detail::anti_chain_type anti_chain;
315 48 : detail::antichain_insert(anti_chain, working.front()); // antichain := antichain united with (impl,spec);
316 : // This line occurs at another place in the code than in
317 : // the original algorithm, where insertion in the anti-chain
318 : // was too late, causing too many impl-spec pairs to be investigated.
319 48 : refinement_statistics<detail::state_states_counter_example_index_triple<COUNTER_EXAMPLE_CONSTRUCTOR>> stats(anti_chain, working);
320 :
321 341 : while (!working.empty()) // while working!=empty
322 : {
323 157 : detail::state_states_counter_example_index_triple < COUNTER_EXAMPLE_CONSTRUCTOR > impl_spec; // pop (impl,spec) from working;
324 157 : impl_spec.swap(working.front());
325 157 : stats.max_working = std::max(working.size(), stats.max_working);
326 157 : stats.max_antichain = std::max(anti_chain.size(), stats.max_antichain);
327 157 : working.pop_front(); // At this point it could be checked whether impl_spec still exists in anti_chain.
328 : // Small scale experiments show that this is a little bit more expensive than doing the explicit check below.
329 :
330 157 : bool spec_diverges = false;
331 157 : if (refinement == refinement_type::failures_divergence)
332 : {
333 : // Only compute when the result is required.
334 92 : for (detail::state_type s : impl_spec.states())
335 : {
336 57 : if (weak_property_cache.diverges(s))
337 : {
338 2 : spec_diverges = true;
339 2 : break;
340 : }
341 : }
342 : }
343 :
344 : // if not diverges(spec) or not CheckDiv (refinement == failures_divergence_preorder)
345 157 : if (!spec_diverges || refinement != refinement_type::failures_divergence)
346 : {
347 155 : if (weak_property_cache.diverges(impl_spec.state()) && refinement == refinement_type::failures_divergence) // if impl diverges and CheckDiv
348 : {
349 1 : generate_counter_example.save_counter_example(impl_spec.counter_example_index(),l1);
350 1 : report_statistics(stats);
351 1 : return false; // return false;
352 : }
353 :
354 154 : if (refinement == refinement_type::failures || refinement == refinement_type::failures_divergence)
355 : {
356 103 : detail::label_type offending_action=std::size_t(-1);
357 : // if refusals(impl) not contained in refusals(spec) then
358 103 : if (!detail::refusals_contained_in(impl_spec.state(),
359 : impl_spec.states(),
360 : weak_property_cache,
361 : offending_action,
362 : l1,
363 103 : !generate_counter_example.is_dummy(),
364 103 : generate_counter_example.is_structured()))
365 : {
366 14 : generate_counter_example.save_counter_example(impl_spec.counter_example_index(), l1);
367 14 : report_statistics(stats);
368 14 : return false; // return false;
369 : }
370 : }
371 :
372 510 : for(const transition& t: weak_property_cache.transitions(impl_spec.state()))
373 : {
374 0 : const typename COUNTER_EXAMPLE_CONSTRUCTOR::index_type new_counterexample_index=
375 188 : generate_counter_example.add_transition(t.label(),impl_spec.counter_example_index());
376 188 : detail::set_of_states spec_prime;
377 188 : if (l1.is_tau(l1.apply_hidden_label_map(t.label())) && weak_reduction) // if e=tau then
378 : {
379 11 : spec_prime=impl_spec.states(); // spec' := spec;
380 : }
381 : else
382 : { // spec' := {s' | exists s in spec. s-e->s'};
383 452 : for(const detail::state_type s: impl_spec.states())
384 : {
385 275 : detail::set_of_states reachable_states_from_s_via_e=
386 : detail::collect_reachable_states_via_an_action(s,l1.apply_hidden_label_map(t.label()),weak_property_cache,weak_reduction,l1);
387 275 : spec_prime.insert(reachable_states_from_s_via_e.begin(),reachable_states_from_s_via_e.end());
388 : }
389 : }
390 188 : if (spec_prime.empty()) // if spec'={} then
391 : {
392 6 : generate_counter_example.save_counter_example(new_counterexample_index,l1);
393 6 : report_statistics(stats);
394 6 : return false; // return false;
395 : }
396 : // if (impl',spec') in antichain is not true then
397 182 : ++stats.antichain_inserts;
398 : const detail::state_states_counter_example_index_triple < COUNTER_EXAMPLE_CONSTRUCTOR >
399 182 : impl_spec_counterex(t.to(),spec_prime,new_counterexample_index);
400 182 : if (detail::antichain_insert(anti_chain, impl_spec_counterex))
401 : {
402 118 : ++stats.antichain_misses;
403 118 : if (strategy == lps::exploration_strategy::es_breadth)
404 : {
405 118 : working.push_back(impl_spec_counterex); // add(impl,spec') at the bottom of the working;
406 : }
407 0 : else if (strategy == lps::exploration_strategy::es_depth)
408 : {
409 0 : working.push_front(impl_spec_counterex); // push(impl,spec') into working;
410 : }
411 : }
412 : }
413 : }
414 : }
415 :
416 27 : report_statistics(stats);
417 27 : return true; // return true;
418 48 : }
419 :
420 :
421 : namespace detail
422 : {
423 : /* This function generates the set of states reachable from s within labelled
424 : transition system l1 by internal transitions, provided weak_reduction is true.
425 : Otherwise it generates a set with only state s in it.
426 : */
427 : template < class LTS_TYPE >
428 598 : set_of_states collect_reachable_states_via_taus(
429 : const set_of_states& s,
430 : const lts_cache<LTS_TYPE>& weak_property_cache,
431 : const bool weak_reduction)
432 : {
433 598 : set_of_states result(s);
434 598 : if (!weak_reduction)
435 : {
436 329 : return result;
437 : }
438 269 : set_of_states visited(s);
439 269 : std::deque<state_type> todo_stack(s.begin(),s.end());
440 574 : while (todo_stack.size()>0)
441 : {
442 305 : state_type current_state=todo_stack.front();
443 305 : todo_stack.pop_front();
444 354 : for(const state_type s: weak_property_cache.tau_reachable_states(current_state))
445 : {
446 49 : if (visited.insert(s).second) // The element has been inserted.
447 : {
448 46 : todo_stack.push_back(s);
449 46 : result.insert(s);
450 : }
451 : }
452 : }
453 :
454 269 : return result;
455 269 : }
456 :
457 : template < class LTS_TYPE >
458 323 : set_of_states collect_reachable_states_via_taus(
459 : const state_type s,
460 : const lts_cache<LTS_TYPE>& weak_property_cache,
461 : const bool weak_reduction)
462 : {
463 323 : set_of_states set_with_s({s});
464 646 : return collect_reachable_states_via_taus(set_with_s, weak_property_cache, weak_reduction);
465 323 : }
466 :
467 : template < class LTS_TYPE >
468 275 : set_of_states collect_reachable_states_via_an_action(
469 : const state_type s,
470 : const label_type e, // This is already the hidden action.
471 : const lts_cache<LTS_TYPE>& weak_property_cache,
472 : const bool weak_reduction,
473 : const LTS_TYPE& l)
474 : {
475 275 : const set_of_states set_before_action_e=collect_reachable_states_via_taus(s,weak_property_cache,weak_reduction);
476 275 : set_of_states states_reachable_via_e;
477 570 : for(const state_type s: set_before_action_e)
478 : {
479 776 : for(const transition& t: weak_property_cache.transitions(s))
480 : {
481 : {
482 481 : if (l.apply_hidden_label_map(t.label())==e)
483 : {
484 263 : assert(set_before_action_e.count(t.from())>0);
485 263 : states_reachable_via_e.insert(t.to());
486 : }
487 : }
488 : }
489 : }
490 550 : return collect_reachable_states_via_taus(states_reachable_via_e, weak_property_cache, weak_reduction);
491 275 : }
492 :
493 : /* This function implements the insertion of <p,state(), p.states()> in the anti_chain.
494 : Concretely, this means that p.states() is inserted among the sets s1,...,sn associated to p.state().
495 : It is important that an anti_chain contains for each state a set of states of which
496 : no set is a subset of another. The idea is that if such two sets occur, it is enough
497 : to keep the smallest.
498 : If p.states() is smaller than a set si associated to p.state(), this set is removed.
499 : If p.states() is larger than a set si, there is no need to add p.states(), as a better candidate
500 : is already there.
501 : This function returns true if insertion was succesful, and false otherwise.
502 : */
503 : template < class COUNTER_EXAMPLE_CONSTRUCTOR >
504 230 : inline bool antichain_insert(
505 : anti_chain_type& anti_chain,
506 : const state_states_counter_example_index_triple<COUNTER_EXAMPLE_CONSTRUCTOR>& impl_spec)
507 : {
508 : // First check whether there is a set in the antichain for impl_spec.state() which is smaller than impl_spec.states().
509 : // If so, impl_spec.states() does not have to be inserted in the anti_chain.
510 294 : for(anti_chain_type::const_iterator i=anti_chain.lower_bound(impl_spec.state()); i!=anti_chain.upper_bound(impl_spec.state()); ++i)
511 : {
512 64 : const set_of_states s=i->second;
513 : // If s is included in impl_spec.states()
514 64 : if (std::includes(impl_spec.states().begin(), impl_spec.states().end(), s.begin(),s.end()))
515 : {
516 64 : return false;
517 : }
518 : }
519 :
520 : // Here impl_spec.states() must be inserted in the antichain. Moreover, all sets in the antichain that
521 : // are a superset of impl_spec.states() must be removed.
522 166 : for(anti_chain_type::iterator i=anti_chain.lower_bound(impl_spec.state()); i!=anti_chain.upper_bound(impl_spec.state()); )
523 : {
524 0 : const set_of_states s=i->second;
525 : // if s is a superset of impl_spec.states()
526 : // if (std::includes(impl_spec.states().begin(),impl_spec.states().end(),s.begin(),s.end()))
527 0 : if (std::includes(s.begin(), s.end(), impl_spec.states().begin(),impl_spec.states().end()))
528 : {
529 : // set s must be removed.
530 0 : i=anti_chain.erase(i);
531 : }
532 : else
533 : {
534 0 : ++i;
535 : }
536 : }
537 166 : anti_chain.insert(std::pair<detail::state_type,detail::set_of_states>(impl_spec.state(),impl_spec.states()));
538 166 : return true;
539 : }
540 :
541 : /* Calculate the states that are stable and reachable through tau-steps */
542 : template < class LTS_TYPE >
543 : const set_of_states& calculate_tau_reachable_states(
544 : const set_of_states& states,
545 : const lts_cache<LTS_TYPE>& weak_property_cache)
546 : {
547 : static std::map<set_of_states, set_of_states> cache;
548 : const std::map<set_of_states, set_of_states>::const_iterator i=cache.find(states);
549 : if (i!=cache.end())
550 : {
551 : return i->second;
552 : }
553 :
554 : static set_of_states visited;
555 : assert(visited.empty());
556 : static std::stack < state_type > todo_stack;
557 : assert(todo_stack.empty());
558 : set_of_states result;
559 :
560 : for(const state_type s: states)
561 : {
562 : if (weak_property_cache.stable(s))
563 : {
564 : // Put the outgoing action labels in a set and put these in the result.
565 : result.insert(s);
566 : }
567 : else
568 : {
569 : visited.insert(s);
570 : todo_stack.push(s);
571 : }
572 : }
573 :
574 : while (todo_stack.size()>0)
575 : {
576 : const state_type current_state=todo_stack.top();
577 : todo_stack.pop();
578 : // Consider the states reachable in one tau step.
579 : for(const state_type s: weak_property_cache.tau_reachable_states(current_state))
580 : {
581 : if (weak_property_cache.stable(s))
582 : {
583 : // Put the outgoing action labels in a set and put these in the result.
584 : result.insert(s);
585 : }
586 : else
587 : {
588 : if (visited.insert(s).second) // t.to() is a new state.
589 : {
590 : todo_stack.push(s);
591 : }
592 : }
593 : }
594 : }
595 : cache[states]=result;
596 : visited.clear();
597 : return cache[states];
598 : }
599 :
600 : /// \brief This function checks that the refusals(impl) are contained in the refusals of spec, where
601 : /// the refusals of spec are defined by { r | exists s in spec. r in refusals(s) and stable(r) }.
602 : /// \details This is equivalent to saying that for all enabled actions of impl it must be contained in the enabled actions
603 : /// of every stable state in spec.
604 : /// If enable(t') is not included in enable(s'), their is a problematic action a. This action is returned as "culprit".
605 : /// It can be used to construct an extended counterexample.
606 : template < class LTS_TYPE >
607 103 : bool refusals_contained_in(
608 : const state_type impl,
609 : const set_of_states& spec,
610 : const lts_cache<LTS_TYPE>& weak_property_cache,
611 : label_type& culprit,
612 : const LTS_TYPE& l,
613 : const bool provide_a_counter_example,
614 : const bool structured_output)
615 : {
616 103 : if (!weak_property_cache.stable(impl)) return true; // Checking in case of instability is not necessary, but rather time consuming.
617 :
618 99 : const action_label_set& impl_action_labels = weak_property_cache.action_labels(impl);
619 99 : bool success = false;
620 :
621 : // Compare the obtained enable set of s' with all those of the specification.
622 130 : for(const state_type s : spec)
623 : {
624 : // Only stable states in this set should be checked.
625 116 : if (!weak_property_cache.stable(s)) { continue; }
626 :
627 : // Check whether the enabled actions of spec are included in the enabled actions of impl.
628 : // This is equivalent to checking that all spec_action_labels are in the impl_enabled_action_set.
629 115 : const action_label_set& spec_action_labels = weak_property_cache.action_labels(s);
630 :
631 : // Warning: std::includes checks whether the second range is included in the first.
632 115 : bool inclusion_success = std::includes(impl_action_labels.begin(), impl_action_labels.end(),
633 : spec_action_labels.begin(), spec_action_labels.end());
634 115 : if (inclusion_success)
635 : {
636 85 : success = true;
637 85 : break;
638 : }
639 : else
640 : {
641 : // Find the offending action.
642 35 : for(const label_type a : spec_action_labels)
643 : {
644 35 : if (impl_action_labels.count(a) == 0) // We want to know which action caused the problem.
645 : {
646 30 : culprit = a;
647 30 : break;
648 : }
649 : }
650 : }
651 : }
652 :
653 99 : if (!success && provide_a_counter_example)
654 : {
655 : // Print the acceptance set of the implementation
656 0 : if (impl_action_labels.empty())
657 : {
658 0 : if (structured_output)
659 : {
660 0 : std::cout << "left-acceptance:\n";
661 : }
662 : else
663 : {
664 0 : mCRL2log(log::verbose) << "The acceptance of the left process is empty.\n";
665 : }
666 : }
667 : else
668 : {
669 0 : if (structured_output)
670 : {
671 0 : std::cout << "left-acceptance: ";
672 : }
673 : else
674 : {
675 0 : mCRL2log(log::verbose) << "A stable acceptance set of the left process is:\n";
676 : }
677 0 : std::string sep = "";
678 0 : for (const label_type a: impl_action_labels)
679 : {
680 0 : if (structured_output)
681 : {
682 0 : std::cout << sep << l.action_label(a);
683 0 : sep = ";";
684 : }
685 : else
686 : {
687 0 : mCRL2log(log::verbose) << l.action_label(a) << "\n";
688 : }
689 : }
690 0 : if (structured_output)
691 : {
692 0 : std::cout << "\n";
693 : }
694 0 : }
695 :
696 : // Print the acceptance sets of the specification.
697 0 : if (spec.empty())
698 : {
699 0 : if (structured_output)
700 : {
701 0 : std::cout << "right-acceptance-sets: 0\n";
702 : }
703 : else
704 : {
705 0 : mCRL2log(log::verbose) << "The process at the right has no acceptance sets.\n";
706 : }
707 : }
708 : else
709 : {
710 0 : set_of_states stable;
711 : // Only the stable specification states contributed to this counter example.
712 0 : std::copy_if(spec.begin(), spec.end(), std::inserter(stable,stable.end()), [=](const state_type s){return weak_property_cache.stable(s);});
713 :
714 0 : if (structured_output)
715 : {
716 0 : std::cout << "right-acceptance-sets: " << stable.size () << "\n";
717 : }
718 : else
719 : {
720 0 : mCRL2log(log::verbose) << "Below all corresponding stable acceptance sets of the right process are provided:\n";
721 : }
722 0 : for (const state_type s: stable)
723 : {
724 0 : const action_label_set& spec_action_labels = weak_property_cache.action_labels(s);
725 0 : if (structured_output)
726 : {
727 0 : std::cout << "right-acceptance: ";
728 : }
729 : else
730 : {
731 0 : mCRL2log(log::verbose) << "An acceptance set of the right process is:\n";
732 : }
733 0 : std::string sep = "";
734 0 : for (const label_type a: spec_action_labels)
735 : {
736 0 : if (structured_output)
737 : {
738 0 : std::cout << sep << l.action_label(a);
739 0 : sep = ";";
740 : }
741 : else
742 : {
743 0 : mCRL2log(log::verbose) << l.action_label(a) << "\n";
744 : }
745 : }
746 0 : if (structured_output)
747 : {
748 0 : std::cout << "\n";
749 : }
750 : }
751 0 : }
752 0 : if (!structured_output)
753 : {
754 0 : mCRL2log(log::verbose) << "Finished printing acceptance sets.\n";
755 : }
756 : // Done printing acceptance sets.
757 : }
758 :
759 99 : return success;
760 : }
761 :
762 :
763 : } // namespace detail
764 : } // namespace lts
765 : } // namespace mcrl2
766 :
767 : #endif // LIBLTS_FAILURES_REFINEMENT_H
|