Browse Source

fixed bug related to instantaneous reward properties in formula parser

Former-commit-id: 8d799f8678
tempestpy_adaptions
dehnert 9 years ago
parent
commit
94fd4cd9a8
  1. 4
      src/parser/FormulaParser.cpp

4
src/parser/FormulaParser.cpp

@ -406,8 +406,8 @@ namespace storm {
return std::shared_ptr<storm::logic::Formula const>(new storm::logic::InstantaneousRewardFormula(static_cast<uint_fast64_t>(boost::get<unsigned>(timeBound)))); return std::shared_ptr<storm::logic::Formula const>(new storm::logic::InstantaneousRewardFormula(static_cast<uint_fast64_t>(boost::get<unsigned>(timeBound))));
} else { } else {
double timeBoundAsDouble = boost::get<double>(timeBound); double timeBoundAsDouble = boost::get<double>(timeBound);
STORM_LOG_THROW(timeBoundAsDouble >= 0, storm::exceptions::WrongFormatException, "Cumulative reward property must have non-negative bound.");
return std::shared_ptr<storm::logic::Formula const>(new storm::logic::InstantaneousRewardFormula(static_cast<uint_fast64_t>(timeBoundAsDouble)));
STORM_LOG_THROW(timeBoundAsDouble >= 0, storm::exceptions::WrongFormatException, "Instantaneous reward property must have non-negative bound.");
return std::shared_ptr<storm::logic::Formula const>(new storm::logic::InstantaneousRewardFormula(timeBoundAsDouble));
} }
} }

Loading…
Cancel
Save