LCOV - code coverage report
Current view: top level - lts/include/mcrl2/lts/detail - liblts_tau_star_reduce.h (source / functions) Hit Total Coverage
Test: mcrl2_coverage.info.cleaned Lines: 104 104 100.0 %
Date: 2020-07-11 00:44:39 Functions: 4 4 100.0 %
Legend: Lines: hit not hit

          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             : /// \file lts/detail/liblts_tau_star_reduce.h
      10             : 
      11             : #ifndef _LIBLTS_TAUSTARREDUCE_H
      12             : #define _LIBLTS_TAUSTARREDUCE_H
      13             : 
      14             : #include "mcrl2/lts/lts_utilities.h"
      15             : 
      16             : namespace mcrl2
      17             : {
      18             : namespace lts
      19             : {
      20             : namespace detail
      21             : {
      22             : 
      23             : //Replace sequences tau* a tau* by a single action a.
      24             : 
      25             : 
      26             : enum t_reach { unknown, reached, explored };
      27             : 
      28             : /// \brief This procedure calculates the transitive tau
      29             : ///        closure as a separate vector of transitions, for
      30             : ///        a given transition system.
      31             : /// \parameter l A labelled transition system
      32             : /// \parameter forward A boolean that indicates whether the resulting closure
      33             : //             points forward, to the next state, or backward, to the previous state.
      34             : /// \return A map from states to sets of states indicating for each state those
      35             : //          states that can be reached by one or more tau_steps.
      36             : 
      37             : template < class STATE_LABEL_T, class ACTION_LABEL_T, class LTS_BASE_CLASS >
      38             : std::map < std::size_t,
      39             :            std::set <typename lts<STATE_LABEL_T,ACTION_LABEL_T, LTS_BASE_CLASS>::states_size_type > > 
      40          93 :             calculate_non_reflexive_transitive_tau_closure(lts<STATE_LABEL_T, ACTION_LABEL_T, LTS_BASE_CLASS>& l,
      41             :             const bool forward)
      42             : {
      43             :   typedef typename lts<STATE_LABEL_T, ACTION_LABEL_T, LTS_BASE_CLASS>::states_size_type state_t;
      44             : 
      45             :   typedef std::map < state_t,std::set < state_t > > map_from_states_to_states;
      46          93 :   map_from_states_to_states resulting_tau_transitions;
      47             : 
      48             :   // Copy the internal transitions into the result.
      49         553 :   for(std::vector < mcrl2::lts::transition>::const_iterator i=l.get_transitions().begin(); i!=l.get_transitions().end(); ++i)
      50             :   {
      51         460 :     if (l.is_tau(l.apply_hidden_label_map(i->label())))
      52             :     {
      53         110 :       if (forward) 
      54             :       { 
      55          43 :         resulting_tau_transitions[i->from()].insert(i->to());
      56             :       }
      57             :       else
      58             :       {
      59          67 :         resulting_tau_transitions[i->to()].insert(i->from());
      60             :       }
      61             :     }
      62             :   }
      63             : 
      64          93 :   bool new_state_added=true;
      65         299 :   while (new_state_added)
      66             :   {
      67         103 :     new_state_added=false;
      68         345 :     for(typename map_from_states_to_states::iterator i=resulting_tau_transitions.begin(); 
      69         345 :                        i!=resulting_tau_transitions.end(); ++i)
      70             :     {
      71         242 :       const std::set<std::size_t>& outgoing_states= i->second;
      72         484 :       std::set<std::size_t> new_outgoing_states=outgoing_states;
      73         437 :       for(std::set<std::size_t>::const_iterator j=outgoing_states.begin(); j!=outgoing_states.end(); j++)
      74             :       {
      75         195 :         new_outgoing_states.insert(resulting_tau_transitions[*j].begin(),
      76         195 :                                    resulting_tau_transitions[*j].end());
      77             :       }
      78         242 :       if (i->second.size()<new_outgoing_states.size())
      79             :       { 
      80          15 :         i->second=new_outgoing_states;
      81          15 :         new_state_added=true;
      82             :       }
      83             :     }
      84             :   }
      85             : 
      86          93 :   return resulting_tau_transitions;
      87             : }
      88             : 
      89             : 
      90             : template < class STATE_LABEL_T, class ACTION_LABEL_T, class LTS_BASE_CLASS >
      91          31 : void reflexive_transitive_tau_closure(lts<STATE_LABEL_T, ACTION_LABEL_T, LTS_BASE_CLASS>& l)
      92             : // This method assumes there are no tau loops!
      93             : {
      94             :   typedef typename lts<STATE_LABEL_T, ACTION_LABEL_T, LTS_BASE_CLASS>::states_size_type state_t;
      95          31 :   const std::vector < transition >& original_transitions=l.get_transitions();
      96          62 :   std::set < transition> new_transitions;
      97             : 
      98             :   // Add for every tau*.a tau* transitions sequence a single transition a;
      99          62 :   std::map <state_t, std::set <state_t> > backward_tau_closure=calculate_non_reflexive_transitive_tau_closure(l,false);
     100          62 :   std::map <state_t, std::set <state_t> > forward_tau_closure=calculate_non_reflexive_transitive_tau_closure(l,true);
     101         190 :   for(const transition& t: original_transitions)
     102             :   {
     103         159 :     new_transitions.insert(t);
     104         159 :     std::set<state_t>& new_from_states=backward_tau_closure[t.from()];
     105         159 :     std::set<state_t>& new_to_states=forward_tau_closure[t.to()];
     106         217 :     for(typename std::set<state_t>::const_iterator j_from=new_from_states.begin(); j_from!=new_from_states.end(); ++j_from)
     107             :     {
     108          58 :       new_transitions.insert(transition(*j_from,t.label(),t.to()));
     109          76 :       for(typename std::set<state_t>::const_iterator j_to=new_to_states.begin(); j_to!=new_to_states.end(); ++j_to)
     110             :       {
     111          18 :         new_transitions.insert(transition(*j_from,t.label(),*j_to));
     112             :       }
     113             :     }
     114         229 :     for(typename std::set<state_t>::const_iterator j_to=new_to_states.begin(); j_to!=new_to_states.end(); ++j_to)
     115             :     {
     116          70 :       new_transitions.insert(transition(t.from(),t.label(),*j_to));
     117             :     }
     118             :   }
     119             : 
     120          31 :   l.clear_transitions();
     121             : 
     122         146 :   for(state_t i=0; i<l.num_states(); ++i)
     123             :   {
     124         115 :     new_transitions.insert(transition(i,l.tau_label_index(),i));
     125             :   }
     126             :   
     127             :   // Add the newly generated transitions
     128         417 :   for(std::set < transition >::const_iterator i=new_transitions.begin();
     129         417 :             i!=new_transitions.end(); ++i)
     130             :   {
     131         386 :     l.add_transition(*i);
     132             :   }
     133          31 : }
     134             : 
     135             : 
     136             : /// \brief Removes each transition s-a->s' if also transitions s-a->-tau->s' or s-tau->-a->s' are 
     137             : ///        present. It uses the hidden_label_map to determine whether transitions are internal. 
     138             : template < class STATE_LABEL_T, class ACTION_LABEL_T, class LTS_BASE_CLASS >
     139          31 : void remove_redundant_transitions(lts<STATE_LABEL_T, ACTION_LABEL_T, LTS_BASE_CLASS>& l)
     140             : {
     141             :   typedef typename lts<STATE_LABEL_T, ACTION_LABEL_T, LTS_BASE_CLASS>::states_size_type state_type;
     142             :   typedef typename lts<STATE_LABEL_T, ACTION_LABEL_T, LTS_BASE_CLASS>::labels_size_type label_type;
     143             : 
     144          62 :   outgoing_transitions_per_state_t outgoing_transitions(l.get_transitions(),l.num_states(),true);
     145          31 :   l.clear_transitions();
     146          62 :   std::set < state_type > states_reachable_in_one_visible_action;
     147          62 :   std::set < state_type > states_reachable_in_one_hidden_action;
     148             : 
     149             :   // for(outgoing_transitions_per_state_t::const_iterator i=outgoing_transitions.begin(); i!=outgoing_transitions.end(); ++i)
     150             : 
     151             :   // for(const outgoing_transitions_t& vec: outgoing_transitions)
     152         141 :   for(state_type from=0; from < l.num_states(); from++)
     153             :   {
     154             :     // for(const outgoing_pair_t& p: vec)
     155         344 :     for(size_t j=outgoing_transitions.lowerbound(from); j<outgoing_transitions.upperbound(from); ++j)
     156             :     {
     157         234 :       const outgoing_pair_t& p = outgoing_transitions.get_transitions()[j];
     158         234 :       const state_type from_=from;         // the start state of a transition under consideration. 
     159         234 :       const label_type label_=label(p);    // the label
     160         234 :       const state_type to_=to(p);          // the target state
     161             : 
     162         234 :       states_reachable_in_one_visible_action.clear();
     163         234 :       states_reachable_in_one_hidden_action.clear();
     164             : 
     165             :       // For every transition from-label->to we calculate the sets { s | from -a->s } and { s | from -tau-> s }.
     166             :       // assert(from_<outgoing_transitions.size());
     167             :       // for(const outgoing_pair_t& j: outgoing_transitions[from_])
     168        1034 :       for(size_t j_=outgoing_transitions.lowerbound(from_); j_<outgoing_transitions.upperbound(from_); ++j_)
     169             :       {
     170         800 :         const outgoing_pair_t& j = outgoing_transitions.get_transitions()[j_];
     171         800 :         if (l.is_tau(l.apply_hidden_label_map(label(j))))
     172             :         {
     173         164 :           states_reachable_in_one_hidden_action.insert(to(j));
     174             :         }
     175         636 :         else if (label_==label(j))
     176             :         {
     177         347 :           assert(!l.is_tau(l.apply_hidden_label_map(label_)));
     178         347 :           states_reachable_in_one_visible_action.insert(to(j)); 
     179             :         }
     180             :       }
     181             : 
     182             :       // Now check whether to is reachable in one step from one of the two sets constructed above. If no,
     183             :       // insert the transition in l.transitions. 
     184         234 :       bool found=false;
     185             :       
     186         334 :       for(const state_type& middle: states_reachable_in_one_hidden_action)
     187             :       {
     188             :         // Find a visible step from state middle to state to, unless label is hidden, in which case we search
     189             :         // a hidden step. 
     190             :         // for(const outgoing_pair_t& j: outgoing_transitions[middle])
     191         318 :         for(size_t j_=outgoing_transitions.lowerbound(middle); j_<outgoing_transitions.upperbound(middle); ++j_)
     192             :         {
     193         218 :           const outgoing_pair_t& j=outgoing_transitions.get_transitions()[j_];
     194         218 :           if (l.is_tau(l.apply_hidden_label_map(label_)))
     195             :           { 
     196          77 :             if (l.is_tau(l.apply_hidden_label_map(label(j))) && to(j)==to_)
     197             :             {
     198           2 :               assert(!found);
     199           2 :               found=true; break;
     200             :             }
     201             :           }
     202             :           else // label is visible.
     203             :           {
     204         141 :             if (label(j)==label_ && to(j)==to_)
     205             :             {
     206          50 :               assert(!found);
     207          50 :               found=true; break;
     208             :             }
     209             :           }
     210             :         }
     211         152 :         if (found) break;
     212             :       }
     213             :       
     214         234 :       if (!found && !l.is_tau(l.apply_hidden_label_map(label_)))
     215             :       {
     216         314 :         for(const state_type& middle: states_reachable_in_one_visible_action)
     217             :         {
     218             :           // Find a hidden step from state middle to state to.
     219             :           // for(const outgoing_pair_t& j: outgoing_transitions[middle])
     220         651 :           for(size_t j_=outgoing_transitions.lowerbound(middle); j_<outgoing_transitions.upperbound(middle); ++j_)
     221             :           {
     222         480 :             const outgoing_pair_t& j=outgoing_transitions.get_transitions()[j_];
     223         480 :             if (l.is_tau(l.apply_hidden_label_map(label(j))) && to(j)==to_)
     224             :             { 
     225          35 :               assert(!found);
     226          35 :               found=true; break;
     227             :             } 
     228             :           }
     229         206 :           if (found) break;
     230             :         }
     231             :       }
     232             : 
     233             :       // If no alternative transition is found, add this transition to l.transitions().
     234         234 :       if (!found) 
     235             :       {
     236         147 :         l.add_transition(transition(from_, label_, to_));
     237             :       }
     238             :     }  
     239             :     // from++;
     240             :   }
     241          31 : }
     242             : 
     243             : 
     244             : template < class STATE_LABEL_T, class ACTION_LABEL_T, class LTS_BASE_CLASS >
     245          31 : void tau_star_reduce(lts< STATE_LABEL_T, ACTION_LABEL_T, LTS_BASE_CLASS >& l)
     246             : // This method assumes there are no tau loops!
     247             : {
     248             :   typedef typename lts<STATE_LABEL_T, ACTION_LABEL_T, LTS_BASE_CLASS>::states_size_type state_t;
     249          31 :   std::vector < transition >& original_transitions=l.get_transitions();
     250          62 :   std::set < transition> new_transitions;
     251             : 
     252             :   // Add all the original non tau transitions.
     253         173 :   for(std::vector < transition >::const_iterator i=original_transitions.begin(); i!=original_transitions.end(); ++i)
     254             :   {
     255         142 :     if (!l.is_tau(l.apply_hidden_label_map(i->label())))
     256             :     {
     257         118 :       new_transitions.insert(*i);
     258             :     }
     259             :   }
     260             : 
     261             :   // Add for every tau*.a transitions sequence a single transition a, provided a is not tau.
     262          62 :   std::map <state_t, std::set <state_t> > backward_tau_closure=calculate_non_reflexive_transitive_tau_closure(l,false);
     263         173 :   for(std::vector < transition >::const_iterator i=original_transitions.begin(); i!=original_transitions.end(); ++i)
     264             :   {
     265         142 :     if (!l.is_tau(l.apply_hidden_label_map(i->label())))
     266             :     {
     267         118 :       std::set<state_t>& new_from_states=backward_tau_closure[i->from()];
     268         148 :       for(typename std::set<state_t>::const_iterator j=new_from_states.begin(); j!=new_from_states.end(); ++j)
     269             :       {
     270          30 :         new_transitions.insert(transition(*j,i->label(),i->to()));
     271             :       }
     272             :     }
     273             :   }
     274          31 :   l.clear_transitions();
     275             :   
     276             :   // Add the newly generated transitions
     277         179 :   for(std::set < transition >::const_iterator i=new_transitions.begin();
     278         179 :             i!=new_transitions.end(); ++i)
     279             :   {
     280         148 :     l.add_transition(*i);
     281             :   }
     282             : 
     283          31 :   reachability_check(l, true); // Remove unreachable parts.
     284          31 : }
     285             : 
     286             : }
     287             : }
     288             : }
     289             : #endif // _LIBLTS_TAUSTARREDUCE_H

Generated by: LCOV version 1.13