LCOV - code coverage report
Current view: top level - lts/include/mcrl2/lts - lts.h (source / functions) Hit Total Coverage
Test: mcrl2_coverage.info.cleaned Lines: 123 130 94.6 %
Date: 2019-06-20 00:49:45 Functions: 69 103 67.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 lts.h
      11             :  *
      12             :  * \brief The file containing the core class for transition systems.
      13             :  * \details This is the LTS library's main header file. It declares all publicly
      14             :  * accessible data structures that form the interface of the library.
      15             :  * \author Muck van Weerdenburg, Jan Friso Groote
      16             :  */
      17             : 
      18             : #ifndef MCRL2_LTS_LTS_H
      19             : #define MCRL2_LTS_LTS_H
      20             : 
      21             : #include <string>
      22             : #include <vector>
      23             : #include <map>
      24             : #include <cstdio>
      25             : #include <algorithm>
      26             : #include <cassert>
      27             : #include "mcrl2/lts/transition.h"
      28             : #include "mcrl2/lts/lts_type.h"
      29             : 
      30             : 
      31             : namespace mcrl2
      32             : {
      33             : 
      34             : /** \brief The main LTS namespace.
      35             :  * \details This namespace contains all data structures and members of the LTS
      36             :  * library.
      37             :  */
      38             : namespace lts
      39             : {
      40             : 
      41             : /** \brief A class that contains a labelled transition system.
      42             :     \details The state labels and action labels can be any type.
      43             :         Essentially, a labelled transition system consists of a
      44             :         vector of transitions. Each transition is a triple of
      45             :         three numbers <from, label, to>. For these numbers, there
      46             :         can be associated state labels (for 'from' and 'to'), and
      47             :         action labels (for 'label'). But it is also possible, that
      48             :         no state or action labels are provided. For all action labels
      49             :         it is maintained whether this action label is an internal
      50             :         'tau' action. This can be indicated for each action label
      51             :         separately. Finally, the number of states is recalled as
      52             :         a separate variable.
      53             : */
      54             : 
      55             : template < class STATE_LABEL_T, class ACTION_LABEL_T, class LTS_BASE>
      56        1428 : class lts: public LTS_BASE
      57             : {
      58             :   public:
      59             : 
      60             :     /** \brief The type of state labels.
      61             :     */
      62             :     typedef STATE_LABEL_T state_label_t;
      63             : 
      64             :     /** \brief The type of action labels.
      65             :     */
      66             :     typedef ACTION_LABEL_T action_label_t;
      67             : 
      68             :     /** \brief The type of the used lts base.
      69             :     */
      70             :     typedef LTS_BASE base_t;
      71             : 
      72             :     /** \brief The sort that contains the indices of states.
      73             :     */
      74             :     typedef typename std::vector < STATE_LABEL_T >::size_type states_size_type;
      75             : 
      76             :     /** \brief The sort that represents the indices of labels.
      77             :     */
      78             :     typedef typename std::vector < ACTION_LABEL_T >::size_type labels_size_type;
      79             : 
      80             :     /** \brief The sort that contains indices of transitions.
      81             :     */
      82             :     typedef typename std::vector<transition>::size_type transitions_size_type;
      83             : 
      84             :   protected:
      85             : 
      86             :     states_size_type m_nstates;
      87             :     states_size_type m_init_state;
      88             :     std::vector<transition> m_transitions;
      89             :     std::vector<STATE_LABEL_T> m_state_labels;
      90             :     std::vector<ACTION_LABEL_T> m_action_labels; // At position 0 we always find the label that corresponds to tau.
      91             :     // The following map indicates for every label index, which label is obtained after hiding
      92             :     // actions. This is the identity map by default, and it is filled using a call to the
      93             :     // function hide_actions. 
      94             :     std::map<labels_size_type,labels_size_type> m_hidden_label_map; 
      95             : 
      96             :   public:
      97             : 
      98             :     /** \brief Creates an empty LTS.
      99             :      */
     100         882 :     lts()
     101         882 :      : m_nstates(0)
     102             :     {
     103         882 :       m_action_labels.push_back(ACTION_LABEL_T::tau_action());
     104         882 :     }
     105             : 
     106             :     /** \brief Creates a copy of the supplied LTS.
     107             :      * \param[in] l The LTS to copy. */
     108         300 :     lts(const lts& l):
     109             :       LTS_BASE(l), 
     110             :       m_nstates(l.m_nstates),
     111             :       m_init_state(l.m_init_state),
     112             :       m_transitions(l.m_transitions),
     113             :       m_state_labels(l.m_state_labels),
     114             :       m_action_labels(l.m_action_labels),
     115         300 :       m_hidden_label_map(l.m_hidden_label_map)
     116             :     {
     117         300 :       assert(m_action_labels.size()>0 && m_action_labels[0]==ACTION_LABEL_T::tau_action());
     118         300 :     }
     119             : 
     120             :     /** \brief Swap this lts with the supplied supplied LTS.
     121             :      * \param[in] l The LTS to swap. */
     122          59 :     void swap(lts& l)
     123             :     {
     124          59 :       static_cast<LTS_BASE&>(*this).swap(static_cast<LTS_BASE&>(l));
     125             :       {
     126          59 :         const states_size_type aux=m_init_state;
     127          59 :         m_init_state=l.m_init_state;
     128          59 :         l.m_init_state=aux;
     129             :       }
     130             :       {
     131          59 :         const states_size_type aux=m_nstates;
     132          59 :         m_nstates=l.m_nstates;
     133          59 :         l.m_nstates=aux;
     134             :       }
     135          59 :       m_transitions.swap(l.m_transitions);
     136          59 :       m_state_labels.swap(l.m_state_labels);
     137          59 :       m_action_labels.swap(l.m_action_labels);
     138          59 :       assert(m_action_labels.size()>0 && m_action_labels[0]==ACTION_LABEL_T::tau_action());
     139          59 :       assert(l.m_action_labels.size()>0 && l.m_action_labels[0]==ACTION_LABEL_T::tau_action());
     140          59 :       m_hidden_label_map.swap(l.m_hidden_label_map);
     141          59 :     }
     142             : 
     143             :     /** \brief Gets the number of states of this LTS.
     144             :      * \return The number of states of this LTS. */
     145       44577 :     states_size_type num_states() const
     146             :     {
     147       44577 :       return m_nstates;
     148             :     }
     149             : 
     150             :     /** \brief Provides the state labels of an LTS.
     151             :      ** \return A reference to the state label vector of the LTS.
     152             :     */
     153             :     std::vector<STATE_LABEL_T>& state_labels()
     154             :     {
     155             :       return m_state_labels;
     156             :     }
     157             : 
     158             :     /** \brief Provides the state labels of an LTS.
     159             :      ** \return A reference to the state label vector of the LTS.
     160             :     */
     161             :     const std::vector<STATE_LABEL_T>& state_labels() const
     162             :     {
     163             :       return m_state_labels;
     164             :     }
     165             : 
     166             :     /** \brief Gets the number of state labels of this LTS.
     167             :      *  \details As states do not need to have state labels,
     168             :      *  the number of state labels can differ from the number of
     169             :      *  states.
     170             :      *  \return The number of state labels of this LTS. */
     171          52 :     states_size_type num_state_labels() const
     172             :     {
     173          52 :       return m_state_labels.size();
     174             :     }
     175             : 
     176             :     /** \brief Sets the number of states of this LTS.
     177             :      * \param[in] n The number of states of this LTS.
     178             :      * \param[in] has_state_labels If true state labels are initialised
     179             :      */
     180        1758 :     void set_num_states(const states_size_type n, const bool has_state_labels = true)
     181             :     {
     182        1758 :       m_nstates = n;
     183        1758 :       if (has_state_labels)
     184             :       {
     185         850 :         if (m_state_labels.size() > 0)
     186             :         {
     187           0 :           m_state_labels.resize(n);
     188             :         }
     189             :         else
     190             :         {
     191         850 :           m_state_labels = std::vector<STATE_LABEL_T>();
     192             :         }
     193             :       }
     194             :       else
     195             :       {
     196         908 :         m_state_labels = std::vector<STATE_LABEL_T>();
     197             :       }
     198        1758 :     }
     199             : 
     200             :     /** \brief Gets the number of transitions of this LTS.
     201             :      * \return The number of transitions of this LTS. */
     202        2095 :     transitions_size_type num_transitions() const
     203             :     {
     204        2095 :       return m_transitions.size();
     205             :     }
     206             : 
     207             :     /** \brief Sets the number of action labels of this LTS.
     208             :      * \details If space is reserved for new action labels,
     209             :      *          these are set to the default action label. */
     210          10 :     void set_num_action_labels(const labels_size_type n)
     211             :     {
     212          10 :       m_action_labels.resize(n);
     213          10 :       assert(m_action_labels.size()>0 && m_action_labels[0]==ACTION_LABEL_T::tau_action());
     214          10 :     } 
     215             : 
     216             :     /** \brief Gets the number of action labels of this LTS.
     217             :      * \return The number of action labels of this LTS. */
     218       12325 :     labels_size_type num_action_labels() const
     219             :     {
     220       12325 :       assert(m_action_labels.size()>0 && m_action_labels[0]==ACTION_LABEL_T::tau_action());
     221       12325 :       return m_action_labels.size();
     222             :     }
     223             : 
     224             :     /** \brief Gets the initial state number of this LTS.
     225             :      * \return The number of the initial state of this LTS. */
     226        1237 :     states_size_type initial_state() const
     227             :     {
     228        1237 :       return m_init_state;
     229             :     }
     230             : 
     231             :     /** \brief Sets the initial state number of this LTS.
     232             :      * \param[in] state The number of the state that will become the initial
     233             :      * state. */
     234        1662 :     void set_initial_state(const states_size_type state)
     235             :     {
     236        1662 :       assert(state<m_nstates);
     237        1662 :       m_init_state = state;
     238        1662 :     }
     239             : 
     240             :     /** \brief Adds a state to this LTS.
     241             :      *  \details It is not checked whether the added state already exists.
     242             :      * \param[in] label The label of the state. If one state has a state
     243             :      *             label, all states must have state labels. If
     244             :      *             no state label is given, it must be the case that no
     245             :      *             state has a label.
     246             :      * \return The number of the added state label. */
     247        1913 :     states_size_type add_state(const STATE_LABEL_T& label=STATE_LABEL_T())
     248             :     {
     249        1913 :       if (label!=STATE_LABEL_T())
     250             :       {
     251        1830 :         m_state_labels.resize(m_nstates);
     252        1830 :         m_state_labels.push_back(label);
     253             :       }
     254        1913 :       return m_nstates++;
     255             :     }
     256             : 
     257             :     /** \brief Adds an action with a label to this LTS.
     258             :      * \details It is not checked whether this action label already exists.
     259             :      * \param[in] label The label of the label.
     260             :      * \return The number of the added label. */
     261        3847 :     labels_size_type add_action(const ACTION_LABEL_T& label)
     262             :     {
     263        3847 :       if (label==ACTION_LABEL_T::tau_action())
     264             :       {
     265          59 :         return 0;
     266             :       }
     267        3788 :       const labels_size_type label_index=m_action_labels.size();
     268        3788 :       m_action_labels.push_back(label);
     269        3788 :       return label_index;
     270             :     }
     271             : 
     272             :     /** \brief Provide the index of the label that represents tau.
     273             :      *  \return 0, i.e. the index of the label tau.
     274             :      */
     275         863 :     const labels_size_type tau_label_index() const
     276             :     {
     277         863 :       assert(is_tau(0));
     278         863 :       return 0;
     279             :     }
     280             : 
     281             :     /** \brief Sets the label of a state.
     282             :      * \param[in] state The number of the state.
     283             :      * \param[in] label The label that will be assigned to the state. */
     284           0 :     void set_state_label(const states_size_type state, const STATE_LABEL_T& label)
     285             :     {
     286           0 :       assert(state<m_nstates);
     287           0 :       assert(m_nstates==m_state_labels.size());
     288           0 :       m_state_labels[state] = label;
     289           0 :     }
     290             : 
     291             :     /** \brief The action labels in this lts. 
     292             :         \return The action labels of this lts.  **/
     293             :     const std::vector<ACTION_LABEL_T>& action_labels() const
     294             :     {
     295             :       return m_action_labels;
     296             :     } 
     297             : 
     298             :     /** \brief Sets the label of an action.
     299             :      * \param[in] action The number of the action.
     300             :      * \param[in] label The label that will be assigned to the action. */
     301             :      
     302             :     void set_action_label(const labels_size_type action, const ACTION_LABEL_T& label)
     303             :     {
     304             :       assert(action<m_action_labels.size());
     305             :       assert((action==0) == (label==ACTION_LABEL_T::tau_action())); // a tau action is always stored at index 0.
     306             :       m_action_labels[action] = label;
     307             :     }
     308             : 
     309             :     /** \brief Returns the hidden label map that tells for each label what its corresponding
     310             :                hidden label is.
     311             :         \return The hidden action map */
     312         186 :     const std::map<labels_size_type,labels_size_type>& hidden_label_map() const
     313             :     {
     314         186 :       return m_hidden_label_map;
     315             :     }
     316             : 
     317             :     /** \brief Returns the hidden label map that tells for each label what its corresponding
     318             :                hidden label is.
     319             :         \return The hidden action map */
     320         982 :     std::map<labels_size_type,labels_size_type>& hidden_label_map() 
     321             :     {
     322         982 :       return m_hidden_label_map;
     323             :     }
     324             : 
     325             :     /** \brief Sets the hidden label map that tells for each label what its corresponding
     326             :                hidden label is. 
     327             :       * \param[in] m The new hidden label map. */
     328          52 :     void set_hidden_label_map(const std::map<labels_size_type,labels_size_type>& m)
     329             :     {
     330          52 :       m_hidden_label_map=m;
     331          52 :     }
     332             : 
     333             :     /** \brief Gives for an action label its corresponding hidden action label.
     334             :         \param[in] action The index of an action label.
     335             :         \return The index of the corresponding action label in which actions are hidden. */
     336       66132 :     labels_size_type apply_hidden_label_map(const labels_size_type action) const
     337             :     {
     338       66132 :       const typename std::map<labels_size_type,labels_size_type>::const_iterator i=m_hidden_label_map.find(action);
     339       66132 :       if (i==m_hidden_label_map.end())
     340             :       {
     341       66132 :         return action;
     342             :       }
     343           0 :       return i->second;
     344             :     }
     345             : 
     346             :     /** \brief Gets the label of a state.
     347             :      * \param[in] state The number of the state.
     348             :      * \return The label of the state. */
     349        1106 :     STATE_LABEL_T state_label(const states_size_type state) const
     350             :     {
     351        1106 :       assert(state<m_nstates);
     352        1106 :       assert(m_nstates==m_state_labels.size());
     353        1106 :       return m_state_labels[state];
     354             :     }
     355             : 
     356             :     /** \brief Gets the label of a state.
     357             :      * \param[in] state The number of the state.
     358             :      * \return The label of the state. */
     359             :     bool is_probabilistic(const states_size_type state) const
     360             :     {
     361             :       (void)state;  // Suppress an unused variable warning. 
     362             :       assert(state<m_nstates);
     363             :       return false;
     364             :     }
     365             : 
     366             :     /** \brief Gets the label of an action.
     367             :      *  \param[in] action The number of the action.
     368             :      *  \return The label of the action. */
     369        4583 :     ACTION_LABEL_T action_label(const labels_size_type action) const
     370             :     {
     371        4583 :       assert(action < m_action_labels.size());
     372        4583 :       return m_action_labels[action];
     373             :     }
     374             : 
     375             :     /** \brief Clear the transitions of an lts.
     376             :      *  \param[in] n An optional parameter that indicates how
     377             :      *             many transitions are to be expected. This is
     378             :      *             used to set the reserved size of a vector, to
     379             :      *             prevent unnecessary resizing.
     380             :      *  \details This resets the transition vector in an lts, but
     381             :      *          leaves other related items, such as state or
     382             :      *          action labels untouched. */
     383        1603 :     void clear_transitions(const std::size_t n=0)
     384             :     {
     385        1603 :       m_transitions = std::vector<transition>();
     386        1603 :       m_transitions.reserve(n);
     387        1603 :     }
     388             : 
     389             :     /** \brief Clear the action labels of an lts.
     390             :      *  \details This removes the action labels of an lts.
     391             :      *           It also resets the information
     392             :      *           regarding to what actions labels are tau.
     393             :      *           It will not change the number of action labels. */
     394         201 :     void clear_actions()
     395             :     {
     396         201 :       m_action_labels.clear();
     397         201 :       m_action_labels.push_back(ACTION_LABEL_T::tau_action());
     398         201 :       m_hidden_label_map.clear();
     399         201 :     }
     400             : 
     401             :     /** \brief Clear the labels of an lts.
     402             :      *  \details This removes the action labels of an lts.
     403             :      *           It does not change the number of
     404             :      *           state labels */
     405         542 :     void clear_state_labels()
     406             :     {
     407         542 :       m_state_labels.clear();
     408         542 :     }
     409             : 
     410             :     /** \brief Clear the transitions system.
     411             :      *  \details The state values, action values and transitions are
     412             :      *  reset. The number of states, actions and transitions are set to 0. */
     413         201 :     void clear()
     414             :     {
     415         201 :       clear_state_labels();
     416         201 :       clear_actions();
     417         201 :       clear_transitions();
     418         201 :       m_nstates = 0;
     419         201 :     }
     420             : 
     421             :     /** \brief Gets a const reference to the vector of transitions of the current lts.
     422             :      *  \details As this vector can be huge, it is adviced to avoid
     423             :      *           to copy this vector.
     424             :      * \return   A const reference to the vector. */
     425        5177 :     const std::vector<transition>& get_transitions() const
     426             :     {
     427        5177 :       return m_transitions;
     428             :     }
     429             : 
     430             :     /** \brief Gets a reference to the vector of transitions of the current lts.
     431             :      *  \details As this vector can be huge, it is adviced to avoid
     432             :      *           to copy this vector.
     433             :      * \return   A reference to the vector. */
     434        3294 :     std::vector<transition>& get_transitions()
     435             :     {
     436        3294 :       return m_transitions;
     437             :     }
     438             : 
     439             :     /** \brief Add a transition to the lts.
     440             :         \details The transition can be added, even if there are not (yet) valid state and
     441             :                  action labels for it.
     442             :      */
     443       14514 :     void add_transition(const transition& t)
     444             :     {
     445       14514 :       m_transitions.push_back(t);
     446       14514 :     }
     447             : 
     448             :     /** \brief Checks whether an action is a tau action.
     449             :      * \param[in] action The number of the action.
     450             :      * \retval true if the action is a tau action;
     451             :      * \retval false otherwise.  */
     452       29737 :     bool is_tau(labels_size_type action) const
     453             :     {
     454       29737 :       assert(m_action_labels.size()>0 && m_action_labels[0]==ACTION_LABEL_T::tau_action());
     455       29737 :       return (action==0);
     456             :     }
     457             : 
     458             :     /** \brief Sets all actions with a string that occurs in tau_actions to tau.
     459             :      *  \details After hiding actions, it checks whether action labels are
     460             :      *           equal and merges actions with the same labels in the lts.
     461             :      *  \param[in] tau_actions Vector with strings indicating which actions must be
     462             :      *       transformed to tau's */
     463             :     void hide_actions(const std::vector<std::string>& tau_actions)
     464             :     {
     465             :       using namespace std;
     466             : 
     467             :       if (tau_actions.size()==0)
     468             :       {
     469             :         return;
     470             :       }
     471             : 
     472             :       for (labels_size_type i=0; i< num_action_labels(); ++i)
     473             :       {
     474             :         ACTION_LABEL_T a=action_label(i);
     475             :         a.hide_actions(tau_actions);
     476             :         if (a!=action_label(i))  // If hiding has no effect, nothing needs to be done. 
     477             :         {
     478             :           // Otherwise search whether the new label already exists.
     479             :           // Note that this can be inefficient if there are very many different actions.
     480             :           // This is generally not the case.
     481             :           bool found=false;
     482             :           for (labels_size_type j=0; j<num_action_labels(); ++j)
     483             :           {
     484             :             if (a==action_label(j))
     485             :             {
     486             :               m_hidden_label_map[i]=j;
     487             :               found=true;
     488             :               break;
     489             :             }
     490             :           }
     491             :           if (!found)
     492             :           {
     493             :             assert(a!=ACTION_LABEL_T::tau_action());
     494             :             m_hidden_label_map[i]=add_action(a);
     495             :           }
     496             :         }
     497             :       }
     498             :     }
     499             : 
     500             :     /** \brief Checks whether this LTS has state values associated with its states.
     501             :      * \retval true if the LTS has state information;
     502             :      * \retval false otherwise.
     503             :     */
     504        1631 :     bool has_state_info() const
     505             :     {
     506        1631 :       return m_state_labels.size() > 0;
     507             :     }
     508             : 
     509             :     /** \brief Checks whether this LTS has labels associated with its actions, which are numbers.
     510             :      * \retval true if the LTS has values for labels;
     511             :      * \retval false otherwise.
     512             :     */
     513          52 :     bool has_action_info() const
     514             :     {
     515          52 :       return m_action_labels.size() > 1;
     516             :     }
     517             : 
     518             :     /** \brief Sorts the transitions using a sort style.
     519             :      * \param[in] ts The sort style to use.
     520             :      * \note Deprecated */
     521         480 :     inline void sort_transitions(transition_sort_style ts = src_lbl_tgt)
     522             :     {
     523         480 :       switch (ts)
     524             :       {
     525             :         case lbl_tgt_src:
     526             :         { 
     527         266 :           const detail::compare_transitions_lts compare(hidden_label_map());
     528         266 :           sort(m_transitions.begin(),m_transitions.end(),compare);
     529         266 :           break;
     530             :         }
     531             :         case src_lbl_tgt:
     532             :         default:
     533             :         {
     534         214 :           const detail::compare_transitions_slt compare(hidden_label_map());
     535         214 :           sort(m_transitions.begin(),m_transitions.end(),compare);
     536         214 :           break;
     537             :         }
     538             :       }
     539         480 :     }
     540             : 
     541             : };
     542             : 
     543             : }
     544             : }
     545             : 
     546             : #endif // MCRL2_LTS_LTS_H

Generated by: LCOV version 1.12