LCOV - code coverage report
Current view: top level - lps/include/mcrl2/lps - stochastic_state.h (source / functions) Hit Total Coverage
Test: mcrl2_coverage.info.cleaned Lines: 8 35 22.9 %
Date: 2024-03-08 02:52:28 Functions: 3 6 50.0 %
Legend: Lines: hit not hit

          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

Generated by: LCOV version 1.14