mCRL2
Loading...
Searching...
No Matches
probabilistic_state.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
18#ifndef MCRL2_LTS_PROBABILISTIC_STATE_H
19#define MCRL2_LTS_PROBABILISTIC_STATE_H
20
21#include <sstream>
24
25
26namespace mcrl2
27{
28
29namespace lts
30{
31
47template < class STATE, class PROBABILITY >
49{
50 public:
51
52 friend std::hash<probabilistic_state>;
53
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
74 : m_single_state(STATE(-1))
75 {
76 }
77
82 explicit probabilistic_state(const STATE& s)
84 {
85 }
86
91 {
93 }
94
97 {
101 return *this;
102 }
103
108 template <class STATE_PROBABILITY_PAIR_ITERATOR>
109 probabilistic_state(const STATE_PROBABILITY_PAIR_ITERATOR begin, const STATE_PROBABILITY_PAIR_ITERATOR end)
110 : m_single_state(STATE(-1)),
112 {
113 assert(begin!=end);
115 }
116
120 bool operator==(const probabilistic_state& other) const
121 {
122 if (m_single_state==STATE(-1))
123 {
124 if (other.m_single_state==STATE(-1))
125 {
126 assert(m_probabilistic_state.size()>0);
127 assert(other.m_probabilistic_state.size()>0);
129 }
130 else
131 {
132 return m_probabilistic_state.size()==1 &&
133 other.m_single_state==m_probabilistic_state.front().state();
134 }
135 }
136 else
137 {
138 if (other.m_single_state==STATE(-1))
139 {
140 return other.m_probabilistic_state.size()==1 &&
141 m_single_state==other.m_probabilistic_state.front().state();
142 }
143 else
144 {
145 assert(m_probabilistic_state.size()==0);
146 assert(other.m_probabilistic_state.size()==0);
147 return m_single_state==other.m_single_state;
148 }
149 }
150 }
151
155 bool operator!=(const probabilistic_state& other) const
156 {
157 return !(operator==(other));
158 }
159
163 {
166 }
167
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
185 void set(const STATE& s)
186 {
187 assert(m_probabilistic_state.size()==0);
189 }
190
195 STATE get() const
196 {
197 if (m_probabilistic_state.size()>1)
198 {
199 throw mcrl2::runtime_error("Probabilistic state is not simple\n");
200 }
201 if (m_probabilistic_state.size()==1)
202 {
203 assert(m_probabilistic_state.front().state()!=STATE(-1));
204 return m_probabilistic_state.front().state();
205 }
206 assert(m_single_state!=STATE(-1));
207 return m_single_state;
208 }
209
214 void add(const STATE& s, const PROBABILITY& p)
215 {
216 m_probabilistic_state.emplace_back(s,p);
217 }
218
224 {
225 m_probabilistic_state.shrink_to_fit();
226 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 PROBABILITY sum=PROBABILITY::zero();
231 {
232 assert(p.probability()>PROBABILITY::zero());
233 assert(p.probability()<=PROBABILITY::one());
234 sum=sum+p.probability();
235 }
236 // SVC studio copies empty probabilistic states.
237 assert(m_probabilistic_state.size()==0 || sum==PROBABILITY::one());
238#endif
239 }
240
247 std::size_t size() const
248 {
249 return m_probabilistic_state.size();
250 }
251
254 void clear()
255 {
256 m_single_state=STATE(-1);
257 m_probabilistic_state.clear();
258 }
259
264 {
265 return m_probabilistic_state.begin();
266 }
267
271 {
272 return m_probabilistic_state.end();
273 }
274
278 {
279 return m_probabilistic_state.begin();
280 }
281
285 {
286 return m_probabilistic_state.end();
287 }
288
293 {
294 return m_probabilistic_state.rbegin();
295 }
296
300 {
301 return m_probabilistic_state.rend();
302 }
303
307 {
308 return m_probabilistic_state.rbegin();
309 }
310
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 * */
322template < class STATE, class PROBABILITY >
323inline 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;
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
354template < class STATE, class PROBABILITY >
355inline
356std::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
366namespace std
367{
368
373template < class STATE, class PROBABILITY >
374struct hash< mcrl2::lts::probabilistic_state<STATE, PROBABILITY> >
375{
377 {
378 if (p.m_single_state!=STATE(-1))
379 {
380 assert(p.m_probabilistic_state.size()==0);
381 hash<STATE> state_hasher;
382 hash<PROBABILITY> probability_hasher;
385 probability_hasher(PROBABILITY::one())));
386 }
387 hash<vector<typename mcrl2::lps::state_probability_pair< STATE, PROBABILITY > > > hasher;
388 return hasher(p.m_probabilistic_state);
389 }
390};
391
392} // namespace std
393
394#endif // MCRL2_LTS_PROBABILISTIC_STATE_H
A class that contains a probabilistic state.
void set(const STATE &s)
Set this probabilistic state to a single state with probability one.
const_iterator begin() const
Gets an iterator over pairs of state and probability. This can only be used when the state is stored ...
void construct_internal_vector_representation()
Guarantee that this probabilistic state is internally stored as a vector, such that begin/end,...
probabilistic_state & operator=(const probabilistic_state &other)
Copy assignment constructor.
const_reverse_iterator rbegin() const
Gets a reverse iterator over pairs of state and probability. This can only be used when the state is ...
std::size_t size() const
Gets the number of probabilistic states in the vector representation of this state....
bool operator!=(const probabilistic_state &other) const
Standard equality operator.
iterator begin()
Gets an iterator over pairs of state and probability. This can only be used if the state is internall...
std::vector< state_probability_pair >::const_iterator const_iterator
lps::state_probability_pair< STATE, PROBABILITY > state_probability_pair
STATE get() const
Get a probabilistic state if is is simple, i.e., consists of a single state.
iterator end()
Gets the end iterator over pairs of state and probability.
reverse_iterator rbegin()
Gets a reverse iterator over pairs of state and probability. This can only be used if the state is in...
std::vector< state_probability_pair > m_probabilistic_state
const_iterator end() const
Gets the end iterator over pairs of state and probability.
std::vector< state_probability_pair >::iterator iterator
void swap(probabilistic_state &other)
Swap this probabilistic state.
reverse_iterator rend()
Gets the reverse end iterator over pairs of state and probability.
std::vector< state_probability_pair >::const_reverse_iterator const_reverse_iterator
bool operator==(const probabilistic_state &other) const
Standard equality operator.
void clear()
Makes the probabilistic state empty.
probabilistic_state(const STATE_PROBABILITY_PAIR_ITERATOR begin, const STATE_PROBABILITY_PAIR_ITERATOR end)
Creates a probabilistic state on the basis of state_probability_pairs.
std::vector< state_probability_pair >::reverse_iterator reverse_iterator
probabilistic_state(const probabilistic_state &other)
Copy constructor.
void shrink_to_fit()
If a probabilistic state is ready, shrinking it to minimal size might be useful to reduce its memory ...
probabilistic_state()
Default constructor.
probabilistic_state(const STATE &s)
Constructor of a probabilistic state from a non probabilistic state.
void add(const STATE &s, const PROBABILITY &p)
Add a state with a probability to the probabilistic state.
const_reverse_iterator rend() const
Gets the reverse end iterator over pairs of state and probability.
Standard exception class for reporting runtime errors.
Definition exception.h:27
Exception classes for use in libraries and tools.
std::string pp(const abstraction &x)
Definition data.cpp:39
std::ostream & operator<<(std::ostream &out, const abstraction &x)
Definition abstraction.h:94
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.
void swap(atermpp::unprotected_aterm &t1, atermpp::unprotected_aterm &t2) noexcept
Swaps two aterms.
Definition aterm.h:384
This file contains a class with a state/probability pair.
std::size_t operator()(const mcrl2::lts::probabilistic_state< STATE, PROBABILITY > &p) const
#define hash(l, r, m)
Definition tree_set.cpp:23