diff --git a/.travis.yml b/.travis.yml
index 4995abe2d..7279e2999 100644
--- a/.travis.yml
+++ b/.travis.yml
@@ -39,31 +39,6 @@ jobs:
# Stage: Build (1st run)
###
- # osx
- - stage: Build (1st run)
- os: osx
- osx_image: xcode9.1
- compiler: clang
- env: CONFIG=DefaultDebug COMPILER=clang STL=libc++
- install:
- - rm -rf build
- - travis/install_osx.sh
- script:
- - travis/build.sh Build1
- after_failure:
- - find build -iname '*err*.log' -type f -print -exec cat {} \;
- - stage: Build (1st run)
- os: osx
- osx_image: xcode9.1
- compiler: clang
- env: CONFIG=DefaultRelease COMPILER=clang STL=libc++
- install:
- - rm -rf build
- - travis/install_osx.sh
- script:
- - travis/build.sh Build1
- after_failure:
- - find build -iname '*err*.log' -type f -print -exec cat {} \;
# ubuntu-16.10
- stage: Build (1st run)
os: linux
@@ -96,29 +71,6 @@ jobs:
# Stage: Build (2nd run)
###
- # osx
- - stage: Build (2nd run)
- os: osx
- osx_image: xcode9.1
- compiler: clang
- env: CONFIG=DefaultDebug COMPILER=clang STL=libc++
- install:
- - travis/install_osx.sh
- script:
- - travis/build.sh Build2
- after_failure:
- - find build -iname '*err*.log' -type f -print -exec cat {} \;
- - stage: Build (2nd run)
- os: osx
- osx_image: xcode9.1
- compiler: clang
- env: CONFIG=DefaultRelease COMPILER=clang STL=libc++
- install:
- - travis/install_osx.sh
- script:
- - travis/build.sh Build2
- after_failure:
- - find build -iname '*err*.log' -type f -print -exec cat {} \;
# ubuntu-16.10
- stage: Build (2nd run)
os: linux
@@ -149,29 +101,6 @@ jobs:
# Stage: Build (3rd run)
###
- # osx
- - stage: Build (3rd run)
- os: osx
- osx_image: xcode9.1
- compiler: clang
- env: CONFIG=DefaultDebug COMPILER=clang STL=libc++
- install:
- - travis/install_osx.sh
- script:
- - travis/build.sh Build3
- after_failure:
- - find build -iname '*err*.log' -type f -print -exec cat {} \;
- - stage: Build (3rd run)
- os: osx
- osx_image: xcode9.1
- compiler: clang
- env: CONFIG=DefaultRelease COMPILER=clang STL=libc++
- install:
- - travis/install_osx.sh
- script:
- - travis/build.sh Build3
- after_failure:
- - find build -iname '*err*.log' -type f -print -exec cat {} \;
# ubuntu-16.10
- stage: Build (3rd run)
os: linux
@@ -202,29 +131,6 @@ jobs:
# Stage: Build (4th run)
###
- # osx
- - stage: Build (4th run)
- os: osx
- osx_image: xcode9.1
- compiler: clang
- env: CONFIG=DefaultDebug COMPILER=clang STL=libc++
- install:
- - travis/install_osx.sh
- script:
- - travis/build.sh BuildLast
- after_failure:
- - find build -iname '*err*.log' -type f -print -exec cat {} \;
- - stage: Build (4th run)
- os: osx
- osx_image: xcode9.1
- compiler: clang
- env: CONFIG=DefaultRelease COMPILER=clang STL=libc++
- install:
- - travis/install_osx.sh
- script:
- - travis/build.sh BuildLast
- after_failure:
- - find build -iname '*err*.log' -type f -print -exec cat {} \;
# ubuntu-16.10
- stage: Build (4th run)
os: linux
@@ -255,29 +161,6 @@ jobs:
# Stage: Test all
###
- # osx
- - stage: Test all
- os: osx
- osx_image: xcode9.1
- compiler: clang
- env: CONFIG=DefaultDebug COMPILER=clang STL=libc++
- install:
- - travis/install_osx.sh
- script:
- - travis/build.sh TestAll
- after_failure:
- - find build -iname '*err*.log' -type f -print -exec cat {} \;
- - stage: Test all
- os: osx
- osx_image: xcode9.1
- compiler: clang
- env: CONFIG=DefaultRelease COMPILER=clang STL=libc++
- install:
- - travis/install_osx.sh
- script:
- - travis/build.sh TestAll
- after_failure:
- - find build -iname '*err*.log' -type f -print -exec cat {} \;
# ubuntu-16.10
- stage: Test all
os: linux
diff --git a/src/storm-pars/api/region.h b/src/storm-pars/api/region.h
index 27d35d526..56aba0cf3 100644
--- a/src/storm-pars/api/region.h
+++ b/src/storm-pars/api/region.h
@@ -81,7 +81,7 @@ namespace storm {
}
template <typename ParametricType, typename ConstantType>
- std::shared_ptr<storm::modelchecker::RegionModelChecker<ParametricType>> initializeParameterLiftingRegionModelChecker(Environment const& env, std::shared_ptr<storm::models::sparse::Model<ParametricType>> const& model, storm::modelchecker::CheckTask<storm::logic::Formula, ParametricType> const& task) {
+ std::shared_ptr<storm::modelchecker::RegionModelChecker<ParametricType>> initializeParameterLiftingRegionModelChecker(Environment const& env, std::shared_ptr<storm::models::sparse::Model<ParametricType>> const& model, storm::modelchecker::CheckTask<storm::logic::Formula, ParametricType> const& task, bool generateSplitEstimates = false, bool allowModelSimplification = true) {
STORM_LOG_WARN_COND(storm::utility::parameterlifting::validateParameterLiftingSound(*model, task.getFormula()), "Could not validate whether parameter lifting is applicable. Please validate manually...");
@@ -105,13 +105,13 @@ namespace storm {
STORM_LOG_THROW(false, storm::exceptions::InvalidOperationException, "Unable to perform parameterLifting on the provided model type.");
}
- checker->specify(env, consideredModel, task);
+ checker->specify(env, consideredModel, task, generateSplitEstimates, allowModelSimplification);
return checker;
}
template <typename ParametricType, typename ImpreciseType, typename PreciseType>
- std::shared_ptr<storm::modelchecker::RegionModelChecker<ParametricType>> initializeValidatingRegionModelChecker(Environment const& env, std::shared_ptr<storm::models::sparse::Model<ParametricType>> const& model, storm::modelchecker::CheckTask<storm::logic::Formula, ParametricType> const& task) {
+ std::shared_ptr<storm::modelchecker::RegionModelChecker<ParametricType>> initializeValidatingRegionModelChecker(Environment const& env, std::shared_ptr<storm::models::sparse::Model<ParametricType>> const& model, storm::modelchecker::CheckTask<storm::logic::Formula, ParametricType> const& task, bool generateSplitEstimates = false, bool allowModelSimplification = true) {
STORM_LOG_WARN_COND(storm::utility::parameterlifting::validateParameterLiftingSound(*model, task.getFormula()), "Could not validate whether parameter lifting is applicable. Please validate manually...");
@@ -135,7 +135,7 @@ namespace storm {
STORM_LOG_THROW(false, storm::exceptions::InvalidOperationException, "Unable to perform parameterLifting on the provided model type.");
}
- checker->specify(env, consideredModel, task);
+ checker->specify(env, consideredModel, task, generateSplitEstimates, allowModelSimplification);
return checker;
}
diff --git a/src/storm-pars/modelchecker/region/RegionModelChecker.h b/src/storm-pars/modelchecker/region/RegionModelChecker.h
index 72f56bf73..11cf160e4 100644
--- a/src/storm-pars/modelchecker/region/RegionModelChecker.h
+++ b/src/storm-pars/modelchecker/region/RegionModelChecker.h
@@ -28,7 +28,8 @@ namespace storm {
virtual ~RegionModelChecker() = default;
virtual bool canHandle(std::shared_ptr<storm::models::ModelBase> parametricModel, CheckTask<storm::logic::Formula, ParametricType> const& checkTask) const = 0;
- virtual void specify(Environment const& env, std::shared_ptr<storm::models::ModelBase> parametricModel, CheckTask<storm::logic::Formula, ParametricType> const& checkTask, bool generateRegionSplitEstimates = false) = 0;
+ virtual void specify(Environment const& env, std::shared_ptr<storm::models::ModelBase> parametricModel, CheckTask<storm::logic::Formula, ParametricType> const& checkTask, bool generateRegionSplitEstimates, bool allowModelSimplifications = true) = 0;
+
/*!
* Analyzes the given region.
@@ -45,7 +46,7 @@ namespace storm {
* 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(Environment const& env, std::vector<storm::storage::ParameterRegion<ParametricType>> const& regions, std::vector<RegionResultHypothesis> const& hypotheses, bool sampleVerticesOfRegion = false) ;
-
+
virtual ParametricType getBoundAtInitState(Environment const& env, storm::storage::ParameterRegion<ParametricType> const& region, storm::solver::OptimizationDirection const& dirForParameters);
/*!
diff --git a/src/storm-pars/modelchecker/region/SparseDtmcParameterLiftingModelChecker.cpp b/src/storm-pars/modelchecker/region/SparseDtmcParameterLiftingModelChecker.cpp
index 9c009ccee..b5c2ab11e 100644
--- a/src/storm-pars/modelchecker/region/SparseDtmcParameterLiftingModelChecker.cpp
+++ b/src/storm-pars/modelchecker/region/SparseDtmcParameterLiftingModelChecker.cpp
@@ -48,14 +48,13 @@ namespace storm {
}
template <typename SparseModelType, typename ConstantType>
- void SparseDtmcParameterLiftingModelChecker<SparseModelType, ConstantType>::specify(Environment const& env, std::shared_ptr<storm::models::ModelBase> parametricModel, CheckTask<storm::logic::Formula, typename SparseModelType::ValueType> const& checkTask, bool generateRegionSplitEstimates) {
+ void SparseDtmcParameterLiftingModelChecker<SparseModelType, ConstantType>::specify(Environment const& env, std::shared_ptr<storm::models::ModelBase> parametricModel, CheckTask<storm::logic::Formula, typename SparseModelType::ValueType> const& checkTask, bool generateRegionSplitEstimates, bool allowModelSimplification) {
auto dtmc = parametricModel->template as<SparseModelType>();
- specify(env, dtmc, checkTask, generateRegionSplitEstimates, false);
+ specify_internal(env, dtmc, checkTask, generateRegionSplitEstimates, !allowModelSimplification);
}
template <typename SparseModelType, typename ConstantType>
- void SparseDtmcParameterLiftingModelChecker<SparseModelType, ConstantType>::specify(Environment const& env, std::shared_ptr<SparseModelType> parametricModel, CheckTask<storm::logic::Formula, typename SparseModelType::ValueType> const& checkTask, bool generateRegionSplitEstimates, bool skipModelSimplification) {
-
+ void SparseDtmcParameterLiftingModelChecker<SparseModelType, ConstantType>::specify_internal(Environment const& env, std::shared_ptr<SparseModelType> parametricModel, CheckTask<storm::logic::Formula, typename SparseModelType::ValueType> const& checkTask, bool generateRegionSplitEstimates, bool skipModelSimplification) {
STORM_LOG_ASSERT(this->canHandle(parametricModel, checkTask), "specified model and formula can not be handled by this.");
reset();
@@ -140,7 +139,7 @@ namespace storm {
// if there are maybestates, create the parameterLifter
if (!maybeStates.empty()) {
// Create the vector of one-step probabilities to go to target states.
- std::vector<typename SparseModelType::ValueType> b = this->parametricModel->getTransitionMatrix().getConstrainedRowSumVector(storm::storage::BitVector(this->parametricModel->getTransitionMatrix().getRowCount(), true), psiStates);
+ std::vector<typename SparseModelType::ValueType> b = this->parametricModel->getTransitionMatrix().getConstrainedRowSumVector(storm::storage::BitVector(this->parametricModel->getTransitionMatrix().getRowCount(), true), statesWithProbability01.second);
parameterLifter = std::make_unique<storm::transformer::ParameterLifter<typename SparseModelType::ValueType, ConstantType>>(this->parametricModel->getTransitionMatrix(), b, maybeStates, maybeStates, regionSplitEstimationsEnabled);
}
diff --git a/src/storm-pars/modelchecker/region/SparseDtmcParameterLiftingModelChecker.h b/src/storm-pars/modelchecker/region/SparseDtmcParameterLiftingModelChecker.h
index 88231e76c..03dc1747a 100644
--- a/src/storm-pars/modelchecker/region/SparseDtmcParameterLiftingModelChecker.h
+++ b/src/storm-pars/modelchecker/region/SparseDtmcParameterLiftingModelChecker.h
@@ -23,9 +23,10 @@ namespace storm {
virtual ~SparseDtmcParameterLiftingModelChecker() = default;
virtual bool canHandle(std::shared_ptr<storm::models::ModelBase> parametricModel, CheckTask<storm::logic::Formula, typename SparseModelType::ValueType> const& checkTask) const override;
- virtual void specify(Environment const& env, std::shared_ptr<storm::models::ModelBase> parametricModel, CheckTask<storm::logic::Formula, typename SparseModelType::ValueType> const& checkTask, bool generateRegionSplitEstimates = false) override;
- void specify(Environment const& env, std::shared_ptr<SparseModelType> parametricModel, CheckTask<storm::logic::Formula, typename SparseModelType::ValueType> const& checkTask, bool generateRegionSplitEstimates, bool skipModelSimplification);
-
+
+ virtual void specify(Environment const& env, std::shared_ptr<storm::models::ModelBase> parametricModel, CheckTask<storm::logic::Formula, typename SparseModelType::ValueType> const& checkTask, bool generateRegionSplitEstimates = false, bool allowModelSimplification = true) override;
+ void specify_internal(Environment const& env, std::shared_ptr<SparseModelType> parametricModel, CheckTask<storm::logic::Formula, typename SparseModelType::ValueType> const& checkTask, bool generateRegionSplitEstimates, bool skipModelSimplification);
+
boost::optional<storm::storage::Scheduler<ConstantType>> getCurrentMinScheduler();
boost::optional<storm::storage::Scheduler<ConstantType>> getCurrentMaxScheduler();
diff --git a/src/storm-pars/modelchecker/region/SparseMdpParameterLiftingModelChecker.cpp b/src/storm-pars/modelchecker/region/SparseMdpParameterLiftingModelChecker.cpp
index 55a1b65a7..de1f47b24 100644
--- a/src/storm-pars/modelchecker/region/SparseMdpParameterLiftingModelChecker.cpp
+++ b/src/storm-pars/modelchecker/region/SparseMdpParameterLiftingModelChecker.cpp
@@ -45,13 +45,14 @@ namespace storm {
}
template <typename SparseModelType, typename ConstantType>
- void SparseMdpParameterLiftingModelChecker<SparseModelType, ConstantType>::specify(Environment const& env, std::shared_ptr<storm::models::ModelBase> parametricModel, CheckTask<storm::logic::Formula, typename SparseModelType::ValueType> const& checkTask, bool generateRegionSplitEstimates) {
+ void SparseMdpParameterLiftingModelChecker<SparseModelType, ConstantType>::specify(Environment const& env, std::shared_ptr<storm::models::ModelBase> parametricModel, CheckTask<storm::logic::Formula, typename SparseModelType::ValueType> const& checkTask, bool generateRegionSplitEstimates, bool allowModelSimplifications) {
auto mdp = parametricModel->template as<SparseModelType>();
- specify(env, mdp, checkTask, generateRegionSplitEstimates, false);
+ specify_internal(env, mdp, checkTask, generateRegionSplitEstimates, false);
}
template <typename SparseModelType, typename ConstantType>
- void SparseMdpParameterLiftingModelChecker<SparseModelType, ConstantType>::specify(Environment const& env, std::shared_ptr<SparseModelType> parametricModel, CheckTask<storm::logic::Formula, typename SparseModelType::ValueType> const& checkTask, bool generateRegionSplitEstimates, bool skipModelSimplification) {
+ void SparseMdpParameterLiftingModelChecker<SparseModelType, ConstantType>::specify_internal(Environment const& env, std::shared_ptr<SparseModelType> parametricModel, CheckTask<storm::logic::Formula, typename SparseModelType::ValueType> const& checkTask, bool generateRegionSplitEstimates, bool skipModelSimplification) {
+
STORM_LOG_ASSERT(this->canHandle(parametricModel, checkTask), "specified model and formula can not be handled by this.");
diff --git a/src/storm-pars/modelchecker/region/SparseMdpParameterLiftingModelChecker.h b/src/storm-pars/modelchecker/region/SparseMdpParameterLiftingModelChecker.h
index cffab74ed..d29525e2e 100644
--- a/src/storm-pars/modelchecker/region/SparseMdpParameterLiftingModelChecker.h
+++ b/src/storm-pars/modelchecker/region/SparseMdpParameterLiftingModelChecker.h
@@ -25,8 +25,8 @@ namespace storm {
virtual ~SparseMdpParameterLiftingModelChecker() = default;
virtual bool canHandle(std::shared_ptr<storm::models::ModelBase> parametricModel, CheckTask<storm::logic::Formula, typename SparseModelType::ValueType> const& checkTask) const override;
- virtual void specify(Environment const& env, std::shared_ptr<storm::models::ModelBase> parametricModel, CheckTask<storm::logic::Formula, typename SparseModelType::ValueType> const& checkTask, bool generateRegionSplitEstimates = false) override;
- void specify(Environment const& env, std::shared_ptr<SparseModelType> parametricModel, CheckTask<storm::logic::Formula, typename SparseModelType::ValueType> const& checkTask, bool generateRegionSplitEstimates, bool skipModelSimplification);
+ virtual void specify(Environment const& env, std::shared_ptr<storm::models::ModelBase> parametricModel, CheckTask<storm::logic::Formula, typename SparseModelType::ValueType> const& checkTask, bool generateRegionSplitEstimates = false, bool allowModelSimplification = true) override;
+ void specify_internal(Environment const& env, std::shared_ptr<SparseModelType> parametricModel, CheckTask<storm::logic::Formula, typename SparseModelType::ValueType> const& checkTask, bool generateRegionSplitEstimates, bool skipModelSimplification);
boost::optional<storm::storage::Scheduler<ConstantType>> getCurrentMinScheduler();
boost::optional<storm::storage::Scheduler<ConstantType>> getCurrentMaxScheduler();
diff --git a/src/storm-pars/modelchecker/region/ValidatingSparseDtmcParameterLiftingModelChecker.cpp b/src/storm-pars/modelchecker/region/ValidatingSparseDtmcParameterLiftingModelChecker.cpp
index e84f6c9d0..2e9bf221b 100644
--- a/src/storm-pars/modelchecker/region/ValidatingSparseDtmcParameterLiftingModelChecker.cpp
+++ b/src/storm-pars/modelchecker/region/ValidatingSparseDtmcParameterLiftingModelChecker.cpp
@@ -15,7 +15,7 @@ namespace storm {
}
template <typename SparseModelType, typename ImpreciseType, typename PreciseType>
- void ValidatingSparseDtmcParameterLiftingModelChecker<SparseModelType, ImpreciseType, PreciseType>::specify(Environment const& env, std::shared_ptr<storm::models::ModelBase> parametricModel, CheckTask<storm::logic::Formula, typename SparseModelType::ValueType> const& checkTask, bool generateRegionSplitEstimates) {
+ void ValidatingSparseDtmcParameterLiftingModelChecker<SparseModelType, ImpreciseType, PreciseType>::specify(Environment const& env, std::shared_ptr<storm::models::ModelBase> parametricModel, CheckTask<storm::logic::Formula, typename SparseModelType::ValueType> const& checkTask, bool generateRegionSplitEstimates, bool allowModelSimplifications) {
STORM_LOG_ASSERT(this->canHandle(parametricModel, checkTask), "specified model and formula can not be handled by this.");
auto dtmc = parametricModel->template as<SparseModelType>();
diff --git a/src/storm-pars/modelchecker/region/ValidatingSparseDtmcParameterLiftingModelChecker.h b/src/storm-pars/modelchecker/region/ValidatingSparseDtmcParameterLiftingModelChecker.h
index 5aed6b5d3..e99792eed 100644
--- a/src/storm-pars/modelchecker/region/ValidatingSparseDtmcParameterLiftingModelChecker.h
+++ b/src/storm-pars/modelchecker/region/ValidatingSparseDtmcParameterLiftingModelChecker.h
@@ -12,7 +12,7 @@ namespace storm {
ValidatingSparseDtmcParameterLiftingModelChecker();
virtual ~ValidatingSparseDtmcParameterLiftingModelChecker() = default;
- virtual void specify(Environment const& env, std::shared_ptr<storm::models::ModelBase> parametricModel, CheckTask<storm::logic::Formula, typename SparseModelType::ValueType> const& checkTask, bool generateRegionSplitEstimates = false) override;
+ virtual void specify(Environment const& env, std::shared_ptr<storm::models::ModelBase> parametricModel, CheckTask<storm::logic::Formula, typename SparseModelType::ValueType> const& checkTask, bool generateRegionSplitEstimates = false, bool allowModelSimplifications = true) override;
protected:
virtual SparseParameterLiftingModelChecker<SparseModelType, ImpreciseType>& getImpreciseChecker() override;
diff --git a/src/storm-pars/modelchecker/region/ValidatingSparseMdpParameterLiftingModelChecker.cpp b/src/storm-pars/modelchecker/region/ValidatingSparseMdpParameterLiftingModelChecker.cpp
index a3c01b4bd..444dd334c 100644
--- a/src/storm-pars/modelchecker/region/ValidatingSparseMdpParameterLiftingModelChecker.cpp
+++ b/src/storm-pars/modelchecker/region/ValidatingSparseMdpParameterLiftingModelChecker.cpp
@@ -16,7 +16,7 @@ namespace storm {
template <typename SparseModelType, typename ImpreciseType, typename PreciseType>
- void ValidatingSparseMdpParameterLiftingModelChecker<SparseModelType, ImpreciseType, PreciseType>::specify(Environment const& env, std::shared_ptr<storm::models::ModelBase> parametricModel, CheckTask<storm::logic::Formula, typename SparseModelType::ValueType> const& checkTask, bool generateRegionSplitEstimates) {
+ void ValidatingSparseMdpParameterLiftingModelChecker<SparseModelType, ImpreciseType, PreciseType>::specify(Environment const& env, std::shared_ptr<storm::models::ModelBase> parametricModel, CheckTask<storm::logic::Formula, typename SparseModelType::ValueType> const& checkTask, bool generateRegionSplitEstimates, bool allowModelSimplifications) {
STORM_LOG_ASSERT(this->canHandle(parametricModel, checkTask), "specified model and formula can not be handled by this.");
auto mdp = parametricModel->template as<SparseModelType>();
diff --git a/src/storm-pars/modelchecker/region/ValidatingSparseMdpParameterLiftingModelChecker.h b/src/storm-pars/modelchecker/region/ValidatingSparseMdpParameterLiftingModelChecker.h
index d6ef0ba74..9147e574e 100644
--- a/src/storm-pars/modelchecker/region/ValidatingSparseMdpParameterLiftingModelChecker.h
+++ b/src/storm-pars/modelchecker/region/ValidatingSparseMdpParameterLiftingModelChecker.h
@@ -12,7 +12,7 @@ namespace storm {
ValidatingSparseMdpParameterLiftingModelChecker();
virtual ~ValidatingSparseMdpParameterLiftingModelChecker() = default;
- virtual void specify(Environment const& env, std::shared_ptr<storm::models::ModelBase> parametricModel, CheckTask<storm::logic::Formula, typename SparseModelType::ValueType> const& checkTask, bool generateRegionSplitEstimates = false) override;
+ virtual void specify(Environment const& env, std::shared_ptr<storm::models::ModelBase> parametricModel, CheckTask<storm::logic::Formula, typename SparseModelType::ValueType> const& checkTask, bool generateRegionSplitEstimates = false, bool allowModelSimplifications = true) override;
protected:
virtual SparseParameterLiftingModelChecker<SparseModelType, ImpreciseType>& getImpreciseChecker() override;
diff --git a/src/storm/modelchecker/multiobjective/pcaa/StandardPcaaWeightVectorChecker.cpp b/src/storm/modelchecker/multiobjective/pcaa/StandardPcaaWeightVectorChecker.cpp
index 8ce496426..bd93a44ef 100644
--- a/src/storm/modelchecker/multiobjective/pcaa/StandardPcaaWeightVectorChecker.cpp
+++ b/src/storm/modelchecker/multiobjective/pcaa/StandardPcaaWeightVectorChecker.cpp
@@ -8,6 +8,8 @@
#include "storm/models/sparse/MarkovAutomaton.h"
#include "storm/models/sparse/StandardRewardModel.h"
#include "storm/modelchecker/prctl/helper/SparseDtmcPrctlHelper.h"
+#include "storm/modelchecker/prctl/helper/DsMpiUpperRewardBoundsComputer.h"
+#include "storm/modelchecker/prctl/helper/BaierUpperRewardBoundsComputer.h"
#include "storm/solver/MinMaxLinearEquationSolver.h"
#include "storm/utility/graph.h"
#include "storm/utility/macros.h"
@@ -42,12 +44,13 @@ namespace storm {
// Build a subsystem of the preprocessor result model that discards states that yield infinite reward for all schedulers.
// We can also merge the states that will have reward zero anyway.
storm::storage::BitVector maybeStates = preprocessorResult.rewardLessInfinityEStates.get() & ~preprocessorResult.reward0AStates;
+ storm::storage::BitVector finiteRewardChoices = preprocessorResult.preprocessedModel->getTransitionMatrix().getRowFilter(preprocessorResult.rewardLessInfinityEStates.get(), preprocessorResult.rewardLessInfinityEStates.get());
std::set<std::string> relevantRewardModels;
for (auto const& obj : this->objectives) {
obj.formula->gatherReferencedRewardModels(relevantRewardModels);
}
storm::transformer::GoalStateMerger<SparseModelType> merger(*preprocessorResult.preprocessedModel);
- auto mergerResult = merger.mergeTargetAndSinkStates(maybeStates, preprocessorResult.reward0AStates, storm::storage::BitVector(maybeStates.size(), false), std::vector<std::string>(relevantRewardModels.begin(), relevantRewardModels.end()));
+ auto mergerResult = merger.mergeTargetAndSinkStates(maybeStates, preprocessorResult.reward0AStates, storm::storage::BitVector(maybeStates.size(), false), std::vector<std::string>(relevantRewardModels.begin(), relevantRewardModels.end()), finiteRewardChoices);
// Initialize data specific for the considered model type
initializeModelTypeSpecificData(*mergerResult.model);
@@ -175,20 +178,17 @@ namespace storm {
std::unique_ptr<storm::solver::MinMaxLinearEquationSolver<ValueType>> solver = solverFactory.create(env, ecQuotient->matrix);
solver->setTrackScheduler(true);
solver->setHasUniqueSolution(true);
+ solver->setOptimizationDirection(storm::solver::OptimizationDirection::Maximize);
auto req = solver->getRequirements(env, storm::solver::OptimizationDirection::Maximize, true);
- boost::optional<ValueType> lowerBound = this->computeWeightedResultBound(true, weightVector, objectivesWithNoUpperTimeBound);
- if (lowerBound) {
- solver->setLowerBound(lowerBound.get());
+ setBoundsToSolver(*solver, req.requiresLowerBounds(), req.requiresUpperBounds(), weightVector, objectivesWithNoUpperTimeBound, ecQuotient->matrix, ecQuotient->rowsWithSumLessOne, ecQuotient->auxChoiceValues);
+ if (solver->hasLowerBound()) {
req.clearLowerBounds();
}
- boost::optional<ValueType> upperBound = this->computeWeightedResultBound(false, weightVector, objectivesWithNoUpperTimeBound);
- if (upperBound) {
- solver->setUpperBound(upperBound.get());
+ if (solver->hasUpperBound()) {
req.clearUpperBounds();
}
STORM_LOG_THROW(req.empty(), storm::exceptions::UncheckedRequirementException, "At least one requirement was not checked.");
solver->setRequirementsChecked(true);
- solver->setOptimizationDirection(storm::solver::OptimizationDirection::Maximize);
// Use the (0...0) vector as initial guess for the solution.
std::fill(ecQuotient->auxStateValues.begin(), ecQuotient->auxStateValues.end(), storm::utility::zero<ValueType>());
@@ -208,11 +208,11 @@ namespace storm {
if (storm::solver::minimize(this->objectives[objIndex].formula->getOptimalityType())) {
storm::utility::vector::scaleVectorInPlace(objectiveResults[objIndex], -storm::utility::one<ValueType>());
}
- for (uint_fast64_t objIndex2 = 0; objIndex2 < this->objectives.size(); ++objIndex2) {
- if (objIndex != objIndex2) {
- objectiveResults[objIndex2] = std::vector<ValueType>(transitionMatrix.getRowGroupCount(), storm::utility::zero<ValueType>());
- }
- }
+ for (uint_fast64_t objIndex2 = 0; objIndex2 < this->objectives.size(); ++objIndex2) {
+ if (objIndex != objIndex2) {
+ objectiveResults[objIndex2] = std::vector<ValueType>(transitionMatrix.getRowGroupCount(), storm::utility::zero<ValueType>());
+ }
+ }
} else {
storm::storage::SparseMatrix<ValueType> deterministicMatrix = transitionMatrix.selectRowsFromRowGroups(this->optimalChoices, true);
storm::storage::SparseMatrix<ValueType> deterministicBackwardTransitions = deterministicMatrix.transpose();
@@ -262,17 +262,19 @@ namespace storm {
std::vector<ValueType> b = storm::utility::vector::filterVector(deterministicStateRewards, maybeStates);
// Now solve the resulting equation system.
- std::unique_ptr<storm::solver::LinearEquationSolver<ValueType>> solver = linearEquationSolverFactory.create(env, std::move(submatrix));
+ std::unique_ptr<storm::solver::LinearEquationSolver<ValueType>> solver = linearEquationSolverFactory.create(env, submatrix);
auto req = solver->getRequirements(env);
solver->clearBounds();
- if (obj.lowerResultBound) {
+ storm::storage::BitVector submatrixRowsWithSumLessOne = deterministicMatrix.getRowFilter(maybeStates, maybeStates) % maybeStates;
+ submatrixRowsWithSumLessOne.complement();
+ this->setBoundsToSolver(*solver, req.requiresLowerBounds(), req.requiresUpperBounds(), objIndex, submatrix, submatrixRowsWithSumLessOne, b);
+ if (solver->hasLowerBound()) {
req.clearLowerBounds();
- solver->setLowerBound(*obj.lowerResultBound);
}
- if (obj.upperResultBound) {
- solver->setUpperBound(*obj.upperResultBound);
+ if (solver->hasUpperBound()) {
req.clearUpperBounds();
}
+
STORM_LOG_THROW(req.empty(), storm::exceptions::UncheckedRequirementException, "At least one requirement of the LinearEquationSolver was not met.");
solver->solveEquations(env, x, b);
@@ -311,11 +313,26 @@ namespace storm {
// Remove neutral end components, i.e., ECs in which no reward is earned.
auto ecElimResult = storm::transformer::EndComponentEliminator<ValueType>::transform(transitionMatrix, subsystemStates, ecChoicesHint & newReward0Choices, reward0EStates);
+ storm::storage::BitVector rowsWithSumLessOne(ecElimResult.matrix.getRowCount(), false);
+ for (uint64_t row = 0; row < rowsWithSumLessOne.size(); ++row) {
+ if (ecElimResult.matrix.getRow(row).getNumberOfEntries() == 0) {
+ rowsWithSumLessOne.set(row, true);
+ } else {
+ for (auto const& entry : transitionMatrix.getRow(ecElimResult.newToOldRowMapping[row])) {
+ if (!subsystemStates.get(entry.getColumn())) {
+ rowsWithSumLessOne.set(row, true);
+ break;
+ }
+ }
+ }
+ }
+
ecQuotient = EcQuotient();
ecQuotient->matrix = std::move(ecElimResult.matrix);
ecQuotient->ecqToOriginalChoiceMapping = std::move(ecElimResult.newToOldRowMapping);
ecQuotient->originalToEcqStateMapping = std::move(ecElimResult.oldToNewStateMapping);
ecQuotient->origReward0Choices = std::move(newReward0Choices);
+ ecQuotient->rowsWithSumLessOne = std::move(rowsWithSumLessOne);
ecQuotient->auxStateValues.reserve(transitionMatrix.getRowGroupCount());
ecQuotient->auxStateValues.resize(ecQuotient->matrix.getRowGroupCount());
ecQuotient->auxChoiceValues.reserve(transitionMatrix.getRowCount());
@@ -323,6 +340,91 @@ namespace storm {
}
}
+ template <class SparseModelType>
+ void StandardPcaaWeightVectorChecker<SparseModelType>::setBoundsToSolver(storm::solver::AbstractEquationSolver<ValueType>& solver, bool requiresLower, bool requiresUpper, uint64_t objIndex, storm::storage::SparseMatrix<ValueType> const& transitions, storm::storage::BitVector const& rowsWithSumLessOne, std::vector<ValueType> const& rewards) const {
+
+ // Check whether bounds are already available
+ if (this->objectives[objIndex].lowerResultBound) {
+ solver.setLowerBound(this->objectives[objIndex].lowerResultBound.get());
+ }
+ if (this->objectives[objIndex].upperResultBound) {
+ solver.setUpperBound(this->objectives[objIndex].upperResultBound.get());
+ }
+
+ if ((requiresLower && !solver.hasLowerBound()) || (requiresUpper && !solver.hasUpperBound())) {
+ computeAndSetBoundsToSolver(solver, requiresLower, requiresUpper, transitions, rowsWithSumLessOne, rewards);
+ }
+ }
+
+ template <class SparseModelType>
+ void StandardPcaaWeightVectorChecker<SparseModelType>::setBoundsToSolver(storm::solver::AbstractEquationSolver<ValueType>& solver, bool requiresLower, bool requiresUpper, std::vector<ValueType> const& weightVector, storm::storage::BitVector const& objectiveFilter, storm::storage::SparseMatrix<ValueType> const& transitions, storm::storage::BitVector const& rowsWithSumLessOne, std::vector<ValueType> const& rewards) const {
+
+ // Check whether bounds are already available
+ boost::optional<ValueType> lowerBound = this->computeWeightedResultBound(true, weightVector, objectiveFilter);
+ if (lowerBound) {
+ solver.setLowerBound(lowerBound.get());
+ }
+ boost::optional<ValueType> upperBound = this->computeWeightedResultBound(false, weightVector, objectiveFilter);
+ if (upperBound) {
+ solver.setUpperBound(upperBound.get());
+ }
+
+ if ((requiresLower && !solver.hasLowerBound()) || (requiresUpper && !solver.hasUpperBound())) {
+ computeAndSetBoundsToSolver(solver, requiresLower, requiresUpper, transitions, rowsWithSumLessOne, rewards);
+ }
+ }
+
+ template <class SparseModelType>
+ void StandardPcaaWeightVectorChecker<SparseModelType>::computeAndSetBoundsToSolver(storm::solver::AbstractEquationSolver<ValueType>& solver, bool requiresLower, bool requiresUpper, storm::storage::SparseMatrix<ValueType> const& transitions, storm::storage::BitVector const& rowsWithSumLessOne, std::vector<ValueType> const& rewards) const {
+
+ // Compute the one step target probs
+ std::vector<ValueType> oneStepTargetProbs(transitions.getRowCount(), storm::utility::zero<ValueType>());
+ for (auto const& row : rowsWithSumLessOne) {
+ oneStepTargetProbs[row] = storm::utility::one<ValueType>() - transitions.getRowSum(row);
+ }
+
+ if (requiresLower && !solver.hasLowerBound()) {
+ // Compute lower bounds
+ std::vector<ValueType> negativeRewards;
+ negativeRewards.reserve(transitions.getRowCount());
+ uint64_t row = 0;
+ for (auto const& rew : rewards) {
+ if (rew < storm::utility::zero<ValueType>()) {
+ negativeRewards.resize(row, storm::utility::zero<ValueType>());
+ negativeRewards.push_back(-rew);
+ }
+ ++row;
+ }
+ if (!negativeRewards.empty()) {
+ negativeRewards.resize(row, storm::utility::zero<ValueType>());
+ std::vector<ValueType> lowerBounds = storm::modelchecker::helper::DsMpiMdpUpperRewardBoundsComputer<ValueType>(transitions, negativeRewards, oneStepTargetProbs).computeUpperBounds();
+ storm::utility::vector::scaleVectorInPlace(lowerBounds, -storm::utility::one<ValueType>());
+ solver.setLowerBounds(std::move(lowerBounds));
+ } else {
+ solver.setLowerBound(storm::utility::zero<ValueType>());
+ }
+ }
+
+ // Compute upper bounds
+ if (requiresUpper && !solver.hasUpperBound()) {
+ std::vector<ValueType> positiveRewards;
+ positiveRewards.reserve(transitions.getRowCount());
+ uint64_t row = 0;
+ for (auto const& rew : rewards) {
+ if (rew > storm::utility::zero<ValueType>()) {
+ positiveRewards.resize(row, storm::utility::zero<ValueType>());
+ positiveRewards.push_back(rew);
+ }
+ ++row;
+ }
+ if (!positiveRewards.empty()) {
+ positiveRewards.resize(row, storm::utility::zero<ValueType>());
+ solver.setUpperBound(storm::modelchecker::helper::BaierUpperRewardBoundsComputer<ValueType>(transitions, positiveRewards, oneStepTargetProbs).computeUpperBound());
+ } else {
+ solver.setUpperBound(storm::utility::zero<ValueType>());
+ }
+ }
+ }
template <class SparseModelType>
void StandardPcaaWeightVectorChecker<SparseModelType>::transformReducedSolutionToOriginalModel(storm::storage::SparseMatrix<ValueType> const& reducedMatrix,
diff --git a/src/storm/modelchecker/multiobjective/pcaa/StandardPcaaWeightVectorChecker.h b/src/storm/modelchecker/multiobjective/pcaa/StandardPcaaWeightVectorChecker.h
index 86cd79c7f..2f0a27f33 100644
--- a/src/storm/modelchecker/multiobjective/pcaa/StandardPcaaWeightVectorChecker.h
+++ b/src/storm/modelchecker/multiobjective/pcaa/StandardPcaaWeightVectorChecker.h
@@ -1,5 +1,6 @@
#pragma once
+#include "storm/solver/AbstractEquationSolver.h"
#include "storm/storage/BitVector.h"
#include "storm/storage/SparseMatrix.h"
#include "storm/storage/Scheduler.h"
@@ -93,6 +94,11 @@ namespace storm {
void updateEcQuotient(std::vector<ValueType> const& weightedRewardVector);
+
+ void setBoundsToSolver(storm::solver::AbstractEquationSolver<ValueType>& solver, bool requiresLower, bool requiresUpper, uint64_t objIndex, storm::storage::SparseMatrix<ValueType> const& transitions, storm::storage::BitVector const& rowsWithSumLessOne, std::vector<ValueType> const& rewards) const;
+ void setBoundsToSolver(storm::solver::AbstractEquationSolver<ValueType>& solver, bool requiresLower, bool requiresUpper, std::vector<ValueType> const& weightVector, storm::storage::BitVector const& objectiveFilter, storm::storage::SparseMatrix<ValueType> const& transitions, storm::storage::BitVector const& rowsWithSumLessOne, std::vector<ValueType> const& rewards) const;
+ void computeAndSetBoundsToSolver(storm::solver::AbstractEquationSolver<ValueType>& solver, bool requiresLower, bool requiresUpper, storm::storage::SparseMatrix<ValueType> const& transitions, storm::storage::BitVector const& rowsWithSumLessOne, std::vector<ValueType> const& rewards) const;
+
/*!
* Transforms the results of a min-max-solver that considers a reduced model (without end components) to a result for the original (unreduced) model
*/
@@ -141,6 +147,7 @@ namespace storm {
std::vector<uint_fast64_t> ecqToOriginalChoiceMapping;
std::vector<uint_fast64_t> originalToEcqStateMapping;
storm::storage::BitVector origReward0Choices;
+ storm::storage::BitVector rowsWithSumLessOne;
std::vector<ValueType> auxStateValues;
std::vector<ValueType> auxChoiceValues;
diff --git a/src/storm/transformer/GoalStateMerger.cpp b/src/storm/transformer/GoalStateMerger.cpp
index 49497237e..7707bd3f1 100644
--- a/src/storm/transformer/GoalStateMerger.cpp
+++ b/src/storm/transformer/GoalStateMerger.cpp
@@ -24,10 +24,10 @@ namespace storm {
}
template <typename SparseModelType>
- typename GoalStateMerger<SparseModelType>::ReturnType GoalStateMerger<SparseModelType>::mergeTargetAndSinkStates(storm::storage::BitVector const& maybeStates, storm::storage::BitVector const& targetStates, storm::storage::BitVector const& sinkStates, std::vector<std::string> const& selectedRewardModels) const {
+ typename GoalStateMerger<SparseModelType>::ReturnType GoalStateMerger<SparseModelType>::mergeTargetAndSinkStates(storm::storage::BitVector const& maybeStates, storm::storage::BitVector const& targetStates, storm::storage::BitVector const& sinkStates, std::vector<std::string> const& selectedRewardModels, boost::optional<storm::storage::BitVector> const& choiceFilter) const {
STORM_LOG_THROW(maybeStates.isDisjointFrom(targetStates) && targetStates.isDisjointFrom(sinkStates) && sinkStates.isDisjointFrom(maybeStates), storm::exceptions::InvalidArgumentException, "maybestates, targetstates, and sinkstates are assumed to be disjoint when creating the submodel. However, this is not the case.");
- auto result = initialize(maybeStates, targetStates, sinkStates);
+ auto result = initialize(maybeStates, targetStates, sinkStates, choiceFilter);
auto transitionMatrix = buildTransitionMatrix(maybeStates, result.first, result.second);
auto labeling = buildStateLabeling(maybeStates, targetStates, sinkStates, result.first);
@@ -39,7 +39,7 @@ namespace storm {
}
template <typename SparseModelType>
- std::pair<typename GoalStateMerger<SparseModelType>::ReturnType, uint_fast64_t> GoalStateMerger<SparseModelType>::initialize(storm::storage::BitVector const& maybeStates, storm::storage::BitVector const& targetStates, storm::storage::BitVector const& sinkStates) const {
+ std::pair<typename GoalStateMerger<SparseModelType>::ReturnType, uint_fast64_t> GoalStateMerger<SparseModelType>::initialize(storm::storage::BitVector const& maybeStates, storm::storage::BitVector const& targetStates, storm::storage::BitVector const& sinkStates, boost::optional<storm::storage::BitVector> const& choiceFilter) const {
storm::storage::SparseMatrix<typename SparseModelType::ValueType> const& origMatrix = originalModel.getTransitionMatrix();
@@ -58,33 +58,35 @@ namespace storm {
for (uint_fast64_t row = origMatrix.getRowGroupIndices()[state]; row < endOfRowGroup; ++row) {
uint_fast64_t transitionsToMaybeStates = 0;
bool keepThisRow(true), hasTransitionToTarget(false), hasTransitionToSink(false);
- for (auto const& entry : origMatrix.getRow(row)) {
- if (maybeStates.get(entry.getColumn())) {
- ++transitionsToMaybeStates;
- } else if (targetStates.get(entry.getColumn())) {
- hasTransitionToTarget = true;
- } else if (sinkStates.get(entry.getColumn())) {
- hasTransitionToSink = true;
- } else {
- keepThisRow = false;
- break;
- }
- }
- if (keepThisRow) {
- stateIsDeadlock = false;
- result.keptChoices.set(row, true);
- transitionCount += transitionsToMaybeStates;
- if (hasTransitionToTarget) {
- ++transitionCount;
- targetStateRequired = true;
+ if (!choiceFilter || choiceFilter.get().get(row)) {
+ for (auto const& entry : origMatrix.getRow(row)) {
+ if (maybeStates.get(entry.getColumn())) {
+ ++transitionsToMaybeStates;
+ } else if (targetStates.get(entry.getColumn())) {
+ hasTransitionToTarget = true;
+ } else if (sinkStates.get(entry.getColumn())) {
+ hasTransitionToSink = true;
+ } else {
+ keepThisRow = false;
+ break;
+ }
}
- if (hasTransitionToSink) {
- ++transitionCount;
- sinkStateRequired = true;
+ if (keepThisRow) {
+ stateIsDeadlock = false;
+ result.keptChoices.set(row, true);
+ transitionCount += transitionsToMaybeStates;
+ if (hasTransitionToTarget) {
+ ++transitionCount;
+ targetStateRequired = true;
+ }
+ if (hasTransitionToSink) {
+ ++transitionCount;
+ sinkStateRequired = true;
+ }
}
}
- STORM_LOG_THROW(!stateIsDeadlock, storm::exceptions::InvalidArgumentException, "Merging goal states leads to deadlocks!");
}
+ STORM_LOG_THROW(!stateIsDeadlock, storm::exceptions::InvalidArgumentException, "Merging goal states leads to deadlocks!");
++stateCount;
}
diff --git a/src/storm/transformer/GoalStateMerger.h b/src/storm/transformer/GoalStateMerger.h
index bc9dadcda..f79a127a6 100644
--- a/src/storm/transformer/GoalStateMerger.h
+++ b/src/storm/transformer/GoalStateMerger.h
@@ -35,6 +35,8 @@ namespace storm {
* * one target state to which all transitions to a state selected by targetStates are redirected and
* * one sink state to which all transitions to a state selected by sinkStates are redirected.
*
+ * If a choiceFilter is given, choices on maybestates that are not selected by the filter will be removed.
+ *
* Notes:
* * the target (or sink) state is not created, if it is not reachable
* * the target (or sink) state will get a label iff it is reachable and at least one of the given targetStates (sinkStates) have that label.
@@ -43,7 +45,7 @@ namespace storm {
* * It is assumed that maybeStates, targetStates, and sinkStates are pairwise disjoint. Otherwise an exception is thrown.
* * The order of the maybeStates will not be affected (i.e. s_1 < s_2 in the input model implies s'_1 < s'_2 in the output model).
*/
- ReturnType mergeTargetAndSinkStates(storm::storage::BitVector const& maybeStates, storm::storage::BitVector const& targetStates, storm::storage::BitVector const& sinkStates, std::vector<std::string> const& selectedRewardModels = std::vector<std::string>()) const;
+ ReturnType mergeTargetAndSinkStates(storm::storage::BitVector const& maybeStates, storm::storage::BitVector const& targetStates, storm::storage::BitVector const& sinkStates, std::vector<std::string> const& selectedRewardModels = std::vector<std::string>(), boost::optional<storm::storage::BitVector> const& choiceFilter = boost::none) const;
private:
SparseModelType const& originalModel;
@@ -53,7 +55,7 @@ namespace storm {
*
* @return The initialized result and the number of transitions of the result model
*/
- std::pair<ReturnType, uint_fast64_t> initialize(storm::storage::BitVector const& maybeStates, storm::storage::BitVector const& targetStates, storm::storage::BitVector const& sinkStates) const;
+ std::pair<ReturnType, uint_fast64_t> initialize(storm::storage::BitVector const& maybeStates, storm::storage::BitVector const& targetStates, storm::storage::BitVector const& sinkStates, boost::optional<storm::storage::BitVector> const& choiceFilter = boost::none) const;
/*!
* Builds the transition matrix of the resulting model
diff --git a/src/test/storm-pars/modelchecker/SparseDtmcParameterLiftingTest.cpp b/src/test/storm-pars/modelchecker/SparseDtmcParameterLiftingTest.cpp
index 44e35f5c7..b00b44c0d 100644
--- a/src/test/storm-pars/modelchecker/SparseDtmcParameterLiftingTest.cpp
+++ b/src/test/storm-pars/modelchecker/SparseDtmcParameterLiftingTest.cpp
@@ -79,6 +79,36 @@ namespace {
EXPECT_EQ(storm::modelchecker::RegionResult::AllViolated, regionChecker->analyzeRegion(this->env(), allVioRegion, storm::modelchecker::RegionResultHypothesis::Unknown,storm::modelchecker::RegionResult::Unknown, true));
}
+
+ TYPED_TEST(SparseDtmcParameterLiftingTest, Brp_Prob_no_simplification) {
+ typedef typename TestFixture::ValueType ValueType;
+
+ std::string programFile = STORM_TEST_RESOURCES_DIR "/pdtmc/brp16_2.pm";
+ std::string formulaAsString = "P<=0.84 [F s=5 ]";
+ std::string constantsAsString = ""; //e.g. pL=0.9,TOACK=0.5
+
+ // Program and formula
+ storm::prism::Program program = storm::api::parseProgram(programFile);
+ program = storm::utility::prism::preprocess(program, constantsAsString);
+ std::vector<std::shared_ptr<const storm::logic::Formula>> formulas = storm::api::extractFormulasFromProperties(storm::api::parsePropertiesForPrismProgram(formulaAsString, program));
+ std::shared_ptr<storm::models::sparse::Dtmc<storm::RationalFunction>> model = storm::api::buildSparseModel<storm::RationalFunction>(program, formulas)->as<storm::models::sparse::Dtmc<storm::RationalFunction>>();
+
+ auto modelParameters = storm::models::sparse::getProbabilityParameters(*model);
+ auto rewParameters = storm::models::sparse::getRewardParameters(*model);
+ modelParameters.insert(rewParameters.begin(), rewParameters.end());
+
+ auto regionChecker = storm::api::initializeParameterLiftingRegionModelChecker<storm::RationalFunction, ValueType>(this->env(), model, storm::api::createTask<storm::RationalFunction>(formulas[0], true), false, false);
+
+ //start testing
+ auto allSatRegion=storm::api::parseRegion<storm::RationalFunction>("0.7<=pL<=0.9,0.75<=pK<=0.95", modelParameters);
+ 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(this->env(), allSatRegion, storm::modelchecker::RegionResultHypothesis::Unknown, storm::modelchecker::RegionResult::Unknown, true));
+ EXPECT_EQ(storm::modelchecker::RegionResult::ExistsBoth, regionChecker->analyzeRegion(this->env(), exBothRegion, storm::modelchecker::RegionResultHypothesis::Unknown,storm::modelchecker::RegionResult::Unknown, true));
+ EXPECT_EQ(storm::modelchecker::RegionResult::AllViolated, regionChecker->analyzeRegion(this->env(), allVioRegion, storm::modelchecker::RegionResultHypothesis::Unknown,storm::modelchecker::RegionResult::Unknown, true));
+
+ }
TYPED_TEST(SparseDtmcParameterLiftingTest, Brp_Rew) {
typedef typename TestFixture::ValueType ValueType;