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: 11 34 32.4 %
Date: 2020-09-16 00:45:56 Functions: 7 10 70.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/lps/state.h"
      18             : 
      19             : namespace mcrl2 {
      20             : 
      21             : namespace lps {
      22             : 
      23             : inline
      24         510 : const data::data_expression& real_zero()
      25             : {
      26         510 :   static data::data_expression result = data::sort_real::creal(data::sort_int::cint(data::sort_nat::c0()), data::sort_pos::c1());
      27         510 :   return result;
      28             : }
      29             : 
      30             : inline
      31           6 : const data::data_expression& real_one()
      32             : {
      33           6 :   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());
      34           6 :   return result;
      35             : }
      36             : 
      37             : // invariant: the elements of states must be unique
      38             : // invariant: the elements of probabilities must be >= 0
      39             : // invariant: the elements of probabilities must sum up to 1
      40             : // invariant: |probabilities| = |states|
      41         546 : struct stochastic_state
      42             : {
      43             :   // TODO: use a more efficient representation
      44             :   std::vector<data::data_expression> probabilities;
      45             :   std::vector<state> states;
      46             : 
      47         348 :   stochastic_state() = default;
      48             : 
      49             :   explicit stochastic_state(const state& s)
      50             :     : probabilities{real_one()}, states{s}
      51             :   {}
      52             : 
      53             :   void push_back(const data::data_expression& probability, const state& s)
      54             :   {
      55             :     probabilities.push_back(probability);
      56             :     states.push_back(s);
      57             :   }
      58             : };
      59             : 
      60             : inline
      61          56 : std::string print_probability(const data::data_expression& x)
      62             : {
      63          56 :   const auto& x_ = atermpp::down_cast<data::application>(x);
      64          56 :   return data::pp(x_[0]) + '/' + data::pp(x_[1]);
      65             : }
      66             : 
      67             : inline
      68           0 : void check_probability(const data::data_expression& x, const data::rewriter& rewr)
      69             : {
      70           0 :   const auto& x_ = atermpp::down_cast<data::application>(x);
      71           0 :   if (x_.head().size() != 3)
      72             :   {
      73           0 :     throw mcrl2::runtime_error("The probability " + data::pp(x) + " is not a proper rational number.");
      74             :   }
      75           0 :   if (x_.head() != data::sort_real::creal())
      76             :   {
      77           0 :     throw mcrl2::runtime_error("Probability is not a closed expression with a proper enumerator and denominator: " + data::pp(x) + ".");
      78             :   }
      79           0 :   if (rewr(data::greater_equal(x, real_zero())) != data::sort_bool::true_())
      80             :   {
      81           0 :     throw mcrl2::runtime_error("Probability is smaller than zero: " + data::pp(x) + ".");
      82             :   }
      83           0 :   if (rewr(data::greater_equal(real_one(), x)) != data::sort_bool::true_())
      84             :   {
      85           0 :     throw mcrl2::runtime_error("Probability is greater than one: " + data::pp(x) + ".");
      86             :   }
      87           0 : }
      88             : 
      89             : inline
      90           0 : void check_stochastic_state(const stochastic_state& s, const data::rewriter& rewr)
      91             : {
      92           0 :   data::data_expression probability = real_zero();
      93           0 :   for (const data::data_expression& prob: s.probabilities)
      94             :   {
      95           0 :     check_probability(prob, rewr);
      96           0 :     probability = data::sort_real::plus(probability, prob);
      97             :   }
      98           0 :   probability = rewr(probability);
      99           0 :   if (probability != real_one())
     100             :   {
     101           0 :     std::vector<std::string> v;
     102           0 :     for (const data::data_expression& prob: s.probabilities)
     103             :     {
     104           0 :       v.push_back(print_probability(prob));
     105             :     }
     106           0 :     throw mcrl2::runtime_error("The probabilities " + core::detail::print_list(v) + " do not add up to one.");
     107             :   }
     108           0 : }
     109             : 
     110             : } // namespace lps
     111             : 
     112             : } // namespace mcrl2
     113             : 
     114             : #endif // MCRL2_LPS_STOCHASTIC_STATE_H

Generated by: LCOV version 1.13