LCOV - code coverage report
Current view: top level - lts/include/mcrl2/lts/detail - liblts_failures_refinement.h (source / functions) Hit Total Coverage
Test: mcrl2_coverage.info.cleaned Lines: 190 243 78.2 %
Date: 2024-03-08 02:52:28 Functions: 22 33 66.7 %
Legend: Lines: hit not hit

          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

Generated by: LCOV version 1.14