LCOV - code coverage report
Current view: top level - lts/include/mcrl2/lts - probabilistic_state.h (source / functions) Hit Total Coverage
Test: mcrl2_coverage.info.cleaned Lines: 56 56 100.0 %
Date: 2019-06-20 00:49:45 Functions: 30 30 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 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 <vector>
      22             : #include <sstream>
      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             : */
      39             : 
      40             : template < class STATE, class PROBABILITY >
      41       14884 : class probabilistic_state
      42             : {
      43             :   public:
      44             : 
      45             :     friend std::hash<probabilistic_state>;
      46             : 
      47             :     typedef typename lps::state_probability_pair< STATE, PROBABILITY > state_probability_pair;
      48             :     typedef STATE state_t;
      49             :     typedef PROBABILITY probability_t;
      50             :     typedef typename std::vector<state_probability_pair>::iterator iterator;
      51             :     typedef typename std::vector<state_probability_pair>::const_iterator const_iterator;
      52             : 
      53             :   protected:
      54             : 
      55             :     std::vector<state_probability_pair> m_probabilistic_state; // A vector with states and their associated probability.
      56             :                                                                // The sum of all probabilities in the vector must be one.
      57             : 
      58             :   public:
      59             : 
      60             :     /** \brief Default constructor
      61             :      **/
      62        1923 :     probabilistic_state()
      63        1923 :     {
      64        1923 :       m_probabilistic_state.reserve(1);
      65        1923 :     }
      66             : 
      67             :     /** \brief Constructor of a probabilistic state from a non probabilistic state.
      68             :      *  \param[in] s A state.
      69             :      *  \return The generated probabilistic state.
      70             :      **/
      71        2462 :     explicit probabilistic_state(const STATE& s)
      72        2462 :       : m_probabilistic_state(1,state_probability_pair(s,PROBABILITY::one()))
      73             :     {
      74        2462 :       shrink_to_fit();
      75        2462 :     }
      76             : 
      77             :     /** \brief Copy constructor
      78             :      **/
      79        8438 :     probabilistic_state(const probabilistic_state& s)
      80        8438 :       : m_probabilistic_state(s.m_probabilistic_state)
      81             :     {
      82        8438 :       shrink_to_fit();
      83        8438 :     }
      84             : 
      85             :     /** \brief Creates a probabilistic state on the basis of state_probability_pairs.
      86             :      * \param[in] begin Iterator to the first state_probability_pair.
      87             :      * \param[in] end Iterator to the last state_probability_pair.
      88             :      * \return Resulting probabilistic state.  **/
      89             :     template <class STATE_PROBABILITY_PAIR_ITERATOR>
      90         918 :     probabilistic_state(const STATE_PROBABILITY_PAIR_ITERATOR begin, const STATE_PROBABILITY_PAIR_ITERATOR end)
      91         918 :       : m_probabilistic_state(begin,end)
      92             :     {
      93         918 :       assert(begin!=end);
      94         918 :       shrink_to_fit();
      95         918 :     }
      96             : 
      97             :     /** \brief Standard equality operator.
      98             :      *  \result Returns true iff the probabilistic states are equal.
      99             :      */
     100         188 :     bool operator==(const probabilistic_state& other) const
     101             :     {
     102         188 :       return m_probabilistic_state==other.m_probabilistic_state;
     103             :     }
     104             : 
     105             :     /** \brief Swap this probabilistic state.
     106             :      * \param[in] s A probabilistic state. */
     107          91 :     void swap(probabilistic_state& s)
     108             :     {
     109          91 :       m_probabilistic_state.swap(s.m_probabilistic_state);
     110          91 :     };
     111             : 
     112             :     /** \brief Set this probabilistic state to a single state with probability one.
     113             :      * \details It is assumed that the given state probability pair does not have
     114             :                any element.
     115             :      * \param[in] s The state. */
     116         538 :     void set(const STATE& s)
     117             :     {
     118         538 :       assert(size()==0);
     119         538 :       m_probabilistic_state.emplace_back(s, PROBABILITY::one());
     120         538 :       shrink_to_fit();
     121         538 :     };
     122             : 
     123             :     /** \brief Add a state with a probability to the probabilistic state
     124             :      * \param[in] s The state to be added.
     125             :      * \param[in] p The probability of this state.
     126             :      **/
     127        1220 :     void add(const STATE& s, const PROBABILITY& p)
     128             :     {
     129        1220 :       m_probabilistic_state.emplace_back(s,p);
     130        1220 :     }
     131             : 
     132             :     /** \brief If a probabilistic state is ready, shrinking it to minimal size might be useful
     133             :      *         to reduce its memory usage. A requirement is that the sum of the probabilities must
     134             :      *         be one.
     135             :      */
     136       12356 :     void shrink_to_fit()
     137             :     {
     138       12356 :       m_probabilistic_state.shrink_to_fit();
     139             : #ifndef NDEBUG
     140       24712 :       PROBABILITY sum=PROBABILITY::zero();
     141       27071 :       for(const state_probability_pair& p: m_probabilistic_state)
     142             :       {
     143       14715 :         assert(p.probability()>PROBABILITY::zero());
     144       14715 :         assert(p.probability()<=PROBABILITY::one());
     145       14715 :         sum=sum+p.probability();
     146             :       }
     147             :       // SVC studio copies empty probabilistic states.
     148       12356 :       assert(m_probabilistic_state.size()==0 || sum==PROBABILITY::one());
     149             : #endif
     150       12356 :     }
     151             : 
     152             :     /** \brief Gets the number of probabilistic labels of this LTS.
     153             :      * \return The number of action labels of this LTS. */
     154        5756 :     std::size_t size() const
     155             :     {
     156        5756 :       return m_probabilistic_state.size();
     157             :     }
     158             : 
     159             :     /** \brief Makes the probabilistic state empty.
     160             :      */
     161         299 :     void clear()
     162             :     {
     163         299 :       m_probabilistic_state.clear();
     164         299 :     }
     165             : 
     166             :     /** \brief Gets an iterator over pairs of state and probability.
     167             :      *  \return The iterator pointing at the first state probability pair. */
     168        4556 :     const_iterator begin() const
     169             :     {
     170        4556 :       return m_probabilistic_state.cbegin();
     171             :     }
     172             : 
     173             :     /** \brief Gets the end iterator over pairs of state and probability.
     174             :      *  \return The iterator pointing beyond the last state probability pair in a probabilistic state. */
     175        2146 :     const_iterator end() const
     176             :     {
     177        2146 :       return m_probabilistic_state.cend();
     178             :     }
     179             : 
     180             :     /** \brief Gets an iterator over pairs of state and probability.
     181             :      *  \return The iterator pointing at the first state probability pair. */
     182        2276 :     iterator begin()
     183             :     {
     184        2276 :       return m_probabilistic_state.begin();
     185             :     }
     186             : 
     187             :     /** \brief Gets the end iterator over pairs of state and probability.
     188             :      *  \return The iterator pointing beyond the last state probability pair in a probabilistic state. */
     189        1688 :     iterator end()
     190             :     {
     191        1688 :       return m_probabilistic_state.end();
     192             :     }
     193             : 
     194             : };
     195             : 
     196             : 
     197             : /* \brief A pretty print operator on action labels, returning it as a string.
     198             :  * */
     199             : template < class STATE, class PROBABILITY >
     200             : inline std::string pp(const probabilistic_state<STATE, PROBABILITY>& l)
     201             : {
     202             :   std::stringstream str;
     203             :   bool first=true;
     204             :   for(const lps::state_probability_pair<STATE, PROBABILITY>& p: l)
     205             :   {
     206             :     if (first)
     207             :     {
     208             :       first=false;
     209             :     }
     210             :     else
     211             :     {
     212             :       str << ", ";
     213             :     }
     214             :     str << "[" << p.state() << ", " << p.probability() << "]";
     215             :   }
     216             : 
     217             :   return str.str();
     218             : }
     219             : 
     220             : /** \brief Pretty print to an outstream.
     221             :  */
     222             : template < class STATE, class PROBABILITY >
     223             : inline
     224             : std::ostream& operator<<(std::ostream& out, const probabilistic_state<STATE, PROBABILITY>& l)
     225             : {
     226             :   return out << pp(l);
     227             : }
     228             : 
     229             : 
     230             : 
     231             : } // namespace lts
     232             : } // namespace mcrl2
     233             : 
     234             : namespace std
     235             : {
     236             : 
     237             : /// \brief specialization of the standard std::hash function.
     238             : template < class STATE, class PROBABILITY >
     239          14 : struct hash< mcrl2::lts::probabilistic_state<STATE, PROBABILITY> >
     240             : {
     241         290 :   std::size_t operator()(const mcrl2::lts::probabilistic_state<STATE, PROBABILITY>& p) const
     242             :   {
     243             :     hash<vector<typename mcrl2::lps::state_probability_pair< STATE, PROBABILITY > > > hasher;
     244         290 :     return hasher(p.m_probabilistic_state);
     245             :   }
     246             : };
     247             : 
     248             : } // namespace std
     249             : 
     250             : #endif // MCRL2_LTS_PROBABILISTIC_STATE_H

Generated by: LCOV version 1.12