From 8b05837e7701e05e522447786e32a321ed52d0b6 Mon Sep 17 00:00:00 2001 From: Matthias Volk Date: Wed, 21 Oct 2020 10:09:45 +0200 Subject: [PATCH] Fixed assertion for RationalFunction --- src/storm-pomdp/transformer/ObservationTraceUnfolder.cpp | 8 +++++--- 1 file changed, 5 insertions(+), 3 deletions(-) diff --git a/src/storm-pomdp/transformer/ObservationTraceUnfolder.cpp b/src/storm-pomdp/transformer/ObservationTraceUnfolder.cpp index e8e21b908..36901c3e9 100644 --- a/src/storm-pomdp/transformer/ObservationTraceUnfolder.cpp +++ b/src/storm-pomdp/transformer/ObservationTraceUnfolder.cpp @@ -1,6 +1,7 @@ #include "storm/exceptions/InvalidArgumentException.h" #include "storm-pomdp/transformer/ObservationTraceUnfolder.h" #include "storm/storage/expressions/ExpressionManager.h" +#include "storm/utility/ConstantsComparator.h" #undef _VERBOSE_OBSERVATION_UNFOLDING @@ -131,13 +132,14 @@ namespace storm { // Now, take care of the last step. uint64_t sinkState = newStateIndex; uint64_t targetState = newStateIndex + 1; + auto cc = storm::utility::ConstantsComparator(); for (auto const& unfoldedToOldEntry : unfoldedToOldNextStep) { svbuilder.addState(unfoldedToOldEntry.first, {}, {static_cast(unfoldedToOldEntry.second)}); transitionMatrixBuilder.newRowGroup(newRowGroupStart); STORM_LOG_ASSERT(risk.size() > unfoldedToOldEntry.second, "Must be a state"); - STORM_LOG_ASSERT(risk[unfoldedToOldEntry.second] <= storm::utility::one(), "Risk must be a probability"); - STORM_LOG_ASSERT(risk[unfoldedToOldEntry.second] >= storm::utility::zero(), "Risk must be a probability"); + STORM_LOG_ASSERT(!cc.isLess(storm::utility::one(), risk[unfoldedToOldEntry.second]), "Risk must be a probability"); + STORM_LOG_ASSERT(!cc.isLess(risk[unfoldedToOldEntry.second], storm::utility::zero()), "Risk must be a probability"); //std::cout << "risk is" << risk[unfoldedToOldEntry.second] << std::endl; if (!storm::utility::isOne(risk[unfoldedToOldEntry.second])) { transitionMatrixBuilder.addNextValue(newRowGroupStart, sinkState, @@ -197,4 +199,4 @@ namespace storm { template class ObservationTraceUnfolder; } -} \ No newline at end of file +}