mCRL2
Loading...
Searching...
No Matches
state_probability_pair.h
Go to the documentation of this file.
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
19#ifndef MCRL2_LPS_STATE_PROBABILITY_PAIR_H
20#define MCRL2_LPS_STATE_PROBABILITY_PAIR_H
21
22#include <cassert>
23#include <iostream>
26
27namespace mcrl2
28{
29namespace lps
30{
31
32template < class STATE, class PROBABILITY >
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
45 state_probability_pair(const STATE& state, const PROBABILITY& probability)
46 : m_state(state),
48 {
49 assert(probability!=PROBABILITY::zero());
50 }
51
56
62
66 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 return m_state==other.m_state &&
73 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 return m_state==other.m_state && m_probability==other.m_probability;
79 }
80 }
81
83 const STATE& state() const
84 {
85 return m_state;
86 }
87
89 STATE& state()
90 {
91 return m_state;
92 }
93
95 const PROBABILITY& probability() const
96 {
97 return m_probability;
98 }
99
101 PROBABILITY& probability()
102 {
103 return m_probability;
104 }
105
106};
107
108} // namespace lps
109} // namespace mcrl2
110
111namespace std
112{
113
114template < class STATE, class PROBABILITY >
115struct hash<mcrl2::lps::state_probability_pair<STATE,PROBABILITY> >
116{
118 {
119 hash<STATE> state_hasher;
120 hash<PROBABILITY> probability_hasher;
121 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
The term_appl class represents function application.
Read-only balanced binary tree of terms.
STATE & state()
Get the state in a state probability pair.
state_probability_pair(state_probability_pair &&p)=default
state_probability_pair & operator=(state_probability_pair &&p)=default
state_probability_pair(const state_probability_pair &p)=default
Copy constructor;.
state_probability_pair & operator=(const state_probability_pair &p)=default
Standard assignment.
const PROBABILITY & probability() const
get the probability from a state proability pair.
const STATE & state() const
Get the state from a state probability pair.
PROBABILITY & probability()
Set the probability in a state probability pair.
state_probability_pair(const STATE &state, const PROBABILITY &probability)
constructor.
bool operator==(const state_probability_pair &other) const
Standard equality operator.
This file contains a specialisation for hashes on pairs. This is not a part of the standard,...
std::size_t hash_combine(const std::size_t h1, const std::size_t h2)
A class that takes a linear process specification and checks all tau-summands of that LPS for conflue...
Definition indexed_set.h:72
STL namespace.
std::size_t operator()(const mcrl2::lps::state_probability_pair< STATE, PROBABILITY > &p) const
#define hash(l, r, m)
Definition tree_set.cpp:23