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: 52 52 100.0 %
Date: 2019-06-19 00:50:04 Functions: 14 14 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             : inline std::size_t apply_map(const std::size_t n, std::map<transition::size_type,transition::size_type>& mapping)
      37             : {
      38             :   const std::map<transition::size_type,transition::size_type>::const_iterator i=mapping.find(n);
      39             :   if (i==mapping.end())  // not found
      40             :   {
      41             :     return n;
      42             :   }
      43             :   return i->second;
      44             : }
      45             : 
      46             : 
      47             : } // end namespace detail 
      48             : 
      49             : /// \brief Type for exploring transitions per state.
      50             : typedef std::multimap<transition::size_type, std::pair<transition::size_type, transition::size_type> >
      51             : outgoing_transitions_per_state_t;
      52             : 
      53             : /// \brief From state of an iterator exploring transitions per outgoing state.
      54        4745 : inline std::size_t from(const outgoing_transitions_per_state_t::const_iterator& i)
      55             : {
      56        4745 :   return i->first;
      57             : }
      58             : 
      59             : /// \brief Label of an iterator exploring transitions per outgoing state.
      60        5222 : inline std::size_t label(const outgoing_transitions_per_state_t::const_iterator& i)
      61             : {
      62        5222 :   return i->second.first;
      63             : }
      64             : 
      65             : /// \brief To state of an iterator exploring transitions per outgoing state.
      66        5017 : inline std::size_t to(const outgoing_transitions_per_state_t::const_iterator& i)
      67             : {
      68        5017 :   return i->second.second;
      69             : }
      70             : 
      71             : /// \brief Provide the transitions as a multimap accessible per outgoing state, useful
      72             : ///        for for instance state space exploration.
      73          70 : inline outgoing_transitions_per_state_t transitions_per_outgoing_state(const std::vector<transition>& trans)
      74             : {
      75          70 :   outgoing_transitions_per_state_t result;
      76         546 :   for (const transition& t: trans)
      77             :   {
      78             :     result.insert(std::pair<transition::size_type, std::pair<transition::size_type, transition::size_type> >(
      79         476 :                     t.from(), std::pair<transition::size_type, transition::size_type>(t.label(), t.to())));
      80             :   }
      81          70 :   return result;
      82             : }
      83             : 
      84             : /// \brief Provide the transitions as a multimap accessible per outgoing state, useful
      85             : ///        for for instance state space exploration.
      86          89 : inline outgoing_transitions_per_state_t transitions_per_outgoing_state(
      87             :                     const std::vector<transition>& trans, 
      88             :                     const std::map<transition::size_type,transition::size_type>& hide_label_map)
      89             : {
      90          89 :   outgoing_transitions_per_state_t result;
      91         848 :   for (const transition& t: trans)
      92             :   {
      93             :     result.insert(std::pair<transition::size_type, std::pair<transition::size_type, transition::size_type> >(
      94         759 :                     t.from(), std::pair<transition::size_type, transition::size_type>(detail::apply_map(t.label(),hide_label_map), t.to())));
      95             :   }
      96          89 :   return result;
      97             : } 
      98             : 
      99             : /// \brief Provide the transitions as a multimap accessible per outgoing state, useful
     100             : ///        for for instance state space exploration.
     101             : inline outgoing_transitions_per_state_t transitions_per_outgoing_state_reversed(const std::vector<transition>& trans)
     102             : {
     103             :   outgoing_transitions_per_state_t result;
     104             :   for (const transition& t: trans)
     105             :   {
     106             :     result.insert(std::pair<transition::size_type, std::pair<transition::size_type, transition::size_type> >(
     107             :                     t.to(), std::pair<transition::size_type, transition::size_type>(t.label(), t.from())));
     108             :   }
     109             :   return result;
     110             : }
     111             : 
     112             : /// \brief Type for exploring transitions per state and action.
     113             : /// \brief Provide the transitions as a multimap accessible per outgoing state, useful
     114             : ///        for for instance state space exploration.
     115          33 : inline outgoing_transitions_per_state_t transitions_per_outgoing_state_reversed(
     116             :                   const std::vector<transition>& trans, 
     117             :                   const std::map<transition::size_type,transition::size_type>& hide_label_map)
     118             : {
     119          33 :   outgoing_transitions_per_state_t result;
     120         522 :   for (const transition& t: trans)
     121             :   {
     122             :     result.insert(std::pair<transition::size_type, std::pair<transition::size_type, transition::size_type> >(
     123         489 :                     t.to(), std::pair<transition::size_type, transition::size_type>(detail::apply_map(t.label(),hide_label_map), t.from())));
     124             :   }
     125          33 :   return result;
     126             : } 
     127             : 
     128             : /// \brief Type for exploring transitions per state and action.
     129             : typedef std::multimap<std::pair<transition::size_type, transition::size_type>, transition::size_type>
     130             : outgoing_transitions_per_state_action_t;
     131             : 
     132             : /// \brief From state of an iterator exploring transitions per outgoing state and action.
     133        1092 : inline std::size_t from(const outgoing_transitions_per_state_action_t::const_iterator& i)
     134             : {
     135        1092 :   return i->first.first;
     136             : }
     137             : 
     138             : /// \brief Label of an iterator exploring transitions per outgoing state and action.
     139         394 : inline std::size_t label(const outgoing_transitions_per_state_action_t::const_iterator& i)
     140             : {
     141         394 :   return i->first.second;
     142             : }
     143             : 
     144             : /// \brief To state of an iterator exploring transitions per outgoing state and action.
     145        5565 : inline std::size_t to(const outgoing_transitions_per_state_action_t::const_iterator& i)
     146             : {
     147        5565 :   return i->second;
     148             : }
     149             : 
     150             : /// \brief Provide the transitions as a multimap accessible per from state and label.
     151             : inline outgoing_transitions_per_state_action_t transitions_per_outgoing_state_action_pair(const std::vector<transition>& trans)
     152             : {
     153             :   outgoing_transitions_per_state_action_t result;
     154             :   for (const transition& t: trans)
     155             :   {
     156             :     result.insert(std::pair<std::pair<transition::size_type, transition::size_type>, transition::size_type>(
     157             :                     std::pair<transition::size_type, transition::size_type>(t.from(), t.label()), t.to()));
     158             :   }
     159             :   return result;
     160             : }
     161             : 
     162             : /// \brief Provide the transitions as a multimap accessible per from state and label.
     163          88 : inline outgoing_transitions_per_state_action_t transitions_per_outgoing_state_action_pair(
     164             :                  const std::vector<transition>& trans, 
     165             :                  const std::map<transition::size_type,transition::size_type>& hide_label_map)
     166             : {
     167          88 :   outgoing_transitions_per_state_action_t result;
     168         858 :   for (const transition& t: trans)
     169             :   {
     170             :     result.insert(std::pair<std::pair<transition::size_type, transition::size_type>, transition::size_type>(
     171         770 :                     std::pair<transition::size_type, transition::size_type>(t.from(), detail::apply_map(t.label(),hide_label_map)), t.to()));
     172             :   }
     173          88 :   return result;
     174             : } 
     175             : 
     176             : /// \brief Provide the transitions as a multimap accessible per from state and label, ordered backwardly.
     177             : inline outgoing_transitions_per_state_action_t transitions_per_outgoing_state_action_pair_reversed(const std::vector<transition>& trans)
     178             : {
     179             :   outgoing_transitions_per_state_action_t result;
     180             :   for (const transition& t: trans)
     181             :   {
     182             :     result.insert(std::pair<std::pair<transition::size_type, transition::size_type>, transition::size_type>(
     183             :                     std::pair<transition::size_type, transition::size_type>(t.to(), t.label()), t.from()));
     184             :   }
     185             :   return result;
     186             : }
     187             : 
     188             : /// \brief Provide the transitions as a multimap accessible per from state and label, ordered backwardly.
     189          54 : inline outgoing_transitions_per_state_action_t transitions_per_outgoing_state_action_pair_reversed(
     190             :                 const std::vector<transition>& trans,
     191             :                 const std::map<transition::size_type,transition::size_type>& hide_label_map)
     192             : {
     193          54 :   outgoing_transitions_per_state_action_t result;
     194         619 :   for (const transition& t: trans)
     195             :   {
     196             :     result.insert(std::pair<std::pair<transition::size_type, transition::size_type>, transition::size_type>(
     197         565 :                     std::pair<transition::size_type, transition::size_type>(t.to(), detail::apply_map(t.label(),hide_label_map)), t.from()));
     198             :   }
     199          54 :   return result;
     200             : } 
     201             : 
     202             : namespace detail
     203             : {
     204             : // Yields a label with an obscure name referring to divergence.
     205             : 
     206             : template < class LABEL_TYPE >
     207             : // LABEL_TYPE make_divergence_label(const std::string& s, const LABEL_TYPE& l)
     208          14 : LABEL_TYPE make_divergence_label(const std::string& s)
     209             : {
     210          14 :   return LABEL_TYPE(s);
     211             : }
     212             : 
     213             : template <>
     214             : inline mcrl2::lts::action_label_lts make_divergence_label<mcrl2::lts::action_label_lts>(const std::string& s)
     215             : {
     216             :   return action_label_lts(lps::multi_action(process::action(process::action_label(core::identifier_string(s),
     217             :                                                                                   data::sort_expression_list()),
     218             :                                                             data::data_expression_list())));
     219             : }
     220             : 
     221             : // Make a new divergent_transition_label and replace each self loop with it.
     222             : // Return the number of the divergent transition label.
     223             : template < class LTS_TYPE >
     224          14 : std::size_t mark_explicit_divergence_transitions(LTS_TYPE& l)
     225             : {
     226             :   // Below we create an odd action label, representing divergence.
     227          28 :   const typename LTS_TYPE::action_label_t lab=make_divergence_label<typename LTS_TYPE::action_label_t>("!@*&divergence&*@!"); 
     228          14 :   std::size_t divergent_transition_label=l.add_action(lab);
     229          14 :   assert(divergent_transition_label+1==l.num_action_labels());
     230          92 :   for(transition& t: l.get_transitions())
     231             :   {
     232          78 :     if (l.is_tau(l.apply_hidden_label_map(t.label())) && t.to()==t.from())
     233             :     {
     234           8 :       t = transition(t.to(),divergent_transition_label,t.to());
     235             :     }
     236             :   }
     237          28 :   return divergent_transition_label;
     238             : }
     239             : 
     240             : // Replace each transition in a state that is an outgoing divergent_transition with a tau_loop in that state.
     241             : template < class LTS_TYPE >
     242          14 : void unmark_explicit_divergence_transitions(LTS_TYPE& l, const std::size_t divergent_transition_label)
     243             : {
     244          88 :   for(transition& t: l.get_transitions())
     245             :   {
     246          74 :     if (t.label()==divergent_transition_label)
     247             :     { 
     248           8 :       t = transition(t.from(),l.tau_label_index(),t.from());
     249             :     }
     250             :   }
     251          14 : }
     252             : 
     253             : } // namespace detail
     254             : 
     255             : }
     256             : }
     257             : 
     258             : #endif // MCRL2_LTS_LTS_UTILITIES_H

Generated by: LCOV version 1.12