Line data Source code
1 : // Author(s): Wieger Wesselink 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 : /// \file mcrl2/lps/stochastic_state.h 10 : /// \brief add your file description here. 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" 17 : #include "mcrl2/data/real_utilities.h" 18 : #include "mcrl2/lps/state.h" 19 : 20 : namespace mcrl2 { 21 : 22 : namespace lps { 23 : 24 : /* inline 25 : const 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 : 31 : inline 32 : const 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| 42 : struct stochastic_state 43 : { 44 : // TODO: use a more efficient representation 45 : std::vector<data::data_expression> probabilities; 46 : std::vector<state> states; 47 : 48 61 : 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 208 : void clear() 61 : { 62 208 : probabilities.clear(); 63 208 : states.clear(); 64 208 : } 65 : 66 0 : std::size_t size() const 67 : { 68 0 : assert(states.size()==probabilities.size()); 69 0 : return states.size(); 70 : } 71 : }; 72 : 73 : inline 74 84 : std::string print_probability(const data::data_expression& x) 75 : { 76 84 : const auto& x_ = atermpp::down_cast<data::application>(x); 77 168 : return data::pp(x_[0]) + '/' + data::pp(x_[1]); 78 : } 79 : 80 : inline 81 0 : void check_probability(const data::data_expression& x, const data::rewriter& rewr) 82 : { 83 0 : const auto& x_ = atermpp::down_cast<data::application>(x); 84 0 : if (x_.head().size() != 3) 85 : { 86 0 : throw mcrl2::runtime_error("The probability " + data::pp(x) + " is not a proper rational number."); 87 : } 88 0 : if (x_.head() != data::sort_real::creal()) 89 : { 90 0 : throw mcrl2::runtime_error("Probability is not a closed expression with a proper enumerator and denominator: " + data::pp(x) + "."); 91 : } 92 0 : if (rewr(data::greater_equal(x, data::sort_real::real_zero())) != data::sort_bool::true_()) 93 : { 94 0 : throw mcrl2::runtime_error("Probability is smaller than zero: " + data::pp(x) + "."); 95 : } 96 0 : if (rewr(data::greater_equal(data::sort_real::real_one(), x)) != data::sort_bool::true_()) 97 : { 98 0 : throw mcrl2::runtime_error("Probability is greater than one: " + data::pp(x) + "."); 99 : } 100 0 : } 101 : 102 : inline 103 0 : void check_stochastic_state(const stochastic_state& s, const data::rewriter& rewr) 104 : { 105 0 : data::data_expression probability = data::sort_real::real_zero(); 106 0 : for (const data::data_expression& prob: s.probabilities) 107 : { 108 0 : check_probability(prob, rewr); 109 0 : probability = data::sort_real::plus(probability, prob); 110 : } 111 0 : probability = rewr(probability); 112 0 : if (probability != data::sort_real::real_one()) 113 : { 114 0 : std::vector<std::string> v; 115 0 : for (const data::data_expression& prob: s.probabilities) 116 : { 117 0 : v.push_back(print_probability(prob)); 118 : } 119 0 : throw mcrl2::runtime_error("The probabilities " + core::detail::print_list(v) + " do not add up to one, but to " + pp(probability) + "." ); 120 0 : } 121 0 : } 122 : 123 : } // namespace lps 124 : 125 : } // namespace mcrl2 126 : 127 : #endif // MCRL2_LPS_STOCHASTIC_STATE_H