diff --git a/src/storm-pars-cli/storm-pars.cpp b/src/storm-pars-cli/storm-pars.cpp index bc52f85dc..52d6dff39 100644 --- a/src/storm-pars-cli/storm-pars.cpp +++ b/src/storm-pars-cli/storm-pars.cpp @@ -224,7 +224,7 @@ namespace storm { STORM_PRINT_AND_LOG(" with iterative refinement until " << (1.0 - regionSettings.getRefinementThreshold()) * 100.0 << "% is covered." << std::endl); verificationCallback = [&] (std::shared_ptr const& formula) { ValueType refinementThreshold = storm::utility::convertNumber(regionSettings.getRefinementThreshold()); - std::unique_ptr> result = storm::api::checkAndRefineRegionWithSparseEngine(model, storm::api::createTask(formula, true), regions.front(), refinementThreshold, engine); + std::unique_ptr> result = storm::api::checkAndRefineRegionWithSparseEngine(model, storm::api::createTask(formula, true), regions.front(), engine, refinementThreshold); return result; }; } else { @@ -237,7 +237,7 @@ namespace storm { postprocessingCallback = [&] (std::unique_ptr const& result) { if (parametricSettings.exportResultToFile()) { - storm::api::exportRegionCheckResultToFile(result, parametricSettings.exportResultPath()); + storm::api::exportRegionCheckResultToFile(result, parametricSettings.exportResultPath(), false); } }; diff --git a/src/storm-pars/api/region.h b/src/storm-pars/api/region.h index a8cc6bbe2..85a481d2d 100644 --- a/src/storm-pars/api/region.h +++ b/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 - std::unique_ptr> checkRegionsWithSparseEngine(std::shared_ptr> const& model, storm::modelchecker::CheckTask const& task, std::vector> const& regions, storm::modelchecker::RegionCheckEngine engine) { + std::unique_ptr> checkRegionsWithSparseEngine(std::shared_ptr> const& model, storm::modelchecker::CheckTask const& task, std::vector> const& regions, storm::modelchecker::RegionCheckEngine engine, std::vector const& hypotheses, bool sampleVerticesOfRegions) { auto regionChecker = initializeRegionModelChecker(model, task, engine); - return regionChecker->analyzeRegions(regions, true); + return regionChecker->analyzeRegions(regions, hypotheses, sampleVerticesOfRegions); } - template - std::unique_ptr> checkAndRefineRegionWithSparseEngine(std::shared_ptr> const& model, storm::modelchecker::CheckTask const& task, storm::storage::ParameterRegion const& region, ValueType const& refinementThreshold, storm::modelchecker::RegionCheckEngine engine) { + std::unique_ptr> checkRegionsWithSparseEngine(std::shared_ptr> const& model, storm::modelchecker::CheckTask const& task, std::vector> const& regions, storm::modelchecker::RegionCheckEngine engine, storm::modelchecker::RegionResultHypothesis const& hypothesis = storm::modelchecker::RegionResultHypothesis::Unknown, bool sampleVerticesOfRegions = false) { + std::vector 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 + std::unique_ptr> checkAndRefineRegionWithSparseEngine(std::shared_ptr> const& model, storm::modelchecker::CheckTask const& task, storm::storage::ParameterRegion const& region, storm::modelchecker::RegionCheckEngine engine, boost::optional const& coverageThreshold, boost::optional 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 - void exportRegionCheckResultToFile(std::unique_ptr const& checkResult, std::string const& filename) { + void exportRegionCheckResultToFile(std::unique_ptr const& checkResult, std::string const& filename, bool onlyConclusiveResults = false) { auto const* regionCheckResult = dynamic_cast 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; + } } } diff --git a/src/storm-pars/modelchecker/region/RegionModelChecker.cpp b/src/storm-pars/modelchecker/region/RegionModelChecker.cpp index a2a19451d..23ba29489 100644 --- a/src/storm-pars/modelchecker/region/RegionModelChecker.cpp +++ b/src/storm-pars/modelchecker/region/RegionModelChecker.cpp @@ -28,31 +28,40 @@ namespace storm { } template - std::unique_ptr> RegionModelChecker::analyzeRegions(std::vector> const& regions, bool sampleVerticesOfRegion) { + std::unique_ptr> RegionModelChecker::analyzeRegions(std::vector> const& regions, std::vector 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, 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>(std::move(result)); } template - std::unique_ptr> RegionModelChecker::performRegionRefinement(storm::storage::ParameterRegion const& region, ParametricType const& threshold) { + std::unique_ptr> RegionModelChecker::performRegionRefinement(storm::storage::ParameterRegion const& region, boost::optional const& coverageThreshold, boost::optional depthThreshold, RegionResultHypothesis const& hypothesis) { STORM_LOG_INFO("Applying refinement on region: " << region.toString(true) << " ."); - auto thresholdAsCoefficient = storm::utility::convertNumber(threshold); + auto thresholdAsCoefficient = coverageThreshold ? storm::utility::convertNumber(coverageThreshold.get()) : storm::utility::zero(); auto areaOfParameterSpace = region.area(); auto fractionOfUndiscoveredArea = storm::utility::one(); auto fractionOfAllSatArea = storm::utility::zero(); auto fractionOfAllViolatedArea = storm::utility::zero(); - std::queue, RegionResult>> unprocessedRegions; + // The resulting (sub-)regions std::vector, RegionResult>> result; + + // FIFO queues storing the data for the regions that we still need to process. + std::queue, RegionResult>> unprocessedRegions; + std::queue refinementDepths; unprocessedRegions.emplace(region, RegionResult::Unknown); + refinementDepths.push(0); + uint_fast64_t numOfAnalyzedRegions = 0; CoefficientType displayedProgress = storm::utility::zero(); if (storm::settings::getModule().isShowStatisticsSet()) { @@ -69,12 +78,13 @@ namespace storm { displayedProgress = storm::utility::zero(); } - 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(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(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> 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> 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().isShowStatisticsSet()) { while (displayedProgress < storm::utility::one() - 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().isShowStatisticsSet()) { while (displayedProgress < storm::utility::one()) { STORM_PRINT_AND_LOG("-"); diff --git a/src/storm-pars/modelchecker/region/RegionModelChecker.h b/src/storm-pars/modelchecker/region/RegionModelChecker.h index a8f1fdf01..c1a558800 100644 --- a/src/storm-pars/modelchecker/region/RegionModelChecker.h +++ b/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 const& region, RegionResult const& initialResult = RegionResult::Unknown, bool sampleVerticesOfRegion = false) = 0; + virtual RegionResult analyzeRegion(storm::storage::ParameterRegion 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> analyzeRegions(std::vector> const& regions, bool sampleVerticesOfRegion = false) ; + std::unique_ptr> analyzeRegions(std::vector> const& regions, std::vector 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> performRegionRefinement(storm::storage::ParameterRegion const& region, ParametricType const& threshold); + std::unique_ptr> performRegionRefinement(storm::storage::ParameterRegion const& region, boost::optional const& coverageThreshold, boost::optional depthThreshold = boost::none, RegionResultHypothesis const& hypothesis = RegionResultHypothesis::Unknown); }; diff --git a/src/storm-pars/modelchecker/region/RegionResultHypothesis.cpp b/src/storm-pars/modelchecker/region/RegionResultHypothesis.cpp new file mode 100644 index 000000000..3f0968fbc --- /dev/null +++ b/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; + } + } +} diff --git a/src/storm-pars/modelchecker/region/RegionResultHypothesis.h b/src/storm-pars/modelchecker/region/RegionResultHypothesis.h new file mode 100644 index 000000000..3288fba9c --- /dev/null +++ b/src/storm-pars/modelchecker/region/RegionResultHypothesis.h @@ -0,0 +1,19 @@ +#pragma once + +#include + +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); + } +} + diff --git a/src/storm-pars/modelchecker/region/SparseParameterLiftingModelChecker.cpp b/src/storm-pars/modelchecker/region/SparseParameterLiftingModelChecker.cpp index 17610df87..d0b2af22b 100644 --- a/src/storm-pars/modelchecker/region/SparseParameterLiftingModelChecker.cpp +++ b/src/storm-pars/modelchecker/region/SparseParameterLiftingModelChecker.cpp @@ -47,8 +47,8 @@ namespace storm { } template - RegionResult SparseParameterLiftingModelChecker::analyzeRegion(storm::storage::ParameterRegion const& region, RegionResult const& initialResult, bool sampleVerticesOfRegion) { - + RegionResult SparseParameterLiftingModelChecker::analyzeRegion(storm::storage::ParameterRegion 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()]) { diff --git a/src/storm-pars/modelchecker/region/SparseParameterLiftingModelChecker.h b/src/storm-pars/modelchecker/region/SparseParameterLiftingModelChecker.h index b8abd518c..e0cabd5f0 100644 --- a/src/storm-pars/modelchecker/region/SparseParameterLiftingModelChecker.h +++ b/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 const& region, RegionResult const& initialResult = RegionResult::Unknown, bool sampleVerticesOfRegion = false) override; + virtual RegionResult analyzeRegion(storm::storage::ParameterRegion 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. diff --git a/src/storm-pars/modelchecker/region/ValidatingSparseParameterLiftingModelChecker.cpp b/src/storm-pars/modelchecker/region/ValidatingSparseParameterLiftingModelChecker.cpp index d3dabab63..8f3ffaad3 100644 --- a/src/storm-pars/modelchecker/region/ValidatingSparseParameterLiftingModelChecker.cpp +++ b/src/storm-pars/modelchecker/region/ValidatingSparseParameterLiftingModelChecker.cpp @@ -28,9 +28,10 @@ namespace storm { }; template - RegionResult ValidatingSparseParameterLiftingModelChecker::analyzeRegion(storm::storage::ParameterRegion const& region, RegionResult const& initialResult, bool sampleVerticesOfRegion) { + RegionResult ValidatingSparseParameterLiftingModelChecker::analyzeRegion(storm::storage::ParameterRegion 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; + } } } } diff --git a/src/storm-pars/modelchecker/region/ValidatingSparseParameterLiftingModelChecker.h b/src/storm-pars/modelchecker/region/ValidatingSparseParameterLiftingModelChecker.h index 7f9789ebf..8fa6a4114 100644 --- a/src/storm-pars/modelchecker/region/ValidatingSparseParameterLiftingModelChecker.h +++ b/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 const& region, RegionResult const& initialResult = RegionResult::Unknown, bool sampleVerticesOfRegion = false) override; + virtual RegionResult analyzeRegion(storm::storage::ParameterRegion const& region, RegionResultHypothesis const& hypothesis = RegionResultHypothesis::Unknown, RegionResult const& initialResult = RegionResult::Unknown, bool sampleVerticesOfRegion = false) override; protected: diff --git a/src/storm-pars/modelchecker/results/RegionRefinementCheckResult.cpp b/src/storm-pars/modelchecker/results/RegionRefinementCheckResult.cpp index 3cf8d1e1d..605865c04 100644 --- a/src/storm-pars/modelchecker/results/RegionRefinementCheckResult.cpp +++ b/src/storm-pars/modelchecker/results/RegionRefinementCheckResult.cpp @@ -58,6 +58,9 @@ namespace storm { bool currRegionComplete = false; CoefficientType coveredArea = storm::utility::zero(); 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 interesctionSizeX = std::min(xUpper, r.first.getUpperBoundary(x)) - std::max(xLower, r.first.getLowerBoundary(x)); diff --git a/src/test/storm-pars/modelchecker/SparseDtmcParameterLiftingTest.cpp b/src/test/storm-pars/modelchecker/SparseDtmcParameterLiftingTest.cpp index 31def397a..f87f4c652 100644 --- a/src/test/storm-pars/modelchecker/SparseDtmcParameterLiftingTest.cpp +++ b/src/test/storm-pars/modelchecker/SparseDtmcParameterLiftingTest.cpp @@ -31,9 +31,9 @@ TEST(SparseDtmcParameterLiftingTest, Brp_Prob) { auto exBothRegion=storm::api::parseRegion("0.4<=pL<=0.65,0.75<=pK<=0.95", modelParameters); auto allVioRegion=storm::api::parseRegion("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("0.6<=pK<=0.9,0.5<=TOMsg<=0.95", modelParameters); auto allVioRegion=storm::api::parseRegion("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("0.6<=pK<=0.9,0.5<=TOMsg<=0.95", modelParameters); auto allVioRegion=storm::api::parseRegion("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("0.4<=pL<=0.65,0.75<=pK<=0.95", modelParameters); auto allVioRegion=storm::api::parseRegion("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("0.6<=pK<=0.9,0.5<=TOMsg<=0.95", modelParameters); auto allVioRegion=storm::api::parseRegion("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("0.6<=pK<=0.9,0.5<=TOMsg<=0.95", modelParameters); auto allVioRegion=storm::api::parseRegion("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("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("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("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("0.8<=PF<=0.95,0.2<=badC<=0.2", modelParameters); auto allVioHardRegion=storm::api::parseRegion("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("0.8<=PF<=0.95,0.2<=badC<=0.2", modelParameters); auto allVioHardRegion=storm::api::parseRegion("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("0.8<=PF<=0.9", modelParameters); auto allVioRegion=storm::api::parseRegion("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("", 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(); } diff --git a/src/test/storm-pars/modelchecker/SparseMdpParameterLiftingTest.cpp b/src/test/storm-pars/modelchecker/SparseMdpParameterLiftingTest.cpp index fd690b876..b5a4138ec 100644 --- a/src/test/storm-pars/modelchecker/SparseMdpParameterLiftingTest.cpp +++ b/src/test/storm-pars/modelchecker/SparseMdpParameterLiftingTest.cpp @@ -30,9 +30,9 @@ TEST(SparseMdpParameterLiftingTest, two_dice_Prob) { auto allVioRegion = storm::api::parseRegion("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("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("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("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("0.4<=p1<=0.65,0.5<=p2<=0.7", modelParameters); auto allVioRegion = storm::api::parseRegion("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("0.4<=pL<=0.65,0.75<=pK<=0.95", modelParameters); auto allVioRegion=storm::api::parseRegion("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("0.6<=pK<=0.9,0.5<=TOMsg<=0.95", modelParameters); auto allVioRegion=storm::api::parseRegion("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("0.6<=pK<=0.9,0.5<=TOMsg<=0.95", modelParameters); auto allVioRegion=storm::api::parseRegion("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("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("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("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(); }