Allow unnecessary parameters in region string

src/storm-pars/parser/ParameterRegionParser.cpp

@@ -1,3 +1,4 @@
+#include <storm/exceptions/WrongFormatException.h>
 #include "storm-pars/parser/ParameterRegionParser.h"
 
 #include "storm/utility/macros.h"
@@ -10,13 +11,13 @@ namespace storm {
 
         template<typename ParametricType>
         void ParameterRegionParser<ParametricType>::parseParameterBoundaries(Valuation& lowerBoundaries, Valuation& upperBoundaries, std::string const& parameterBoundariesString, std::set<VariableType> 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<VariableType>(v);
+                    break;
                 }
             }
-            STORM_LOG_ASSERT(var, "Could not find parameter " << parameter << " in the set of considered variables");
-            
-            CoefficientType lb = storm::utility::convertNumber<CoefficientType>(parameterBoundariesString.substr(0,positionOfFirstRelation));
-            CoefficientType ub = storm::utility::convertNumber<CoefficientType>(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<CoefficientType>(parameterBoundariesString.substr(0,positionOfFirstRelation));
+                CoefficientType ub = storm::utility::convertNumber<CoefficientType>(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<typename ParametricType>
@@ -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<ParametricType>(std::move(lowerBoundaries), std::move(upperBoundaries));
         }