From 5bdcb66fcb4ad96c7e7b612a72326752381d9a18 Mon Sep 17 00:00:00 2001 From: Tim Quatmann Date: Wed, 18 Mar 2020 09:53:03 +0100 Subject: [PATCH] Fixes for reward formulas --- src/storm-pomdp/analysis/FormulaInformation.cpp | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/storm-pomdp/analysis/FormulaInformation.cpp b/src/storm-pomdp/analysis/FormulaInformation.cpp index 836abf881..8bb00450c 100644 --- a/src/storm-pomdp/analysis/FormulaInformation.cpp +++ b/src/storm-pomdp/analysis/FormulaInformation.cpp @@ -137,7 +137,7 @@ namespace storm { template FormulaInformation getFormulaInformation(PomdpType const& pomdp, storm::logic::RewardOperatorFormula const& formula) { STORM_LOG_THROW(formula.hasOptimalityType(), storm::exceptions::InvalidPropertyException, "The property does not specify an optimization direction (min/max)"); - STORM_LOG_WARN_COND(formula.hasBound(), "The reward threshold for the given property will be ignored."); + STORM_LOG_WARN_COND(!formula.hasBound(), "The reward threshold for the given property will be ignored."); std::string rewardModelName = ""; if (formula.hasRewardModelName()) { rewardModelName = formula.getRewardModelName(); @@ -152,7 +152,7 @@ namespace storm { targetStatesFormula = subformula.asEventuallyFormula().getSubformula().asSharedPointer(); } if (targetStatesFormula && targetStatesFormula->isInFragment(storm::logic::propositional())) { - FormulaInformation result(FormulaInformation::Type::NonNestedReachabilityProbability, formula.getOptimalityType(), rewardModelName); + FormulaInformation result(FormulaInformation::Type::NonNestedExpectedRewardFormula, formula.getOptimalityType(), rewardModelName); result.updateTargetStates(pomdp, getStates(*targetStatesFormula, false, pomdp)); return result; }