Merge branch 'master' into prismlang-sim

.github/workflows/buildtest.yml

@@ -45,7 +45,7 @@ jobs:
       - name: Init Docker
         run: sudo docker run -d -it --name storm --privileged movesrwth/storm-basesystem:${{ matrix.distro }}
       - name: Git clone
-        run: sudo docker exec storm git clone --depth 1 --branch $STORM_BRANCH $STORM_GIT_URL /opt/storm
+        run: sudo docker exec storm git clone --branch $STORM_BRANCH $STORM_GIT_URL /opt/storm
       - name: Run cmake
         run: sudo docker exec storm bash -c "mkdir /opt/storm/build; cd /opt/storm/build; cmake .. ${CMAKE_ARGS}"
       - name: Build storm
@@ -115,7 +115,7 @@ jobs:
         # Build & TEST & DEPLOY STORM
         #####
       - name: Git clone
-        run: sudo docker exec storm git clone --depth 1 --branch $STORM_BRANCH $STORM_GIT_URL /opt/storm
+        run: sudo docker exec storm git clone --branch $STORM_BRANCH $STORM_GIT_URL /opt/storm
       - name: Run cmake
         run: sudo docker exec storm bash -c "mkdir /opt/storm/build; cd /opt/storm/build; cmake .. ${CMAKE_ARGS}"
       - name: Build storm

src/storm-pars/api/region.h

@@ -39,7 +39,7 @@ namespace storm {
         };
 
         template <typename ValueType>
-        std::vector<storm::storage::ParameterRegion<ValueType>> parseRegions(std::string const& inputString, std::set<typename storm::storage::ParameterRegion<ValueType>::VariableType> const& consideredVariables, boost::optional<int> splittingThreshold = boost::none) {
+        std::vector<storm::storage::ParameterRegion<ValueType>> parseRegions(std::string const& inputString, std::set<typename storm::storage::ParameterRegion<ValueType>::VariableType> const& consideredVariables, boost::optional<int> const& splittingThreshold = boost::none) {
             // If the given input string looks like a file (containing a dot and there exists a file with that name),
             // we try to parse it as a file, otherwise we assume it's a region string.
             if (inputString.find(".") != std::string::npos && std::ifstream(inputString).good()) {
@@ -50,12 +50,12 @@ namespace storm {
         }
 
         template <typename ValueType>
-        storm::storage::ParameterRegion<ValueType> createRegion(std::string const& inputString, std::set<typename storm::storage::ParameterRegion<ValueType>::VariableType> const& consideredVariables, boost::optional<int> splittingThreshold= boost::none) {
+        storm::storage::ParameterRegion<ValueType> createRegion(std::string const& inputString, std::set<typename storm::storage::ParameterRegion<ValueType>::VariableType> const& consideredVariables, boost::optional<int> const& splittingThreshold = boost::none) {
             return storm::parser::ParameterRegionParser<ValueType>().createRegion(inputString, consideredVariables, splittingThreshold);
         }
 
         template <typename ValueType>
-        std::vector<storm::storage::ParameterRegion<ValueType>> parseRegions(std::string const& inputString, storm::models::ModelBase const& model, boost::optional<int> splittingThreshold= boost::none) {
+        std::vector<storm::storage::ParameterRegion<ValueType>> parseRegions(std::string const& inputString, storm::models::ModelBase const& model, boost::optional<int> const& splittingThreshold = boost::none) {
             std::set<typename storm::storage::ParameterRegion<ValueType>::VariableType> modelParameters;
             if (model.isSparseModel()) {
                 auto const& sparseModel = dynamic_cast<storm::models::sparse::Model<ValueType> const&>(model);
@@ -69,7 +69,7 @@ namespace storm {
         }
 
         template <typename ValueType>
-        std::vector<storm::storage::ParameterRegion<ValueType>> createRegion(std::string const& inputString, storm::models::ModelBase const& model, boost::optional<int> splittingThreshold= boost::none) {
+        std::vector<storm::storage::ParameterRegion<ValueType>> createRegion(std::string const& inputString, storm::models::ModelBase const& model, boost::optional<int> const& splittingThreshold = boost::none) {
             std::set<typename storm::storage::ParameterRegion<ValueType>::VariableType> modelParameters;
             if (model.isSparseModel()) {
                 auto const& sparseModel = dynamic_cast<storm::models::sparse::Model<ValueType> const&>(model);
@@ -83,7 +83,7 @@ namespace storm {
         }
         
         template <typename ValueType>
-        storm::storage::ParameterRegion<ValueType> parseRegion(std::string const& inputString, std::set<typename storm::storage::ParameterRegion<ValueType>::VariableType> const& consideredVariables, boost::optional<int> splittingThreshold= boost::none) {
+        storm::storage::ParameterRegion<ValueType> parseRegion(std::string const& inputString, std::set<typename storm::storage::ParameterRegion<ValueType>::VariableType> const& consideredVariables, boost::optional<int> const& splittingThreshold = boost::none) {
             // Handle the "empty region" case
             if (inputString == "" && consideredVariables.empty()) {
                 return storm::storage::ParameterRegion<ValueType>();
@@ -95,7 +95,7 @@ namespace storm {
         }
         
         template <typename ValueType>
-        storm::storage::ParameterRegion<ValueType> parseRegion(std::string const& inputString, storm::models::ModelBase const& model, boost::optional<int> splittingThreshold= boost::none) {
+        storm::storage::ParameterRegion<ValueType> parseRegion(std::string const& inputString, storm::models::ModelBase const& model, boost::optional<int> const& splittingThreshold = boost::none) {
             // Handle the "empty region" case
             if (inputString == "" && !model.hasParameters()) {
                 return storm::storage::ParameterRegion<ValueType>();

src/storm-pars/modelchecker/region/SparseParameterLiftingModelChecker.cpp

@@ -247,11 +247,8 @@ namespace storm {
             storm::utility::Stopwatch boundsWatch(false);
             auto numberOfPLACallsBounds = 0;
             ConstantType initBound;
-            if (minimize) {
             initBound = storm::utility::zero<ConstantType>();
-            } else {
-                initBound = storm::utility::one<ConstantType>();
-            }
+            bool first = true;
             if (useMonotonicity) {
                 if (this->isUseBoundsSet()) {
                     numberOfPLACallsBounds++;
@@ -273,18 +270,11 @@ namespace storm {
                 monotonicityWatch.stop();
                 STORM_LOG_INFO(std::endl << "Total time for monotonicity checking: " << monotonicityWatch << "." << std::endl << std::endl);
 
-                if (minimize) {
                 regionQueue.emplace(region, order, monRes, initBound);
-                } else {
-                    regionQueue.emplace(region, order, monRes, initBound);
-                }
-            } else {
-                if (minimize) {
-                    regionQueue.emplace(region, nullptr, nullptr, initBound);
+                first = false;
             } else {
                 regionQueue.emplace(region, nullptr, nullptr, initBound);
             }
-            }
 
             // The results
             boost::optional<ConstantType> value;
@@ -309,7 +299,6 @@ namespace storm {
             auto numberOfPLACalls = 0;
             auto numberOfOrderCopies = 0;
             auto numberOfMonResCopies = 0;
-            bool first = true;
             storm::utility::Stopwatch loopWatch(true);
             if (!(useMonotonicity && regionQueue.top().localMonRes->getGlobalMonotonicityResult()->isDone() && regionQueue.top().localMonRes->getGlobalMonotonicityResult()->isAllMonotonicity())) {
                 // Doing the extremal computation, only when we don't use monotonicity or there are possibly not monotone variables.
@@ -325,8 +314,9 @@ namespace storm {
                     std::vector<storm::storage::ParameterRegion<typename SparseModelType::ValueType>> newRegions;
 
                     // Check whether this region needs further investigation based on the bound of the parent region
-                    bool investigateBounds = (minimize && currBound < value.get() - storm::utility::convertNumber<ConstantType>(precision))
+                    bool investigateBounds = first || (minimize && currBound < value.get() - storm::utility::convertNumber<ConstantType>(precision))
                                              || (!minimize && currBound > value.get() + storm::utility::convertNumber<ConstantType>(precision));
+                    first = false;
                     if (investigateBounds) {
                         numberOfPLACalls++;
                         auto bounds = getBound(env, currRegion, dir, localMonotonicityResult)->template asExplicitQuantitativeCheckResult<ConstantType>().getValueVector();

src/storm-pars/parser/ParameterRegionParser.cpp

@@ -42,7 +42,7 @@ namespace storm {
         }
 
         template<typename ParametricType>
-        storm::storage::ParameterRegion<ParametricType> ParameterRegionParser<ParametricType>::parseRegion(std::string const& regionString, std::set<VariableType> const& consideredVariables, boost::optional<int> splittingThreshold) {
+        storm::storage::ParameterRegion<ParametricType> ParameterRegionParser<ParametricType>::parseRegion(std::string const& regionString, std::set<VariableType> const& consideredVariables, boost::optional<int> const& splittingThreshold) {
             Valuation lowerBoundaries;
             Valuation upperBoundaries;
             std::vector<std::string> parameterBoundaries;
@@ -66,7 +66,7 @@ namespace storm {
         }
 
         template<typename ParametricType>
-        storm::storage::ParameterRegion<ParametricType> ParameterRegionParser<ParametricType>::createRegion(std::string const& regionBound, std::set<VariableType> const& consideredVariables, boost::optional<int> splittingThreshold) {
+        storm::storage::ParameterRegion<ParametricType> ParameterRegionParser<ParametricType>::createRegion(std::string const& regionBound, std::set<VariableType> const& consideredVariables, boost::optional<int> const& splittingThreshold) {
             Valuation lowerBoundaries;
             Valuation upperBoundaries;
             std::vector<std::string> parameterBoundaries;
@@ -84,7 +84,7 @@ namespace storm {
         }
 
         template<typename ParametricType>
-        std::vector<storm::storage::ParameterRegion<ParametricType>> ParameterRegionParser<ParametricType>::parseMultipleRegions(std::string const& regionsString, std::set<VariableType> const& consideredVariables, boost::optional<int> splittingThreshold) {
+        std::vector<storm::storage::ParameterRegion<ParametricType>> ParameterRegionParser<ParametricType>::parseMultipleRegions(std::string const& regionsString, std::set<VariableType> const& consideredVariables, boost::optional<int> const& splittingThreshold) {
             std::vector<storm::storage::ParameterRegion<ParametricType>> result;
             std::vector<std::string> regionsStrVec;
             boost::split(regionsStrVec, regionsString, boost::is_any_of(";"));
@@ -97,7 +97,7 @@ namespace storm {
         }
 
         template<typename ParametricType>
-        std::vector<storm::storage::ParameterRegion<ParametricType>> ParameterRegionParser<ParametricType>::parseMultipleRegionsFromFile(std::string const& fileName, std::set<VariableType> const& consideredVariables, boost::optional<int> splittingThreshold) {
+        std::vector<storm::storage::ParameterRegion<ParametricType>> ParameterRegionParser<ParametricType>::parseMultipleRegionsFromFile(std::string const& fileName, std::set<VariableType> const& consideredVariables, boost::optional<int> const& splittingThreshold) {
      
             // Open file and initialize result.
             std::ifstream inputFileStream;

src/storm-pars/parser/ParameterRegionParser.h

@@ -25,21 +25,21 @@ namespace storm {
              * Parse a single region from a string of the form "0.3<=p<=0.5,0.4<=q<=0.7".
              *
              */
-            static storm::storage::ParameterRegion<ParametricType> parseRegion(std::string const& regionString, std::set<VariableType> const& consideredVariables, boost::optional<int> splittingThreshold = boost::none);
-            static storm::storage::ParameterRegion<ParametricType> createRegion(std::string const& regionBound, std::set<VariableType> const& consideredVariables, boost::optional<int> splittingThreshold = boost::none);
+            static storm::storage::ParameterRegion<ParametricType> parseRegion(std::string const& regionString, std::set<VariableType> const& consideredVariables, boost::optional<int> const& splittingThreshold = boost::none);
+            static storm::storage::ParameterRegion<ParametricType> createRegion(std::string const& regionBound, std::set<VariableType> const& consideredVariables, boost::optional<int> const& splittingThreshold = boost::none);
 
             /*
              * Parse a vector of region from a string of the form "0.3<=p<=0.5,0.4<=q<=0.7;0.1<=p<=0.3,0.2<=q<=0.4".
              *
              */
-            static std::vector<storm::storage::ParameterRegion<ParametricType>> parseMultipleRegions(std::string const& regionsString, std::set<VariableType> const& consideredVariables, boost::optional<int> splittingThreshold = boost::none);
+            static std::vector<storm::storage::ParameterRegion<ParametricType>> parseMultipleRegions(std::string const& regionsString, std::set<VariableType> const& consideredVariables, boost::optional<int> const& splittingThreshold = boost::none);
             
 
             /*
              * Parse multiple regions from a file
              *
              */
-            static std::vector<storm::storage::ParameterRegion<ParametricType>> parseMultipleRegionsFromFile(std::string const& fileName, std::set<VariableType> const& consideredVariables, boost::optional<int> splittingThreshold = boost::none);
+            static std::vector<storm::storage::ParameterRegion<ParametricType>> parseMultipleRegionsFromFile(std::string const& fileName, std::set<VariableType> const& consideredVariables, boost::optional<int> const& splittingThreshold = boost::none);
             
         };
     }

src/storm-parsers/parser/PrismParser.cpp

@@ -453,7 +453,7 @@ namespace storm {
                 return false;
             }
             return true;
-        };
+        }
 
         bool PrismParser::isFreshIdentifier(std::string const& identifier) {
             if (!this->secondRun && this->manager->hasVariable(identifier)) {