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 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 Jan Friso Groote
      16             :  */
      17             : 
      18             : #ifndef MCRL2_LTS_PROBABILISTIC_STATE_H
      19             : #define MCRL2_LTS_PROBABILISTIC_STATE_H
      20             : 
      21             : #include <sstream>
      22             : #include "mcrl2/utilities/exception.h"
      23             : #include "mcrl2/lps/state_probability_pair.h"
      24             : 
      25             : 
      26             : namespace mcrl2
      27             : {
      28             : 
      29             : namespace lts
      30             : {
      31             : 
      32             : /** \brief A class that contains a probabilistic state.
      33             :     \details A probabilistic state is essentially a sequence
      34             :              of pairs of a state and a probability. The probability
      35             :              indicates the likelyhood with which that particular
      36             :              state can be reached. The sum of all probabilities
      37             :              in a probabilistic state is one. 
      38             :              Internally, it is either stored as single state, 
      39             :              or as a vector of states. 
      40             :              When using a probabilistic state, a user should
      41             :              be aware which of the two internal representations are used.
      42             :              After calling "construct_internal_vector_representation"
      43             :              it is guaranteed that the state is stored as a vector,
      44             :              and iterators over begin/end, and cbegin/cend can be used.
      45             : */
      46             : 
      47             : template < class STATE, class PROBABILITY >
      48             : class probabilistic_state
      49             : {
      50             :   public:
      51             : 
      52             :     friend std::hash<probabilistic_state>;
      53             : 
      54             :     typedef typename lps::state_probability_pair< STATE, PROBABILITY > state_probability_pair;
      55             :     typedef STATE state_t;
      56             :     typedef PROBABILITY probability_t;
      57             :     typedef typename std::vector<state_probability_pair>::iterator iterator;
      58             :     typedef typename std::vector<state_probability_pair>::const_iterator const_iterator;
      59             :     typedef typename std::vector<state_probability_pair>::reverse_iterator reverse_iterator;
      60             :     typedef typename std::vector<state_probability_pair>::const_reverse_iterator const_reverse_iterator;
      61             : 
      62             :   protected:
      63             : 
      64             :     STATE m_single_state;                                      // If there is only one state, this is stored as
      65             :                                                                // a base state with implicit probability 1. 
      66             :     std::vector<state_probability_pair> m_probabilistic_state; // A vector with states and their associated probability.
      67             :                                                                // The sum of all probabilities in the vector must be one.
      68             :                                              
      69             :   public:
      70             : 
      71             :     /** \brief Default constructor
      72             :      **/
      73        2160 :     probabilistic_state()
      74        2160 :       : m_single_state(STATE(-1))
      75             :     {
      76        2160 :     }
      77             : 
      78             :     /** \brief Constructor of a probabilistic state from a non probabilistic state.
      79             :      *  \param[in] s A state.
      80             :      *  \return The generated probabilistic state.
      81             :      **/
      82        1337 :     explicit probabilistic_state(const STATE& s)
      83        1337 :       : m_single_state(s)
      84             :     {
      85        1337 :     }
      86             : 
      87             :     /** \brief Copy constructor **/
      88        5550 :     probabilistic_state(const probabilistic_state& other)
      89        5550 :       : m_single_state(other.m_single_state),
      90        5550 :         m_probabilistic_state(other.m_probabilistic_state)
      91             :     {
      92        5550 :       shrink_to_fit();
      93        5550 :     }
      94             : 
      95             :     /** \brief Copy assignment constructor **/
      96        1104 :     probabilistic_state& operator=(const probabilistic_state& other)
      97             :     {
      98        1104 :       m_single_state= other.m_single_state;
      99        1104 :       m_probabilistic_state = other.m_probabilistic_state;
     100        1104 :       shrink_to_fit();
     101        1104 :       return *this;
     102             :     }
     103             : 
     104             :     /** \brief Creates a probabilistic state on the basis of state_probability_pairs.
     105             :      * \param[in] begin Iterator to the first state_probability_pair.
     106             :      * \param[in] end Iterator to the last state_probability_pair.
     107             :      * \return Resulting probabilistic state.  **/
     108             :     template <class STATE_PROBABILITY_PAIR_ITERATOR>
     109         112 :     probabilistic_state(const STATE_PROBABILITY_PAIR_ITERATOR begin, const STATE_PROBABILITY_PAIR_ITERATOR end)
     110         112 :       : m_single_state(STATE(-1)),
     111         112 :         m_probabilistic_state(begin,end)
     112             :     {
     113         112 :       assert(begin!=end);
     114         112 :       shrink_to_fit();
     115         112 :     }
     116             : 
     117             :     /** \brief Standard equality operator.
     118             :      *  \result Returns true iff the probabilistic states are equal.
     119             :      */
     120         500 :     bool operator==(const probabilistic_state& other) const
     121             :     {
     122         500 :       if (m_single_state==STATE(-1))
     123             :       {
     124         468 :         if (other.m_single_state==STATE(-1))
     125             :         {
     126         468 :           assert(m_probabilistic_state.size()>0);
     127         468 :           assert(other.m_probabilistic_state.size()>0);
     128         468 :           return m_probabilistic_state==other.m_probabilistic_state;
     129             :         }
     130             :         else 
     131             :         {
     132           0 :           return m_probabilistic_state.size()==1 &&
     133           0 :                  other.m_single_state==m_probabilistic_state.front().state();
     134             :         }
     135             :       }
     136             :       else
     137             :       {
     138          32 :         if (other.m_single_state==STATE(-1))
     139             :         {
     140           4 :           return other.m_probabilistic_state.size()==1 &&
     141           4 :                  m_single_state==other.m_probabilistic_state.front().state();
     142             :         }
     143             :         else
     144             :         {
     145          30 :           assert(m_probabilistic_state.size()==0);
     146          30 :           assert(other.m_probabilistic_state.size()==0);
     147          30 :           return m_single_state==other.m_single_state;
     148             :         }
     149             :       }
     150             :     }
     151             : 
     152             :     /** \brief Standard equality operator.
     153             :      *  \result Returns true iff the probabilistic states are equal.
     154             :      */
     155             :     bool operator!=(const probabilistic_state& other) const
     156             :     {
     157             :       return !(operator==(other)); 
     158             :     }
     159             : 
     160             :     /** \brief Swap this probabilistic state.
     161             :      * \param[in] s A probabilistic state. */
     162         129 :     void swap(probabilistic_state& other)
     163             :     {
     164         129 :       std::swap(m_single_state,other.m_single_state);
     165         129 :       m_probabilistic_state.swap(other.m_probabilistic_state);
     166         129 :     }
     167             : 
     168             :     /** \brief Guarantee that this probabilistic state is internally stored as
     169             :      **        a vector, such that begin/end, cbegin/cend and size are properly 
     170             :      **        defined. */
     171             :     void construct_internal_vector_representation()
     172             :     {
     173             :       if (m_single_state!=STATE(-1))
     174             :       {
     175             :         assert(m_probabilistic_state.size()==0);
     176             :         m_probabilistic_state.emplace_back(m_single_state,PROBABILITY::one());
     177             :         m_single_state=STATE(-1);
     178             :       }
     179             :     }
     180             : 
     181             :     /** \brief Set this probabilistic state to a single state with probability one.
     182             :      * \details It is assumed that the given state probability pair does not have
     183             :                any element.
     184             :      * \param[in] s The state. */
     185         715 :     void set(const STATE& s)
     186             :     {
     187         715 :       assert(m_probabilistic_state.size()==0);
     188         715 :       m_single_state=s; 
     189         715 :     }
     190             : 
     191             :     /** \brief Get a probabilistic state if is is simple, i.e., consists of a single state. 
     192             :      * \details It is assumed that the given state probability pair does not have
     193             :                any element.
     194             :      * \param[in] s The state. */
     195        3360 :     STATE get() const
     196             :     {
     197        3360 :       if (m_probabilistic_state.size()>1)
     198             :       {
     199           0 :         throw mcrl2::runtime_error("Probabilistic state is not simple\n");
     200             :       }
     201        3360 :       if (m_probabilistic_state.size()==1)
     202             :       {
     203           0 :         assert(m_probabilistic_state.front().state()!=STATE(-1));
     204           0 :         return m_probabilistic_state.front().state();
     205             :       }
     206        3360 :       assert(m_single_state!=STATE(-1));
     207        3360 :       return m_single_state; 
     208             :     }
     209             : 
     210             :     /** \brief Add a state with a probability to the probabilistic state
     211             :      * \param[in] s The state to be added.
     212             :      * \param[in] p The probability of this state.
     213             :      **/
     214        1709 :     void add(const STATE& s, const PROBABILITY& p)
     215             :     {
     216        1709 :       m_probabilistic_state.emplace_back(s,p);
     217        1709 :     }
     218             : 
     219             :     /** \brief If a probabilistic state is ready, shrinking it to minimal size might be useful
     220             :      *         to reduce its memory usage. A requirement is that the sum of the probabilities must
     221             :      *         be one.
     222             :      */
     223        6822 :     void shrink_to_fit()
     224             :     {
     225        6822 :       m_probabilistic_state.shrink_to_fit();
     226        6822 :       assert((m_probabilistic_state.size()>1 && m_single_state==std::size_t(-1)) ||
     227             :              (m_probabilistic_state.size()==0 && m_single_state!=std::size_t(-1)));
     228             : #ifndef NDEBUG
     229        6822 :       PROBABILITY sum=PROBABILITY::zero();
     230       12872 :       for(const state_probability_pair& p: m_probabilistic_state)
     231             :       {
     232        6050 :         assert(p.probability()>PROBABILITY::zero());
     233        6050 :         assert(p.probability()<=PROBABILITY::one());
     234        6050 :         sum=sum+p.probability();
     235             :       }
     236             :       // SVC studio copies empty probabilistic states.
     237        6822 :       assert(m_probabilistic_state.size()==0 || sum==PROBABILITY::one());
     238             : #endif
     239        6822 :     }
     240             : 
     241             :     /** \brief Gets the number of probabilistic states in the vector representation of this state.
     242             :      **        If the state is stored as a simple number this size returns 0. So, 0 means that there
     243             :      **        is one state, which should then be obtained using get(). If the size is larger than 0
     244             :      **        the state is stored in a vector, and it must be accessed throught the iterators begin()
     245             :      **        and n. 
     246             :      * \return The number of probabilistic states, where 0 means there is one simple state. */
     247        6693 :     std::size_t size() const
     248             :     {
     249        6693 :       return m_probabilistic_state.size();
     250             :     }
     251             : 
     252             :     /** \brief Makes the probabilistic state empty.
     253             :      */
     254         453 :     void clear()
     255             :     {
     256         453 :       m_single_state=STATE(-1);
     257         453 :       m_probabilistic_state.clear();
     258         453 :     }
     259             : 
     260             :     /** \brief Gets an iterator over pairs of state and probability. This can only be used when the state is stored 
     261             :      **        internally as a vector.  
     262             :      *  \return The iterator pointing at the first state probability pair. */
     263        1388 :     const_iterator begin() const
     264             :     {
     265        1388 :       return m_probabilistic_state.begin();
     266             :     }
     267             : 
     268             :     /** \brief Gets the end iterator over pairs of state and probability.
     269             :      ** \return The iterator pointing beyond the last state probability pair in a probabilistic state. */
     270        1384 :     const_iterator end() const
     271             :     {
     272        1384 :       return m_probabilistic_state.end();
     273             :     }
     274             : 
     275             :     /** \brief Gets an iterator over pairs of state and probability. This can only be used if the state is internally stored as a vector. 
     276             :      ** \return The iterator pointing at the first state probability pair. */
     277         992 :     iterator begin()
     278             :     {
     279         992 :       return m_probabilistic_state.begin();
     280             :     }
     281             : 
     282             :     /** \brief Gets the end iterator over pairs of state and probability.
     283             :      ** \return The iterator pointing beyond the last state probability pair in a probabilistic state. */
     284         992 :     iterator end()
     285             :     {
     286         992 :       return m_probabilistic_state.end();
     287             :     }
     288             : 
     289             :     /** \brief Gets a reverse iterator over pairs of state and probability. This can only be used when the state is stored 
     290             :      **        internally as a vector.  
     291             :      *  \return The iterator pointing at the last state probability pair. */
     292             :     const_reverse_iterator rbegin() const
     293             :     {
     294             :       return m_probabilistic_state.rbegin();
     295             :     }
     296             : 
     297             :     /** \brief Gets the reverse end iterator over pairs of state and probability.
     298             :      ** \return The iterator pointing before the first state probability pair in a probabilistic state. */
     299             :     const_reverse_iterator rend() const
     300             :     {
     301             :       return m_probabilistic_state.rend();
     302             :     }
     303             : 
     304             :     /** \brief Gets a reverse iterator over pairs of state and probability. This can only be used if the state is internally stored as a vector. 
     305             :      ** \return The iterator pointing at the last state probability pair. */
     306             :     reverse_iterator rbegin()
     307             :     {
     308             :       return m_probabilistic_state.rbegin();
     309             :     }
     310             : 
     311             :     /** \brief Gets the reverse end iterator over pairs of state and probability.
     312             :      ** \return The iterator pointing before the first state probability pair in a probabilistic state. */
     313             :     reverse_iterator rend()
     314             :     {
     315             :       return m_probabilistic_state.rend();
     316             :     }
     317             : };
     318             : 
     319             : 
     320             : /* \brief A pretty print operator on action labels, returning it as a string.
     321             :  * */
     322             : template < class STATE, class PROBABILITY >
     323             : inline std::string pp(const probabilistic_state<STATE, PROBABILITY>& l)
     324             : {
     325             :   std::stringstream str;
     326             :   if (l.size()<=1)
     327             :   {
     328             :     str << "[ " << l.get() << ": 1.0 ]";
     329             :   }
     330             :   else
     331             :   {
     332             :     str << "[ ";
     333             :     bool first=true;
     334             :     for(const lps::state_probability_pair<STATE, PROBABILITY>& p: l)
     335             :     {
     336             :       if (first)
     337             :       {
     338             :         first=false;
     339             :       }
     340             :       else
     341             :       {
     342             :         str << "; ";
     343             :       }
     344             :       str << p.state() << ": " << p.probability();
     345             :     }
     346             :     str << " ]";
     347             :   }
     348             : 
     349             :   return str.str();
     350             : }
     351             : 
     352             : /** \brief Pretty print to an outstream.
     353             :  */
     354             : template < class STATE, class PROBABILITY >
     355             : inline
     356             : std::ostream& operator<<(std::ostream& out, const probabilistic_state<STATE, PROBABILITY>& l)
     357             : {
     358             :   return out << pp(l);
     359             : }
     360             : 
     361             : 
     362             : 
     363             : } // namespace lts
     364             : } // namespace mcrl2
     365             : 
     366             : namespace std
     367             : {
     368             : 
     369             : /// \brief Specialization of the standard std::hash function.
     370             : /// \details It is essential that this hash function yields the same has for a singular
     371             : ///          state in a distribution, stored as a number with implicit probability 1, or
     372             : ///          as a vector of length 1. 
     373             : template < class STATE, class PROBABILITY >
     374             : struct hash< mcrl2::lts::probabilistic_state<STATE, PROBABILITY> >
     375             : {
     376         533 :   std::size_t operator()(const mcrl2::lts::probabilistic_state<STATE, PROBABILITY>& p) const
     377             :   {
     378         533 :     if (p.m_single_state!=STATE(-1))
     379             :     {
     380          30 :       assert(p.m_probabilistic_state.size()==0);
     381             :       hash<STATE> state_hasher;
     382             :       hash<PROBABILITY> probability_hasher;
     383          36 :       return mcrl2::utilities::detail::hash_combine(0, 
     384          30 :                    mcrl2::utilities::detail::hash_combine(state_hasher(p.m_single_state), 
     385          57 :                                                           probability_hasher(PROBABILITY::one())));
     386             :     }
     387             :     hash<vector<typename mcrl2::lps::state_probability_pair< STATE, PROBABILITY > > > hasher;
     388         503 :     return hasher(p.m_probabilistic_state);
     389             :   }
     390             : };
     391             : 
     392             : } // namespace std
     393             : 
     394             : #endif // MCRL2_LTS_PROBABILISTIC_STATE_H