Merge remote-tracking branch 'upstream/master'

resources/3rdparty/CMakeLists.txt

@@ -404,6 +404,12 @@ include(${STORM_3RDPARTY_SOURCE_DIR}/include_xerces.cmake)
 ##
 #############################################################
 
+if(STORM_SHIPPED_CARL)
+    set(sylvan_dep carl)
+else()
+    set(sylvan_dep lib_carl)
+endif()
+
 ExternalProject_Add(
         sylvan
         DOWNLOAD_COMMAND ""
@@ -416,6 +422,7 @@ ExternalProject_Add(
         INSTALL_DIR ${STORM_3RDPARTY_BINARY_DIR}/sylvan
         LOG_CONFIGURE ON
         LOG_BUILD ON
+        DEPENDS ${sylvan_dep}
         BUILD_BYPRODUCTS ${STORM_3RDPARTY_BINARY_DIR}/sylvan/src/libsylvan${STATIC_EXT}
 )
 
@@ -427,9 +434,7 @@ message(STATUS "Storm - Using shipped version of sylvan.")
 message(STATUS "Storm - Linking with sylvan.")
 add_imported_library(sylvan STATIC ${Sylvan_LIBRARY} ${Sylvan_INCLUDE_DIR})
 add_dependencies(sylvan_STATIC sylvan)
-if(STORM_SHIPPED_CARL)
-	add_dependencies(sylvan carl)
-endif()
+
 list(APPEND STORM_DEP_TARGETS sylvan_STATIC)
 
 find_package(Hwloc QUIET REQUIRED)

src/storm-pars-cli/storm-pars.cpp

@@ -209,28 +209,37 @@ namespace storm {
             std::function<std::unique_ptr<storm::modelchecker::CheckResult>(std::shared_ptr<storm::logic::Formula const> const& formula)> verificationCallback;
             std::function<void(std::unique_ptr<storm::modelchecker::CheckResult> const&)> postprocessingCallback;
             
+            STORM_PRINT_AND_LOG(std::endl);
+            if (regionSettings.isHypothesisSet()) {
+                STORM_PRINT_AND_LOG("Checking hypothesis " << regionSettings.getHypothesis() << " on ");
+            } else {
+                STORM_PRINT_AND_LOG("Analyzing ");
+            }
             if (regions.size() == 1) {
-                STORM_PRINT_AND_LOG(std::endl << "Analyzing parameter region " << regions.front());
+                STORM_PRINT_AND_LOG("parameter region " << regions.front());
             } else {
-                STORM_PRINT_AND_LOG(std::endl << "Analyzing " << regions.size() << " parameter regions");
+                STORM_PRINT_AND_LOG(regions.size() << " parameter regions");
             }
-                
             auto engine = regionSettings.getRegionCheckEngine();
             STORM_PRINT_AND_LOG(" using " << engine);
         
             // Check the given set of regions with or without refinement
             if (regionSettings.isRefineSet()) {
                 STORM_LOG_THROW(regions.size() == 1, storm::exceptions::NotSupportedException, "Region refinement is not supported for multiple initial regions.");
-                STORM_PRINT_AND_LOG(" with iterative refinement until " << (1.0 - regionSettings.getRefinementThreshold()) * 100.0 << "% is covered." << std::endl);
+                STORM_PRINT_AND_LOG(" with iterative refinement until " << (1.0 - regionSettings.getCoverageThreshold()) * 100.0 << "% is covered." << (regionSettings.isDepthLimitSet() ? " Depth limit is " + std::to_string(regionSettings.getDepthLimit()) + "." : "") << std::endl);
                 verificationCallback = [&] (std::shared_ptr<storm::logic::Formula const> const& formula) {
-                                        ValueType refinementThreshold = storm::utility::convertNumber<ValueType>(regionSettings.getRefinementThreshold());
-                                        std::unique_ptr<storm::modelchecker::RegionRefinementCheckResult<ValueType>> result = storm::api::checkAndRefineRegionWithSparseEngine<ValueType>(model, storm::api::createTask<ValueType>(formula, true), regions.front(), refinementThreshold, engine);
+                                        ValueType refinementThreshold = storm::utility::convertNumber<ValueType>(regionSettings.getCoverageThreshold());
+                                        boost::optional<uint64_t> optionalDepthLimit;
+                                        if (regionSettings.isDepthLimitSet()) {
+                                            optionalDepthLimit = regionSettings.getDepthLimit();
+                                        }
+                                        std::unique_ptr<storm::modelchecker::RegionRefinementCheckResult<ValueType>> result = storm::api::checkAndRefineRegionWithSparseEngine<ValueType>(model, storm::api::createTask<ValueType>(formula, true), regions.front(), engine, refinementThreshold, optionalDepthLimit, regionSettings.getHypothesis());
                                         return result;
                                     };
             } else {
                 STORM_PRINT_AND_LOG("." << std::endl);
                 verificationCallback = [&] (std::shared_ptr<storm::logic::Formula const> const& formula) {
-                                        std::unique_ptr<storm::modelchecker::CheckResult> result = storm::api::checkRegionsWithSparseEngine<ValueType>(model, storm::api::createTask<ValueType>(formula, true), regions, engine);
+                                        std::unique_ptr<storm::modelchecker::CheckResult> result = storm::api::checkRegionsWithSparseEngine<ValueType>(model, storm::api::createTask<ValueType>(formula, true), regions, engine, regionSettings.getHypothesis());
                                         return result;
                                     };
             }

src/storm-pars/api/export.h

@@ -0,0 +1,34 @@
+#include "storm/utility/file.h"
+#include "storm/utility/macros.h"
+#include "storm/exceptions/NotSupportedException.h"
+#include "storm/analysis/GraphConditions.h"
+
+namespace storm {
+    namespace api {
+
+        template <typename ValueType>
+        void exportParametricResultToFile(ValueType const& result, storm::analysis::ConstraintCollector<ValueType> const& constraintCollector, std::string const& path) {
+            STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Cannot export non-parametric result.");
+        }
+
+        template <>
+        inline void exportParametricResultToFile(storm::RationalFunction const& result, storm::analysis::ConstraintCollector<storm::RationalFunction> const& constraintCollector, std::string const& path) {
+            std::ofstream filestream;
+            storm::utility::openFile(path, filestream);
+            filestream << "$Parameters: ";
+            std::set<storm::RationalFunctionVariable> vars = result.gatherVariables();
+            std::copy(vars.begin(), vars.end(), std::ostream_iterator<storm::RationalFunctionVariable>(filestream, "; "));
+            filestream << std::endl;
+            filestream << "$Result: " << result.toString(false, true) << std::endl;
+            filestream << "$Well-formed Constraints: " << std::endl;
+            std::vector<std::string> stringConstraints;
+            std::transform(constraintCollector.getWellformedConstraints().begin(), constraintCollector.getWellformedConstraints().end(), std::back_inserter(stringConstraints), [](carl::Formula<typename storm::Polynomial::PolyType> const& c) ->  std::string { return c.toString();});
+            std::copy(stringConstraints.begin(), stringConstraints.end(), std::ostream_iterator<std::string>(filestream, "\n"));
+            filestream << "$Graph-preserving Constraints: " << std::endl;
+            stringConstraints.clear();
+            std::transform(constraintCollector.getGraphPreservingConstraints().begin(), constraintCollector.getGraphPreservingConstraints().end(), std::back_inserter(stringConstraints), [](carl::Formula<typename storm::Polynomial::PolyType> const& c) ->  std::string { return c.toString();});
+            std::copy(stringConstraints.begin(), stringConstraints.end(), std::ostream_iterator<std::string>(filestream, "\n"));
+            storm::utility::closeFile(filestream);
+        }
+    }
+}

src/storm-pars/api/region.h

@@ -13,6 +13,7 @@
 #include "storm-pars/modelchecker/region/SparseMdpParameterLiftingModelChecker.h"
 #include "storm-pars/modelchecker/region/ValidatingSparseMdpParameterLiftingModelChecker.h"
 #include "storm-pars/modelchecker/region/ValidatingSparseDtmcParameterLiftingModelChecker.h"
+#include "storm-pars/modelchecker/region/RegionResultHypothesis.h"
 #include "storm-pars/parser/ParameterRegionParser.h"
 #include "storm-pars/storage/ParameterRegion.h"
 #include "storm-pars/utility/parameterlifting.h"
@@ -153,21 +154,33 @@ namespace storm {
         }
         
         template <typename ValueType>
-        std::unique_ptr<storm::modelchecker::RegionCheckResult<ValueType>> checkRegionsWithSparseEngine(std::shared_ptr<storm::models::sparse::Model<ValueType>> const& model, storm::modelchecker::CheckTask<storm::logic::Formula, ValueType> const& task, std::vector<storm::storage::ParameterRegion<ValueType>> const& regions, storm::modelchecker::RegionCheckEngine engine) {
+        std::unique_ptr<storm::modelchecker::RegionCheckResult<ValueType>> checkRegionsWithSparseEngine(std::shared_ptr<storm::models::sparse::Model<ValueType>> const& model, storm::modelchecker::CheckTask<storm::logic::Formula, ValueType> const& task, std::vector<storm::storage::ParameterRegion<ValueType>> const& regions, storm::modelchecker::RegionCheckEngine engine, std::vector<storm::modelchecker::RegionResultHypothesis> const& hypotheses, bool sampleVerticesOfRegions) {
             auto regionChecker = initializeRegionModelChecker(model, task, engine);
-            return regionChecker->analyzeRegions(regions, true);
+            return regionChecker->analyzeRegions(regions, hypotheses, sampleVerticesOfRegions);
         }
     
-        
         template <typename ValueType>
-        std::unique_ptr<storm::modelchecker::RegionRefinementCheckResult<ValueType>> checkAndRefineRegionWithSparseEngine(std::shared_ptr<storm::models::sparse::Model<ValueType>> const& model, storm::modelchecker::CheckTask<storm::logic::Formula, ValueType> const& task, storm::storage::ParameterRegion<ValueType> const& region, ValueType const& refinementThreshold, storm::modelchecker::RegionCheckEngine engine) {
+        std::unique_ptr<storm::modelchecker::RegionCheckResult<ValueType>> checkRegionsWithSparseEngine(std::shared_ptr<storm::models::sparse::Model<ValueType>> const& model, storm::modelchecker::CheckTask<storm::logic::Formula, ValueType> const& task, std::vector<storm::storage::ParameterRegion<ValueType>> const& regions, storm::modelchecker::RegionCheckEngine engine, storm::modelchecker::RegionResultHypothesis const& hypothesis = storm::modelchecker::RegionResultHypothesis::Unknown, bool sampleVerticesOfRegions = false) {
+            std::vector<storm::modelchecker::RegionResultHypothesis> hypotheses(regions.size(), hypothesis);
+            return checkRegionsWithSparseEngine(model, task, regions, engine, hypotheses, sampleVerticesOfRegions);
+        }
+    
+        /*!
+         * Checks and iteratively refines the given region with the sparse engine
+         * @param engine The considered region checking engine
+         * @param coverageThreshold if given, the refinement stops as soon as the fraction of the area of the subregions with inconclusive result is less then this threshold
+         * @param refinementDepthThreshold if given, the refinement stops at the given depth. depth=0 means no refinement.
+         * @param hypothesis if not 'unknown', it is only checked whether the hypothesis holds (and NOT the complementary result).
+         */
+        template <typename ValueType>
+        std::unique_ptr<storm::modelchecker::RegionRefinementCheckResult<ValueType>> checkAndRefineRegionWithSparseEngine(std::shared_ptr<storm::models::sparse::Model<ValueType>> const& model, storm::modelchecker::CheckTask<storm::logic::Formula, ValueType> const& task, storm::storage::ParameterRegion<ValueType> const& region, storm::modelchecker::RegionCheckEngine engine, boost::optional<ValueType> const& coverageThreshold, boost::optional<uint64_t> const& refinementDepthThreshold = boost::none, storm::modelchecker::RegionResultHypothesis hypothesis = storm::modelchecker::RegionResultHypothesis::Unknown) {
             auto regionChecker = initializeRegionModelChecker(model, task, engine);
-            return regionChecker->performRegionRefinement(region, refinementThreshold);
+            return regionChecker->performRegionRefinement(region, coverageThreshold, refinementDepthThreshold, hypothesis);
         }
         
 
         template <typename ValueType>
-        void exportRegionCheckResultToFile(std::unique_ptr<storm::modelchecker::CheckResult> const& checkResult, std::string const& filename) {
+        void exportRegionCheckResultToFile(std::unique_ptr<storm::modelchecker::CheckResult> const& checkResult, std::string const& filename, bool onlyConclusiveResults = false) {
 
             auto const* regionCheckResult = dynamic_cast<storm::modelchecker::RegionCheckResult<ValueType> const*>(checkResult.get());
             STORM_LOG_THROW(regionCheckResult != nullptr, storm::exceptions::UnexpectedException, "Can not export region check result: The given checkresult does not have the expected type.");
@@ -175,7 +188,9 @@ namespace storm {
             std::ofstream filestream;
             storm::utility::openFile(filename, filestream);
             for (auto const& res : regionCheckResult->getRegionResults()) {
+                if (!onlyConclusiveResults || res.second == storm::modelchecker::RegionResult::AllViolated || res.second == storm::modelchecker::RegionResult::AllSat) {
                     filestream << res.second << ": " << res.first << std::endl;
+                }
             }
         }
     

src/storm-pars/api/storm-pars.h

@@ -1,3 +1,4 @@
 #pragma once
 
 #include "storm-pars/api/region.h"
+#include "storm-pars/api/export.h"

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

@@ -28,31 +28,40 @@ namespace storm {
             }
         
             template <typename ParametricType>
-            std::unique_ptr<storm::modelchecker::RegionCheckResult<ParametricType>> RegionModelChecker<ParametricType>::analyzeRegions(std::vector<storm::storage::ParameterRegion<ParametricType>> const& regions, bool sampleVerticesOfRegion) {
+            std::unique_ptr<storm::modelchecker::RegionCheckResult<ParametricType>> RegionModelChecker<ParametricType>::analyzeRegions(std::vector<storm::storage::ParameterRegion<ParametricType>> const& regions, std::vector<RegionResultHypothesis> const& hypotheses, bool sampleVerticesOfRegion) {
                 
+                STORM_LOG_THROW(regions.size() == hypotheses.size(), storm::exceptions::InvalidArgumentException, "The number of regions and the number of hypotheses do not match");
                 std::vector<std::pair<storm::storage::ParameterRegion<ParametricType>, storm::modelchecker::RegionResult>> result;
                 
+                auto hypothesisIt = hypotheses.begin();
                 for (auto const& region : regions) {
-                    storm::modelchecker::RegionResult regionRes = analyzeRegion(region, storm::modelchecker::RegionResult::Unknown, sampleVerticesOfRegion);
+                    storm::modelchecker::RegionResult regionRes = analyzeRegion(region, *hypothesisIt, storm::modelchecker::RegionResult::Unknown, sampleVerticesOfRegion);
                     result.emplace_back(region, regionRes);
+                    ++hypothesisIt;
                 }
                 
                 return std::make_unique<storm::modelchecker::RegionCheckResult<ParametricType>>(std::move(result));
             }
 
             template <typename ParametricType>
-            std::unique_ptr<storm::modelchecker::RegionRefinementCheckResult<ParametricType>> RegionModelChecker<ParametricType>::performRegionRefinement(storm::storage::ParameterRegion<ParametricType> const& region, ParametricType const& threshold) {
+            std::unique_ptr<storm::modelchecker::RegionRefinementCheckResult<ParametricType>> RegionModelChecker<ParametricType>::performRegionRefinement(storm::storage::ParameterRegion<ParametricType> const& region, boost::optional<ParametricType> const& coverageThreshold, boost::optional<uint64_t> depthThreshold, RegionResultHypothesis const& hypothesis) {
                 STORM_LOG_INFO("Applying refinement on region: " << region.toString(true) << " .");
                 
-                auto thresholdAsCoefficient = storm::utility::convertNumber<CoefficientType>(threshold);
+                auto thresholdAsCoefficient = coverageThreshold ? storm::utility::convertNumber<CoefficientType>(coverageThreshold.get()) : storm::utility::zero<CoefficientType>();
                 auto areaOfParameterSpace = region.area();
                 auto fractionOfUndiscoveredArea = storm::utility::one<CoefficientType>();
                 auto fractionOfAllSatArea = storm::utility::zero<CoefficientType>();
                 auto fractionOfAllViolatedArea = storm::utility::zero<CoefficientType>();
                 
-                std::queue<std::pair<storm::storage::ParameterRegion<ParametricType>, RegionResult>> unprocessedRegions;
+                // The resulting (sub-)regions
                 std::vector<std::pair<storm::storage::ParameterRegion<ParametricType>, RegionResult>> result;
+                
+                // FIFO queues storing the data for the regions that we still need to process.
+                std::queue<std::pair<storm::storage::ParameterRegion<ParametricType>, RegionResult>> unprocessedRegions;
+                std::queue<uint64_t> refinementDepths;
                 unprocessedRegions.emplace(region, RegionResult::Unknown);
+                refinementDepths.push(0);
+                
                 uint_fast64_t numOfAnalyzedRegions = 0;
                 CoefficientType displayedProgress = storm::utility::zero<CoefficientType>();
                 if (storm::settings::getModule<storm::settings::modules::CoreSettings>().isShowStatisticsSet()) {
@@ -69,12 +78,13 @@ namespace storm {
                     displayedProgress = storm::utility::zero<CoefficientType>();
                 }
 
-                while (fractionOfUndiscoveredArea > thresholdAsCoefficient) {
-                    STORM_LOG_THROW(!unprocessedRegions.empty(), storm::exceptions::InvalidStateException, "Threshold for undiscovered area not reached but no unprocessed regions left.");
-                    STORM_LOG_INFO("Analyzing region #" << numOfAnalyzedRegions << " (" << storm::utility::convertNumber<double>(fractionOfUndiscoveredArea) * 100 << "% still unknown)");
+                while (fractionOfUndiscoveredArea > thresholdAsCoefficient && !unprocessedRegions.empty()) {
+                    assert(unprocessedRegions.size() == refinementDepths.size());
+                    uint64_t currentDepth = refinementDepths.front();
+                    STORM_LOG_INFO("Analyzing region #" << numOfAnalyzedRegions << " (Refinement depth " << currentDepth << "; " << storm::utility::convertNumber<double>(fractionOfUndiscoveredArea) * 100 << "% still unknown)");
                     auto& currentRegion = unprocessedRegions.front().first;
                     auto& res = unprocessedRegions.front().second;
-                    res = analyzeRegion(currentRegion, res, false);
+                    res = analyzeRegion(currentRegion, hypothesis, res, false);
                     switch (res) {
                         case RegionResult::AllSat:
                             fractionOfUndiscoveredArea -= currentRegion.area() / areaOfParameterSpace;
@@ -87,18 +97,26 @@ namespace storm {
                             result.push_back(std::move(unprocessedRegions.front()));
                             break;
                         default:
-                            std::vector<storm::storage::ParameterRegion<ParametricType>> newRegions;
-                            currentRegion.split(currentRegion.getCenterPoint(), newRegions);
-                            RegionResult initResForNewRegions = (res == RegionResult::CenterSat) ? RegionResult::ExistsSat :
-                                                                     ((res == RegionResult::CenterViolated) ? RegionResult::ExistsViolated :
-                                                                      RegionResult::Unknown);
-                            for(auto& newRegion : newRegions) {
-                                unprocessedRegions.emplace(std::move(newRegion), initResForNewRegions);
+                            // Split the region as long as the desired refinement depth is not reached.
+                            if (!depthThreshold || currentDepth < depthThreshold.get()) {
+                                std::vector<storm::storage::ParameterRegion<ParametricType>> newRegions;
+                                currentRegion.split(currentRegion.getCenterPoint(), newRegions);
+                                RegionResult initResForNewRegions = (res == RegionResult::CenterSat) ? RegionResult::ExistsSat :
+                                                                         ((res == RegionResult::CenterViolated) ? RegionResult::ExistsViolated :
+                                                                          RegionResult::Unknown);
+                                for (auto& newRegion : newRegions) {
+                                    unprocessedRegions.emplace(std::move(newRegion), initResForNewRegions);
+                                    refinementDepths.push(currentDepth + 1);
+                                }
+                            } else {
+                                // If the region is not further refined, it is still added to the result
+                                result.push_back(std::move(unprocessedRegions.front()));
                             }
                             break;
                     }
                     ++numOfAnalyzedRegions;
                     unprocessedRegions.pop();
+                    refinementDepths.pop();
                     if (storm::settings::getModule<storm::settings::modules::CoreSettings>().isShowStatisticsSet()) {
                         while (displayedProgress < storm::utility::one<CoefficientType>() - fractionOfUndiscoveredArea) {
                             STORM_PRINT_AND_LOG("#");
@@ -107,6 +125,12 @@ namespace storm {
                     }
                 }
                 
+                // Add the still unprocessed regions to the result
+                while (!unprocessedRegions.empty()) {
+                    result.push_back(std::move(unprocessedRegions.front()));
+                    unprocessedRegions.pop();
+                }
+                
                 if (storm::settings::getModule<storm::settings::modules::CoreSettings>().isShowStatisticsSet()) {
                     while (displayedProgress < storm::utility::one<CoefficientType>()) {
                         STORM_PRINT_AND_LOG("-");

src/storm-pars/modelchecker/region/RegionModelChecker.h

@@ -5,6 +5,7 @@
 #include "storm-pars/modelchecker/results/RegionCheckResult.h"
 #include "storm-pars/modelchecker/results/RegionRefinementCheckResult.h"
 #include "storm-pars/modelchecker/region/RegionResult.h"
+#include "storm-pars/modelchecker/region/RegionResultHypothesis.h"
 #include "storm-pars/storage/ParameterRegion.h"
 
 #include "storm/models/ModelBase.h"
@@ -27,22 +28,29 @@ namespace storm {
             
             /*!
              * Analyzes the given region.
-             * An initial region result can be given to simplify the analysis (e.g. if the initial result is ExistsSat, we do not check for AllViolated).
-             * If supported by this model checker, it is possible to sample the vertices of the region whenever AllSat/AllViolated could not be shown.
+             * @param hypothesis if not 'unknown', the region checker only tries to show the hypothesis
+             * @param initialResult encodes what is already known about this region
+             * @param sampleVerticesOfRegion enables sampling of the vertices of the region in cases where AllSat/AllViolated could not be shown.
              */
-            virtual RegionResult analyzeRegion(storm::storage::ParameterRegion<ParametricType> const& region, RegionResult const& initialResult = RegionResult::Unknown, bool sampleVerticesOfRegion = false) = 0;
+            virtual RegionResult analyzeRegion(storm::storage::ParameterRegion<ParametricType> const& region, RegionResultHypothesis const& hypothesis = RegionResultHypothesis::Unknown, RegionResult const& initialResult = RegionResult::Unknown, bool sampleVerticesOfRegion = false) = 0;
             
              /*!
              * Analyzes the given regions.
+             * @param hypothesis if not 'unknown', we only try to show the hypothesis for each region
+
              * If supported by this model checker, it is possible to sample the vertices of the regions whenever AllSat/AllViolated could not be shown.
              */
-            std::unique_ptr<storm::modelchecker::RegionCheckResult<ParametricType>> analyzeRegions(std::vector<storm::storage::ParameterRegion<ParametricType>> const& regions, bool sampleVerticesOfRegion = false) ;
+            std::unique_ptr<storm::modelchecker::RegionCheckResult<ParametricType>> analyzeRegions(std::vector<storm::storage::ParameterRegion<ParametricType>> const& regions, std::vector<RegionResultHypothesis> const& hypotheses, bool sampleVerticesOfRegion = false) ;
             
             /*!
              * Iteratively refines the region until the region analysis yields a conclusive result (AllSat or AllViolated).
-             * The refinement stops as soon as the fraction of the area of the subregions with inconclusive result is less then the given threshold
+             * @param region the considered region
+             * @param coverageThreshold if given, the refinement stops as soon as the fraction of the area of the subregions with inconclusive result is less then this threshold
+             * @param depthThreshold if given, the refinement stops at the given depth. depth=0 means no refinement.
+             * @param hypothesis if not 'unknown', it is only checked whether the hypothesis holds within the given region.
+             *
              */
-            std::unique_ptr<storm::modelchecker::RegionRefinementCheckResult<ParametricType>> performRegionRefinement(storm::storage::ParameterRegion<ParametricType> const& region, ParametricType const& threshold);
+            std::unique_ptr<storm::modelchecker::RegionRefinementCheckResult<ParametricType>> performRegionRefinement(storm::storage::ParameterRegion<ParametricType> const& region, boost::optional<ParametricType> const& coverageThreshold, boost::optional<uint64_t> depthThreshold = boost::none, RegionResultHypothesis const& hypothesis = RegionResultHypothesis::Unknown);
             
         };
 

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

@@ -0,0 +1,25 @@
+#include "storm-pars/modelchecker/region/RegionResultHypothesis.h"
+
+#include "storm/utility/macros.h"
+#include "storm/exceptions/NotImplementedException.h"
+
+namespace storm {
+    namespace modelchecker {
+        std::ostream& operator<<(std::ostream& os, RegionResultHypothesis const& regionResultHypothesis) {
+            switch (regionResultHypothesis) {
+                case RegionResultHypothesis::Unknown:
+                    os << "Unknown";
+                    break;
+                case RegionResultHypothesis::AllSat:
+                    os << "AllSat?";
+                    break;
+                case RegionResultHypothesis::AllViolated:
+                    os << "AllViolated?";
+                    break;
+                default:
+                    STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Could not get a string from the region result hypothesis. The case has not been implemented");
+            }
+            return os;
+        }
+    }
+}

src/storm-pars/modelchecker/region/RegionResultHypothesis.h

@@ -0,0 +1,19 @@
+#pragma once
+
+#include <ostream>
+
+namespace storm {
+    namespace modelchecker {
+        /*!
+         * hypothesis for the result for a single Parameter Region
+         */
+        enum class RegionResultHypothesis {
+            Unknown,
+            AllSat,
+            AllViolated
+        };
+        
+        std::ostream& operator<<(std::ostream& os, RegionResultHypothesis const& regionResultHypothesis);
+    }
+}
+

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

@@ -47,8 +47,8 @@ namespace storm {
         }
         
         template <typename SparseModelType, typename ConstantType>
-        RegionResult SparseParameterLiftingModelChecker<SparseModelType, ConstantType>::analyzeRegion(storm::storage::ParameterRegion<typename SparseModelType::ValueType> const& region, RegionResult const& initialResult, bool sampleVerticesOfRegion) {
-        
+        RegionResult SparseParameterLiftingModelChecker<SparseModelType, ConstantType>::analyzeRegion(storm::storage::ParameterRegion<typename SparseModelType::ValueType> const& region, RegionResultHypothesis const& hypothesis, RegionResult const& initialResult, bool sampleVerticesOfRegion) {
+
             STORM_LOG_THROW(this->currentCheckTask->isOnlyInitialStatesRelevantSet(), storm::exceptions::NotSupportedException, "Analyzing regions with parameter lifting requires a property where only the value in the initial states is relevant.");
             STORM_LOG_THROW(this->currentCheckTask->isBoundSet(), storm::exceptions::NotSupportedException, "Analyzing regions with parameter lifting requires a bounded property.");
             STORM_LOG_THROW(this->parametricModel->getInitialStates().getNumberOfSetBits() == 1, storm::exceptions::NotSupportedException, "Analyzing regions with parameter lifting requires a model with a single initial state.");
@@ -56,12 +56,12 @@ namespace storm {
             RegionResult result = initialResult;
 
             // Check if we need to check the formula on one point to decide whether to show AllSat or AllViolated
-            if (result == RegionResult::Unknown) {
+            if (hypothesis == RegionResultHypothesis::Unknown && result == RegionResult::Unknown) {
                  result = getInstantiationChecker().check(region.getCenterPoint())->asExplicitQualitativeCheckResult()[*this->parametricModel->getInitialStates().begin()] ? RegionResult::CenterSat : RegionResult::CenterViolated;
             }
             
-            // try to prove AllSat or AllViolated, depending on the obtained result
-            if (result == RegionResult::ExistsSat || result == RegionResult::CenterSat) {
+            // try to prove AllSat or AllViolated, depending on the hypothesis or the current result
+            if (hypothesis == RegionResultHypothesis::AllSat || result == RegionResult::ExistsSat || result == RegionResult::CenterSat) {
                 // show AllSat:
                 storm::solver::OptimizationDirection parameterOptimizationDirection = isLowerBound(this->currentCheckTask->getBound().comparisonType) ? storm::solver::OptimizationDirection::Minimize : storm::solver::OptimizationDirection::Maximize;
                 if (this->check(region, parameterOptimizationDirection)->asExplicitQualitativeCheckResult()[*this->parametricModel->getInitialStates().begin()]) {
@@ -69,7 +69,7 @@ namespace storm {
                 } else if (sampleVerticesOfRegion) {
                     result = sampleVertices(region, result);
                 }
-            } else if (result == RegionResult::ExistsViolated || result == RegionResult::CenterViolated) {
+            } else if (hypothesis == RegionResultHypothesis::AllViolated || result == RegionResult::ExistsViolated || result == RegionResult::CenterViolated) {
                 // show AllViolated:
                 storm::solver::OptimizationDirection parameterOptimizationDirection = isLowerBound(this->currentCheckTask->getBound().comparisonType) ? storm::solver::OptimizationDirection::Maximize : storm::solver::OptimizationDirection::Minimize;
                 if (!this->check(region, parameterOptimizationDirection)->asExplicitQualitativeCheckResult()[*this->parametricModel->getInitialStates().begin()]) {

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

@@ -28,12 +28,8 @@ namespace storm {
 
             /*!
              * Analyzes the given region by means of parameter lifting.
-             * We first check whether there is one point in the region for which the property is satisfied/violated.
-             * If the given initialResults already indicates that there is such a point, this step is skipped.
-             * Then, we check whether ALL points in the region violate/satisfy the property
-             *
              */
-            virtual RegionResult analyzeRegion(storm::storage::ParameterRegion<typename SparseModelType::ValueType> const& region, RegionResult const& initialResult = RegionResult::Unknown, bool sampleVerticesOfRegion = false) override;
+            virtual RegionResult analyzeRegion(storm::storage::ParameterRegion<typename SparseModelType::ValueType> const& region, RegionResultHypothesis const& hypothesis = RegionResultHypothesis::Unknown, RegionResult const& initialResult = RegionResult::Unknown, bool sampleVerticesOfRegion = false) override;
 
             /*!
              * Analyzes the 2^#parameters corner points of the given region.

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

@@ -28,9 +28,10 @@ namespace storm {
         };
  
         template <typename SparseModelType, typename ImpreciseType, typename PreciseType>
-        RegionResult ValidatingSparseParameterLiftingModelChecker<SparseModelType, ImpreciseType, PreciseType>::analyzeRegion(storm::storage::ParameterRegion<typename SparseModelType::ValueType> const& region, RegionResult const& initialResult, bool sampleVerticesOfRegion) {
+        RegionResult ValidatingSparseParameterLiftingModelChecker<SparseModelType, ImpreciseType, PreciseType>::analyzeRegion(storm::storage::ParameterRegion<typename SparseModelType::ValueType> const& region, RegionResultHypothesis const& hypothesis, RegionResult const& initialResult, bool sampleVerticesOfRegion) {
+
         
-            RegionResult currentResult = getImpreciseChecker().analyzeRegion(region, initialResult);
+            RegionResult currentResult = getImpreciseChecker().analyzeRegion(region, hypothesis, initialResult, false);
             
             if (currentResult == RegionResult::AllSat || currentResult == RegionResult::AllViolated) {
                 applyHintsToPreciseChecker();
@@ -48,13 +49,15 @@ namespace storm {
                     currentResult = RegionResult::Unknown;
                     ++numOfWrongRegions;
                     
-                    // Check the other direction
-                    parameterOptDir = storm::solver::invert(parameterOptDir);
-                    preciseResult = getPreciseChecker().check(region, parameterOptDir)->asExplicitQualitativeCheckResult()[*getPreciseChecker().getConsideredParametricModel().getInitialStates().begin()];
-                    if (preciseResult && parameterOptDir == getPreciseChecker().getCurrentCheckTask().getOptimizationDirection()) {
-                        currentResult = RegionResult::AllSat;
-                    } else if (!preciseResult && parameterOptDir == storm::solver::invert(getPreciseChecker().getCurrentCheckTask().getOptimizationDirection())) {
-                        currentResult = RegionResult::AllViolated;
+                    // Check the other direction in case no hypothesis was given
+                    if (hypothesis == RegionResultHypothesis::Unknown) {
+                        parameterOptDir = storm::solver::invert(parameterOptDir);
+                        preciseResult = getPreciseChecker().check(region, parameterOptDir)->asExplicitQualitativeCheckResult()[*getPreciseChecker().getConsideredParametricModel().getInitialStates().begin()];
+                        if (preciseResult && parameterOptDir == getPreciseChecker().getCurrentCheckTask().getOptimizationDirection()) {
+                            currentResult = RegionResult::AllSat;
+                        } else if (!preciseResult && parameterOptDir == storm::solver::invert(getPreciseChecker().getCurrentCheckTask().getOptimizationDirection())) {
+                            currentResult = RegionResult::AllViolated;
+                        }
                     }
                 }
             }

src/storm-pars/modelchecker/region/ValidatingSparseParameterLiftingModelChecker.h

@@ -23,7 +23,7 @@ namespace storm {
              * We first apply unsound solution methods (standard value iteratio with doubles) and then validate the obtained result
              * by means of exact and soud methods.
              */
-            virtual RegionResult analyzeRegion(storm::storage::ParameterRegion<typename SparseModelType::ValueType> const& region, RegionResult const& initialResult = RegionResult::Unknown, bool sampleVerticesOfRegion = false) override;
+            virtual RegionResult analyzeRegion(storm::storage::ParameterRegion<typename SparseModelType::ValueType> const& region, RegionResultHypothesis const& hypothesis = RegionResultHypothesis::Unknown, RegionResult const& initialResult = RegionResult::Unknown, bool sampleVerticesOfRegion = false) override;
 
         protected:
             

src/storm-pars/modelchecker/results/RegionRefinementCheckResult.cpp

@@ -58,6 +58,9 @@ namespace storm {
                         bool currRegionComplete = false;
                         CoefficientType coveredArea = storm::utility::zero<CoefficientType>();
                         for (auto const& r : this->getRegionResults()) {
+                            if (r.second != storm::modelchecker::RegionResult::AllSat && r.second != storm::modelchecker::RegionResult::AllViolated) {
+                                continue;
+                            }
                             CoefficientType interesctionSizeY = std::min(yUpper, r.first.getUpperBoundary(y)) - std::max(yLower, r.first.getLowerBoundary(y));
                             interesctionSizeY = std::max(interesctionSizeY, storm::utility::zero<CoefficientType>());
                             CoefficientType interesctionSizeX = std::min(xUpper, r.first.getUpperBoundary(x)) - std::max(xLower, r.first.getLowerBoundary(x));

src/storm-pars/settings/modules/RegionSettings.cpp

@@ -1,3 +1,4 @@
+#include <storm-pars/modelchecker/region/RegionResultHypothesis.h>
 #include "storm-pars/settings/modules/RegionSettings.h"
 
 #include "storm/settings/Option.h"
@@ -7,6 +8,7 @@
 
 #include "storm/utility/macros.h"
 #include "storm/exceptions/IllegalArgumentValueException.h"
+#include "storm/exceptions/InvalidOperationException.h"
 
 namespace storm {
     namespace settings {
@@ -15,6 +17,8 @@ namespace storm {
             const std::string RegionSettings::moduleName = "region";
             const std::string RegionSettings::regionOptionName = "region";
             const std::string RegionSettings::regionShortOptionName = "reg";
+            const std::string RegionSettings::hypothesisOptionName = "hypothesis";
+            const std::string RegionSettings::hypothesisShortOptionName = "hyp";
             const std::string RegionSettings::refineOptionName = "refine";
             const std::string RegionSettings::checkEngineOptionName = "engine";
             const std::string RegionSettings::printNoIllustrationOptionName = "noillustration";
@@ -24,8 +28,13 @@ namespace storm {
                 this->addOption(storm::settings::OptionBuilder(moduleName, regionOptionName, false, "Sets the region(s) considered for analysis.").setShortName(regionShortOptionName)
                                 .addArgument(storm::settings::ArgumentBuilder::createStringArgument("regioninput", "The region(s) given in format a<=x<=b,c<=y<=d seperated by ';'. Can also be a file.").build()).build());
                 
+                std::vector<std::string> hypotheses = {"unknown", "allsat", "allviolated"};
+                this->addOption(storm::settings::OptionBuilder(moduleName, hypothesisOptionName, false, "Sets a hypothesis for region analysis. If given, the region(s) are only analyzed w.r.t. that hypothesis.").setShortName(hypothesisShortOptionName)
+                                .addArgument(storm::settings::ArgumentBuilder::createStringArgument("hypothesis", "The hypothesis.").addValidatorString(ArgumentValidatorFactory::createMultipleChoiceValidator(hypotheses)).setDefaultValueString("unknown").build()).build());
+                
                 this->addOption(storm::settings::OptionBuilder(moduleName, refineOptionName, false, "Enables region refinement.")
-                                .addArgument(storm::settings::ArgumentBuilder::createDoubleArgument("threshold", "Refinement converges if the fraction of unknown area falls below this threshold.").setDefaultValueDouble(0.05).addValidatorDouble(storm::settings::ArgumentValidatorFactory::createDoubleRangeValidatorExcluding(0.0,1.0)).build()).build());
+                                .addArgument(storm::settings::ArgumentBuilder::createDoubleArgument("coverage-threshold", "Refinement converges if the fraction of unknown area falls below this threshold.").setDefaultValueDouble(0.05).addValidatorDouble(storm::settings::ArgumentValidatorFactory::createDoubleRangeValidatorIncluding(0.0,1.0)).build())
+                                .addArgument(storm::settings::ArgumentBuilder::createIntegerArgument("depth-limit", "If given, limits the number of times a region is refined.").setDefaultValueInteger(-1).build()).build());
                 
                 std::vector<std::string> engines = {"pl", "exactpl", "validatingpl"};
                 this->addOption(storm::settings::OptionBuilder(moduleName, checkEngineOptionName, true, "Sets which engine is used for analyzing regions.")
@@ -44,12 +53,44 @@ namespace storm {
                 return this->getOption(regionOptionName).getArgumentByName("regioninput").getValueAsString();
             }
             
+            bool RegionSettings::isHypothesisSet() const {
+                return this->getOption(hypothesisOptionName).getHasOptionBeenSet();
+            }
+            
+            storm::modelchecker::RegionResultHypothesis RegionSettings::getHypothesis() const {
+                std::string hypString = this->getOption(hypothesisOptionName).getArgumentByName("hypothesis").getValueAsString();
+                
+                storm::modelchecker::RegionResultHypothesis result;
+                
+                if (hypString == "unknown") {
+                    result = storm::modelchecker::RegionResultHypothesis::Unknown;
+                } else if (hypString == "allsat") {
+                    result = storm::modelchecker::RegionResultHypothesis::AllSat;
+                } else if (hypString == "allviolated") {
+                    result = storm::modelchecker::RegionResultHypothesis::AllViolated;
+                } else {
+                    STORM_LOG_THROW(false, storm::exceptions::IllegalArgumentValueException, "Hypothesis " << hypString << " not known.");
+                }
+                
+                return result;
+            }
+            
             bool RegionSettings::isRefineSet() const {
                 return this->getOption(refineOptionName).getHasOptionBeenSet();
             }
             
-            double RegionSettings::getRefinementThreshold() const {
-                return this->getOption(refineOptionName).getArgumentByName("threshold").getValueAsDouble();
+            double RegionSettings::getCoverageThreshold() const {
+                return this->getOption(refineOptionName).getArgumentByName("coverage-threshold").getValueAsDouble();
+            }
+            
+            bool RegionSettings::isDepthLimitSet() const {
+                return this->getOption(refineOptionName).getArgumentByName("depth-limit").getHasBeenSet() && this->getOption(refineOptionName).getArgumentByName("depth-limit").getValueAsInteger() >= 0;
+            }
+            
+            uint64_t RegionSettings::getDepthLimit() const {
+                int64_t depth = this->getOption(refineOptionName).getArgumentByName("depth-limit").getValueAsInteger();
+                STORM_LOG_THROW(depth >= 0, storm::exceptions::InvalidOperationException, "Tried to retrieve the depth limit but it was not set.");
+                return (uint64_t) depth;
             }
             
             storm::modelchecker::RegionCheckEngine RegionSettings::getRegionCheckEngine() const {

src/storm-pars/settings/modules/RegionSettings.h

@@ -1,6 +1,7 @@
 #pragma once
 
 #include "storm-pars/modelchecker/region/RegionCheckEngine.h"
+#include "storm-pars/modelchecker/region/RegionResultHypothesis.h"
 
 #include "storm/settings/modules/ModuleSettings.h"
 
@@ -29,6 +30,16 @@ namespace storm {
 				 */
 				std::string getRegionString() const;
 				
+				/*!
+				 * Retrieves whether region(s) were declared
+				 */
+				bool isHypothesisSet() const;
+				
+				/*!
+				 * Retrieves the region definition string
+				 */
+				storm::modelchecker::RegionResultHypothesis getHypothesis() const;
+				
 				/*!
 				 * Retrieves whether region refinement is enabled
 				 */
@@ -38,8 +49,18 @@ namespace storm {
 				 * Retrieves the threshold considered for iterative region refinement.
 				 * The refinement converges as soon as the fraction of unknown area falls below this threshold
 				 */
-				double getRefinementThreshold() const;
+				double getCoverageThreshold() const;
 				
+                /*!
+                 * Retrieves whether a depth threshold has been set for refinement
+                 */
+                bool isDepthLimitSet() const;
+                
+                /*!
+                 * Returns the depth threshold (if set). It is illegal to call this method if no depth threshold has been set.
+                 */
+                uint64_t getDepthLimit() const;
+                
 				/*!
 				 * Retrieves which type of region check should be performed
 				 */
@@ -60,6 +81,8 @@ namespace storm {
             private:
 				const static std::string regionOptionName;
 				const static std::string regionShortOptionName;
+				const static std::string hypothesisOptionName;
+				const static std::string hypothesisShortOptionName;
 				const static std::string refineOptionName;
 				const static std::string checkEngineOptionName;
 				const static std::string printNoIllustrationOptionName;

src/storm/api/export.h

@@ -2,7 +2,6 @@
 
 #include "storm/storage/jani/JSONExporter.h"
 
-#include "storm/analysis/GraphConditions.h"
 
 #include "storm/settings/SettingsManager.h"
 #include "storm/settings/modules/JaniExportSettings.h"
@@ -10,7 +9,6 @@
 #include "storm/utility/DirectEncodingExporter.h"
 #include "storm/utility/file.h"
 #include "storm/utility/macros.h"
-#include "storm/exceptions/NotSupportedException.h"
 
 namespace storm {
     namespace api {
@@ -18,32 +16,7 @@ namespace storm {
         void exportJaniModel(storm::jani::Model const& model, std::vector<storm::jani::Property> const& properties, std::string const& filename);
         
         void exportJaniModelAsDot(storm::jani::Model const& model, std::string const& filename);
-        
-        template <typename ValueType>
-        void exportParametricResultToFile(ValueType const& result, storm::analysis::ConstraintCollector<ValueType> const& constraintCollector, std::string const& path) {
-            STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Cannot export non-parametric result.");
-        }
-        
-        template <>
-        inline void exportParametricResultToFile(storm::RationalFunction const& result, storm::analysis::ConstraintCollector<storm::RationalFunction> const& constraintCollector, std::string const& path) {
-            std::ofstream filestream;
-            storm::utility::openFile(path, filestream);
-            filestream << "!Parameters: ";
-            std::set<storm::RationalFunctionVariable> vars = result.gatherVariables();
-            std::copy(vars.begin(), vars.end(), std::ostream_iterator<storm::RationalFunctionVariable>(filestream, "; "));
-            filestream << std::endl;
-            filestream << "!Result: " << result << std::endl;
-            filestream << "!Well-formed Constraints: " << std::endl;
-            std::vector<std::string> stringConstraints;
-            std::transform(constraintCollector.getWellformedConstraints().begin(), constraintCollector.getWellformedConstraints().end(), std::back_inserter(stringConstraints), [](carl::Formula<typename storm::Polynomial::PolyType> const& c) ->  std::string { return c.toString();});
-            std::copy(stringConstraints.begin(), stringConstraints.end(), std::ostream_iterator<std::string>(filestream, "\n"));
-            filestream << "!Graph-preserving Constraints: " << std::endl;
-            stringConstraints.clear();
-            std::transform(constraintCollector.getGraphPreservingConstraints().begin(), constraintCollector.getGraphPreservingConstraints().end(), std::back_inserter(stringConstraints), [](carl::Formula<typename storm::Polynomial::PolyType> const& c) ->  std::string { return c.toString();});
-            std::copy(stringConstraints.begin(), stringConstraints.end(), std::ostream_iterator<std::string>(filestream, "\n"));
-            storm::utility::closeFile(filestream);
-        }
-        
+
         template <typename ValueType>
         void exportSparseModelAsDrn(std::shared_ptr<storm::models::sparse::Model<ValueType>> const& model, std::string const& filename, std::vector<std::string> const& parameterNames) {
             std::ofstream stream;

src/storm/builder/BuilderOptions.cpp

@@ -35,7 +35,7 @@ namespace storm {
             return boost::get<storm::expressions::Expression>(labelOrExpression);
         }
         
-        BuilderOptions::BuilderOptions(bool buildAllRewardModels, bool buildAllLabels) : buildAllRewardModels(buildAllRewardModels), buildAllLabels(buildAllLabels), buildChoiceLabels(false), buildStateValuations(false), buildChoiceOrigins(false), explorationChecks(false) {
+        BuilderOptions::BuilderOptions(bool buildAllRewardModels, bool buildAllLabels) : buildAllRewardModels(buildAllRewardModels), buildAllLabels(buildAllLabels), buildChoiceLabels(false), buildStateValuations(false), buildChoiceOrigins(false), explorationChecks(false), explorationShowProgress(false), explorationShowProgressDelay(0) {
             // Intentionally left empty.
         }
         
@@ -55,6 +55,8 @@ namespace storm {
             }
             
             explorationChecks = storm::settings::getModule<storm::settings::modules::IOSettings>().isExplorationChecksSet();
+            explorationShowProgress = storm::settings::getModule<storm::settings::modules::IOSettings>().isExplorationShowProgressSet();
+            explorationShowProgressDelay = storm::settings::getModule<storm::settings::modules::IOSettings>().getExplorationShowProgressDelay();
         }
         
         void BuilderOptions::preserveFormula(storm::logic::Formula const& formula) {
@@ -163,6 +165,14 @@ namespace storm {
         bool BuilderOptions::isExplorationChecksSet() const {
             return explorationChecks;
         }
+        
+        bool BuilderOptions::isExplorationShowProgressSet() const {
+            return explorationShowProgress;
+        }
+
+        uint64_t BuilderOptions::getExplorationShowProgressDelay() const {
+            return explorationShowProgressDelay;
+        }
 
         BuilderOptions& BuilderOptions::setExplorationChecks(bool newValue) {
             explorationChecks = newValue;

src/storm/builder/BuilderOptions.h

@@ -94,6 +94,8 @@ namespace storm {
             bool isBuildAllRewardModelsSet() const;
             bool isBuildAllLabelsSet() const;
             bool isExplorationChecksSet() const;
+            bool isExplorationShowProgressSet() const;
+            uint64_t getExplorationShowProgressDelay() const;
             
             BuilderOptions& setBuildAllRewardModels();
             BuilderOptions& addRewardModel(std::string const& rewardModelName);
@@ -139,6 +141,12 @@ namespace storm {
             
             /// A flag that stores whether exploration checks are to be performed.
             bool explorationChecks;
+            
+            /// A flag that stores whether the progress of exploration is to be printed.
+            bool explorationShowProgress;
+            
+            /// The delay for printing progress information.
+            uint64_t explorationShowProgressDelay;
         };
         
     }

src/storm/builder/ExplicitModelBuilder.cpp

@@ -131,6 +131,11 @@ namespace storm {
             uint_fast64_t currentRowGroup = 0;
             uint_fast64_t currentRow = 0;
 
+            auto timeOfStart = std::chrono::high_resolution_clock::now();
+            auto timeOfLastMessage = std::chrono::high_resolution_clock::now();
+            uint64_t numberOfExploredStates = 0;
+            uint64_t numberOfExploredStatesSinceLastMessage = 0;
+            
             // Perform a search through the model.
             while (!statesToExplore.empty()) {
                 // Get the first state in the queue.
@@ -234,6 +239,21 @@ namespace storm {
                     }
                     ++currentRowGroup;
                 }
+                
+                if (generator->getOptions().isExplorationShowProgressSet()) {
+                    ++numberOfExploredStatesSinceLastMessage;
+                    ++numberOfExploredStates;
+                    
+                    auto now = std::chrono::high_resolution_clock::now();
+                    auto durationSinceLastMessage = std::chrono::duration_cast<std::chrono::seconds>(now - timeOfLastMessage).count();
+                    if (static_cast<uint64_t>(durationSinceLastMessage) >= generator->getOptions().getExplorationShowProgressDelay()) {
+                        auto statesPerSecond = numberOfExploredStatesSinceLastMessage / durationSinceLastMessage;
+                        auto durationSinceStart = std::chrono::duration_cast<std::chrono::seconds>(now - timeOfStart).count();
+                        std::cout << "Explored " << numberOfExploredStates << " states in " << durationSinceStart << " seconds (currently " << statesPerSecond << " states per second)." << std::endl;
+                        timeOfLastMessage = std::chrono::high_resolution_clock::now();
+                        numberOfExploredStatesSinceLastMessage = 0;
+                    }
+                }
             }
             
             if (markovianStates) {

src/storm/builder/jit/ExplicitJitJaniModelBuilder.cpp

@@ -73,12 +73,16 @@ namespace storm {
                 if (settings.isCompilerFlagsSet()) {
                     compilerFlags = settings.getCompilerFlags();
                 } else {
+                    std::stringstream flagStream;
 #ifdef LINUX
-                    compilerFlags = "-std=c++14 -fPIC -O3 -march=native -shared";
+                    flagStream << "-std=c++14 -fPIC -march=native -shared ";
 #endif
 #ifdef MACOSX
-                    compilerFlags = "-std=c++14 -stdlib=libc++ -fPIC -march=native -O3 -shared -undefined dynamic_lookup ";
+                    flagStream << "-std=c++14 -stdlib=libc++ -fPIC -march=native -shared -undefined dynamic_lookup ";
 #endif
+                    
+                    flagStream << "-O" << settings.getOptimizationLevel();
+                    compilerFlags = flagStream.str();
                 }
                 if (settings.isBoostIncludeDirectorySet()) {
                     boostIncludeDirectory = settings.getBoostIncludeDirectory();
@@ -523,6 +527,15 @@ namespace storm {
                 }
                 modelData["exploration_checks"] = cpptempl::make_data(list);
                 list = cpptempl::data_list();
+                if (options.isExplorationShowProgressSet()) {
+                    list.push_back(cpptempl::data_map());
+                }
+                modelData["expl_progress"] = cpptempl::make_data(list);
+                
+                std::stringstream progressDelayStream;
+                progressDelayStream << options.getExplorationShowProgressDelay();
+                modelData["expl_progress_interval"] = cpptempl::make_data(progressDelayStream.str());
+                list = cpptempl::data_list();
                 if (std::is_same<storm::RationalNumber, ValueType>::value) {
                     list.push_back(cpptempl::data_map());
                 }
@@ -537,7 +550,7 @@ namespace storm {
                     list.push_back(cpptempl::data_map());
                 }
                 modelData["double"] = cpptempl::make_data(list);
-
+                
                 list = cpptempl::data_list();
                 if (storm::settings::getModule<storm::settings::modules::CoreSettings>().isDontFixDeadlocksSet()) {
                     list.push_back(cpptempl::data_map());
@@ -1171,7 +1184,7 @@ namespace storm {
                     indent(vectorSource, indentLevel) << "}" << std::endl << std::endl;
                 }
                 
-                indent(vectorSource, indentLevel) << "void get_edges_" << synchronizationVectorIndex << "(StateType const& state, std::vector<std::reference_wrapper<Edge const>>& edges, uint64_t position) {" << std::endl;
+                indent(vectorSource, indentLevel) << "void get_edges_" << synchronizationVectorIndex << "(StateType const& state, TransientVariables const& transientIn, std::vector<std::reference_wrapper<Edge const>>& edges, uint64_t position) {" << std::endl;
                 position = 0;
                 uint64_t participatingPosition = 0;
                 for (auto const& inputActionName : synchronizationVector.getInput()) {
@@ -1184,7 +1197,7 @@ namespace storm {
                         for (auto const& edge : automaton.getEdges()) {
                             if (edge.getActionIndex() == actionIndex) {
                                 std::string edgeName = automaton.getName() + "_" + std::to_string(edgeIndex);
-                                indent(vectorSource, indentLevel + 2) << "if (edge_enabled_" << edgeName  << "(state)) {" << std::endl;
+                                indent(vectorSource, indentLevel + 2) << "if (edge_enabled_" << edgeName  << "(state, transientIn)) {" << std::endl;
                                 indent(vectorSource, indentLevel + 3) << "edges.emplace_back(edge_" << edgeName << ");" << std::endl;
                                 indent(vectorSource, indentLevel + 2) << "}" << std::endl;
                             }
@@ -1198,7 +1211,7 @@ namespace storm {
                 }
                 indent(vectorSource, indentLevel) << "}" << std::endl << std::endl;
                 
-                indent(vectorSource, indentLevel) << "void exploreSynchronizationVector_" << synchronizationVectorIndex << "(StateType const& state, StateBehaviour<IndexType, ValueType>& behaviour, StateSet<StateType>& statesToExplore) {" << std::endl;
+                indent(vectorSource, indentLevel) << "void exploreSynchronizationVector_" << synchronizationVectorIndex << "(StateType const& state, TransientVariables const& transientIn, StateBehaviour<IndexType, ValueType>& behaviour, StateSet<StateType>& statesToExplore) {" << std::endl;
                 indent(vectorSource, indentLevel + 1) << "#ifndef NDEBUG" << std::endl;
                 indent(vectorSource, indentLevel + 1) << "std::cout << \"exploring synchronization vector " << synchronizationVectorIndex << "\" << std::endl;" << std::endl;
                 indent(vectorSource, indentLevel + 1) << "#endif" << std::endl;
@@ -1207,7 +1220,7 @@ namespace storm {
                 participatingPosition = 0;
                 for (auto const& input : synchronizationVector.getInput()) {
                     if (!storm::jani::SynchronizationVector::isNoActionInput(input)) {
-                        indent(vectorSource, indentLevel + 1) << "get_edges_" << synchronizationVectorIndex << "(state, edges[" << participatingPosition << "], " << participatingPosition << ");" << std::endl;
+                        indent(vectorSource, indentLevel + 1) << "get_edges_" << synchronizationVectorIndex << "(state, transientIn, edges[" << participatingPosition << "], " << participatingPosition << ");" << std::endl;
                         indent(vectorSource, indentLevel + 1) << "if (edges[" << participatingPosition << "].empty()) {" << std::endl;
                         indent(vectorSource, indentLevel + 2) << "return;" << std::endl;
                         indent(vectorSource, indentLevel + 1) << "}" << std::endl;
@@ -1642,12 +1655,17 @@ namespace storm {
                 std::string sourceTemplate = R"(
 #define NDEBUG
                 
+{% if expl_progress %}
+#define EXPL_PROGRESS
+{% endif %}
+                
 #include <cstdint>
 #include <iostream>
 #include <vector>
 #include <queue>
 #include <cmath>
 #include <unordered_map>
+#include <chrono>
 #include <boost/dll/alias.hpp>
                 
 {% if exact %}
@@ -1902,7 +1920,7 @@ namespace storm {
                             {% endif %}
                             
                             // Non-synchronizing edges.
-                            {% for edge in nonsynch_edges %}static bool edge_enabled_{$edge.name}(StateType const& in) {
+                            {% for edge in nonsynch_edges %}static bool edge_enabled_{$edge.name}(StateType const& in, TransientVariables const& transientIn) {
                                 if ({$edge.guard}) {
                                     return true;
                                 }
@@ -1979,7 +1997,7 @@ namespace storm {
                             {% endfor %}{% endfor %}
                             
                             // Synchronizing edges.
-                            {% for edge in synch_edges %}static bool edge_enabled_{$edge.name}(StateType const& in) {
+                            {% for edge in synch_edges %}static bool edge_enabled_{$edge.name}(StateType const& in, TransientVariables const& transientIn) {
                                 if ({$edge.guard}) {
                                     return true;
                                 }
@@ -2109,7 +2127,7 @@ namespace storm {
                                 DestinationWithoutTransientFunctionPtr destinationWithoutTransientFunction;
                             };
                             
-                            typedef bool (*EdgeEnabledFunctionPtr)(StateType const&);
+                            typedef bool (*EdgeEnabledFunctionPtr)(StateType const&, TransientVariables const& transientIn);
                             typedef void (*EdgeTransientFunctionPtr)(StateType const&, TransientVariables const& transientIn, TransientVariables& out {% if exploration_checks %}, VariableWrites& variableWrites {% endif %});
                             
                             class Edge {
@@ -2124,8 +2142,8 @@ namespace storm {
                                     // Intentionally left empty.
                                 }
                                 
-                                bool isEnabled(StateType const& in) const {
-                                    return edgeEnabledFunction(in);
+                                bool isEnabled(StateType const& in, TransientVariables const& transientIn) const {
+                                    return edgeEnabledFunction(in, transientIn);
                                 }
                                 
                                 void addDestination(Destination const& destination) {
@@ -2175,7 +2193,7 @@ namespace storm {
                             
                             class JitBuilder : public JitModelBuilderInterface<IndexType, ValueType> {
                             public:
-                                JitBuilder(ModelComponentsBuilder<IndexType, ValueType>& modelComponentsBuilder) : JitModelBuilderInterface(modelComponentsBuilder) {
+                                JitBuilder(ModelComponentsBuilder<IndexType, ValueType>& modelComponentsBuilder) : JitModelBuilderInterface(modelComponentsBuilder), timeOfStart(std::chrono::high_resolution_clock::now()), timeOfLastMessage(std::chrono::high_resolution_clock::now()), numberOfExploredStates(0), numberOfExploredStatesSinceLastMessage(0) {
                                     {% for state in initialStates %}{
                                         StateType state;
                                         {% for assignment in state %}state.{$assignment.variable} = {$assignment.value};
@@ -2258,6 +2276,7 @@ namespace storm {
                                     getOrAddIndex(initialState, statesToExplore);
                                     
                                     StateBehaviour<IndexType, ValueType> behaviour;
+                                    
                                     while (!statesToExplore.empty()) {
                                         StateType currentState = statesToExplore.get();
                                         IndexType currentIndex = getIndex(currentState);
@@ -2281,10 +2300,10 @@ namespace storm {
                                             {% endfor %}
                                             
                                             // Explore all edges that do not take part in synchronization vectors.
-                                            exploreNonSynchronizingEdges(currentState, behaviour, statesToExplore);
+                                            exploreNonSynchronizingEdges(currentState, transientOut, behaviour, statesToExplore);
                                             
                                             // Explore all edges that participate in synchronization vectors.
-                                            exploreSynchronizingEdges(currentState, behaviour, statesToExplore);
+                                            exploreSynchronizingEdges(currentState, transientOut, behaviour, statesToExplore);
                                         }
 
                                         {% if dontFixDeadlocks %}
@@ -2296,6 +2315,21 @@ namespace storm {
 
                                         this->addStateBehaviour(currentIndex, behaviour);
                                         behaviour.clear();
+                                        
+#ifdef EXPL_PROGRESS
+                                        ++numberOfExploredStatesSinceLastMessage;
+                                        ++numberOfExploredStates;
+
+                                        auto now = std::chrono::high_resolution_clock::now();
+                                        auto durationSinceLastMessage = std::chrono::duration_cast<std::chrono::seconds>(now - timeOfLastMessage).count();
+                                        if (static_cast<uint64_t>(durationSinceLastMessage) >= {$expl_progress_interval}) {
+                                            auto statesPerSecond = numberOfExploredStatesSinceLastMessage / durationSinceLastMessage;
+                                            auto durationSinceStart = std::chrono::duration_cast<std::chrono::seconds>(now - timeOfStart).count();
+                                            std::cout << "Explored " << numberOfExploredStates << " states in " << durationSinceStart << " seconds (currently " << statesPerSecond << " states per second)." << std::endl;
+                                            timeOfLastMessage = std::chrono::high_resolution_clock::now();
+                                            numberOfExploredStatesSinceLastMessage = 0;
+                                        }
+#endif
                                     }
                                 }
                                 
@@ -2307,7 +2341,7 @@ namespace storm {
                                     return false;
                                 }
                                 
-                                void exploreNonSynchronizingEdges(StateType const& in, StateBehaviour<IndexType, ValueType>& behaviour, StateSet<StateType>& statesToExplore) {
+                                void exploreNonSynchronizingEdges(StateType const& in, TransientVariables const& transientIn, StateBehaviour<IndexType, ValueType>& behaviour, StateSet<StateType>& statesToExplore) {
                                     {% for edge in nonsynch_edges %}{
                                         if ({$edge.guard}) {
                                             Choice<IndexType, ValueType>& choice = behaviour.addChoice(!model_is_deterministic() && !model_is_discrete_time() && {$edge.markovian});
@@ -2347,9 +2381,9 @@ namespace storm {
                                 {% for vector in synch_vectors %}{$vector.functions}
                                 {% endfor %}
                                 
-                                void exploreSynchronizingEdges(StateType const& state, StateBehaviour<IndexType, ValueType>& behaviour, StateSet<StateType>& statesToExplore) {
+                                void exploreSynchronizingEdges(StateType const& state, TransientVariables const& transientIn, StateBehaviour<IndexType, ValueType>& behaviour, StateSet<StateType>& statesToExplore) {
                                     {% for vector in synch_vectors %}{
-                                        exploreSynchronizationVector_{$vector.index}(state, behaviour, statesToExplore);
+                                        exploreSynchronizationVector_{$vector.index}(state, transientIn, behaviour, statesToExplore);
                                     }
                                     {% endfor %}
                                 }
@@ -2391,14 +2425,22 @@ namespace storm {
                                 }
                                 
                             private:
+                                // State storage.
                                 spp::sparse_hash_map<StateType, IndexType> stateIds;
                                 std::vector<StateType> initialStates;
                                 std::vector<IndexType> deadlockStates;
-                                
+
+                                // Edges.
                                 {% for edge in nonsynch_edges %}Edge edge_{$edge.name};
                                 {% endfor %}
                                 {% for edge in synch_edges %}Edge edge_{$edge.name};
                                 {% endfor %}
+                                
+                                // Statistics.
+                                std::chrono::high_resolution_clock::time_point timeOfStart;
+                                std::chrono::high_resolution_clock::time_point timeOfLastMessage;
+                                uint64_t numberOfExploredStates;
+                                uint64_t numberOfExploredStatesSinceLastMessage;
                             };
                             
                             BOOST_DLL_ALIAS(storm::builder::jit::JitBuilder::create, create_builder)

src/storm/cli/cli.cpp

@@ -311,8 +311,6 @@ namespace storm {
                 transformToJani |= transformToJaniForJit;
                 
                 if (transformToJani) {
-                    SymbolicInput output;
-
                     storm::prism::Program const& model = output.model.get().asPrismProgram();
                     auto modelAndRenaming = model.toJaniWithLabelRenaming(true);
                     output.model = modelAndRenaming.first;
@@ -683,7 +681,9 @@ namespace storm {
                                             } else {
                                                 filter = storm::api::verifyWithSparseEngine<ValueType>(sparseModel, storm::api::createTask<ValueType>(states, false));
                                             }
-                                            result->filter(filter->asQualitativeCheckResult());
+                                            if (result && filter) {
+                                                result->filter(filter->asQualitativeCheckResult());
+                                            }
                                             return result;
                                         });
         }
@@ -703,8 +703,9 @@ namespace storm {
                 } else {
                     filter = storm::api::verifyWithHybridEngine<DdType, ValueType>(symbolicModel, storm::api::createTask<ValueType>(states, false));
                 }
-                
-                result->filter(filter->asQualitativeCheckResult());
+                if (result && filter) {
+                    result->filter(filter->asQualitativeCheckResult());
+                }
                 return result;
             });
         }
@@ -724,8 +725,9 @@ namespace storm {
                 } else {
                     filter = storm::api::verifyWithDdEngine<DdType, ValueType>(symbolicModel, storm::api::createTask<ValueType>(states, false));
                 }
-                
-                result->filter(filter->asQualitativeCheckResult());
+                if (result && filter) {
+                    result->filter(filter->asQualitativeCheckResult());
+                }
                 return result;
             });
         }

src/storm/logic/FragmentChecker.cpp

@@ -24,6 +24,9 @@ namespace storm {
             if (specification.isOperatorAtTopLevelRequired()) {
                 result &= f.isOperatorFormula();
             }
+            if (specification.isMultiObjectiveFormulaAtTopLevelRequired()) {
+                result &= f.isMultiObjectiveFormula();
+            }
             
             return result;
         }

src/storm/logic/FragmentSpecification.cpp

@@ -88,6 +88,7 @@ namespace storm {
             FragmentSpecification multiObjective = propositional();
             
             multiObjective.setMultiObjectiveFormulasAllowed(true);
+            multiObjective.setMultiObjectiveFormulaAtTopLevelRequired(true);
             multiObjective.setOperatorsAtTopLevelOfMultiObjectiveFormulasRequired(true);
             multiObjective.setProbabilityOperatorsAllowed(true);
             multiObjective.setUntilFormulasAllowed(true);
@@ -148,6 +149,7 @@ namespace storm {
             quantitativeOperatorResults = true;
             
             operatorAtTopLevelRequired = false;
+            multiObjectiveFormulaAtTopLevelRequired = false;
             operatorsAtTopLevelOfMultiObjectiveFormulasRequired = false;
         }
         
@@ -489,6 +491,15 @@ namespace storm {
             return *this;
         }
 
+        bool FragmentSpecification::isMultiObjectiveFormulaAtTopLevelRequired() const {
+            return multiObjectiveFormulaAtTopLevelRequired;
+        }
+        
+        FragmentSpecification& FragmentSpecification::setMultiObjectiveFormulaAtTopLevelRequired(bool newValue) {
+            multiObjectiveFormulaAtTopLevelRequired = newValue;
+            return *this;
+        }
+
         bool FragmentSpecification::areOperatorsAtTopLevelOfMultiObjectiveFormulasRequired() const {
             return operatorsAtTopLevelOfMultiObjectiveFormulasRequired;
         }

src/storm/logic/FragmentSpecification.h

@@ -118,6 +118,9 @@ namespace storm {
             bool isOperatorAtTopLevelRequired() const;
             FragmentSpecification& setOperatorAtTopLevelRequired(bool newValue);
             
+            bool isMultiObjectiveFormulaAtTopLevelRequired() const;
+            FragmentSpecification& setMultiObjectiveFormulaAtTopLevelRequired(bool newValue);
+            
             bool areOperatorsAtTopLevelOfMultiObjectiveFormulasRequired() const;
             FragmentSpecification& setOperatorsAtTopLevelOfMultiObjectiveFormulasRequired(bool newValue);
             
@@ -170,6 +173,7 @@ namespace storm {
             bool quantitativeOperatorResults;
             bool qualitativeOperatorResults;
             bool operatorAtTopLevelRequired;
+            bool multiObjectiveFormulaAtTopLevelRequired;
             bool operatorsAtTopLevelOfMultiObjectiveFormulasRequired;
         };
         

src/storm/modelchecker/csl/SparseMarkovAutomatonCslModelChecker.cpp

@@ -39,8 +39,8 @@ namespace storm {
             } else {
                 // Check whether we consider a multi-objective formula
                 // For multi-objective model checking, each initial state  requires an individual scheduler (in contrast to single objective model checking). Let's exclude multiple initial states.
-                if(this->getModel().getInitialStates().getNumberOfSetBits() > 1) return false;
-                if(!checkTask.isOnlyInitialStatesRelevantSet()) return false;
+                if (this->getModel().getInitialStates().getNumberOfSetBits() > 1) return false;
+                if (!checkTask.isOnlyInitialStatesRelevantSet()) return false;
                 return formula.isInFragment(storm::logic::multiObjective().setTimeAllowed(true).setTimeBoundedUntilFormulasAllowed(true));
             }
         }

src/storm/modelchecker/multiobjective/Objective.h

@@ -5,6 +5,7 @@
 #include "storm/logic/Formula.h"
 #include "storm/logic/Bound.h"
 #include "storm/logic/TimeBound.h"
+#include "storm/logic/TimeBoundType.h"
 #include "storm/solver/OptimizationDirection.h"
 
 namespace storm {
@@ -28,8 +29,9 @@ namespace storm {
                 // if originalFormula does ot specifies one, the direction is derived from the bound.
                 storm::solver::OptimizationDirection optimizationDirection;
                 
-                // Lower and upper time/step bouds
+                // Lower and upper time/step/reward bouds
                 boost::optional<storm::logic::TimeBound> lowerTimeBound, upperTimeBound;
+                boost::optional<storm::logic::TimeBoundReference> timeBoundReference;
                 
                 boost::optional<ValueType> lowerResultBound, upperResultBound;
                 

src/storm/modelchecker/multiobjective/SparseMultiObjectivePreprocessor.cpp

@@ -1,7 +1,7 @@
 #include "storm/modelchecker/multiobjective/SparseMultiObjectivePreprocessor.h"
 
 #include <algorithm>
-#include <storm/transformer/GoalStateMerger.h>
+#include <set>
 
 #include "storm/models/sparse/Mdp.h"
 #include "storm/models/sparse/MarkovAutomaton.h"
@@ -12,7 +12,7 @@
 #include "storm/storage/memorystructure/MemoryStructureBuilder.h"
 #include "storm/storage/memorystructure/SparseModelMemoryProduct.h"
 #include "storm/storage/expressions/ExpressionManager.h"
-#include "storm/transformer/SubsystemBuilder.h"
+#include "storm/transformer/GoalStateMerger.h"
 #include "storm/utility/macros.h"
 #include "storm/utility/vector.h"
 #include "storm/utility/graph.h"
@@ -266,8 +266,6 @@ namespace storm {
             
             template<typename SparseModelType>
             void SparseMultiObjectivePreprocessor<SparseModelType>::preprocessBoundedUntilFormula(storm::logic::BoundedUntilFormula const& formula, PreprocessorData& data) {
-                STORM_LOG_THROW(!data.originalModel.isOfType(storm::models::ModelType::MarkovAutomaton) || !formula.getTimeBoundReference().isStepBound(), storm::exceptions::InvalidPropertyException, "Multi-objective model checking currently does not support STEP-bounded properties for Markov automata.");
-                
                 if (formula.hasLowerBound()) {
                     STORM_LOG_THROW(!formula.getLowerBound().containsVariables(), storm::exceptions::InvalidPropertyException, "The lower time bound for the formula " << formula << " still contains variables");
                     if (!storm::utility::isZero(formula.getLowerBound<double>()) || formula.isLowerBoundStrict()) {
@@ -280,6 +278,8 @@ namespace storm {
                         data.objectives.back()->upperTimeBound = storm::logic::TimeBound(formula.isUpperBoundStrict(), formula.getUpperBound());
                     }
                 }
+                
+                data.objectives.back()->timeBoundReference = formula.getTimeBoundReference();
                 preprocessUntilFormula(storm::logic::UntilFormula(formula.getLeftSubformula().asSharedPointer(), formula.getRightSubformula().asSharedPointer()), data);
             }
             
@@ -375,6 +375,9 @@ namespace storm {
                 std::set<std::string> relevantRewardModels;
                 for (auto const& obj : result.objectives) {
                     relevantRewardModels.insert(*obj.rewardModelName);
+                    if (obj.timeBoundReference && obj.timeBoundReference->isRewardBound()) {
+                        relevantRewardModels.insert(obj.timeBoundReference->getRewardName());
+                    }
                 }
                 
                 // Build a subsystem that discards states that yield infinite reward for all schedulers.

src/storm/modelchecker/multiobjective/pcaa/SparseMaPcaaWeightVectorChecker.cpp

@@ -41,6 +41,10 @@ namespace storm {
             template <class SparseMaModelType>
             void SparseMaPcaaWeightVectorChecker<SparseMaModelType>::boundedPhase(std::vector<ValueType> const& weightVector, std::vector<ValueType>& weightedRewardVector) {
                 
+                for (auto const& obj : this->objectives) {
+                    STORM_LOG_THROW(!obj.timeBoundReference || obj.timeBoundReference->isTimeBound(), storm::exceptions::InvalidPropertyException, "Multi-objective model checking of Markov automata is only supported for time-bounded formulass.");
+                }
+                
                 // Split the preprocessed model into transitions from/to probabilistic/Markovian states.
                 SubModel MS = createSubModel(true, weightedRewardVector);
                 SubModel PS = createSubModel(false, weightedRewardVector);

src/storm/modelchecker/multiobjective/pcaa/SparseMdpPcaaWeightVectorChecker.cpp

@@ -6,6 +6,9 @@
 #include "storm/utility/macros.h"
 #include "storm/utility/vector.h"
 #include "storm/exceptions/InvalidPropertyException.h"
+#include "storm/exceptions/IllegalArgumentException.h"
+#include "storm/exceptions/NotSupportedException.h"
+#include "storm/exceptions/UnexpectedException.h"
 
 
 namespace storm {
@@ -28,6 +31,24 @@ namespace storm {
             
             template <class SparseMdpModelType>
             void SparseMdpPcaaWeightVectorChecker<SparseMdpModelType>::boundedPhase(std::vector<ValueType> const& weightVector, std::vector<ValueType>& weightedRewardVector) {
+                // Check whether reward bounded objectives occur.
+                bool containsRewardBoundedObjectives = false;
+                for (auto const& obj : this->objectives) {
+                    if (obj.timeBoundReference && obj.timeBoundReference->isRewardBound()) {
+                        containsRewardBoundedObjectives = true;
+                        break;
+                    }
+                }
+                
+                if (containsRewardBoundedObjectives) {
+                    boundedPhaseWithRewardBounds(weightVector, weightedRewardVector);
+                } else {
+                    boundedPhaseOnlyStepBounds(weightVector, weightedRewardVector);
+                }
+            }
+
+            template <class SparseMdpModelType>
+            void SparseMdpPcaaWeightVectorChecker<SparseMdpModelType>::boundedPhaseOnlyStepBounds(std::vector<ValueType> const& weightVector, std::vector<ValueType>& weightedRewardVector) {
                 // Allocate some memory so this does not need to happen for each time epoch
                 std::vector<uint_fast64_t> optimalChoicesInCurrentEpoch(this->model.getNumberOfStates());
                 std::vector<ValueType> choiceValues(weightedRewardVector.size());
@@ -97,6 +118,13 @@ namespace storm {
                 }
             }
             
+            
+            template <class SparseMdpModelType>
+            void SparseMdpPcaaWeightVectorChecker<SparseMdpModelType>::boundedPhaseWithRewardBounds(std::vector<ValueType> const& weightVector, std::vector<ValueType>& weightedRewardVector) {
+                STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Multi-objective model checking with reward bounded objectives is not supported.");
+            }
+            
+            
             template class SparseMdpPcaaWeightVectorChecker<storm::models::sparse::Mdp<double>>;
 #ifdef STORM_HAVE_CARL
             template class SparseMdpPcaaWeightVectorChecker<storm::models::sparse::Mdp<storm::RationalNumber>>;

src/storm/modelchecker/multiobjective/pcaa/SparseMdpPcaaWeightVectorChecker.h

@@ -19,6 +19,7 @@ namespace storm {
             class SparseMdpPcaaWeightVectorChecker : public SparsePcaaWeightVectorChecker<SparseMdpModelType> {
             public:
                 typedef typename SparseMdpModelType::ValueType ValueType;
+                typedef typename SparseMdpModelType::RewardModelType RewardModelType;
             
                 /*
                  * Creates a weight vextor checker.
@@ -40,16 +41,32 @@ namespace storm {
             private:
                 
                 /*!
-                 * For each time epoch (starting with the maximal stepBound occurring in the objectives), this method
-                 * - determines the objectives that are relevant in the current time epoch
-                 * - determines the maximizing scheduler for the weighted reward vector of these objectives
-                 * - computes the values of these objectives w.r.t. this scheduler
+                 * Computes the maximizing scheduler for the weighted sum of the objectives, including also step or reward bounded objectives.
+                 * Moreover, the values of the individual objectives are computed w.r.t. this scheduler.
                  *
                  * @param weightVector the weight vector of the current check
                  * @param weightedRewardVector the weighted rewards considering the unbounded objectives. Will be invalidated after calling this.
                  */
                 virtual void boundedPhase(std::vector<ValueType> const& weightVector, std::vector<ValueType>& weightedRewardVector) override;
-  
+                
+                /*!
+                 * Computes the bounded phase for the case that only step bounded objectives are considered.
+                 *
+                 * @param weightVector the weight vector of the current check
+                 * @param weightedRewardVector the weighted rewards considering the unbounded objectives. Will be invalidated after calling this.
+                 */
+                void boundedPhaseOnlyStepBounds(std::vector<ValueType> const& weightVector, std::vector<ValueType>& weightedRewardVector);
+                
+                /*!
+                 * Computes the bounded phase for the case that also reward bounded objectives occurr.
+                 *
+                 * @param weightVector the weight vector of the current check
+                 * @param weightedRewardVector the weighted rewards considering the unbounded objectives. Will be invalidated after calling this.
+                 */
+                void boundedPhaseWithRewardBounds(std::vector<ValueType> const& weightVector, std::vector<ValueType>& weightedRewardVector);
+                
+ 
+                
             };
             
         }

src/storm/modelchecker/prctl/SparseMdpPrctlModelChecker.cpp

@@ -48,8 +48,8 @@ namespace storm {
             } else {
                 // Check whether we consider a multi-objective formula
                 // For multi-objective model checking, each initial state requires an individual scheduler (in contrast to single-objective model checking). Let's exclude multiple initial states.
-                if(this->getModel().getInitialStates().getNumberOfSetBits() > 1) return false;
-                if(!checkTask.isOnlyInitialStatesRelevantSet()) return false;
+                if (this->getModel().getInitialStates().getNumberOfSetBits() > 1) return false;
+                if (!checkTask.isOnlyInitialStatesRelevantSet()) return false;
                 return formula.isInFragment(storm::logic::multiObjective().setCumulativeRewardFormulasAllowed(true));
             }
         }

src/storm/settings/ArgumentValidators.cpp

@@ -133,6 +133,10 @@ namespace storm {
             return createRangeValidatorExcluding<double>(lowerBound, upperBound);
         }
         
+        std::shared_ptr<ArgumentValidator<double>> ArgumentValidatorFactory::createDoubleRangeValidatorIncluding(double lowerBound, double upperBound) {
+            return createRangeValidatorIncluding<double>(lowerBound, upperBound);
+        }
+        
         std::shared_ptr<ArgumentValidator<int64_t>> ArgumentValidatorFactory::createIntegerGreaterValidator(int_fast64_t lowerBound) {
             return createGreaterValidator<int64_t>(lowerBound, false);
         }
@@ -174,6 +178,11 @@ namespace storm {
             return std::make_unique<RangeArgumentValidator<ValueType>>(lowerBound, upperBound, false, false);
         }
         
+        template <typename ValueType>
+        std::shared_ptr<ArgumentValidator<ValueType>> ArgumentValidatorFactory::createRangeValidatorIncluding(ValueType lowerBound, ValueType upperBound) {
+            return std::make_unique<RangeArgumentValidator<ValueType>>(lowerBound, upperBound, true, true);
+        }
+        
         template <typename ValueType>
         std::shared_ptr<ArgumentValidator<ValueType>> ArgumentValidatorFactory::createGreaterValidator(ValueType lowerBound, bool equalAllowed) {
             return std::make_unique<RangeArgumentValidator<ValueType>>(lowerBound, boost::none, equalAllowed, false);

src/storm/settings/ArgumentValidators.h

@@ -70,6 +70,8 @@ namespace storm {
             static std::shared_ptr<ArgumentValidator<uint64_t>> createUnsignedRangeValidatorExcluding(uint64_t lowerBound, uint64_t upperBound);
             static std::shared_ptr<ArgumentValidator<double>> createDoubleRangeValidatorExcluding(double lowerBound, double upperBound);
             
+            static std::shared_ptr<ArgumentValidator<double>> createDoubleRangeValidatorIncluding(double lowerBound, double upperBound);
+            
             static std::shared_ptr<ArgumentValidator<int64_t>> createIntegerGreaterValidator(int_fast64_t lowerBound);
             static std::shared_ptr<ArgumentValidator<uint64_t>> createUnsignedGreaterValidator(uint64_t lowerBound);
             static std::shared_ptr<ArgumentValidator<double>> createDoubleGreaterValidator(double lowerBound);
@@ -87,6 +89,9 @@ namespace storm {
             template <typename ValueType>
             static std::shared_ptr<ArgumentValidator<ValueType>> createRangeValidatorExcluding(ValueType lowerBound, ValueType upperBound);
             
+            template <typename ValueType>
+            static std::shared_ptr<ArgumentValidator<ValueType>> createRangeValidatorIncluding(ValueType lowerBound, ValueType upperBound);
+            
             template <typename ValueType>
             static std::shared_ptr<ArgumentValidator<ValueType>> createGreaterValidator(ValueType lowerBound, bool equalAllowed);
         };

src/storm/settings/modules/IOSettings.cpp

@@ -34,6 +34,8 @@ namespace storm {
             const std::string IOSettings::explorationOrderOptionShortName = "eo";
             const std::string IOSettings::explorationChecksOptionName = "explchecks";
             const std::string IOSettings::explorationChecksOptionShortName = "ec";
+            const std::string IOSettings::explorationShowProgressOptionName = "explprog";
+            const std::string IOSettings::explorationShowProgressOptionShortName = "ep";
             const std::string IOSettings::transitionRewardsOptionName = "transrew";
             const std::string IOSettings::stateRewardsOptionName = "staterew";
             const std::string IOSettings::choiceLabelingOptionName = "choicelab";
@@ -84,6 +86,7 @@ namespace storm {
                 this->addOption(storm::settings::OptionBuilder(moduleName, explorationOrderOptionName, false, "Sets which exploration order to use.").setShortName(explorationOrderOptionShortName)
                                 .addArgument(storm::settings::ArgumentBuilder::createStringArgument("name", "The name of the exploration order to choose.").addValidatorString(ArgumentValidatorFactory::createMultipleChoiceValidator(explorationOrders)).setDefaultValueString("bfs").build()).build());
                 this->addOption(storm::settings::OptionBuilder(moduleName, explorationChecksOptionName, false, "If set, additional checks (if available) are performed during model exploration to debug the model.").setShortName(explorationChecksOptionShortName).build());
+                this->addOption(storm::settings::OptionBuilder(moduleName, explorationShowProgressOptionName, false, "Sets when additional information (if available) about the exploration progress is printed.").setShortName(explorationShowProgressOptionShortName).addArgument(storm::settings::ArgumentBuilder::createUnsignedIntegerArgument("delay", "The delay to wait between emitting information.").setDefaultValueUnsignedInteger(0).build()).build());
 
                 this->addOption(storm::settings::OptionBuilder(moduleName, transitionRewardsOptionName, false, "If given, the transition rewards are read from this file and added to the explicit model. Note that this requires the model to be given as an explicit model (i.e., via --" + explicitOptionName + ").")
                                 .addArgument(storm::settings::ArgumentBuilder::createStringArgument("filename", "The file from which to read the transition rewards.").addValidatorString(ArgumentValidatorFactory::createExistingFileValidator()).build()).build());
@@ -195,6 +198,14 @@ namespace storm {
                 return this->getOption(explorationChecksOptionName).getHasOptionBeenSet();
             }
             
+            bool IOSettings::isExplorationShowProgressSet() const {
+                return this->getOption(explorationShowProgressOptionName).getArgumentByName("delay").getValueAsUnsignedInteger() > 0;
+            }
+
+            uint64_t IOSettings::getExplorationShowProgressDelay() const {
+                return this->getOption(explorationShowProgressOptionName).getArgumentByName("delay").getValueAsUnsignedInteger();
+            }
+            
             bool IOSettings::isTransitionRewardsSet() const {
                 return this->getOption(transitionRewardsOptionName).getHasOptionBeenSet();
             }
@@ -268,6 +279,7 @@ namespace storm {
             }
 
 			void IOSettings::finalize() {
+                // Intentionally left empty.
             }
 
             bool IOSettings::check() const {

src/storm/settings/modules/IOSettings.h

@@ -179,6 +179,20 @@ namespace storm {
                  */
                 bool isExplorationChecksSet() const;
                 
+                /*!
+                 * Retrieves whether to show information about exploration progress.
+                 *
+                 * @return True if information is to be shown.
+                 */
+                bool isExplorationShowProgressSet() const;
+                
+                /*!
+                 * Retrieves the delay for printing information about the exploration progress.
+                 *
+                 * @return The desired delay in seconds. If 0, no information about the progress shall be printed.
+                 */
+                uint64_t getExplorationShowProgressDelay() const;
+                
                 /*!
                  * Retrieves the exploration order if it was set.
                  *
@@ -334,6 +348,8 @@ namespace storm {
                 static const std::string jitOptionName;
                 static const std::string explorationChecksOptionName;
                 static const std::string explorationChecksOptionShortName;
+                static const std::string explorationShowProgressOptionName;
+                static const std::string explorationShowProgressOptionShortName;
                 static const std::string explorationOrderOptionName;
                 static const std::string explorationOrderOptionShortName;
                 static const std::string transitionRewardsOptionName;

src/storm/settings/modules/JitBuilderSettings.cpp

@@ -20,6 +20,7 @@ namespace storm {
             const std::string JitBuilderSettings::boostIncludeDirectoryOptionName = "boost";
             const std::string JitBuilderSettings::carlIncludeDirectoryOptionName = "carl";
             const std::string JitBuilderSettings::compilerFlagsOptionName = "cxxflags";
+            const std::string JitBuilderSettings::optimizationLevelOptionName = "opt";
 
             JitBuilderSettings::JitBuilderSettings() : ModuleSettings(moduleName) {
                 this->addOption(storm::settings::OptionBuilder(moduleName, doctorOptionName, false, "Show debugging information on why the jit-based model builder is not working on your system.").build());
@@ -33,6 +34,8 @@ namespace storm {
                                 .addArgument(storm::settings::ArgumentBuilder::createStringArgument("dir", "The directory containing the carl headers.").build()).build());
                 this->addOption(storm::settings::OptionBuilder(moduleName, compilerFlagsOptionName, false, "The flags passed to the compiler.")
                                 .addArgument(storm::settings::ArgumentBuilder::createStringArgument("flags", "The compiler flags.").build()).build());
+                this->addOption(storm::settings::OptionBuilder(moduleName, optimizationLevelOptionName, false, "The optimization level to use.")
+                                .addArgument(storm::settings::ArgumentBuilder::createUnsignedIntegerArgument("level", "The compiler flags.").setDefaultValueUnsignedInteger(3).build()).build());
             }
             
             bool JitBuilderSettings::isCompilerSet() const {
@@ -79,6 +82,10 @@ namespace storm {
                 return this->getOption(compilerFlagsOptionName).getArgumentByName("flags").getValueAsString();
             }
             
+            uint64_t JitBuilderSettings::getOptimizationLevel() const {
+                return this->getOption(optimizationLevelOptionName).getArgumentByName("level").getValueAsUnsignedInteger();
+            }
+            
             void JitBuilderSettings::finalize() {
                 // Intentionally left empty.
             }

src/storm/settings/modules/JitBuilderSettings.h

@@ -30,6 +30,8 @@ namespace storm {
                 bool isCompilerFlagsSet() const;
                 std::string getCompilerFlags() const;
                 
+                uint64_t getOptimizationLevel() const;
+                
                 bool check() const override;
                 void finalize() override;
                 
@@ -42,6 +44,7 @@ namespace storm {
                 static const std::string carlIncludeDirectoryOptionName;
                 static const std::string compilerFlagsOptionName;
                 static const std::string doctorOptionName;
+                static const std::string optimizationLevelOptionName;
             };
             
         }

src/storm/utility/export.h

@@ -1,10 +1,3 @@
-/** 
- * @file:   export.h
- * @author: Sebastian Junges
- *
- * @since October 7, 2014
- */
-
 #ifndef STORM_UTILITY_EXPORT_H_
 #define STORM_UTILITY_EXPORT_H_
 
@@ -14,32 +7,12 @@
 #include "storm/utility/macros.h"
 #include "storm/utility/file.h"
 
-//#include "storm/storage/parameters.h"
-//#include "storm/settings/modules/ParametricSettings.h"
-//#include "storm/modelchecker/reachability/CollectConstraints.h"
+
 
 namespace storm {
     namespace utility {
 
-            /* TODO Fix me
-        template<typename ValueType>	
-        void exportParametricMcResult(const ValueType& mcresult, storm::modelchecker::reachability::CollectConstraints<storm::RationalFunction> const& constraintCollector) {
-            std::string path = storm::settings::getModule<storm::settings::modules::ParametricSettings>().exportResultPath();
-            std::ofstream filestream;
-            filestream.open(path);
-            // todo add checks.
-            filestream << "!Parameters: ";
-            std::set<storm::RationalFunctionVariable> vars = mcresult.gatherVariables();
-            std::copy(vars.begin(), vars.end(), std::ostream_iterator<storm::RationalFunctionVariable>(filestream, ", "));
-            filestream << std::endl;
-            filestream << "!Result: " << mcresult << std::endl;
-            filestream << "!Well-formed Constraints: " << std::endl;
-            std::copy(constraintCollector.wellformedConstraints().begin(), constraintCollector.wellformedConstraints().end(), std::ostream_iterator<carl::Constraint<ValueType>>(filestream, "\n"));
-            filestream << "!Graph-preserving Constraints: " << std::endl;
-            std::copy(constraintCollector.graphPreservingConstraints().begin(), constraintCollector.graphPreservingConstraints().end(), std::ostream_iterator<carl::Constraint<ValueType>>(filestream, "\n"));
-            filestream.close();
-        }
-        */
+
         
         template <typename ValueType>
         inline void exportDataToCSVFile(std::string filepath, std::vector<std::vector<ValueType>> const& data, boost::optional<std::vector<std::string>> const& columnHeaders) {

src/test/storm-pars/modelchecker/SparseDtmcParameterLiftingTest.cpp

@@ -31,9 +31,9 @@ TEST(SparseDtmcParameterLiftingTest, Brp_Prob) {
     auto exBothRegion=storm::api::parseRegion<storm::RationalFunction>("0.4<=pL<=0.65,0.75<=pK<=0.95", modelParameters);
     auto allVioRegion=storm::api::parseRegion<storm::RationalFunction>("0.1<=pL<=0.73,0.2<=pK<=0.715", modelParameters);
 
-    EXPECT_EQ(storm::modelchecker::RegionResult::AllSat, regionChecker->analyzeRegion(allSatRegion, storm::modelchecker::RegionResult::Unknown, true));
-    EXPECT_EQ(storm::modelchecker::RegionResult::ExistsBoth, regionChecker->analyzeRegion(exBothRegion, storm::modelchecker::RegionResult::Unknown, true));
-    EXPECT_EQ(storm::modelchecker::RegionResult::AllViolated, regionChecker->analyzeRegion(allVioRegion, storm::modelchecker::RegionResult::Unknown, true));
+    EXPECT_EQ(storm::modelchecker::RegionResult::AllSat, regionChecker->analyzeRegion(allSatRegion, storm::modelchecker::RegionResultHypothesis::Unknown, storm::modelchecker::RegionResult::Unknown, true));
+    EXPECT_EQ(storm::modelchecker::RegionResult::ExistsBoth, regionChecker->analyzeRegion(exBothRegion, storm::modelchecker::RegionResultHypothesis::Unknown,storm::modelchecker::RegionResult::Unknown, true));
+    EXPECT_EQ(storm::modelchecker::RegionResult::AllViolated, regionChecker->analyzeRegion(allVioRegion, storm::modelchecker::RegionResultHypothesis::Unknown,storm::modelchecker::RegionResult::Unknown, true));
 
     carl::VariablePool::getInstance().clear();
 }
@@ -60,9 +60,9 @@ TEST(SparseDtmcParameterLiftingTest, Brp_Rew) {
     auto exBothRegion=storm::api::parseRegion<storm::RationalFunction>("0.6<=pK<=0.9,0.5<=TOMsg<=0.95", modelParameters);
     auto allVioRegion=storm::api::parseRegion<storm::RationalFunction>("0.1<=pK<=0.3,0.2<=TOMsg<=0.3", modelParameters);
 
-    EXPECT_EQ(storm::modelchecker::RegionResult::AllSat, regionChecker->analyzeRegion(allSatRegion, storm::modelchecker::RegionResult::Unknown, true));
-    EXPECT_EQ(storm::modelchecker::RegionResult::ExistsBoth, regionChecker->analyzeRegion(exBothRegion, storm::modelchecker::RegionResult::Unknown, true));
-    EXPECT_EQ(storm::modelchecker::RegionResult::AllViolated, regionChecker->analyzeRegion(allVioRegion, storm::modelchecker::RegionResult::Unknown, true));
+    EXPECT_EQ(storm::modelchecker::RegionResult::AllSat, regionChecker->analyzeRegion(allSatRegion, storm::modelchecker::RegionResultHypothesis::Unknown, storm::modelchecker::RegionResult::Unknown, true));
+    EXPECT_EQ(storm::modelchecker::RegionResult::ExistsBoth, regionChecker->analyzeRegion(exBothRegion, storm::modelchecker::RegionResultHypothesis::Unknown, storm::modelchecker::RegionResult::Unknown, true));
+    EXPECT_EQ(storm::modelchecker::RegionResult::AllViolated, regionChecker->analyzeRegion(allVioRegion, storm::modelchecker::RegionResultHypothesis::Unknown, storm::modelchecker::RegionResult::Unknown, true));
     
     carl::VariablePool::getInstance().clear();
 }
@@ -89,9 +89,9 @@ TEST(SparseDtmcParameterLiftingTest, Brp_Rew_Bounded) {
     auto exBothRegion=storm::api::parseRegion<storm::RationalFunction>("0.6<=pK<=0.9,0.5<=TOMsg<=0.95", modelParameters);
     auto allVioRegion=storm::api::parseRegion<storm::RationalFunction>("0.1<=pK<=0.3,0.2<=TOMsg<=0.3", modelParameters);
 
-    EXPECT_EQ(storm::modelchecker::RegionResult::AllSat, regionChecker->analyzeRegion(allSatRegion, storm::modelchecker::RegionResult::Unknown, true));
-    EXPECT_EQ(storm::modelchecker::RegionResult::ExistsBoth, regionChecker->analyzeRegion(exBothRegion, storm::modelchecker::RegionResult::Unknown, true));
-    EXPECT_EQ(storm::modelchecker::RegionResult::AllViolated, regionChecker->analyzeRegion(allVioRegion, storm::modelchecker::RegionResult::Unknown, true));
+    EXPECT_EQ(storm::modelchecker::RegionResult::AllSat, regionChecker->analyzeRegion(allSatRegion, storm::modelchecker::RegionResultHypothesis::Unknown, storm::modelchecker::RegionResult::Unknown, true));
+    EXPECT_EQ(storm::modelchecker::RegionResult::ExistsBoth, regionChecker->analyzeRegion(exBothRegion, storm::modelchecker::RegionResultHypothesis::Unknown, storm::modelchecker::RegionResult::Unknown, true));
+    EXPECT_EQ(storm::modelchecker::RegionResult::AllViolated, regionChecker->analyzeRegion(allVioRegion, storm::modelchecker::RegionResultHypothesis::Unknown, storm::modelchecker::RegionResult::Unknown, true));
     
     carl::VariablePool::getInstance().clear();
 }
@@ -119,9 +119,9 @@ TEST(SparseDtmcParameterLiftingTest, Brp_Prob_exactValidation) {
     auto exBothRegion=storm::api::parseRegion<storm::RationalFunction>("0.4<=pL<=0.65,0.75<=pK<=0.95", modelParameters);
     auto allVioRegion=storm::api::parseRegion<storm::RationalFunction>("0.1<=pL<=0.73,0.2<=pK<=0.715", modelParameters);
 
-    EXPECT_EQ(storm::modelchecker::RegionResult::AllSat, regionChecker->analyzeRegion(allSatRegion, storm::modelchecker::RegionResult::Unknown, true));
-    EXPECT_EQ(storm::modelchecker::RegionResult::ExistsBoth, regionChecker->analyzeRegion(exBothRegion, storm::modelchecker::RegionResult::Unknown, true));
-    EXPECT_EQ(storm::modelchecker::RegionResult::AllViolated, regionChecker->analyzeRegion(allVioRegion, storm::modelchecker::RegionResult::Unknown, true));
+    EXPECT_EQ(storm::modelchecker::RegionResult::AllSat, regionChecker->analyzeRegion(allSatRegion, storm::modelchecker::RegionResultHypothesis::Unknown, storm::modelchecker::RegionResult::Unknown, true));
+    EXPECT_EQ(storm::modelchecker::RegionResult::ExistsBoth, regionChecker->analyzeRegion(exBothRegion, storm::modelchecker::RegionResultHypothesis::Unknown, storm::modelchecker::RegionResult::Unknown, true));
+    EXPECT_EQ(storm::modelchecker::RegionResult::AllViolated, regionChecker->analyzeRegion(allVioRegion, storm::modelchecker::RegionResultHypothesis::Unknown, storm::modelchecker::RegionResult::Unknown, true));
 
     carl::VariablePool::getInstance().clear();
 }
@@ -148,9 +148,9 @@ TEST(SparseDtmcParameterLiftingTest, Brp_Rew_exactValidation) {
     auto exBothRegion=storm::api::parseRegion<storm::RationalFunction>("0.6<=pK<=0.9,0.5<=TOMsg<=0.95", modelParameters);
     auto allVioRegion=storm::api::parseRegion<storm::RationalFunction>("0.1<=pK<=0.3,0.2<=TOMsg<=0.3", modelParameters);
 
-    EXPECT_EQ(storm::modelchecker::RegionResult::AllSat, regionChecker->analyzeRegion(allSatRegion, storm::modelchecker::RegionResult::Unknown, true));
-    EXPECT_EQ(storm::modelchecker::RegionResult::ExistsBoth, regionChecker->analyzeRegion(exBothRegion, storm::modelchecker::RegionResult::Unknown, true));
-    EXPECT_EQ(storm::modelchecker::RegionResult::AllViolated, regionChecker->analyzeRegion(allVioRegion, storm::modelchecker::RegionResult::Unknown, true));
+    EXPECT_EQ(storm::modelchecker::RegionResult::AllSat, regionChecker->analyzeRegion(allSatRegion, storm::modelchecker::RegionResultHypothesis::Unknown, storm::modelchecker::RegionResult::Unknown, true));
+    EXPECT_EQ(storm::modelchecker::RegionResult::ExistsBoth, regionChecker->analyzeRegion(exBothRegion, storm::modelchecker::RegionResultHypothesis::Unknown, storm::modelchecker::RegionResult::Unknown, true));
+    EXPECT_EQ(storm::modelchecker::RegionResult::AllViolated, regionChecker->analyzeRegion(allVioRegion, storm::modelchecker::RegionResultHypothesis::Unknown, storm::modelchecker::RegionResult::Unknown, true));
     
     carl::VariablePool::getInstance().clear();
 }
@@ -177,9 +177,9 @@ TEST(SparseDtmcParameterLiftingTest, Brp_Rew_Bounded_exactValidation) {
     auto exBothRegion=storm::api::parseRegion<storm::RationalFunction>("0.6<=pK<=0.9,0.5<=TOMsg<=0.95", modelParameters);
     auto allVioRegion=storm::api::parseRegion<storm::RationalFunction>("0.1<=pK<=0.3,0.2<=TOMsg<=0.3", modelParameters);
 
-    EXPECT_EQ(storm::modelchecker::RegionResult::AllSat, regionChecker->analyzeRegion(allSatRegion, storm::modelchecker::RegionResult::Unknown, true));
-    EXPECT_EQ(storm::modelchecker::RegionResult::ExistsBoth, regionChecker->analyzeRegion(exBothRegion, storm::modelchecker::RegionResult::Unknown, true));
-    EXPECT_EQ(storm::modelchecker::RegionResult::AllViolated, regionChecker->analyzeRegion(allVioRegion, storm::modelchecker::RegionResult::Unknown, true));
+    EXPECT_EQ(storm::modelchecker::RegionResult::AllSat, regionChecker->analyzeRegion(allSatRegion, storm::modelchecker::RegionResultHypothesis::Unknown, storm::modelchecker::RegionResult::Unknown, true));
+    EXPECT_EQ(storm::modelchecker::RegionResult::ExistsBoth, regionChecker->analyzeRegion(exBothRegion, storm::modelchecker::RegionResultHypothesis::Unknown, storm::modelchecker::RegionResult::Unknown, true));
+    EXPECT_EQ(storm::modelchecker::RegionResult::AllViolated, regionChecker->analyzeRegion(allVioRegion, storm::modelchecker::RegionResultHypothesis::Unknown, storm::modelchecker::RegionResult::Unknown, true));
     
     carl::VariablePool::getInstance().clear();
 }
@@ -204,7 +204,7 @@ TEST(SparseDtmcParameterLiftingTest, Brp_Rew_Infty) {
     //start testing
     auto allSatRegion=storm::api::parseRegion<storm::RationalFunction>("0.7<=pK<=0.9,0.6<=pL<=0.85,0.9<=TOMsg<=0.95,0.85<=TOAck<=0.9", modelParameters);
     
-    EXPECT_EQ(storm::modelchecker::RegionResult::AllSat, regionChecker->analyzeRegion(allSatRegion, storm::modelchecker::RegionResult::Unknown, true));
+    EXPECT_EQ(storm::modelchecker::RegionResult::AllSat, regionChecker->analyzeRegion(allSatRegion, storm::modelchecker::RegionResultHypothesis::Unknown, storm::modelchecker::RegionResult::Unknown, true));
 
     carl::VariablePool::getInstance().clear();
 }
@@ -231,9 +231,9 @@ TEST(SparseDtmcParameterLiftingTest, Brp_Rew_4Par) {
     auto exBothRegion=storm::api::parseRegion<storm::RationalFunction>("0.1<=pK<=0.7,0.2<=pL<=0.8,0.15<=TOMsg<=0.65,0.3<=TOAck<=0.9", modelParameters);
     auto allVioRegion=storm::api::parseRegion<storm::RationalFunction>("0.1<=pK<=0.4,0.2<=pL<=0.3,0.15<=TOMsg<=0.3,0.1<=TOAck<=0.2", modelParameters);
 
-    EXPECT_EQ(storm::modelchecker::RegionResult::AllSat, regionChecker->analyzeRegion(allSatRegion, storm::modelchecker::RegionResult::Unknown, true));
-    EXPECT_EQ(storm::modelchecker::RegionResult::ExistsBoth, regionChecker->analyzeRegion(exBothRegion, storm::modelchecker::RegionResult::Unknown, true));
-    EXPECT_EQ(storm::modelchecker::RegionResult::AllViolated, regionChecker->analyzeRegion(allVioRegion, storm::modelchecker::RegionResult::Unknown, true));
+    EXPECT_EQ(storm::modelchecker::RegionResult::AllSat, regionChecker->analyzeRegion(allSatRegion, storm::modelchecker::RegionResultHypothesis::Unknown, storm::modelchecker::RegionResult::Unknown, true));
+    EXPECT_EQ(storm::modelchecker::RegionResult::ExistsBoth, regionChecker->analyzeRegion(exBothRegion, storm::modelchecker::RegionResultHypothesis::Unknown, storm::modelchecker::RegionResult::Unknown, true));
+    EXPECT_EQ(storm::modelchecker::RegionResult::AllViolated, regionChecker->analyzeRegion(allVioRegion, storm::modelchecker::RegionResultHypothesis::Unknown, storm::modelchecker::RegionResult::Unknown, true));
     
     carl::VariablePool::getInstance().clear();
 }
@@ -262,10 +262,10 @@ TEST(SparseDtmcParameterLiftingTest, Crowds_Prob) {
     auto allVioRegion=storm::api::parseRegion<storm::RationalFunction>("0.8<=PF<=0.95,0.2<=badC<=0.2", modelParameters);
     auto allVioHardRegion=storm::api::parseRegion<storm::RationalFunction>("0.8<=PF<=0.95,0.2<=badC<=0.9", modelParameters);
 
-    EXPECT_EQ(storm::modelchecker::RegionResult::AllSat, regionChecker->analyzeRegion(allSatRegion, storm::modelchecker::RegionResult::Unknown, true));
-    EXPECT_EQ(storm::modelchecker::RegionResult::ExistsBoth, regionChecker->analyzeRegion(exBothRegion, storm::modelchecker::RegionResult::Unknown, true));
-    EXPECT_EQ(storm::modelchecker::RegionResult::AllViolated, regionChecker->analyzeRegion(allVioRegion, storm::modelchecker::RegionResult::Unknown, true));
-    EXPECT_EQ(storm::modelchecker::RegionResult::CenterViolated, regionChecker->analyzeRegion(allVioHardRegion, storm::modelchecker::RegionResult::Unknown, true));
+    EXPECT_EQ(storm::modelchecker::RegionResult::AllSat, regionChecker->analyzeRegion(allSatRegion, storm::modelchecker::RegionResultHypothesis::Unknown, storm::modelchecker::RegionResult::Unknown, true));
+    EXPECT_EQ(storm::modelchecker::RegionResult::ExistsBoth, regionChecker->analyzeRegion(exBothRegion, storm::modelchecker::RegionResultHypothesis::Unknown, storm::modelchecker::RegionResult::Unknown, true));
+    EXPECT_EQ(storm::modelchecker::RegionResult::AllViolated, regionChecker->analyzeRegion(allVioRegion, storm::modelchecker::RegionResultHypothesis::Unknown, storm::modelchecker::RegionResult::Unknown, true));
+    EXPECT_EQ(storm::modelchecker::RegionResult::CenterViolated, regionChecker->analyzeRegion(allVioHardRegion, storm::modelchecker::RegionResultHypothesis::Unknown, storm::modelchecker::RegionResult::Unknown, true));
 
     carl::VariablePool::getInstance().clear();
 }
@@ -294,10 +294,10 @@ TEST(SparseDtmcParameterLiftingTest, Crowds_Prob_stepBounded) {
     auto allVioRegion=storm::api::parseRegion<storm::RationalFunction>("0.8<=PF<=0.95,0.2<=badC<=0.2", modelParameters);
     auto allVioHardRegion=storm::api::parseRegion<storm::RationalFunction>("0.8<=PF<=0.95,0.2<=badC<=0.9", modelParameters);
 
-    EXPECT_EQ(storm::modelchecker::RegionResult::AllSat, regionChecker->analyzeRegion(allSatRegion, storm::modelchecker::RegionResult::Unknown, true));
-    EXPECT_EQ(storm::modelchecker::RegionResult::ExistsBoth, regionChecker->analyzeRegion(exBothRegion, storm::modelchecker::RegionResult::Unknown, true));
-    EXPECT_EQ(storm::modelchecker::RegionResult::AllViolated, regionChecker->analyzeRegion(allVioRegion, storm::modelchecker::RegionResult::Unknown, true));
-    EXPECT_EQ(storm::modelchecker::RegionResult::CenterViolated, regionChecker->analyzeRegion(allVioHardRegion, storm::modelchecker::RegionResult::Unknown, true));
+    EXPECT_EQ(storm::modelchecker::RegionResult::AllSat, regionChecker->analyzeRegion(allSatRegion, storm::modelchecker::RegionResultHypothesis::Unknown, storm::modelchecker::RegionResult::Unknown, true));
+    EXPECT_EQ(storm::modelchecker::RegionResult::ExistsBoth, regionChecker->analyzeRegion(exBothRegion, storm::modelchecker::RegionResultHypothesis::Unknown, storm::modelchecker::RegionResult::Unknown, true));
+    EXPECT_EQ(storm::modelchecker::RegionResult::AllViolated, regionChecker->analyzeRegion(allVioRegion, storm::modelchecker::RegionResultHypothesis::Unknown, storm::modelchecker::RegionResult::Unknown, true));
+    EXPECT_EQ(storm::modelchecker::RegionResult::CenterViolated, regionChecker->analyzeRegion(allVioHardRegion, storm::modelchecker::RegionResultHypothesis::Unknown, storm::modelchecker::RegionResult::Unknown, true));
 
     carl::VariablePool::getInstance().clear();
 }
@@ -326,9 +326,9 @@ TEST(SparseDtmcParameterLiftingTest, Crowds_Prob_1Par) {
     auto exBothRegion=storm::api::parseRegion<storm::RationalFunction>("0.8<=PF<=0.9", modelParameters);
     auto allVioRegion=storm::api::parseRegion<storm::RationalFunction>("0.01<=PF<=0.8", modelParameters);
 
-    EXPECT_EQ(storm::modelchecker::RegionResult::AllSat, regionChecker->analyzeRegion(allSatRegion, storm::modelchecker::RegionResult::Unknown, true));
-    EXPECT_EQ(storm::modelchecker::RegionResult::ExistsBoth, regionChecker->analyzeRegion(exBothRegion, storm::modelchecker::RegionResult::Unknown, true));
-    EXPECT_EQ(storm::modelchecker::RegionResult::AllViolated, regionChecker->analyzeRegion(allVioRegion, storm::modelchecker::RegionResult::Unknown, true));
+    EXPECT_EQ(storm::modelchecker::RegionResult::AllSat, regionChecker->analyzeRegion(allSatRegion, storm::modelchecker::RegionResultHypothesis::Unknown, storm::modelchecker::RegionResult::Unknown, true));
+    EXPECT_EQ(storm::modelchecker::RegionResult::ExistsBoth, regionChecker->analyzeRegion(exBothRegion, storm::modelchecker::RegionResultHypothesis::Unknown, storm::modelchecker::RegionResult::Unknown, true));
+    EXPECT_EQ(storm::modelchecker::RegionResult::AllViolated, regionChecker->analyzeRegion(allVioRegion, storm::modelchecker::RegionResultHypothesis::Unknown, storm::modelchecker::RegionResult::Unknown, true));
     
     carl::VariablePool::getInstance().clear();
 }
@@ -354,7 +354,7 @@ TEST(SparseDtmcParameterLiftingTest, Crowds_Prob_Const) {
     //start testing
     auto allSatRegion=storm::api::parseRegion<storm::RationalFunction>("", modelParameters);
     
-    EXPECT_EQ(storm::modelchecker::RegionResult::AllSat, regionChecker->analyzeRegion(allSatRegion, storm::modelchecker::RegionResult::Unknown, true));
+    EXPECT_EQ(storm::modelchecker::RegionResult::AllSat, regionChecker->analyzeRegion(allSatRegion, storm::modelchecker::RegionResultHypothesis::Unknown, storm::modelchecker::RegionResult::Unknown, true));
 
     carl::VariablePool::getInstance().clear();
 }

src/test/storm-pars/modelchecker/SparseMdpParameterLiftingTest.cpp

@@ -30,9 +30,9 @@ TEST(SparseMdpParameterLiftingTest, two_dice_Prob) {
     auto allVioRegion = storm::api::parseRegion<storm::RationalFunction>("0.6<=p1<=0.7,0.6<=p2<=0.6", modelParameters);
 
     
-    EXPECT_EQ(storm::modelchecker::RegionResult::AllSat, regionChecker->analyzeRegion(allSatRegion, storm::modelchecker::RegionResult::Unknown, true));
-    EXPECT_EQ(storm::modelchecker::RegionResult::ExistsBoth, regionChecker->analyzeRegion(exBothRegion, storm::modelchecker::RegionResult::Unknown, true));
-    EXPECT_EQ(storm::modelchecker::RegionResult::AllViolated, regionChecker->analyzeRegion(allVioRegion, storm::modelchecker::RegionResult::Unknown, true));
+    EXPECT_EQ(storm::modelchecker::RegionResult::AllSat, regionChecker->analyzeRegion(allSatRegion, storm::modelchecker::RegionResultHypothesis::Unknown, storm::modelchecker::RegionResult::Unknown, true));
+    EXPECT_EQ(storm::modelchecker::RegionResult::ExistsBoth, regionChecker->analyzeRegion(exBothRegion, storm::modelchecker::RegionResultHypothesis::Unknown, storm::modelchecker::RegionResult::Unknown, true));
+    EXPECT_EQ(storm::modelchecker::RegionResult::AllViolated, regionChecker->analyzeRegion(allVioRegion, storm::modelchecker::RegionResultHypothesis::Unknown, storm::modelchecker::RegionResult::Unknown, true));
     
     carl::VariablePool::getInstance().clear();
 }
@@ -59,9 +59,9 @@ TEST(SparseMdpParameterLiftingTest, two_dice_Prob_bounded) {
     auto allVioRegion = storm::api::parseRegion<storm::RationalFunction>("0.6<=p1<=0.7,0.6<=p2<=0.6", modelParameters);
 
     
-    EXPECT_EQ(storm::modelchecker::RegionResult::AllSat, regionChecker->analyzeRegion(allSatRegion, storm::modelchecker::RegionResult::Unknown, true));
-    EXPECT_EQ(storm::modelchecker::RegionResult::ExistsBoth, regionChecker->analyzeRegion(exBothRegion, storm::modelchecker::RegionResult::Unknown, true));
-    EXPECT_EQ(storm::modelchecker::RegionResult::AllViolated, regionChecker->analyzeRegion(allVioRegion, storm::modelchecker::RegionResult::Unknown, true));
+    EXPECT_EQ(storm::modelchecker::RegionResult::AllSat, regionChecker->analyzeRegion(allSatRegion, storm::modelchecker::RegionResultHypothesis::Unknown, storm::modelchecker::RegionResult::Unknown, true));
+    EXPECT_EQ(storm::modelchecker::RegionResult::ExistsBoth, regionChecker->analyzeRegion(exBothRegion, storm::modelchecker::RegionResultHypothesis::Unknown, storm::modelchecker::RegionResult::Unknown, true));
+    EXPECT_EQ(storm::modelchecker::RegionResult::AllViolated, regionChecker->analyzeRegion(allVioRegion, storm::modelchecker::RegionResultHypothesis::Unknown, storm::modelchecker::RegionResult::Unknown, true));
     
     carl::VariablePool::getInstance().clear();
 }
@@ -88,9 +88,9 @@ TEST(SparseMdpParameterLiftingTest, two_dice_Prob_exactValidation) {
     auto allVioRegion = storm::api::parseRegion<storm::RationalFunction>("0.6<=p1<=0.7,0.6<=p2<=0.6", modelParameters);
 
     
-    EXPECT_EQ(storm::modelchecker::RegionResult::AllSat, regionChecker->analyzeRegion(allSatRegion, storm::modelchecker::RegionResult::Unknown, true));
-    EXPECT_EQ(storm::modelchecker::RegionResult::ExistsBoth, regionChecker->analyzeRegion(exBothRegion, storm::modelchecker::RegionResult::Unknown, true));
-    EXPECT_EQ(storm::modelchecker::RegionResult::AllViolated, regionChecker->analyzeRegion(allVioRegion, storm::modelchecker::RegionResult::Unknown, true));
+    EXPECT_EQ(storm::modelchecker::RegionResult::AllSat, regionChecker->analyzeRegion(allSatRegion, storm::modelchecker::RegionResultHypothesis::Unknown, storm::modelchecker::RegionResult::Unknown, true));
+    EXPECT_EQ(storm::modelchecker::RegionResult::ExistsBoth, regionChecker->analyzeRegion(exBothRegion, storm::modelchecker::RegionResultHypothesis::Unknown, storm::modelchecker::RegionResult::Unknown, true));
+    EXPECT_EQ(storm::modelchecker::RegionResult::AllViolated, regionChecker->analyzeRegion(allVioRegion, storm::modelchecker::RegionResultHypothesis::Unknown, storm::modelchecker::RegionResult::Unknown, true));
     
     carl::VariablePool::getInstance().clear();
 }
@@ -117,9 +117,9 @@ TEST(SparseMdpParameterLiftingTest, two_dice_Prob_bounded_exactValidation) {
     auto allVioRegion = storm::api::parseRegion<storm::RationalFunction>("0.6<=p1<=0.7,0.6<=p2<=0.6", modelParameters);
 
     
-    EXPECT_EQ(storm::modelchecker::RegionResult::AllSat, regionChecker->analyzeRegion(allSatRegion, storm::modelchecker::RegionResult::Unknown, true));
-    EXPECT_EQ(storm::modelchecker::RegionResult::ExistsBoth, regionChecker->analyzeRegion(exBothRegion, storm::modelchecker::RegionResult::Unknown, true));
-    EXPECT_EQ(storm::modelchecker::RegionResult::AllViolated, regionChecker->analyzeRegion(allVioRegion, storm::modelchecker::RegionResult::Unknown, true));
+    EXPECT_EQ(storm::modelchecker::RegionResult::AllSat, regionChecker->analyzeRegion(allSatRegion, storm::modelchecker::RegionResultHypothesis::Unknown, storm::modelchecker::RegionResult::Unknown, true));
+    EXPECT_EQ(storm::modelchecker::RegionResult::ExistsBoth, regionChecker->analyzeRegion(exBothRegion, storm::modelchecker::RegionResultHypothesis::Unknown, storm::modelchecker::RegionResult::Unknown, true));
+    EXPECT_EQ(storm::modelchecker::RegionResult::AllViolated, regionChecker->analyzeRegion(allVioRegion, storm::modelchecker::RegionResultHypothesis::Unknown, storm::modelchecker::RegionResult::Unknown, true));
     
     carl::VariablePool::getInstance().clear();
 }
@@ -144,9 +144,9 @@ TEST(SparseMdpParameterLiftingTest, coin_Prob) {
     auto exBothRegion = storm::api::parseRegion<storm::RationalFunction>("0.4<=p1<=0.65,0.5<=p2<=0.7", modelParameters);
     auto allVioRegion = storm::api::parseRegion<storm::RationalFunction>("0.4<=p1<=0.7,0.55<=p2<=0.6", modelParameters);
         
-    EXPECT_EQ(storm::modelchecker::RegionResult::AllSat, regionChecker->analyzeRegion(allSatRegion, storm::modelchecker::RegionResult::Unknown, true));
-    EXPECT_EQ(storm::modelchecker::RegionResult::ExistsBoth, regionChecker->analyzeRegion(exBothRegion, storm::modelchecker::RegionResult::Unknown, true));
-    EXPECT_EQ(storm::modelchecker::RegionResult::AllViolated, regionChecker->analyzeRegion(allVioRegion, storm::modelchecker::RegionResult::Unknown, true));
+    EXPECT_EQ(storm::modelchecker::RegionResult::AllSat, regionChecker->analyzeRegion(allSatRegion, storm::modelchecker::RegionResultHypothesis::Unknown, storm::modelchecker::RegionResult::Unknown, true));
+    EXPECT_EQ(storm::modelchecker::RegionResult::ExistsBoth, regionChecker->analyzeRegion(exBothRegion, storm::modelchecker::RegionResultHypothesis::Unknown, storm::modelchecker::RegionResult::Unknown, true));
+    EXPECT_EQ(storm::modelchecker::RegionResult::AllViolated, regionChecker->analyzeRegion(allVioRegion, storm::modelchecker::RegionResultHypothesis::Unknown, storm::modelchecker::RegionResult::Unknown, true));
 
     carl::VariablePool::getInstance().clear();
 }
@@ -173,9 +173,9 @@ TEST(SparseMdpParameterLiftingTest, brp_Prop) {
     auto exBothRegion=storm::api::parseRegion<storm::RationalFunction>("0.4<=pL<=0.65,0.75<=pK<=0.95", modelParameters);
     auto allVioRegion=storm::api::parseRegion<storm::RationalFunction>("0.1<=pL<=0.73,0.2<=pK<=0.715", modelParameters);
         
-    EXPECT_EQ(storm::modelchecker::RegionResult::AllSat, regionChecker->analyzeRegion(allSatRegion, storm::modelchecker::RegionResult::Unknown, true));
-    EXPECT_EQ(storm::modelchecker::RegionResult::ExistsBoth, regionChecker->analyzeRegion(exBothRegion, storm::modelchecker::RegionResult::Unknown, true));
-    EXPECT_EQ(storm::modelchecker::RegionResult::AllViolated, regionChecker->analyzeRegion(allVioRegion, storm::modelchecker::RegionResult::Unknown, true));
+    EXPECT_EQ(storm::modelchecker::RegionResult::AllSat, regionChecker->analyzeRegion(allSatRegion, storm::modelchecker::RegionResultHypothesis::Unknown, storm::modelchecker::RegionResult::Unknown, true));
+    EXPECT_EQ(storm::modelchecker::RegionResult::ExistsBoth, regionChecker->analyzeRegion(exBothRegion, storm::modelchecker::RegionResultHypothesis::Unknown, storm::modelchecker::RegionResult::Unknown, true));
+    EXPECT_EQ(storm::modelchecker::RegionResult::AllViolated, regionChecker->analyzeRegion(allVioRegion, storm::modelchecker::RegionResultHypothesis::Unknown, storm::modelchecker::RegionResult::Unknown, true));
 
     carl::VariablePool::getInstance().clear();
 }
@@ -203,9 +203,9 @@ TEST(SparseMdpParameterLiftingTest, brp_Rew) {
     auto exBothRegion=storm::api::parseRegion<storm::RationalFunction>("0.6<=pK<=0.9,0.5<=TOMsg<=0.95", modelParameters);
     auto allVioRegion=storm::api::parseRegion<storm::RationalFunction>("0.1<=pK<=0.3,0.2<=TOMsg<=0.3", modelParameters);
 
-    EXPECT_EQ(storm::modelchecker::RegionResult::AllSat, regionChecker->analyzeRegion(allSatRegion, storm::modelchecker::RegionResult::Unknown, true));
-    EXPECT_EQ(storm::modelchecker::RegionResult::ExistsBoth, regionChecker->analyzeRegion(exBothRegion, storm::modelchecker::RegionResult::Unknown, true));
-    EXPECT_EQ(storm::modelchecker::RegionResult::AllViolated, regionChecker->analyzeRegion(allVioRegion, storm::modelchecker::RegionResult::Unknown, true));
+    EXPECT_EQ(storm::modelchecker::RegionResult::AllSat, regionChecker->analyzeRegion(allSatRegion, storm::modelchecker::RegionResultHypothesis::Unknown, storm::modelchecker::RegionResult::Unknown, true));
+    EXPECT_EQ(storm::modelchecker::RegionResult::ExistsBoth, regionChecker->analyzeRegion(exBothRegion, storm::modelchecker::RegionResultHypothesis::Unknown, storm::modelchecker::RegionResult::Unknown, true));
+    EXPECT_EQ(storm::modelchecker::RegionResult::AllViolated, regionChecker->analyzeRegion(allVioRegion, storm::modelchecker::RegionResultHypothesis::Unknown, storm::modelchecker::RegionResult::Unknown, true));
 
     carl::VariablePool::getInstance().clear();
 }
@@ -232,9 +232,9 @@ TEST(SparseMdpParameterLiftingTest, brp_Rew_bounded) {
     auto exBothRegion=storm::api::parseRegion<storm::RationalFunction>("0.6<=pK<=0.9,0.5<=TOMsg<=0.95", modelParameters);
     auto allVioRegion=storm::api::parseRegion<storm::RationalFunction>("0.1<=pK<=0.3,0.2<=TOMsg<=0.3", modelParameters);
 
-    EXPECT_EQ(storm::modelchecker::RegionResult::AllSat, regionChecker->analyzeRegion(allSatRegion, storm::modelchecker::RegionResult::Unknown, true));
-    EXPECT_EQ(storm::modelchecker::RegionResult::ExistsBoth, regionChecker->analyzeRegion(exBothRegion, storm::modelchecker::RegionResult::Unknown, true));
-    EXPECT_EQ(storm::modelchecker::RegionResult::AllViolated, regionChecker->analyzeRegion(allVioRegion, storm::modelchecker::RegionResult::Unknown, true));
+    EXPECT_EQ(storm::modelchecker::RegionResult::AllSat, regionChecker->analyzeRegion(allSatRegion, storm::modelchecker::RegionResultHypothesis::Unknown, storm::modelchecker::RegionResult::Unknown, true));
+    EXPECT_EQ(storm::modelchecker::RegionResult::ExistsBoth, regionChecker->analyzeRegion(exBothRegion, storm::modelchecker::RegionResultHypothesis::Unknown, storm::modelchecker::RegionResult::Unknown, true));
+    EXPECT_EQ(storm::modelchecker::RegionResult::AllViolated, regionChecker->analyzeRegion(allVioRegion, storm::modelchecker::RegionResultHypothesis::Unknown, storm::modelchecker::RegionResult::Unknown, true));
 
     carl::VariablePool::getInstance().clear();
 }
@@ -260,7 +260,7 @@ TEST(SparseMdpParameterLiftingTest, Brp_Rew_Infty) {
     //start testing
     auto allSatRegion=storm::api::parseRegion<storm::RationalFunction>("0.7<=pK<=0.9,0.6<=pL<=0.85,0.9<=TOMsg<=0.95,0.85<=TOAck<=0.9", modelParameters);
     
-    EXPECT_EQ(storm::modelchecker::RegionResult::AllSat, regionChecker->analyzeRegion(allSatRegion, storm::modelchecker::RegionResult::Unknown, true));
+    EXPECT_EQ(storm::modelchecker::RegionResult::AllSat, regionChecker->analyzeRegion(allSatRegion, storm::modelchecker::RegionResultHypothesis::Unknown, storm::modelchecker::RegionResult::Unknown, true));
 
     carl::VariablePool::getInstance().clear();
 }
@@ -287,9 +287,9 @@ TEST(SparseMdpParameterLiftingTest, Brp_Rew_4Par) {
     auto exBothRegion=storm::api::parseRegion<storm::RationalFunction>("0.1<=pK<=0.7,0.2<=pL<=0.8,0.15<=TOMsg<=0.65,0.3<=TOAck<=0.9", modelParameters);
     auto allVioRegion=storm::api::parseRegion<storm::RationalFunction>("0.1<=pK<=0.4,0.2<=pL<=0.3,0.15<=TOMsg<=0.3,0.1<=TOAck<=0.2", modelParameters);
 
-    EXPECT_EQ(storm::modelchecker::RegionResult::AllSat, regionChecker->analyzeRegion(allSatRegion, storm::modelchecker::RegionResult::Unknown, true));
-    EXPECT_EQ(storm::modelchecker::RegionResult::ExistsBoth, regionChecker->analyzeRegion(exBothRegion, storm::modelchecker::RegionResult::Unknown, true));
-    EXPECT_EQ(storm::modelchecker::RegionResult::AllViolated, regionChecker->analyzeRegion(allVioRegion, storm::modelchecker::RegionResult::Unknown, true));
+    EXPECT_EQ(storm::modelchecker::RegionResult::AllSat, regionChecker->analyzeRegion(allSatRegion, storm::modelchecker::RegionResultHypothesis::Unknown, storm::modelchecker::RegionResult::Unknown, true));
+    EXPECT_EQ(storm::modelchecker::RegionResult::ExistsBoth, regionChecker->analyzeRegion(exBothRegion, storm::modelchecker::RegionResultHypothesis::Unknown, storm::modelchecker::RegionResult::Unknown, true));
+    EXPECT_EQ(storm::modelchecker::RegionResult::AllViolated, regionChecker->analyzeRegion(allVioRegion, storm::modelchecker::RegionResultHypothesis::Unknown, storm::modelchecker::RegionResult::Unknown, true));
     
     carl::VariablePool::getInstance().clear();
 }

src/test/storm/logic/FragmentCheckerTest.cpp

@@ -145,26 +145,17 @@ TEST(FragmentCheckerTest, MultiObjective) {
     std::shared_ptr<storm::logic::Formula const> formula;
     
     ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString("\"label\""));
-    EXPECT_TRUE(checker.conformsToSpecification(*formula, multiobjective));
+    EXPECT_FALSE(checker.conformsToSpecification(*formula, multiobjective));
     
     ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString("P=? [F \"label\"]"));
-    EXPECT_TRUE(checker.conformsToSpecification(*formula, multiobjective));
-    
-    ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString("P=? [F P=? [F \"label\"]]"));
-    EXPECT_TRUE(checker.conformsToSpecification(*formula, multiobjective));
-    
-    ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString("R=? [F \"label\"]"));
-    EXPECT_TRUE(checker.conformsToSpecification(*formula, multiobjective));
-    
-    ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString("R=? [C]"));
-    EXPECT_TRUE(checker.conformsToSpecification(*formula, multiobjective));
-    
-    ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString("P=? [F[0.5,1] \"label\"]"));
-    EXPECT_TRUE(checker.conformsToSpecification(*formula, multiobjective));
+    EXPECT_FALSE(checker.conformsToSpecification(*formula, multiobjective));
     
     ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString("multi(R<0.3 [ C ], P<0.6 [F \"label\"] & \"label\" & R<=4[F \"label\"])"));
     EXPECT_FALSE(checker.conformsToSpecification(*formula, multiobjective));
     
+    ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString("Pmax=? [ F multi(R<0.3 [ C ], P<0.6 [F \"label\"] & \"label\" & R<=4[F \"label\"])]"));
+    EXPECT_FALSE(checker.conformsToSpecification(*formula, multiobjective));
+    
     ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString("multi(R<0.3 [ C ], P<0.6 [F \"label\"], \"label\", R<=4[F \"label\"])"));
     EXPECT_FALSE(checker.conformsToSpecification(*formula, multiobjective));