LCOV - code coverage report
Current view: top level - lts/include/mcrl2/lts - lts_utilities.h (source / functions) Hit Total Coverage
Test: mcrl2_coverage.info.cleaned Lines: 67 67 100.0 %
Date: 2019-09-14 00:54:39 Functions: 15 15 100.0 %
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             : 
      10             : /** \file
      11             :  *
      12             :  * \brief This file contains some utility functions to manipulate lts's
      13             :  * \details The function in this file typically allow to present the
      14             :  *          transitions of a state space differently.
      15             :  * \author Jan Friso Groote
      16             :  */
      17             : 
      18             : #ifndef MCRL2_LTS_LTS_UTILITIES_H
      19             : #define MCRL2_LTS_LTS_UTILITIES_H
      20             : 
      21             : #include <map>
      22             : #include <set>
      23             : #include "mcrl2/core/identifier_string.h"
      24             : #include "mcrl2/utilities/logger.h"
      25             : #include "mcrl2/lts/lts_lts.h"
      26             : #include "mcrl2/lts/lts.h"
      27             : 
      28             : namespace mcrl2
      29             : {
      30             : 
      31             : namespace lts
      32             : {
      33             : 
      34             : namespace detail
      35             : {
      36             : 
      37             : inline std::size_t apply_map(const std::size_t n, std::map<transition::size_type,transition::size_type>& mapping)
      38             : {
      39             :   const std::map<transition::size_type,transition::size_type>::const_iterator i=mapping.find(n);
      40             :   if (i==mapping.end())  // not found
      41             :   {
      42             :     return n;
      43             :   }
      44             :   return i->second;
      45             : }
      46             : 
      47             : 
      48             : // An indexed sorted vector below contains the outgoing or incoming transitions per state,
      49             : // grouped per state. The input consists of a vector of transitions. The incoming/outcoming
      50             : // tau transitions are grouped by state in the m_states_with_outgoing_or_incoming_transition. 
      51             : // It is as long as the lts aut has transitions. The vector m_indices is as long as the number
      52             : // of states plus 1. For each state it contains the place in the other vector where its tau transitions
      53             : // start. So, the tau transitions reside at position indices[s] to indices[s+1]. These indices
      54             : // can be acquired using the functions lowerbound and upperbound. 
      55             : // This data structure is chosen due to its minimal memory and time footprint. 
      56             : template <class CONTENT>
      57         194 : class indexed_sorted_vector_for_transitions
      58             : {
      59             :   protected:
      60             :     typedef std::size_t state_type;
      61             :     typedef std::size_t label_type;
      62             :     typedef std::pair<label_type,state_type> label_state_pair;
      63             : 
      64             :     std::vector < CONTENT > m_states_with_outgoing_or_incoming_transition;
      65             :     std::vector <size_t> m_indices;
      66             : 
      67             :   public:
      68             : 
      69         194 :     indexed_sorted_vector_for_transitions(const std::vector < transition >& transitions , state_type num_states, bool outgoing)
      70         194 :      : m_indices(num_states+1,0)
      71             :     {
      72             :       // First count the number of outgoing transitions per state and put it in indices.
      73        2244 :       for(const transition& t: transitions)
      74             :       {
      75        2050 :         m_indices[outgoing?t.from():t.to()]++;
      76             :       }
      77             : 
      78             :       // Calculate the m_indices where the states with outgoing/incoming tau transition must be placed.
      79             :       // Put the starting index for state i at position i-1. When placing the transitions these indices
      80             :       // are decremented properly. 
      81             :       
      82         194 :       size_t sum=0;
      83        1832 :       for(state_type& i: m_indices)  // The vector is changed. This must be a reference. 
      84             :       {
      85        1638 :         sum=sum+i;
      86        1638 :         i=sum;
      87             :       }
      88             : 
      89             :       // Now declare enough space for all transitions and store them in reverse order, while
      90             :       // at the same time decrementing the indices in m_indices. 
      91         194 :       m_states_with_outgoing_or_incoming_transition.resize(sum);
      92        2244 :       for(const transition& t: transitions)
      93             :       {
      94        2050 :         if (outgoing)
      95             :         {
      96        1398 :           assert(t.from()<m_indices.size());
      97        1398 :           assert(m_indices[t.from()]>0);
      98        1398 :           m_indices[t.from()]--;
      99        1398 :           assert(m_indices[t.from()] < m_states_with_outgoing_or_incoming_transition.size());
     100        1398 :           m_states_with_outgoing_or_incoming_transition[m_indices[t.from()]]=label_state_pair(t.label(), t.to());
     101             :         }
     102             :         else
     103             :         {
     104         652 :           assert(t.to()<m_indices.size());
     105         652 :           assert(m_indices[t.to()]>0);
     106         652 :           m_indices[t.to()]--;
     107         652 :           assert(m_indices[t.to()] < m_states_with_outgoing_or_incoming_transition.size());
     108         652 :           m_states_with_outgoing_or_incoming_transition[m_indices[t.to()]]=label_state_pair(t.label(), t.from());
     109             :         }
     110             :       }
     111         194 :       assert(m_indices.at(num_states)==m_states_with_outgoing_or_incoming_transition.size());
     112         194 :     }
     113             : 
     114             :     // Get the indexed transitions. 
     115        7692 :     const std::vector<CONTENT>& get_transitions() const
     116             :     {
     117        7692 :       return m_states_with_outgoing_or_incoming_transition;
     118             :     }
     119             :   
     120             :     // Get the lowest index of incoming/outging transitions stored in m_states_with_outgoing_or_incoming_transition.
     121        4728 :     size_t lowerbound(const state_type s) const
     122             :     {
     123        4728 :       assert(s+1<m_indices.size());
     124        4728 :       return m_indices[s];
     125             :     }
     126             : 
     127             :     // Get 1 beyond the higest index of incoming/outging transitions stored in m_states_with_outgoing_or_incoming_transition.
     128       12329 :     size_t upperbound(const state_type s) const
     129             :     {
     130       12329 :       assert(s+1<m_indices.size());
     131       12329 :       return m_indices[s+1];
     132             :     }
     133             : 
     134             :     // Drastically clear the vectors by resetting its memory usage to minimal. 
     135             :     void clear()   
     136             :     {
     137             :       std::vector <state_type>().swap(m_states_with_outgoing_or_incoming_transition);
     138             :       std::vector <size_t>().swap(m_indices);
     139             :       
     140             :     }
     141             : };
     142             : 
     143             : } // end namespace detail 
     144             : 
     145             : //
     146             : /// \brief Type for exploring transitions per state.
     147             : typedef std::pair<transition::size_type, transition::size_type> outgoing_pair_t;
     148             : 
     149             : typedef detail::indexed_sorted_vector_for_transitions < outgoing_pair_t > outgoing_transitions_per_state_t;
     150             : 
     151             : /// \brief Label of a pair of a label and target state. 
     152        7500 : inline std::size_t label(const outgoing_pair_t& p)
     153             : {
     154        7500 :   return p.first;
     155             : }
     156             : 
     157             : /// \brief Target state of a label state pair. 
     158        9010 : inline std::size_t to(const outgoing_pair_t& p)
     159             : {
     160        9010 :   return p.second;
     161             : }
     162             : 
     163             : /// \brief Type for exploring transitions per state and action.
     164             : typedef std::multimap<std::pair<transition::size_type, transition::size_type>, transition::size_type>
     165             : outgoing_transitions_per_state_action_t;
     166             : 
     167             : /// \brief From state of an iterator exploring transitions per outgoing state and action.
     168        1092 : inline std::size_t from(const outgoing_transitions_per_state_action_t::const_iterator& i)
     169             : {
     170        1092 :   return i->first.first;
     171             : }
     172             : 
     173             : /// \brief Label of an iterator exploring transitions per outgoing state and action.
     174         394 : inline std::size_t label(const outgoing_transitions_per_state_action_t::const_iterator& i)
     175             : {
     176         394 :   return i->first.second;
     177             : }
     178             : 
     179             : /// \brief To state of an iterator exploring transitions per outgoing state and action.
     180        5565 : inline std::size_t to(const outgoing_transitions_per_state_action_t::const_iterator& i)
     181             : {
     182        5565 :   return i->second;
     183             : }
     184             : 
     185             : /// \brief Provide the transitions as a multimap accessible per from state and label.
     186             : inline outgoing_transitions_per_state_action_t transitions_per_outgoing_state_action_pair(const std::vector<transition>& trans)
     187             : {
     188             :   outgoing_transitions_per_state_action_t result;
     189             :   for (const transition& t: trans)
     190             :   {
     191             :     result.insert(std::pair<std::pair<transition::size_type, transition::size_type>, transition::size_type>(
     192             :                     std::pair<transition::size_type, transition::size_type>(t.from(), t.label()), t.to()));
     193             :   }
     194             :   return result;
     195             : }
     196             : 
     197             : /// \brief Provide the transitions as a multimap accessible per from state and label.
     198          88 : inline outgoing_transitions_per_state_action_t transitions_per_outgoing_state_action_pair(
     199             :                  const std::vector<transition>& trans, 
     200             :                  const std::map<transition::size_type,transition::size_type>& hide_label_map)
     201             : {
     202          88 :   outgoing_transitions_per_state_action_t result;
     203         858 :   for (const transition& t: trans)
     204             :   {
     205             :     result.insert(std::pair<std::pair<transition::size_type, transition::size_type>, transition::size_type>(
     206         770 :                     std::pair<transition::size_type, transition::size_type>(t.from(), detail::apply_map(t.label(),hide_label_map)), t.to()));
     207             :   }
     208          88 :   return result;
     209             : } 
     210             : 
     211             : /// \brief Provide the transitions as a multimap accessible per from state and label, ordered backwardly.
     212             : inline outgoing_transitions_per_state_action_t transitions_per_outgoing_state_action_pair_reversed(const std::vector<transition>& trans)
     213             : {
     214             :   outgoing_transitions_per_state_action_t result;
     215             :   for (const transition& t: trans)
     216             :   {
     217             :     result.insert(std::pair<std::pair<transition::size_type, transition::size_type>, transition::size_type>(
     218             :                     std::pair<transition::size_type, transition::size_type>(t.to(), t.label()), t.from()));
     219             :   }
     220             :   return result;
     221             : }
     222             : 
     223             : /// \brief Provide the transitions as a multimap accessible per from state and label, ordered backwardly.
     224          54 : inline outgoing_transitions_per_state_action_t transitions_per_outgoing_state_action_pair_reversed(
     225             :                 const std::vector<transition>& trans,
     226             :                 const std::map<transition::size_type,transition::size_type>& hide_label_map)
     227             : {
     228          54 :   outgoing_transitions_per_state_action_t result;
     229         619 :   for (const transition& t: trans)
     230             :   {
     231             :     result.insert(std::pair<std::pair<transition::size_type, transition::size_type>, transition::size_type>(
     232         565 :                     std::pair<transition::size_type, transition::size_type>(t.to(), detail::apply_map(t.label(),hide_label_map)), t.from()));
     233             :   }
     234          54 :   return result;
     235             : } 
     236             : 
     237             : namespace detail
     238             : {
     239             : // Yields a label with an obscure name referring to divergence.
     240             : 
     241             : template < class LABEL_TYPE >
     242             : // LABEL_TYPE make_divergence_label(const std::string& s, const LABEL_TYPE& l)
     243          14 : LABEL_TYPE make_divergence_label(const std::string& s)
     244             : {
     245          14 :   return LABEL_TYPE(s);
     246             : }
     247             : 
     248             : template <>
     249             : inline mcrl2::lts::action_label_lts make_divergence_label<mcrl2::lts::action_label_lts>(const std::string& s)
     250             : {
     251             :   return action_label_lts(lps::multi_action(process::action(process::action_label(core::identifier_string(s),
     252             :                                                                                   data::sort_expression_list()),
     253             :                                                             data::data_expression_list())));
     254             : }
     255             : 
     256             : // Make a new divergent_transition_label and replace each self loop with it.
     257             : // Return the number of the divergent transition label.
     258             : template < class LTS_TYPE >
     259          14 : std::size_t mark_explicit_divergence_transitions(LTS_TYPE& l)
     260             : {
     261             :   // Below we create an odd action label, representing divergence.
     262          28 :   const typename LTS_TYPE::action_label_t lab=make_divergence_label<typename LTS_TYPE::action_label_t>("!@*&divergence&*@!"); 
     263          14 :   std::size_t divergent_transition_label=l.add_action(lab);
     264          14 :   assert(divergent_transition_label+1==l.num_action_labels());
     265          92 :   for(transition& t: l.get_transitions())
     266             :   {
     267          78 :     if (l.is_tau(l.apply_hidden_label_map(t.label())) && t.to()==t.from())
     268             :     {
     269           8 :       t = transition(t.to(),divergent_transition_label,t.to());
     270             :     }
     271             :   }
     272          28 :   return divergent_transition_label;
     273             : }
     274             : 
     275             : // Replace each transition in a state that is an outgoing divergent_transition with a tau_loop in that state.
     276             : template < class LTS_TYPE >
     277          14 : void unmark_explicit_divergence_transitions(LTS_TYPE& l, const std::size_t divergent_transition_label)
     278             : {
     279          88 :   for(transition& t: l.get_transitions())
     280             :   {
     281          74 :     if (t.label()==divergent_transition_label)
     282             :     { 
     283           8 :       t = transition(t.from(),l.tau_label_index(),t.from());
     284             :     }
     285             :   }
     286          14 : }
     287             : 
     288             : } // namespace detail
     289             : 
     290             : }
     291             : }
     292             : 
     293             : #endif // MCRL2_LTS_LTS_UTILITIES_H

Generated by: LCOV version 1.12