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             : 
      10             : /** \file probabilistic_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_PROBABILISTIC_LTS_H
      19             : #define MCRL2_LTS_PROBABILISTIC_LTS_H
      20             : 
      21             : #include "mcrl2/lts/lts.h"
      22             : #include "mcrl2/lts/probabilistic_state.h"
      23             : 
      24             : 
      25             : namespace mcrl2
      26             : {
      27             : 
      28             : namespace lts
      29             : {
      30             : 
      31             : /** \brief A class that contains a labelled transition system.
      32             :     \details The state labels and action labels can be any type.
      33             :         Essentially, a labelled transition system consists of a
      34             :         vector of transitions. Each transition is a triple of
      35             :         three numbers <from, label, to>. For these numbers, there
      36             :         can be associated state labels (for 'from' and 'to'), and
      37             :         action labels (for 'label'). But it is also possible, that
      38             :         no state or action labels are provided. For all action labels
      39             :         it is maintained whether this action label is an internal
      40             :         'tau' action. This can be indicated for each action label
      41             :         separately. Finally, the number of states is recalled as
      42             :         a separate variable.
      43             : */
      44             : 
      45             : template < class STATE_LABEL_T, class ACTION_LABEL_T, class PROBABILISTIC_STATE_T, class LTS_BASE >
      46             : class probabilistic_lts: public lts<STATE_LABEL_T, ACTION_LABEL_T, LTS_BASE>
      47             : {
      48             :   public:
      49             : 
      50             :     typedef lts<STATE_LABEL_T, ACTION_LABEL_T, LTS_BASE> super;
      51             : 
      52             :     /** \brief The type of probabilistic labels.
      53             :     */
      54             :     typedef PROBABILISTIC_STATE_T probabilistic_state_t;
      55             : 
      56             :     typedef typename super::state_label_t         state_label_t        ;
      57             :     typedef typename super::action_label_t        action_label_t       ;
      58             :     typedef typename super::base_t                base_t               ;
      59             :     typedef typename super::states_size_type      states_size_type     ;
      60             :     typedef typename super::labels_size_type      labels_size_type     ;
      61             :     typedef typename super::transitions_size_type transitions_size_type;
      62             : 
      63             :     /** \brief An indicator that this is a probabilistic lts. 
      64             :     */
      65             :     static constexpr bool is_probabilistic_lts=true;
      66             : 
      67             :   protected:
      68             : 
      69             :     std::vector<PROBABILISTIC_STATE_T> m_probabilistic_states;
      70             :     PROBABILISTIC_STATE_T m_init_probabilistic_state;
      71             : 
      72             :     /* This function is made protected to prevent its use in a probabilistic transition system */  
      73             :     states_size_type initial_state() const
      74             :     {
      75             :       return super::initial_state();
      76             :     }
      77             : 
      78             :     /* This function is made protected to prevent its use in a probabilistic transition system */  
      79         163 :     void set_initial_state(const states_size_type s)
      80             :     {
      81         163 :       super::set_initial_state(s);
      82         163 :     }
      83             : 
      84             :   public:
      85             : 
      86             :     /** \brief Creates an empty LTS.
      87             :      */
      88         149 :     probabilistic_lts()
      89         149 :     {}
      90             : 
      91             :     /** \brief Standard copy constructor. 
      92             :      * \param[in] other The LTS to copy. */
      93          19 :     probabilistic_lts(const probabilistic_lts& other) = default;
      94             : 
      95             :     /** \brief Standard move constructor. 
      96             :      * \param[in] other The LTS to copy. */
      97             :     probabilistic_lts(probabilistic_lts&& other) = default;
      98             : 
      99             :     /** \brief Standard assignment operator.
     100             :      * \param[in] other The LTS to assign. */
     101             :     probabilistic_lts& operator=(const probabilistic_lts& other) = default;
     102             : 
     103             :     /** \brief Standard assignment move operator.
     104             :      * \param[in] other The LTS to assign. */
     105             :     probabilistic_lts& operator=(probabilistic_lts&& other) = default;
     106             : 
     107             :     /** \brief Standard equality operator.
     108             :      * \param[in] other The LTS to compare this probabilistic lts with. */
     109           7 :     bool operator==(const probabilistic_lts& other) const
     110             :     {
     111           7 :       return super::operator==(static_cast<const super&>(other)) &&
     112          14 :              m_probabilistic_states==other.m_probabilistic_states &&
     113          14 :              m_init_probabilistic_state==other.m_init_probabilistic_state;
     114             :     }
     115             : 
     116             :     /** \brief Swap this lts with the supplied supplied LTS.
     117             :      * \param[in] l The LTS to swap. */
     118             :     void swap(probabilistic_lts& other)
     119             :     {
     120             :       super::swap(other);
     121             :       m_probabilistic_states.swap(other.m_probabilistic_states);
     122             :       m_init_probabilistic_state.swap(other.m_init_probabilistic_state);
     123             :     }
     124             : 
     125             :     /** \brief Gets the initial state number of this LTS.
     126             :       * \return The number of the initial state of this LTS. */
     127         335 :     const PROBABILISTIC_STATE_T& initial_probabilistic_state() const
     128             :     {
     129         335 :       return m_init_probabilistic_state;
     130             :     }
     131             : 
     132             :     /** \brief Sets the probabilistic initial state number of this LTS.
     133             :      * \param[in] state The number of the state that will become the initial
     134             :      * state. */
     135         163 :     void set_initial_probabilistic_state(const PROBABILISTIC_STATE_T& state)
     136             :     {
     137             :       // Prevent that the initial state of the lts, which is not used in a probabilistic state
     138             :       // has an arbitrary value.
     139         163 :       set_initial_state(0);
     140         163 :       m_init_probabilistic_state = state;
     141         163 :     }
     142             : 
     143             : 
     144             :     /** \brief Gets the number of probabilistic states of this LTS.
     145             :      * \return The number of action labels of this LTS. */
     146         311 :     labels_size_type num_probabilistic_states() const
     147             :     {
     148         311 :       return m_probabilistic_states.size();
     149             :     }
     150             : 
     151             :     /** \brief Adds a probabilistic state to this LTS.
     152             :      * \details It is not checked whether this probabilistic state already exists.
     153             :      * \param[in] s The probabilistic state.
     154             :      * \return The index of the added probabilistic. */
     155        1491 :     states_size_type add_probabilistic_state(const PROBABILISTIC_STATE_T& s)
     156             :     {
     157        1491 :       const states_size_type label_index=m_probabilistic_states.size();
     158        1491 :       m_probabilistic_states.push_back(s);
     159        1491 :       return label_index;
     160             :     }
     161             : 
     162             :     /** \brief Adds a probabilistic state to this LTS and resets the state to empty.
     163             :      * \details This is more efficient than using add_probabilistic state, as this variant
     164             :      *          does not copy the probabilistic state. It is not checked whether this probabilistic state already exists.
     165             :      * \param[in] s The probabilistic state.
     166             :      * \return The index of the added probabilistic state. */
     167         129 :     states_size_type add_and_reset_probabilistic_state(PROBABILISTIC_STATE_T& s)
     168             :     {
     169         129 :       const states_size_type label_index=m_probabilistic_states.size();
     170         129 :       m_probabilistic_states.emplace_back();
     171         129 :       m_probabilistic_states.back().swap(s);
     172         129 :       return label_index;
     173             :     }
     174             : 
     175             :     /** \brief Sets the probabilistic label corresponding to some index.
     176             :      * \param[in] index The index of the state.
     177             :      * \param[in] s The new probabilistic state belonging to this index. */
     178             :     void set_probabilistic_state(const states_size_type index, const PROBABILISTIC_STATE_T& s)
     179             :     {
     180             :       assert(index<m_probabilistic_states.size());
     181             :       m_probabilistic_states[index] = s;
     182             :     }
     183             : 
     184             :     /** \brief Gets the probabilistic label of an index.
     185             :      *  \param[in] index The index of an action.
     186             :      *  \return The probabilistic state belonging to the index. */
     187        3904 :     const PROBABILISTIC_STATE_T& probabilistic_state(const states_size_type index) const
     188             :     {
     189        3904 :       assert(index < m_probabilistic_states.size());
     190        3904 :       return m_probabilistic_states[index];
     191             :     }
     192             : 
     193             :     /** \brief Clear the probabilistic states in this probabilistic transitions system.
     194             :     */
     195          18 :     void clear_probabilistic_states()
     196             :     {
     197          18 :       m_probabilistic_states.clear();
     198          18 :     }
     199             : 
     200             :     /** \brief Clear the transitions system.
     201             :      *  \details The state values, action values and transitions are
     202             :      *  reset. The number of states, actions and transitions are set to 0. */
     203          67 :     void clear()
     204             :     {
     205          67 :       super::clear();
     206          67 :       m_probabilistic_states.clear();
     207          67 :       m_probabilistic_states.shrink_to_fit();
     208          67 :     }
     209             : };
     210             : 
     211             : }
     212             : }
     213             : 
     214             : #endif // MCRL2_LTS_LTS_H