From d7a22e78d0002e389dd5850a7d0073843b0fc294 Mon Sep 17 00:00:00 2001 From: Matthias Volk Date: Fri, 15 Feb 2019 16:56:49 +0100 Subject: [PATCH] Allow unnecessary parameters in region string --- .../parser/ParameterRegionParser.cpp | 25 +++++++++++++------ 1 file changed, 17 insertions(+), 8 deletions(-) diff --git a/src/storm-pars/parser/ParameterRegionParser.cpp b/src/storm-pars/parser/ParameterRegionParser.cpp index f6345eef1..c7c5bf98e 100644 --- a/src/storm-pars/parser/ParameterRegionParser.cpp +++ b/src/storm-pars/parser/ParameterRegionParser.cpp @@ -1,3 +1,4 @@ +#include #include "storm-pars/parser/ParameterRegionParser.h" #include "storm/utility/macros.h" @@ -10,13 +11,13 @@ namespace storm { template void ParameterRegionParser::parseParameterBoundaries(Valuation& lowerBoundaries, Valuation& upperBoundaries, std::string const& parameterBoundariesString, std::set const& consideredVariables) { - std::string::size_type positionOfFirstRelation = parameterBoundariesString.find("<="); STORM_LOG_THROW(positionOfFirstRelation!=std::string::npos, storm::exceptions::InvalidArgumentException, "When parsing the region" << parameterBoundariesString << " I could not find a '<=' after the first number"); std::string::size_type positionOfSecondRelation = parameterBoundariesString.find("<=", positionOfFirstRelation+2); STORM_LOG_THROW(positionOfSecondRelation!=std::string::npos, storm::exceptions::InvalidArgumentException, "When parsing the region" << parameterBoundariesString << " I could not find a '<=' after the parameter"); std::string parameter = parameterBoundariesString.substr(positionOfFirstRelation+2,positionOfSecondRelation-(positionOfFirstRelation+2)); + //removes all whitespaces from the parameter string: parameter.erase(std::remove_if (parameter.begin(), parameter.end(), ::isspace), parameter.end()); STORM_LOG_THROW(parameter.length()>0, storm::exceptions::InvalidArgumentException, "When parsing the region" << parameterBoundariesString << " I could not find a parameter"); @@ -25,17 +26,19 @@ namespace storm { for (auto const& v : consideredVariables) { std::stringstream stream; stream << v; - std::string vAsString = stream.str(); if (parameter == stream.str()) { var = std::make_unique(v); + break; } } - STORM_LOG_ASSERT(var, "Could not find parameter " << parameter << " in the set of considered variables"); - - CoefficientType lb = storm::utility::convertNumber(parameterBoundariesString.substr(0,positionOfFirstRelation)); - CoefficientType ub = storm::utility::convertNumber(parameterBoundariesString.substr(positionOfSecondRelation+2)); - lowerBoundaries.emplace(std::make_pair(*var, lb)); - upperBoundaries.emplace(std::make_pair(*var, ub)); + if (var) { + CoefficientType lb = storm::utility::convertNumber(parameterBoundariesString.substr(0,positionOfFirstRelation)); + CoefficientType ub = storm::utility::convertNumber(parameterBoundariesString.substr(positionOfSecondRelation+2)); + lowerBoundaries.emplace(std::make_pair(*var, lb)); + upperBoundaries.emplace(std::make_pair(*var, ub)); + } else { + STORM_LOG_WARN("Could not find parameter " << parameter << " in the set of considered variables. Ignoring this parameter."); + } } template @@ -49,6 +52,12 @@ namespace storm { parseParameterBoundaries(lowerBoundaries, upperBoundaries, parameterBoundary, consideredVariables); } } + + // Check that all considered variables are bounded + for (auto const& v : consideredVariables) { + STORM_LOG_THROW(lowerBoundaries.count(v) > 0, storm::exceptions::WrongFormatException, "Variable " << v << " was not defined in region string."); + STORM_LOG_ASSERT(upperBoundaries.count(v) > 0, "Variable " << v << " has a lower but not an upper bound."); + } return storm::storage::ParameterRegion(std::move(lowerBoundaries), std::move(upperBoundaries)); }