diff --git a/src/storm-pars/modelchecker/results/RegionRefinementCheckResult.cpp b/src/storm-pars/modelchecker/results/RegionRefinementCheckResult.cpp index 320dda2e8..7c2a5e18c 100644 --- a/src/storm-pars/modelchecker/results/RegionRefinementCheckResult.cpp +++ b/src/storm-pars/modelchecker/results/RegionRefinementCheckResult.cpp @@ -48,7 +48,10 @@ namespace storm { out << "Region refinement Check result (visualization):" << std::endl; out << " \t x-axis: " << x << " \t y-axis: " << y << " \t S=safe, [ ]=unsafe, -=ambiguous " << std::endl; - for (uint_fast64_t i = 0; i < sizeX+2; ++i) out << "#"; out << std::endl; + for (uint_fast64_t i = 0; i < sizeX+2; ++i) { + out << "#"; + } + out << std::endl; CoefficientType deltaX = (getParameterSpace().getUpperBoundary(x) - getParameterSpace().getLowerBoundary(x)) / storm::utility::convertNumber(sizeX); CoefficientType deltaY = (getParameterSpace().getUpperBoundary(y) - getParameterSpace().getLowerBoundary(y)) / storm::utility::convertNumber(sizeY); @@ -94,7 +97,10 @@ namespace storm { } out << "#" << std::endl; } - for (uint_fast64_t i = 0; i < sizeX+2; ++i) out << "#"; out << std::endl; + for (uint_fast64_t i = 0; i < sizeX+2; ++i) { + out << "#"; + } + out << std::endl; } else { STORM_LOG_WARN("Writing illustration of region check result to a stream is only implemented for two parameters."); } diff --git a/src/storm-parsers/parser/DirectEncodingParser.cpp b/src/storm-parsers/parser/DirectEncodingParser.cpp index 683a87d77..1dd6322d9 100644 --- a/src/storm-parsers/parser/DirectEncodingParser.cpp +++ b/src/storm-parsers/parser/DirectEncodingParser.cpp @@ -164,7 +164,6 @@ namespace storm { // Iterate over all lines std::string line; size_t row = 0; - size_t firstRowOfState = 0; size_t state = 0; bool firstState = true; bool firstActionForState = true; @@ -197,7 +196,6 @@ namespace storm { STORM_LOG_TRACE("new Row Group starts at " << row << "."); builder.newRowGroup(row); } - firstRowOfState = row; if (continuousTime) { // Parse exit rate for CTMC or MA diff --git a/src/storm/logic/CumulativeRewardFormula.cpp b/src/storm/logic/CumulativeRewardFormula.cpp index 7abcdc7e4..33633b319 100644 --- a/src/storm/logic/CumulativeRewardFormula.cpp +++ b/src/storm/logic/CumulativeRewardFormula.cpp @@ -99,7 +99,6 @@ namespace storm { double CumulativeRewardFormula::getBound(unsigned i) const { checkNoVariablesInBound(bounds.at(i).getBound()); double value = bounds.at(i).getBound().evaluateAsDouble(); - STORM_LOG_THROW(value >= 0.0, storm::exceptions::InvalidPropertyException, "Time-bound must not evaluate to negative number."); return value; } @@ -107,7 +106,6 @@ namespace storm { storm::RationalNumber CumulativeRewardFormula::getBound(unsigned i) const { checkNoVariablesInBound(bounds.at(i).getBound()); storm::RationalNumber value = bounds.at(i).getBound().evaluateAsRational(); - STORM_LOG_THROW(value >= storm::utility::zero(), storm::exceptions::InvalidPropertyException, "Time-bound must not evaluate to negative number."); return value; } @@ -115,7 +113,6 @@ namespace storm { uint64_t CumulativeRewardFormula::getBound(unsigned i) const { checkNoVariablesInBound(bounds.at(i).getBound()); uint64_t value = bounds.at(i).getBound().evaluateAsInt(); - STORM_LOG_THROW(value >= 0, storm::exceptions::InvalidPropertyException, "Time-bound must not evaluate to negative number."); return value; } diff --git a/src/storm/logic/InstantaneousRewardFormula.cpp b/src/storm/logic/InstantaneousRewardFormula.cpp index 37bdee1c9..1ed2c1f66 100644 --- a/src/storm/logic/InstantaneousRewardFormula.cpp +++ b/src/storm/logic/InstantaneousRewardFormula.cpp @@ -55,7 +55,7 @@ namespace storm { template <> uint64_t InstantaneousRewardFormula::getBound() const { checkNoVariablesInBound(bound); - uint64_t value = bound.evaluateAsInt(); + int64_t value = bound.evaluateAsInt(); STORM_LOG_THROW(value >= 0, storm::exceptions::InvalidPropertyException, "Time-bound must not evaluate to negative number."); return value; }