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 a class with a state/probability pair. 
      13             :  * \details A state probability pair consists of a state and a probability.
      14             :  *          The probability should be larger than 0 and smaller or equal to 1.
      15             :  * \author Jan Friso Groote
      16             :  */
      17             : 
      18             : 
      19             : #ifndef MCRL2_LPS_STATE_PROBABILITY_PAIR_H
      20             : #define MCRL2_LPS_STATE_PROBABILITY_PAIR_H
      21             : 
      22             : #include <cassert>
      23             : #include <iostream>
      24             : #include "mcrl2/utilities/hash_utility.h"
      25             : #include "mcrl2/atermpp/aterm_appl.h"
      26             : 
      27             : namespace mcrl2
      28             : {
      29             : namespace lps
      30             : {
      31             : 
      32             : template < class STATE, class PROBABILITY >
      33             : class state_probability_pair
      34             : {
      35             :   protected:
      36             :     // A state 
      37             :     STATE m_state;
      38             :     // A data expression of sort Real that indicates the probability of this state
      39             :     PROBABILITY m_probability;
      40             :   public:
      41             : 
      42             :     /// \brief constructor.
      43             :     /// \param state The state.
      44             :     /// \param probability The probability of the occurrence of this state. 
      45        1933 :     state_probability_pair(const STATE& state, const PROBABILITY& probability)
      46        1933 :      : m_state(state), 
      47        1933 :        m_probability(probability)
      48             :     {
      49        1933 :       assert(probability!=PROBABILITY::zero());
      50        1933 :     } 
      51             : 
      52             :     /// \brief Copy constructor;
      53             :     /// \param p The state probability pair to be copied.
      54        5912 :     state_probability_pair(const state_probability_pair& p)=default; 
      55         815 :     state_probability_pair(state_probability_pair&& p)=default; 
      56             : 
      57             :     /// \brief Standard assignment.
      58             :     /// \param p The state probability pair to be assigned.
      59             :     /// \return A reference to the assigned object.
      60          26 :     state_probability_pair& operator=(const state_probability_pair& p)=default; 
      61             :     state_probability_pair& operator=(state_probability_pair&& p)=default; 
      62             : 
      63             :     /** \brief Standard equality operator.
      64             :      *  \result Returns true iff the probabilistic states are equal.
      65             :      */
      66        1301 :     bool operator==(const state_probability_pair& other) const
      67             :     {
      68             :       if constexpr(std::is_convertible<PROBABILITY,atermpp::aterm_appl>::value)
      69             :       {
      70             :         // The probabilities are compared as aterms, and not based on their value, as comparing
      71             :         // probabilities using their value is expensive as it requires an application of the rewriter. 
      72         134 :         return m_state==other.m_state && 
      73         134 :                static_cast<atermpp::aterm_appl>(m_probability)==static_cast<atermpp::aterm_appl>(other.m_probability);
      74             :       }
      75             :       else
      76             :       {
      77             :         static_assert(!std::is_convertible<PROBABILITY,atermpp::aterm>::value);
      78        1223 :         return m_state==other.m_state && m_probability==other.m_probability;
      79             :       }
      80             :     }
      81             : 
      82             :     /// \brief Get the state from a state probability pair.
      83        6815 :     const STATE& state() const
      84             :     {
      85        6815 :       return m_state;
      86             :     }
      87             : 
      88             :     /// \brief Get the state in a state probability pair.
      89        1192 :     STATE& state() 
      90             :     {
      91        1192 :       return m_state;
      92             :     }
      93             : 
      94             :     /// \brief get the probability from a state proability pair.
      95       21049 :     const PROBABILITY& probability() const
      96             :     {
      97       21049 :       return m_probability;
      98             :     }
      99             : 
     100             :     /// \brief Set the probability in a state probability pair.
     101             :     PROBABILITY& probability() 
     102             :     {
     103             :       return m_probability;
     104             :     }
     105             : 
     106             : };
     107             : 
     108             : } // namespace lps
     109             : } // namespace mcrl2 
     110             : 
     111             : namespace std
     112             : {
     113             : 
     114             : template < class STATE, class PROBABILITY >
     115             : struct hash<mcrl2::lps::state_probability_pair<STATE,PROBABILITY> >
     116             : {
     117        1625 :   std::size_t operator()(const mcrl2::lps::state_probability_pair<STATE,PROBABILITY>& p) const
     118             :   {
     119             :     hash<STATE> state_hasher;
     120             :     hash<PROBABILITY> probability_hasher;
     121        3113 :     return mcrl2::utilities::detail::hash_combine(state_hasher(p.state()), probability_hasher(p.probability()));
     122             :   }
     123             : };
     124             : 
     125             : } // end namespace std
     126             : 
     127             : #endif // MCRL2_LPS_STATE_PROBABILITY_PAIR_H