probabilistic_state.h

Go to the documentation of this file.

// Author(s): Jan Friso Groote
// Copyright: see the accompanying file COPYING or copy at
// https://github.com/mCRL2org/mCRL2/blob/master/COPYING
//
// Distributed under the Boost Software License, Version 1.0.
// (See accompanying file LICENSE_1_0.txt or copy at
// http://www.boost.org/LICENSE_1_0.txt)
//
 
#ifndef MCRL2_LTS_PROBABILISTIC_STATE_H
#define MCRL2_LTS_PROBABILISTIC_STATE_H
 
#include <sstream>
#include "mcrl2/utilities/exception.h"
#include "mcrl2/lps/state_probability_pair.h"
 
 
namespace mcrl2
{
 
namespace lts
{
 
template < class STATE, class PROBABILITY >
class probabilistic_state
{
  public:
 
    friend std::hash<probabilistic_state>;
 
    typedef typename lps::state_probability_pair< STATE, PROBABILITY > state_probability_pair;
    typedef STATE state_t;
    typedef PROBABILITY probability_t;
    typedef typename std::vector<state_probability_pair>::iterator iterator;
    typedef typename std::vector<state_probability_pair>::const_iterator const_iterator;
    typedef typename std::vector<state_probability_pair>::reverse_iterator reverse_iterator;
    typedef typename std::vector<state_probability_pair>::const_reverse_iterator const_reverse_iterator;
 
  protected:
 
    STATE m_single_state;                                      // If there is only one state, this is stored as
                                                               // a base state with implicit probability 1. 
    std::vector<state_probability_pair> m_probabilistic_state; // A vector with states and their associated probability.
                                                               // The sum of all probabilities in the vector must be one.
                                             
  public:
 
    probabilistic_state()
      : m_single_state(STATE(-1))
    {
    }
 
    explicit probabilistic_state(const STATE& s)
      : m_single_state(s)
    {
    }
 
    probabilistic_state(const probabilistic_state& other)
      : m_single_state(other.m_single_state),
        m_probabilistic_state(other.m_probabilistic_state)
    {
      shrink_to_fit();
    }
 
    probabilistic_state& operator=(const probabilistic_state& other)
    {
      m_single_state= other.m_single_state;
      m_probabilistic_state = other.m_probabilistic_state;
      shrink_to_fit();
      return *this;
    }
 
    template <class STATE_PROBABILITY_PAIR_ITERATOR>
    probabilistic_state(const STATE_PROBABILITY_PAIR_ITERATOR begin, const STATE_PROBABILITY_PAIR_ITERATOR end)
      : m_single_state(STATE(-1)),
        m_probabilistic_state(begin,end)
    {
      assert(begin!=end);
      shrink_to_fit();
    }
 
    bool operator==(const probabilistic_state& other) const
    {
      if (m_single_state==STATE(-1))
      {
        if (other.m_single_state==STATE(-1))
        {
          assert(m_probabilistic_state.size()>0);
          assert(other.m_probabilistic_state.size()>0);
          return m_probabilistic_state==other.m_probabilistic_state;
        }
        else 
        {
          return m_probabilistic_state.size()==1 &&
                 other.m_single_state==m_probabilistic_state.front().state();
        }
      }
      else
      {
        if (other.m_single_state==STATE(-1))
        {
          return other.m_probabilistic_state.size()==1 &&
                 m_single_state==other.m_probabilistic_state.front().state();
        }
        else
        {
          assert(m_probabilistic_state.size()==0);
          assert(other.m_probabilistic_state.size()==0);
          return m_single_state==other.m_single_state;
        }
      }
    }
 
    bool operator!=(const probabilistic_state& other) const
    {
      return !(operator==(other)); 
    }
 
    void swap(probabilistic_state& other)
    {
      std::swap(m_single_state,other.m_single_state);
      m_probabilistic_state.swap(other.m_probabilistic_state);
    }
 
    void construct_internal_vector_representation()
    {
      if (m_single_state!=STATE(-1))
      {
        assert(m_probabilistic_state.size()==0);
        m_probabilistic_state.emplace_back(m_single_state,PROBABILITY::one());
        m_single_state=STATE(-1);
      }
    }
 
    void set(const STATE& s)
    {
      assert(m_probabilistic_state.size()==0);
      m_single_state=s; 
    }
 
    STATE get() const
    {
      if (m_probabilistic_state.size()>1)
      {
        throw mcrl2::runtime_error("Probabilistic state is not simple\n");
      }
      if (m_probabilistic_state.size()==1)
      {
        assert(m_probabilistic_state.front().state()!=STATE(-1));
        return m_probabilistic_state.front().state();
      }
      assert(m_single_state!=STATE(-1));
      return m_single_state; 
    }
 
    void add(const STATE& s, const PROBABILITY& p)
    {
      m_probabilistic_state.emplace_back(s,p);
    }
 
    void shrink_to_fit()
    {
      m_probabilistic_state.shrink_to_fit();
      assert((m_probabilistic_state.size()>1 && m_single_state==std::size_t(-1)) ||
             (m_probabilistic_state.size()==0 && m_single_state!=std::size_t(-1)));
#ifndef NDEBUG
      PROBABILITY sum=PROBABILITY::zero();
      for(const state_probability_pair& p: m_probabilistic_state)
      {
        assert(p.probability()>PROBABILITY::zero());
        assert(p.probability()<=PROBABILITY::one());
        sum=sum+p.probability();
      }
      // SVC studio copies empty probabilistic states.
      assert(m_probabilistic_state.size()==0 || sum==PROBABILITY::one());
#endif
    }
 
    std::size_t size() const
    {
      return m_probabilistic_state.size();
    }
 
    void clear()
    {
      m_single_state=STATE(-1);
      m_probabilistic_state.clear();
    }
 
    const_iterator begin() const
    {
      return m_probabilistic_state.begin();
    }
 
    const_iterator end() const
    {
      return m_probabilistic_state.end();
    }
 
    iterator begin()
    {
      return m_probabilistic_state.begin();
    }
 
    iterator end()
    {
      return m_probabilistic_state.end();
    }
 
    const_reverse_iterator rbegin() const
    {
      return m_probabilistic_state.rbegin();
    }
 
    const_reverse_iterator rend() const
    {
      return m_probabilistic_state.rend();
    }
 
    reverse_iterator rbegin()
    {
      return m_probabilistic_state.rbegin();
    }
 
    reverse_iterator rend()
    {
      return m_probabilistic_state.rend();
    }
};
 
 
/* \brief A pretty print operator on action labels, returning it as a string.
 * */
template < class STATE, class PROBABILITY >
inline std::string pp(const probabilistic_state<STATE, PROBABILITY>& l)
{
  std::stringstream str;
  if (l.size()<=1)
  {
    str << "[ " << l.get() << ": 1.0 ]";
  }
  else
  {
    str << "[ ";
    bool first=true;
    for(const lps::state_probability_pair<STATE, PROBABILITY>& p: l)
    {
      if (first)
      {
        first=false;
      }
      else
      {
        str << "; ";
      }
      str << p.state() << ": " << p.probability();
    }
    str << " ]";
  }
 
  return str.str();
}
 
template < class STATE, class PROBABILITY >
inline
std::ostream& operator<<(std::ostream& out, const probabilistic_state<STATE, PROBABILITY>& l)
{
  return out << pp(l);
}
 
 
 
} // namespace lts
} // namespace mcrl2
 
namespace std
{
 
template < class STATE, class PROBABILITY >
struct hash< mcrl2::lts::probabilistic_state<STATE, PROBABILITY> >
{
  std::size_t operator()(const mcrl2::lts::probabilistic_state<STATE, PROBABILITY>& p) const
  {
    if (p.m_single_state!=STATE(-1))
    {
      assert(p.m_probabilistic_state.size()==0);
      hash<STATE> state_hasher;
      hash<PROBABILITY> probability_hasher;
      return mcrl2::utilities::detail::hash_combine(0, 
                   mcrl2::utilities::detail::hash_combine(state_hasher(p.m_single_state), 
                                                          probability_hasher(PROBABILITY::one())));
    }
    hash<vector<typename mcrl2::lps::state_probability_pair< STATE, PROBABILITY > > > hasher;
    return hasher(p.m_probabilistic_state);
  }
};
 
} // namespace std
 
#endif // MCRL2_LTS_PROBABILISTIC_STATE_H