mCRL2
Searching...
No Matches
stochastic_state.h
Go to the documentation of this file.
2// Copyright: see the accompanying file COPYING or copy at
3// https://github.com/mCRL2org/mCRL2/blob/master/COPYING
4//
6// (See accompanying file LICENSE_1_0.txt or copy at
8//
11
12#ifndef MCRL2_LPS_STOCHASTIC_STATE_H
13#define MCRL2_LPS_STOCHASTIC_STATE_H
14
15#include "mcrl2/data/print.h"
16#include "mcrl2/data/rewriter.h"
18#include "mcrl2/lps/state.h"
19
20namespace mcrl2 {
21
22namespace lps {
23
24/* inline
25const data::data_expression& real_zero()
26{
27 static data::data_expression result = data::sort_real::creal(data::sort_int::cint(data::sort_nat::c0()), data::sort_pos::c1());
28 return result;
29}
30
31inline
32const data::data_expression& real_one()
33{
34 static data::data_expression result = data::sort_real::creal(data::sort_int::cint(data::sort_nat::cnat(data::sort_pos::c1())), data::sort_pos::c1());
35 return result;
36} */
37
38// invariant: the elements of states must be unique
39// invariant: the elements of probabilities must be >= 0
40// invariant: the elements of probabilities must sum up to 1
41// invariant: |probabilities| = |states|
43{
44 // TODO: use a more efficient representation
45 std::vector<data::data_expression> probabilities;
46 std::vector<state> states;
47
48 stochastic_state() = default;
49
50 explicit stochastic_state(const state& s)
51 : probabilities{data::sort_real::real_one()}, states{s}
52 {}
53
54 void push_back(const data::data_expression& probability, const state& s)
55 {
56 probabilities.push_back(probability);
57 states.push_back(s);
58 }
59
60 void clear()
61 {
62 probabilities.clear();
63 states.clear();
64 }
65
66 std::size_t size() const
67 {
68 assert(states.size()==probabilities.size());
69 return states.size();
70 }
71};
72
73inline
75{
76 const auto& x_ = atermpp::down_cast<data::application>(x);
77 return data::pp(x_[0]) + '/' + data::pp(x_[1]);
78}
79
80inline
82{
83 const auto& x_ = atermpp::down_cast<data::application>(x);
85 {
86 throw mcrl2::runtime_error("The probability " + data::pp(x) + " is not a proper rational number.");
87 }
89 {
90 throw mcrl2::runtime_error("Probability is not a closed expression with a proper enumerator and denominator: " + data::pp(x) + ".");
91 }
93 {
94 throw mcrl2::runtime_error("Probability is smaller than zero: " + data::pp(x) + ".");
95 }
97 {
98 throw mcrl2::runtime_error("Probability is greater than one: " + data::pp(x) + ".");
99 }
100}
101
102inline
104{
106 for (const data::data_expression& prob: s.probabilities)
107 {
108 check_probability(prob, rewr);
109 probability = data::sort_real::plus(probability, prob);
110 }
111 probability = rewr(probability);
112 if (probability != data::sort_real::real_one())
113 {
114 std::vector<std::string> v;
115 for (const data::data_expression& prob: s.probabilities)
116 {
117 v.push_back(print_probability(prob));
118 }
119 throw mcrl2::runtime_error("The probabilities " + core::detail::print_list(v) + " do not add up to one, but to " + pp(probability) + "." );
120 }
121}
122
123} // namespace lps
124
125} // namespace mcrl2
126
127#endif // MCRL2_LPS_STOCHASTIC_STATE_H
Read-only balanced binary tree of terms.
Rewriter that operates on data expressions.
Definition rewriter.h:81
Standard exception class for reporting runtime errors.
Definition exception.h:27
Provides utilities for pretty printing.
The class rewriter.
std::string print_list(const Container &v, const std::string &message="", bool print_index=false, bool boundary_spaces=true)
Creates a string representation of a container.
const function_symbol & true_()
Constructor for function symbol true.
Definition bool.h:77
function_symbol plus(const sort_expression &s0, const sort_expression &s1)
Definition real.h:1059
const function_symbol & creal()
Constructor for function symbol @cReal.
Definition real.h:107
data_expression & real_one()
data_expression & real_zero()
std::string pp(const abstraction &x)
Definition data.cpp:39
function_symbol greater_equal(const sort_expression &s)
Constructor for function symbol >=.
Definition standard.h:351
std::string pp(const action_summand &x)
Definition lps.cpp:26
void check_stochastic_state(const stochastic_state &s, const data::rewriter &rewr)
void check_probability(const data::data_expression &x, const data::rewriter &rewr)
std::string print_probability(const data::data_expression &x)
A class that takes a linear process specification and checks all tau-summands of that LPS for conflue...
Definition indexed_set.h:72
Contains a number of auxiliary functions to recognize reals.
The class summand.
void push_back(const data::data_expression &probability, const state &s)
std::vector< data::data_expression > probabilities
std::vector< state > states