diff --git a/src/storm/modelchecker/parametric/ParameterLifting.cpp b/src/storm/modelchecker/parametric/ParameterLifting.cpp
index 01e44a830..d0ea5dc08 100644
--- a/src/storm/modelchecker/parametric/ParameterLifting.cpp
+++ b/src/storm/modelchecker/parametric/ParameterLifting.cpp
@@ -4,12 +4,6 @@
#include "storm/adapters/CarlAdapter.h"
-#include "storm/modelchecker/parametric/SparseDtmcParameterLiftingModelChecker.h"
-#include "storm/modelchecker/parametric/SparseDtmcInstantiationModelChecker.h"
-#include "storm/modelchecker/parametric/SparseMdpParameterLiftingModelChecker.h"
-#include "storm/modelchecker/parametric/SparseMdpInstantiationModelChecker.h"
-#include "storm/transformer/SparseParametricDtmcSimplifier.h"
-#include "storm/transformer/SparseParametricMdpSimplifier.h"
#include "storm/modelchecker/results/ExplicitQualitativeCheckResult.h"
#include "storm/utility/vector.h"
@@ -29,14 +23,28 @@ namespace storm {
namespace modelchecker {
namespace parametric {
-
+ ParameterLiftingSettings::ParameterLiftingSettings() {
+ // todo: get this form settings
+ this->applyExactValidation = false;
+ }
+
template <typename SparseModelType, typename ConstantType>
- ParameterLifting<SparseModelType, ConstantType>::ParameterLifting(SparseModelType const& parametricModel) : parametricModel(parametricModel){
+ ParameterLifting<SparseModelType, ConstantType>::ParameterLifting(SparseModelType const& parametricModel) : parametricModel(parametricModel) {
initializationStopwatch.start();
STORM_LOG_THROW(parametricModel.getInitialStates().getNumberOfSetBits() == 1, storm::exceptions::NotSupportedException, "Parameter lifting requires models with only one initial state");
initializationStopwatch.stop();
}
-
+
+ template <typename SparseModelType, typename ConstantType>
+ ParameterLiftingSettings const& ParameterLifting<SparseModelType, ConstantType>::getSettings() const {
+ return settings;
+ }
+
+ template <typename SparseModelType, typename ConstantType>
+ void ParameterLifting<SparseModelType, ConstantType>::setSettings(ParameterLiftingSettings const& newSettings) {
+ settings = newSettings;
+ }
+
template <typename SparseModelType, typename ConstantType>
void ParameterLifting<SparseModelType, ConstantType>::specifyFormula(CheckTask<storm::logic::Formula, typename SparseModelType::ValueType> const& checkTask) {
initializationStopwatch.start();
@@ -47,15 +55,20 @@ namespace storm {
initializeUnderlyingCheckers();
currentCheckTask = std::make_unique<storm::modelchecker::CheckTask<storm::logic::Formula, typename SparseModelType::ValueType>>(checkTask.substituteFormula(*currentFormula));
- STORM_LOG_THROW(parameterLiftingChecker->canHandle(*currentCheckTask), storm::exceptions::NotSupportedException, "Parameter lifting is not supported for this property.");
- instantiationChecker->specifyFormula(*currentCheckTask);
+ STORM_LOG_THROW(parameterLiftingChecker->canHandle(*currentCheckTask) &&
+ (!exactParameterLiftingChecker || exactParameterLiftingChecker->canHandle(*currentCheckTask)),
+ storm::exceptions::NotSupportedException, "Parameter lifting is not supported for this property.");
+ if (exactParameterLiftingChecker) {
+ exactParameterLiftingChecker->specifyFormula(*currentCheckTask);
+ }
parameterLiftingChecker->specifyFormula(*currentCheckTask);
+ instantiationChecker->specifyFormula(*currentCheckTask);
initializationStopwatch.stop();
}
template <typename SparseModelType, typename ConstantType>
- RegionCheckResult ParameterLifting<SparseModelType, ConstantType>::analyzeRegion(storm::storage::ParameterRegion<typename SparseModelType::ValueType> const& region, RegionCheckResult const& initialResult, bool sampleVerticesOfRegion) const {
- RegionCheckResult result = initialResult;
+ RegionCheckResult ParameterLifting<SparseModelType, ConstantType>::analyzeRegion(storm::storage::ParameterRegion<typename SparseModelType::ValueType> const& region, RegionCheckResult const& initialResult, bool sampleVerticesOfRegion) {
+ RegionCheckResult result = initialResult;
// Check if we need to check the formula on one point to decide whether to show AllSat or AllViolated
instantiationCheckerStopwatch.start();
@@ -102,15 +115,48 @@ namespace storm {
parameterLiftingCheckerStopwatch.stop();
return result;
}
+
+ template <typename SparseModelType, typename ConstantType>
+ RegionCheckResult ParameterLifting<SparseModelType, ConstantType>::analyzeRegionExactValidation(storm::storage::ParameterRegion<typename SparseModelType::ValueType> const& region, RegionCheckResult const& initialResult) {
+ RegionCheckResult numericResult = analyzeRegion(region, initialResult, false);
+ parameterLiftingCheckerStopwatch.start();
+ if (numericResult == RegionCheckResult::AllSat || numericResult == RegionCheckResult::AllViolated) {
+ applyHintsToExactChecker();
+ }
+ if (numericResult == RegionCheckResult::AllSat) {
+ if(!exactParameterLiftingChecker->check(region, this->currentCheckTask->getOptimizationDirection())->asExplicitQualitativeCheckResult()[*getConsideredParametricModel().getInitialStates().begin()]) {
+ // Numerical result is wrong; Check whether the region is AllViolated!
+ if(!exactParameterLiftingChecker->check(region, storm::solver::invert(this->currentCheckTask->getOptimizationDirection()))->asExplicitQualitativeCheckResult()[*getConsideredParametricModel().getInitialStates().begin()]) {
+ parameterLiftingCheckerStopwatch.stop();
+ return RegionCheckResult::AllViolated;
+ } else {
+ return RegionCheckResult::Unknown;
+ }
+ }
+ } else if (numericResult == RegionCheckResult::AllViolated) {
+ if(exactParameterLiftingChecker->check(region, storm::solver::invert(this->currentCheckTask->getOptimizationDirection()))->asExplicitQualitativeCheckResult()[*getConsideredParametricModel().getInitialStates().begin()]) {
+ // Numerical result is wrong; Check whether the region is AllSat!
+ if(exactParameterLiftingChecker->check(region, this->currentCheckTask->getOptimizationDirection())->asExplicitQualitativeCheckResult()[*getConsideredParametricModel().getInitialStates().begin()]) {
+ parameterLiftingCheckerStopwatch.stop();
+ return RegionCheckResult::AllSat;
+ } else {
+ return RegionCheckResult::Unknown;
+ }
+ }
+ }
+ parameterLiftingCheckerStopwatch.stop();
+ return numericResult;
+ }
+
template <typename SparseModelType, typename ConstantType>
- std::vector<std::pair<storm::storage::ParameterRegion<typename SparseModelType::ValueType>, RegionCheckResult>> ParameterLifting<SparseModelType, ConstantType>::performRegionRefinement(storm::storage::ParameterRegion<typename SparseModelType::ValueType> const& region, typename storm::storage::ParameterRegion<typename SparseModelType::ValueType>::CoefficientType const& threshold) const {
+ std::vector<std::pair<storm::storage::ParameterRegion<typename SparseModelType::ValueType>, RegionCheckResult>> ParameterLifting<SparseModelType, ConstantType>::performRegionRefinement(storm::storage::ParameterRegion<typename SparseModelType::ValueType> const& region, CoefficientType const& threshold) {
STORM_LOG_INFO("Applying refinement on region: " << region.toString(true) << " .");
auto areaOfParameterSpace = region.area();
- auto fractionOfUndiscoveredArea = storm::utility::one<typename storm::storage::ParameterRegion<typename SparseModelType::ValueType>::CoefficientType>();
- auto fractionOfAllSatArea = storm::utility::zero<typename storm::storage::ParameterRegion<typename SparseModelType::ValueType>::CoefficientType>();
- auto fractionOfAllViolatedArea = storm::utility::zero<typename storm::storage::ParameterRegion<typename SparseModelType::ValueType>::CoefficientType>();
+ auto fractionOfUndiscoveredArea = storm::utility::one<CoefficientType>();
+ auto fractionOfAllSatArea = storm::utility::zero<CoefficientType>();
+ auto fractionOfAllViolatedArea = storm::utility::zero<CoefficientType>();
std::vector<std::pair<storm::storage::ParameterRegion<typename SparseModelType::ValueType>, RegionCheckResult>> regions;
regions.emplace_back(region, RegionCheckResult::Unknown);
@@ -122,7 +168,11 @@ namespace storm {
STORM_LOG_INFO("Analyzing region #" << indexOfCurrentRegion << " (" << storm::utility::convertNumber<double>(fractionOfUndiscoveredArea) * 100 << "% still unknown)");
auto const& currentRegion = regions[indexOfCurrentRegion].first;
auto& res = regions[indexOfCurrentRegion].second;
- res = analyzeRegion(currentRegion, res, false);
+ if (settings.applyExactValidation) {
+ res = analyzeRegionExactValidation(currentRegion, res);
+ } else {
+ res = analyzeRegion(currentRegion, res, false);
+ }
switch (res) {
case RegionCheckResult::AllSat:
fractionOfUndiscoveredArea -= currentRegion.area() / areaOfParameterSpace;
@@ -160,16 +210,6 @@ namespace storm {
return storm::utility::vector::filterVector(regions, resultRegions);
}
- template <typename SparseModelType, typename ConstantType>
- SparseParameterLiftingModelChecker<SparseModelType, ConstantType> const& ParameterLifting<SparseModelType, ConstantType>::getParameterLiftingChecker() const {
- return *parameterLiftingChecker;
- }
-
- template <typename SparseModelType, typename ConstantType>
- SparseInstantiationModelChecker<SparseModelType, ConstantType> const& ParameterLifting<SparseModelType, ConstantType>::getInstantiationChecker() const {
- return *instantiationChecker;
- }
-
template <typename SparseModelType, typename ConstantType>
SparseModelType const& ParameterLifting<SparseModelType, ConstantType>::getConsideredParametricModel() const {
if (simplifiedModel) {
@@ -178,48 +218,10 @@ namespace storm {
return parametricModel;
}
}
-
- template <>
- void ParameterLifting<storm::models::sparse::Dtmc<storm::RationalFunction>, double>::initializeUnderlyingCheckers() {
- parameterLiftingChecker = std::make_unique<SparseDtmcParameterLiftingModelChecker<storm::models::sparse::Dtmc<storm::RationalFunction>, double>>(getConsideredParametricModel());
- instantiationChecker = std::make_unique<SparseDtmcInstantiationModelChecker<storm::models::sparse::Dtmc<storm::RationalFunction>, double>>(getConsideredParametricModel());
- }
-
- template <>
- void ParameterLifting<storm::models::sparse::Mdp<storm::RationalFunction>, double>::initializeUnderlyingCheckers() {
- parameterLiftingChecker = std::make_unique<SparseMdpParameterLiftingModelChecker<storm::models::sparse::Mdp<storm::RationalFunction>, double>>(getConsideredParametricModel());
- instantiationChecker = std::make_unique<SparseMdpInstantiationModelChecker<storm::models::sparse::Mdp<storm::RationalFunction>, double>>(getConsideredParametricModel());
- }
-
- template <>
- void ParameterLifting<storm::models::sparse::Dtmc<storm::RationalFunction>, double>::simplifyParametricModel(CheckTask<logic::Formula, storm::RationalFunction> const& checkTask) {
- storm::transformer::SparseParametricDtmcSimplifier<storm::models::sparse::Dtmc<storm::RationalFunction>> simplifier(parametricModel);
- if(simplifier.simplify(checkTask.getFormula())) {
- simplifiedModel = simplifier.getSimplifiedModel();
- currentFormula = simplifier.getSimplifiedFormula();
- } else {
- simplifiedModel = nullptr;
- currentFormula = checkTask.getFormula().asSharedPointer();
- }
- }
-
- template <>
- void ParameterLifting<storm::models::sparse::Mdp<storm::RationalFunction>, double>::simplifyParametricModel(CheckTask<logic::Formula, storm::RationalFunction> const& checkTask) {
- storm::transformer::SparseParametricMdpSimplifier<storm::models::sparse::Mdp<storm::RationalFunction>> simplifier(parametricModel);
- if(simplifier.simplify(checkTask.getFormula())) {
- simplifiedModel = simplifier.getSimplifiedModel();
- currentFormula = simplifier.getSimplifiedFormula();
- } else {
- simplifiedModel = nullptr;
- currentFormula = checkTask.getFormula().asSharedPointer();
- }
- }
template <typename SparseModelType, typename ConstantType>
std::string ParameterLifting<SparseModelType, ConstantType>::visualizeResult(std::vector<std::pair<storm::storage::ParameterRegion<typename SparseModelType::ValueType>, RegionCheckResult>> const& result, storm::storage::ParameterRegion<typename SparseModelType::ValueType> const& parameterSpace, typename storm::storage::ParameterRegion<typename SparseModelType::ValueType>::VariableType const& x, typename storm::storage::ParameterRegion<typename SparseModelType::ValueType>::VariableType const& y) {
- typedef typename storm::storage::ParameterRegion<typename SparseModelType::ValueType>::CoefficientType ValueType;
-
std::stringstream stream;
uint_fast64_t const sizeX = 128;
@@ -229,21 +231,21 @@ namespace storm {
stream << " \t x-axis: " << x << " \t y-axis: " << y << " \t S=safe, [ ]=unsafe, -=ambiguous " << std::endl;
for (uint_fast64_t i = 0; i < sizeX+2; ++i) stream << "#"; stream << std::endl;
- ValueType deltaX = (parameterSpace.getUpperBoundary(x) - parameterSpace.getLowerBoundary(x)) / storm::utility::convertNumber<ValueType>(sizeX);
- ValueType deltaY = (parameterSpace.getUpperBoundary(y) - parameterSpace.getLowerBoundary(y)) / storm::utility::convertNumber<ValueType>(sizeY);
- ValueType printedRegionArea = deltaX * deltaY;
- for (ValueType yUpper = parameterSpace.getUpperBoundary(y); yUpper != parameterSpace.getLowerBoundary(y); yUpper -= deltaY) {
- ValueType yLower = yUpper - deltaY;
+ CoefficientType deltaX = (parameterSpace.getUpperBoundary(x) - parameterSpace.getLowerBoundary(x)) / storm::utility::convertNumber<CoefficientType>(sizeX);
+ CoefficientType deltaY = (parameterSpace.getUpperBoundary(y) - parameterSpace.getLowerBoundary(y)) / storm::utility::convertNumber<CoefficientType>(sizeY);
+ CoefficientType printedRegionArea = deltaX * deltaY;
+ for (CoefficientType yUpper = parameterSpace.getUpperBoundary(y); yUpper != parameterSpace.getLowerBoundary(y); yUpper -= deltaY) {
+ CoefficientType yLower = yUpper - deltaY;
stream << "#";
- for (ValueType xLower = parameterSpace.getLowerBoundary(x); xLower != parameterSpace.getUpperBoundary(x); xLower += deltaX) {
- ValueType xUpper = xLower + deltaX;
+ for (CoefficientType xLower = parameterSpace.getLowerBoundary(x); xLower != parameterSpace.getUpperBoundary(x); xLower += deltaX) {
+ CoefficientType xUpper = xLower + deltaX;
bool currRegionSafe = false;
bool currRegionUnSafe = false;
bool currRegionComplete = false;
- ValueType coveredArea = storm::utility::zero<ValueType>();
+ CoefficientType coveredArea = storm::utility::zero<CoefficientType>();
for (auto const& r : result) {
- ValueType instersectionArea = std::max(storm::utility::zero<ValueType>(), std::min(yUpper, r.first.getUpperBoundary(y)) - std::max(yLower, r.first.getLowerBoundary(y)));
- instersectionArea *= std::max(storm::utility::zero<ValueType>(), std::min(xUpper, r.first.getUpperBoundary(x)) - std::max(xLower, r.first.getLowerBoundary(x)));
+ CoefficientType instersectionArea = std::max(storm::utility::zero<CoefficientType>(), std::min(yUpper, r.first.getUpperBoundary(y)) - std::max(yLower, r.first.getLowerBoundary(y)));
+ instersectionArea *= std::max(storm::utility::zero<CoefficientType>(), std::min(xUpper, r.first.getUpperBoundary(x)) - std::max(xLower, r.first.getLowerBoundary(x)));
if(!storm::utility::isZero(instersectionArea)) {
currRegionSafe = currRegionSafe || r.second == RegionCheckResult::AllSat;
currRegionUnSafe = currRegionUnSafe || r.second == RegionCheckResult::AllViolated;
@@ -272,8 +274,10 @@ namespace storm {
}
#ifdef STORM_HAVE_CARL
- template class ParameterLifting<storm::models::sparse::Dtmc<storm::RationalFunction>, double>;
- template class ParameterLifting<storm::models::sparse::Mdp<storm::RationalFunction>, double>;
+ template class ParameterLifting<storm::models::sparse::Dtmc<storm::RationalFunction>, double>;
+ template class ParameterLifting<storm::models::sparse::Mdp<storm::RationalFunction>, double>;
+ template class ParameterLifting<storm::models::sparse::Dtmc<storm::RationalFunction>, storm::RationalNumber>;
+ template class ParameterLifting<storm::models::sparse::Mdp<storm::RationalFunction>, storm::RationalNumber>;
#endif
} // namespace parametric
} //namespace modelchecker
diff --git a/src/storm/modelchecker/parametric/ParameterLifting.h b/src/storm/modelchecker/parametric/ParameterLifting.h
index b0ea7ef65..c428d1ba9 100644
--- a/src/storm/modelchecker/parametric/ParameterLifting.h
+++ b/src/storm/modelchecker/parametric/ParameterLifting.h
@@ -12,15 +12,24 @@
namespace storm {
namespace modelchecker{
namespace parametric{
+
+ struct ParameterLiftingSettings {
+ ParameterLiftingSettings();
+
+ bool applyExactValidation;
+ };
template<typename SparseModelType, typename ConstantType>
class ParameterLifting {
public:
+
+ typedef typename storm::storage::ParameterRegion<typename SparseModelType::ValueType>::CoefficientType CoefficientType;
ParameterLifting(SparseModelType const& parametricModel);
- ~ParameterLifting() = default;
+ ParameterLiftingSettings const& getSettings() const;
+ void setSettings(ParameterLiftingSettings const& newSettings);
void specifyFormula(CheckTask<storm::logic::Formula, typename SparseModelType::ValueType> const& checkTask);
@@ -29,36 +38,38 @@ namespace storm {
* 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
- * If this does not yield a conclusive result and if the given flag is true, we also sample the vertices of the region
*
*/
- RegionCheckResult analyzeRegion(storm::storage::ParameterRegion<typename SparseModelType::ValueType> const& region, RegionCheckResult const& initialResult = RegionCheckResult::Unknown, bool sampleVerticesOfRegion = false) const;
+ RegionCheckResult analyzeRegion(storm::storage::ParameterRegion<typename SparseModelType::ValueType> const& region, RegionCheckResult const& initialResult = RegionCheckResult::Unknown, bool sampleVerticesOfRegion = false);
+ /*!
+ * Similar to analyze region but additionaly invokes exact parameter lifting to validate results AllSat or AllViolated
+ */
+ RegionCheckResult analyzeRegionExactValidation(storm::storage::ParameterRegion<typename SparseModelType::ValueType> const& region, RegionCheckResult const& initialResult = RegionCheckResult::Unknown);
/*!
* Iteratively refines the region until parameter lifting 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
*/
- std::vector<std::pair<storm::storage::ParameterRegion<typename SparseModelType::ValueType>, RegionCheckResult>> performRegionRefinement(storm::storage::ParameterRegion<typename SparseModelType::ValueType> const& region, typename storm::storage::ParameterRegion<typename SparseModelType::ValueType>::CoefficientType const& threshold) const;
-
- SparseParameterLiftingModelChecker<SparseModelType, ConstantType> const& getParameterLiftingChecker() const;
- SparseInstantiationModelChecker<SparseModelType, ConstantType> const& getInstantiationChecker() const;
+ std::vector<std::pair<storm::storage::ParameterRegion<typename SparseModelType::ValueType>, RegionCheckResult>> performRegionRefinement(storm::storage::ParameterRegion<typename SparseModelType::ValueType> const& region, CoefficientType const& threshold);
static std::string visualizeResult(std::vector<std::pair<storm::storage::ParameterRegion<typename SparseModelType::ValueType>, RegionCheckResult>> const& result, storm::storage::ParameterRegion<typename SparseModelType::ValueType> const& parameterSpace, typename storm::storage::ParameterRegion<typename SparseModelType::ValueType>::VariableType const& x, typename storm::storage::ParameterRegion<typename SparseModelType::ValueType>::VariableType const& y);
- private:
+ protected:
SparseModelType const& getConsideredParametricModel() const;
- void initializeUnderlyingCheckers();
- void simplifyParametricModel(CheckTask<storm::logic::Formula, typename SparseModelType::ValueType> const& checkTask);
-
+ virtual void initializeUnderlyingCheckers() = 0;
+ virtual void simplifyParametricModel(CheckTask<storm::logic::Formula, typename SparseModelType::ValueType> const& checkTask) = 0;
+ virtual void applyHintsToExactChecker() = 0;
SparseModelType const& parametricModel;
+ ParameterLiftingSettings settings;
std::unique_ptr<CheckTask<storm::logic::Formula, typename SparseModelType::ValueType>> currentCheckTask;
std::shared_ptr<storm::logic::Formula const> currentFormula;
std::shared_ptr<SparseModelType> simplifiedModel;
std::unique_ptr<SparseParameterLiftingModelChecker<SparseModelType, ConstantType>> parameterLiftingChecker;
+ std::unique_ptr<SparseParameterLiftingModelChecker<SparseModelType, CoefficientType>> exactParameterLiftingChecker;
std::unique_ptr<SparseInstantiationModelChecker<SparseModelType, ConstantType>> instantiationChecker;
mutable storm::utility::Stopwatch initializationStopwatch, instantiationCheckerStopwatch, parameterLiftingCheckerStopwatch;
diff --git a/src/storm/modelchecker/parametric/SparseDtmcInstantiationModelChecker.cpp b/src/storm/modelchecker/parametric/SparseDtmcInstantiationModelChecker.cpp
index 830113f77..1fd16ebd1 100644
--- a/src/storm/modelchecker/parametric/SparseDtmcInstantiationModelChecker.cpp
+++ b/src/storm/modelchecker/parametric/SparseDtmcInstantiationModelChecker.cpp
@@ -56,6 +56,7 @@ namespace storm {
template class SparseDtmcInstantiationModelChecker<storm::models::sparse::Dtmc<storm::RationalFunction>, double>;
+ template class SparseDtmcInstantiationModelChecker<storm::models::sparse::Dtmc<storm::RationalFunction>, storm::RationalNumber>;
}
}
diff --git a/src/storm/modelchecker/parametric/SparseDtmcParameterLifting.cpp b/src/storm/modelchecker/parametric/SparseDtmcParameterLifting.cpp
new file mode 100644
index 000000000..2ca6ba507
--- /dev/null
+++ b/src/storm/modelchecker/parametric/SparseDtmcParameterLifting.cpp
@@ -0,0 +1,61 @@
+#include "storm/modelchecker/parametric/SparseDtmcParameterLifting.h"
+
+#include "storm/adapters/CarlAdapter.h"
+
+#include "storm/modelchecker/parametric/SparseDtmcParameterLiftingModelChecker.h"
+#include "storm/modelchecker/parametric/SparseDtmcInstantiationModelChecker.h"
+#include "storm/transformer/SparseParametricDtmcSimplifier.h"
+#include "storm/models/sparse/StandardRewardModel.h"
+#include "storm/models/sparse/Dtmc.h"
+#include "SparseMdpParameterLifting.h"
+
+namespace storm {
+ namespace modelchecker {
+ namespace parametric {
+
+ template <typename SparseModelType, typename ConstantType>
+ SparseDtmcParameterLifting<SparseModelType, ConstantType>::SparseDtmcParameterLifting(SparseModelType const& parametricModel) : ParameterLifting<SparseModelType, ConstantType>(parametricModel) {
+ // Intentionally left empty
+ }
+
+ template <typename SparseModelType, typename ConstantType>
+ void SparseDtmcParameterLifting<SparseModelType, ConstantType>::simplifyParametricModel(CheckTask<storm::logic::Formula, typename SparseModelType::ValueType> const& checkTask) {
+ storm::transformer::SparseParametricDtmcSimplifier<SparseModelType> simplifier(this->parametricModel);
+ if(simplifier.simplify(checkTask.getFormula())) {
+ this->simplifiedModel = simplifier.getSimplifiedModel();
+ this->currentFormula = simplifier.getSimplifiedFormula();
+ } else {
+ this->simplifiedModel = nullptr;
+ this->currentFormula = checkTask.getFormula().asSharedPointer();
+ }
+ }
+
+ template <typename SparseModelType, typename ConstantType>
+ void SparseDtmcParameterLifting<SparseModelType, ConstantType>::initializeUnderlyingCheckers() {
+ if (this->settings.applyExactValidation) {
+ STORM_LOG_WARN_COND((std::is_same<ConstantType, typename ParameterLifting<SparseModelType, ConstantType>::CoefficientType>::value) , "Exact validation is not necessarry if the original computation is already exact");
+ this->exactParameterLiftingChecker = std::make_unique<SparseDtmcParameterLiftingModelChecker<SparseModelType, typename ParameterLifting<SparseModelType, ConstantType>::CoefficientType>>(this->getConsideredParametricModel());
+ }
+ this->parameterLiftingChecker = std::make_unique<SparseDtmcParameterLiftingModelChecker<SparseModelType, ConstantType>>(this->getConsideredParametricModel());
+ this->instantiationChecker = std::make_unique<SparseDtmcInstantiationModelChecker<SparseModelType, ConstantType>>(this->getConsideredParametricModel());
+ }
+
+ template <typename SparseModelType, typename ConstantType>
+ void SparseDtmcParameterLifting<SparseModelType, ConstantType>::applyHintsToExactChecker() {
+ auto dtmcPLChecker = dynamic_cast<storm::modelchecker::parametric::SparseDtmcParameterLiftingModelChecker<SparseModelType, ConstantType>*>(this->parameterLiftingChecker.get());
+ STORM_LOG_ASSERT(dtmcPLChecker, "Underlying Parameter lifting checker has unexpected type");
+ auto exactDtmcPLChecker = dynamic_cast<storm::modelchecker::parametric::SparseDtmcParameterLiftingModelChecker<SparseModelType, typename ParameterLifting<SparseModelType, ConstantType>::CoefficientType>*>(this->exactParameterLiftingChecker.get());
+ STORM_LOG_ASSERT(exactDtmcPLChecker, "Underlying exact parameter lifting checker has unexpected type");
+ exactDtmcPLChecker->getCurrentMaxScheduler() = dtmcPLChecker->getCurrentMaxScheduler();
+ exactDtmcPLChecker->getCurrentMinScheduler() = dtmcPLChecker->getCurrentMinScheduler();
+ }
+
+
+#ifdef STORM_HAVE_CARL
+ template class SparseDtmcParameterLifting<storm::models::sparse::Dtmc<storm::RationalFunction>, double>;
+ template class SparseDtmcParameterLifting<storm::models::sparse::Dtmc<storm::RationalFunction>, storm::RationalNumber>;
+#endif
+ } // namespace parametric
+ } //namespace modelchecker
+} //namespace storm
+
diff --git a/src/storm/modelchecker/parametric/SparseDtmcParameterLifting.h b/src/storm/modelchecker/parametric/SparseDtmcParameterLifting.h
new file mode 100644
index 000000000..3d3e66603
--- /dev/null
+++ b/src/storm/modelchecker/parametric/SparseDtmcParameterLifting.h
@@ -0,0 +1,27 @@
+#pragma once
+
+#include <memory>
+
+#include "storm/modelchecker/parametric/ParameterLifting.h"
+
+namespace storm {
+ namespace modelchecker{
+ namespace parametric{
+
+
+ template<typename SparseModelType, typename ConstantType>
+ class SparseDtmcParameterLifting : public ParameterLifting<SparseModelType, ConstantType> {
+
+ public:
+ SparseDtmcParameterLifting(SparseModelType const& parametricModel);
+
+ protected:
+ virtual void simplifyParametricModel(CheckTask<storm::logic::Formula, typename SparseModelType::ValueType> const& checkTask) override;
+ virtual void initializeUnderlyingCheckers() override;
+ virtual void applyHintsToExactChecker() override;
+
+ };
+
+ } //namespace parametric
+ } //namespace modelchecker
+} //namespace storm
diff --git a/src/storm/modelchecker/parametric/SparseDtmcParameterLiftingModelChecker.cpp b/src/storm/modelchecker/parametric/SparseDtmcParameterLiftingModelChecker.cpp
index b98774d2b..28a1547b7 100644
--- a/src/storm/modelchecker/parametric/SparseDtmcParameterLiftingModelChecker.cpp
+++ b/src/storm/modelchecker/parametric/SparseDtmcParameterLiftingModelChecker.cpp
@@ -1,4 +1,4 @@
-#include "SparseDtmcParameterLiftingModelChecker.h"
+#include "storm/modelchecker/parametric/SparseDtmcParameterLiftingModelChecker.h"
#include "storm/adapters/CarlAdapter.h"
#include "storm/modelchecker/propositional/SparsePropositionalModelChecker.h"
@@ -6,6 +6,7 @@
#include "storm/modelchecker/results/ExplicitQuantitativeCheckResult.h"
#include "storm/models/sparse/Dtmc.h"
#include "storm/models/sparse/StandardRewardModel.h"
+#include "storm/solver/StandardMinMaxLinearEquationSolver.h"
#include "storm/utility/vector.h"
#include "storm/utility/graph.h"
@@ -175,6 +176,13 @@ namespace storm {
// Set up the solver
auto solver = solverFactory->create(parameterLifter->getMatrix());
solver->setTrackScheduler(true);
+ if (std::is_same<ConstantType, storm::RationalNumber>::value && dynamic_cast<storm::solver::StandardMinMaxLinearEquationSolver<ConstantType>*>(solver.get())) {
+ STORM_LOG_INFO("Parameter Lifting: Setting solution method for exact MinMaxSolver to policy iteration");
+ auto* standardSolver = dynamic_cast<storm::solver::StandardMinMaxLinearEquationSolver<ConstantType>*>(solver.get());
+ auto settings = standardSolver->getSettings();
+ settings.setSolutionMethod(storm::solver::StandardMinMaxLinearEquationSolverSettings<ConstantType>::SolutionMethod::PolicyIteration);
+ standardSolver->setSettings(settings);
+ }
if(lowerResultBound) solver->setLowerBound(lowerResultBound.get());
if(upperResultBound) solver->setUpperBound(upperResultBound.get());
if(storm::solver::minimize(dirForParameters) && minSched && !stepBound) solver->setSchedulerHint(std::move(minSched.get()));
@@ -188,7 +196,7 @@ namespace storm {
termCond = std::make_unique<storm::solver::TerminateIfFilteredExtremumBelowThreshold<ConstantType>> (relevantStatesInSubsystem, this->currentCheckTask->getBoundThreshold(), true, false);
} else {
// Terminate if the value for ALL relevant states is already above the threshold
- termCond = std::make_unique<storm::solver::TerminateIfFilteredExtremumExceedsThreshold<ConstantType>> (relevantStatesInSubsystem, this->currentCheckTask->getBoundThreshold(), true, true);
+ termCond = std::make_unique<storm::solver::TerminateIfFilteredExtremumExceedsThreshold<ConstantType>> (relevantStatesInSubsystem, true, this->currentCheckTask->getBoundThreshold(), true);
}
solver->setTerminationCondition(std::move(termCond));
}
@@ -231,8 +239,19 @@ namespace storm {
lowerResultBound = boost::none;
upperResultBound = boost::none;
}
-
+
+ template <typename SparseModelType, typename ConstantType>
+ boost::optional<storm::storage::TotalScheduler>& SparseDtmcParameterLiftingModelChecker<SparseModelType, ConstantType>::getCurrentMinScheduler() {
+ return minSched;
+ }
+
+ template <typename SparseModelType, typename ConstantType>
+ boost::optional<storm::storage::TotalScheduler>& SparseDtmcParameterLiftingModelChecker<SparseModelType, ConstantType>::getCurrentMaxScheduler() {
+ return maxSched;
+ }
+
template class SparseDtmcParameterLiftingModelChecker<storm::models::sparse::Dtmc<storm::RationalFunction>, double>;
+ template class SparseDtmcParameterLiftingModelChecker<storm::models::sparse::Dtmc<storm::RationalFunction>, storm::RationalNumber>;
}
}
diff --git a/src/storm/modelchecker/parametric/SparseDtmcParameterLiftingModelChecker.h b/src/storm/modelchecker/parametric/SparseDtmcParameterLiftingModelChecker.h
index 4d810cd48..331219a39 100644
--- a/src/storm/modelchecker/parametric/SparseDtmcParameterLiftingModelChecker.h
+++ b/src/storm/modelchecker/parametric/SparseDtmcParameterLiftingModelChecker.h
@@ -23,6 +23,9 @@ namespace storm {
SparseDtmcParameterLiftingModelChecker(SparseModelType const& parametricModel, std::unique_ptr<storm::solver::MinMaxLinearEquationSolverFactory<ConstantType>>&& solverFactory);
virtual bool canHandle(CheckTask<storm::logic::Formula, typename SparseModelType::ValueType> const& checkTask) const override;
+
+ boost::optional<storm::storage::TotalScheduler>& getCurrentMinScheduler();
+ boost::optional<storm::storage::TotalScheduler>& getCurrentMaxScheduler();
protected:
diff --git a/src/storm/modelchecker/parametric/SparseInstantiationModelChecker.cpp b/src/storm/modelchecker/parametric/SparseInstantiationModelChecker.cpp
index 5fbbf9b6b..b8efac24d 100644
--- a/src/storm/modelchecker/parametric/SparseInstantiationModelChecker.cpp
+++ b/src/storm/modelchecker/parametric/SparseInstantiationModelChecker.cpp
@@ -36,6 +36,9 @@ namespace storm {
template class SparseInstantiationModelChecker<storm::models::sparse::Dtmc<storm::RationalFunction>, double>;
template class SparseInstantiationModelChecker<storm::models::sparse::Mdp<storm::RationalFunction>, double>;
+
+ template class SparseInstantiationModelChecker<storm::models::sparse::Dtmc<storm::RationalFunction>, storm::RationalNumber>;
+ template class SparseInstantiationModelChecker<storm::models::sparse::Mdp<storm::RationalFunction>, storm::RationalNumber>;
}
}
diff --git a/src/storm/modelchecker/parametric/SparseMdpInstantiationModelChecker.cpp b/src/storm/modelchecker/parametric/SparseMdpInstantiationModelChecker.cpp
index 34debd0f5..dcaa88335 100644
--- a/src/storm/modelchecker/parametric/SparseMdpInstantiationModelChecker.cpp
+++ b/src/storm/modelchecker/parametric/SparseMdpInstantiationModelChecker.cpp
@@ -63,6 +63,7 @@ namespace storm {
}
template class SparseMdpInstantiationModelChecker<storm::models::sparse::Mdp<storm::RationalFunction>, double>;
+ template class SparseMdpInstantiationModelChecker<storm::models::sparse::Mdp<storm::RationalFunction>, storm::RationalNumber>;
}
}
diff --git a/src/storm/modelchecker/parametric/SparseMdpParameterLifting.cpp b/src/storm/modelchecker/parametric/SparseMdpParameterLifting.cpp
new file mode 100644
index 000000000..25d222063
--- /dev/null
+++ b/src/storm/modelchecker/parametric/SparseMdpParameterLifting.cpp
@@ -0,0 +1,62 @@
+#include "storm/modelchecker/parametric/SparseMdpParameterLifting.h"
+
+#include "storm/adapters/CarlAdapter.h"
+
+#include "storm/modelchecker/parametric/SparseMdpParameterLiftingModelChecker.h"
+#include "storm/modelchecker/parametric/SparseMdpInstantiationModelChecker.h"
+#include "storm/transformer/SparseParametricMdpSimplifier.h"
+#include "storm/models/sparse/StandardRewardModel.h"
+#include "storm/models/sparse/Mdp.h"
+#include "SparseMdpParameterLifting.h"
+
+namespace storm {
+ namespace modelchecker {
+ namespace parametric {
+
+ template <typename SparseModelType, typename ConstantType>
+ SparseMdpParameterLifting<SparseModelType, ConstantType>::SparseMdpParameterLifting(SparseModelType const& parametricModel) : ParameterLifting<SparseModelType, ConstantType>(parametricModel) {
+ // Intentionally left empty
+ }
+
+ template <typename SparseModelType, typename ConstantType>
+ void SparseMdpParameterLifting<SparseModelType, ConstantType>::simplifyParametricModel(CheckTask<storm::logic::Formula, typename SparseModelType::ValueType> const& checkTask) {
+ storm::transformer::SparseParametricMdpSimplifier<SparseModelType> simplifier(this->parametricModel);
+ if(simplifier.simplify(checkTask.getFormula())) {
+ this->simplifiedModel = simplifier.getSimplifiedModel();
+ this->currentFormula = simplifier.getSimplifiedFormula();
+ } else {
+ this->simplifiedModel = nullptr;
+ this->currentFormula = checkTask.getFormula().asSharedPointer();
+ }
+ }
+
+ template <typename SparseModelType, typename ConstantType>
+ void SparseMdpParameterLifting<SparseModelType, ConstantType>::initializeUnderlyingCheckers() {
+ if (this->settings.applyExactValidation) {
+ STORM_LOG_WARN_COND((std::is_same<ConstantType, typename ParameterLifting<SparseModelType, ConstantType>::CoefficientType>::value), "Exact validation is not necessarry if the original computation is already exact");
+ this->exactParameterLiftingChecker = std::make_unique<SparseMdpParameterLiftingModelChecker<SparseModelType, typename ParameterLifting<SparseModelType, ConstantType>::CoefficientType>>(this->getConsideredParametricModel());
+ }
+ this->parameterLiftingChecker = std::make_unique<SparseMdpParameterLiftingModelChecker<SparseModelType, ConstantType>>(this->getConsideredParametricModel());
+ this->instantiationChecker = std::make_unique<SparseMdpInstantiationModelChecker<SparseModelType, ConstantType>>(this->getConsideredParametricModel());
+ }
+
+ template <typename SparseModelType, typename ConstantType>
+ void SparseMdpParameterLifting<SparseModelType, ConstantType>::applyHintsToExactChecker() {
+ auto MdpPLChecker = dynamic_cast<storm::modelchecker::parametric::SparseMdpParameterLiftingModelChecker<SparseModelType, ConstantType>*>(this->parameterLiftingChecker.get());
+ STORM_LOG_ASSERT(MdpPLChecker, "Underlying Parameter lifting checker has unexpected type");
+ auto exactMdpPLChecker = dynamic_cast<storm::modelchecker::parametric::SparseMdpParameterLiftingModelChecker<SparseModelType, typename ParameterLifting<SparseModelType, ConstantType>::CoefficientType>*>(this->exactParameterLiftingChecker.get());
+ STORM_LOG_ASSERT(exactMdpPLChecker, "Underlying exact parameter lifting checker has unexpected type");
+ exactMdpPLChecker->getCurrentMaxScheduler() = MdpPLChecker->getCurrentMaxScheduler();
+ exactMdpPLChecker->getCurrentMinScheduler() = MdpPLChecker->getCurrentMinScheduler();
+ exactMdpPLChecker->getCurrentPlayer1Scheduler() = MdpPLChecker->getCurrentPlayer1Scheduler();
+ }
+
+
+#ifdef STORM_HAVE_CARL
+ template class SparseMdpParameterLifting<storm::models::sparse::Mdp<storm::RationalFunction>, double>;
+ template class SparseMdpParameterLifting<storm::models::sparse::Mdp<storm::RationalFunction>, storm::RationalNumber>;
+#endif
+ } // namespace parametric
+ } //namespace modelchecker
+} //namespace storm
+
diff --git a/src/storm/modelchecker/parametric/SparseMdpParameterLifting.h b/src/storm/modelchecker/parametric/SparseMdpParameterLifting.h
new file mode 100644
index 000000000..36ee94d85
--- /dev/null
+++ b/src/storm/modelchecker/parametric/SparseMdpParameterLifting.h
@@ -0,0 +1,28 @@
+#pragma once
+
+#include <memory>
+
+#include "storm/modelchecker/parametric/ParameterLifting.h"
+
+namespace storm {
+ namespace modelchecker{
+ namespace parametric{
+
+
+ template<typename SparseModelType, typename ConstantType>
+ class SparseMdpParameterLifting : public ParameterLifting<SparseModelType, ConstantType> {
+
+ public:
+ SparseMdpParameterLifting(SparseModelType const& parametricModel);
+
+ protected:
+
+ virtual void initializeUnderlyingCheckers() override;
+ virtual void simplifyParametricModel(CheckTask<storm::logic::Formula, typename SparseModelType::ValueType> const& checkTask) override;
+ virtual void applyHintsToExactChecker() override;
+
+ };
+
+ } //namespace parametric
+ } //namespace modelchecker
+} //namespace storm
diff --git a/src/storm/modelchecker/parametric/SparseMdpParameterLiftingModelChecker.cpp b/src/storm/modelchecker/parametric/SparseMdpParameterLiftingModelChecker.cpp
index 5b8c0457d..6dd8b191d 100644
--- a/src/storm/modelchecker/parametric/SparseMdpParameterLiftingModelChecker.cpp
+++ b/src/storm/modelchecker/parametric/SparseMdpParameterLiftingModelChecker.cpp
@@ -1,4 +1,4 @@
-#include "SparseMdpParameterLiftingModelChecker.h"
+#include "storm/modelchecker/parametric/SparseMdpParameterLiftingModelChecker.h"
#include "storm/adapters/CarlAdapter.h"
#include "storm/modelchecker/propositional/SparsePropositionalModelChecker.h"
@@ -228,7 +228,7 @@ namespace storm {
termCond = std::make_unique<storm::solver::TerminateIfFilteredExtremumBelowThreshold<ConstantType>> (relevantStatesInSubsystem, this->currentCheckTask->getBoundThreshold(), true, false);
} else {
// Terminate if the value for ALL relevant states is already above the threshold
- termCond = std::make_unique<storm::solver::TerminateIfFilteredExtremumExceedsThreshold<ConstantType>> (relevantStatesInSubsystem, this->currentCheckTask->getBoundThreshold(), true, true);
+ termCond = std::make_unique<storm::solver::TerminateIfFilteredExtremumExceedsThreshold<ConstantType>> (relevantStatesInSubsystem, true, this->currentCheckTask->getBoundThreshold(), true);
}
solver->setTerminationCondition(std::move(termCond));
}
@@ -292,8 +292,24 @@ namespace storm {
upperResultBound = boost::none;
applyPreviousResultAsHint = false;
}
+
+ template <typename SparseModelType, typename ConstantType>
+ boost::optional<storm::storage::TotalScheduler>& SparseMdpParameterLiftingModelChecker<SparseModelType, ConstantType>::getCurrentMinScheduler() {
+ return minSched;
+ }
+
+ template <typename SparseModelType, typename ConstantType>
+ boost::optional<storm::storage::TotalScheduler>& SparseMdpParameterLiftingModelChecker<SparseModelType, ConstantType>::getCurrentMaxScheduler() {
+ return maxSched;
+ }
+
+ template <typename SparseModelType, typename ConstantType>
+ boost::optional<storm::storage::TotalScheduler>& SparseMdpParameterLiftingModelChecker<SparseModelType, ConstantType>::getCurrentPlayer1Scheduler() {
+ return player1Sched;
+ }
template class SparseMdpParameterLiftingModelChecker<storm::models::sparse::Mdp<storm::RationalFunction>, double>;
+ template class SparseMdpParameterLiftingModelChecker<storm::models::sparse::Mdp<storm::RationalFunction>, storm::RationalNumber>;
}
}
}
\ No newline at end of file
diff --git a/src/storm/modelchecker/parametric/SparseMdpParameterLiftingModelChecker.h b/src/storm/modelchecker/parametric/SparseMdpParameterLiftingModelChecker.h
index 76d66bbd7..ab96f4d13 100644
--- a/src/storm/modelchecker/parametric/SparseMdpParameterLiftingModelChecker.h
+++ b/src/storm/modelchecker/parametric/SparseMdpParameterLiftingModelChecker.h
@@ -24,6 +24,10 @@ namespace storm {
virtual bool canHandle(CheckTask<storm::logic::Formula, typename SparseModelType::ValueType> const& checkTask) const override;
+ boost::optional<storm::storage::TotalScheduler>& getCurrentMinScheduler();
+ boost::optional<storm::storage::TotalScheduler>& getCurrentMaxScheduler();
+ boost::optional<storm::storage::TotalScheduler>& getCurrentPlayer1Scheduler();
+
protected:
virtual void specifyBoundedUntilFormula(CheckTask<storm::logic::BoundedUntilFormula, ConstantType> const& checkTask) override;
diff --git a/src/storm/modelchecker/parametric/SparseParameterLiftingModelChecker.cpp b/src/storm/modelchecker/parametric/SparseParameterLiftingModelChecker.cpp
index e16cff9b1..1c8ffa269 100644
--- a/src/storm/modelchecker/parametric/SparseParameterLiftingModelChecker.cpp
+++ b/src/storm/modelchecker/parametric/SparseParameterLiftingModelChecker.cpp
@@ -86,6 +86,8 @@ namespace storm {
template class SparseParameterLiftingModelChecker<storm::models::sparse::Dtmc<storm::RationalFunction>, double>;
template class SparseParameterLiftingModelChecker<storm::models::sparse::Mdp<storm::RationalFunction>, double>;
+ template class SparseParameterLiftingModelChecker<storm::models::sparse::Dtmc<storm::RationalFunction>, storm::RationalNumber>;
+ template class SparseParameterLiftingModelChecker<storm::models::sparse::Mdp<storm::RationalFunction>, storm::RationalNumber>;
}
}
diff --git a/src/storm/models/sparse/StochasticTwoPlayerGame.cpp b/src/storm/models/sparse/StochasticTwoPlayerGame.cpp
index e37d5cceb..6ac6f93e4 100644
--- a/src/storm/models/sparse/StochasticTwoPlayerGame.cpp
+++ b/src/storm/models/sparse/StochasticTwoPlayerGame.cpp
@@ -66,6 +66,7 @@ namespace storm {
#ifdef STORM_HAVE_CARL
template class StochasticTwoPlayerGame<storm::RationalFunction>;
+ template class StochasticTwoPlayerGame<storm::RationalNumber>;
#endif
} // namespace sparse
diff --git a/src/storm/settings/modules/ParametricSettings.cpp b/src/storm/settings/modules/ParametricSettings.cpp
index 76ca0adc9..e7e764426 100644
--- a/src/storm/settings/modules/ParametricSettings.cpp
+++ b/src/storm/settings/modules/ParametricSettings.cpp
@@ -18,6 +18,7 @@ namespace storm {
const std::string ParametricSettings::exportResultDestinationPathOptionName = "resultfile";
const std::string ParametricSettings::parameterSpaceOptionName = "parameterspace";
const std::string ParametricSettings::refinementThresholdOptionName = "refinementthreshold";
+ const std::string ParametricSettings::exactValidationOptionName = "exactvalidation";
const std::string ParametricSettings::derivativesOptionName = "derivatives";
ParametricSettings::ParametricSettings() : ModuleSettings(moduleName) {
@@ -31,6 +32,7 @@ namespace storm {
.addArgument(storm::settings::ArgumentBuilder::createStringArgument("region", "The parameter-space (given in format a<=x<=b,c<=y<=d).").build()).build());
this->addOption(storm::settings::OptionBuilder(moduleName, refinementThresholdOptionName, true, "Parameter space refinement converges if the fraction of unknown area falls below this threshold.")
.addArgument(storm::settings::ArgumentBuilder::createDoubleArgument("threshold", "The threshold").setDefaultValueDouble(0.05).addValidatorDouble(storm::settings::ArgumentValidatorFactory::createDoubleRangeValidatorExcluding(0.0,1.0)).build()).build());
+ this->addOption(storm::settings::OptionBuilder(moduleName, exactValidationOptionName, true, "Sets whether numerical results from Parameter lifting should be validated with exact techniques.").build());
this->addOption(storm::settings::OptionBuilder(moduleName, derivativesOptionName, true, "Sets whether to generate the derivatives of the resulting rational function.").build());
}
@@ -54,6 +56,10 @@ namespace storm {
return this->getOption(refinementThresholdOptionName).getArgumentByName("threshold").getValueAsDouble();
}
+ bool ParametricSettings::isExactValidationSet() const {
+ return this->getOption(exactValidationOptionName).getHasOptionBeenSet();
+ }
+
bool ParametricSettings::exportToSmt2File() const {
return this->getOption(exportSmt2DestinationPathOptionName).getHasOptionBeenSet();
}
diff --git a/src/storm/settings/modules/ParametricSettings.h b/src/storm/settings/modules/ParametricSettings.h
index ac0cd9673..54f2bbf86 100644
--- a/src/storm/settings/modules/ParametricSettings.h
+++ b/src/storm/settings/modules/ParametricSettings.h
@@ -55,6 +55,11 @@ namespace storm {
*/
double getRefinementThreshold() const;
+ /*!
+ * Retrieves whether exact validation should be performed
+ */
+ bool isExactValidationSet() const;
+
/**
* Retrieves whether the encoding of the transition system should be exported to a file.
* @return True iff the smt file should be encoded.
@@ -88,6 +93,7 @@ namespace storm {
const static std::string exportResultDestinationPathOptionName;
const static std::string parameterSpaceOptionName;
const static std::string refinementThresholdOptionName;
+ const static std::string exactValidationOptionName;
const static std::string derivativesOptionName;
};
diff --git a/src/storm/solver/GameSolver.cpp b/src/storm/solver/GameSolver.cpp
index 64d490e7c..4b27fca14 100644
--- a/src/storm/solver/GameSolver.cpp
+++ b/src/storm/solver/GameSolver.cpp
@@ -51,7 +51,6 @@ namespace storm {
storm::utility::vector::selectVectorValues<ValueType>(tmpResult, selectedRows, b);
// Solve the resulting equation system.
- // Note that the linEqSolver might consider a slightly different interpretation of "equalModuloPrecision". Hence, we iteratively increase its precision.
auto submatrixSolver = storm::solver::GeneralLinearEquationSolverFactory<ValueType>().create(std::move(inducedMatrix));
submatrixSolver->setCachingEnabled(true);
if (this->lowerBound) { submatrixSolver->setLowerBound(this->lowerBound.get()); }
diff --git a/src/storm/transformer/ParameterLifter.cpp b/src/storm/transformer/ParameterLifter.cpp
index 507db6ddc..9fe1d333d 100644
--- a/src/storm/transformer/ParameterLifter.cpp
+++ b/src/storm/transformer/ParameterLifter.cpp
@@ -275,5 +275,6 @@ namespace storm {
}
template class ParameterLifter<storm::RationalFunction, double>;
+ template class ParameterLifter<storm::RationalFunction, storm::RationalNumber>;
}
}
diff --git a/src/storm/utility/ModelInstantiator.cpp b/src/storm/utility/ModelInstantiator.cpp
index 3887bfd33..997257b8d 100644
--- a/src/storm/utility/ModelInstantiator.cpp
+++ b/src/storm/utility/ModelInstantiator.cpp
@@ -154,6 +154,12 @@ namespace storm {
template class ModelInstantiator<storm::models::sparse::Ctmc<storm::RationalFunction>, storm::models::sparse::Ctmc<double>>;
template class ModelInstantiator<storm::models::sparse::MarkovAutomaton<storm::RationalFunction>, storm::models::sparse::MarkovAutomaton<double>>;
template class ModelInstantiator<storm::models::sparse::StochasticTwoPlayerGame<storm::RationalFunction>, storm::models::sparse::StochasticTwoPlayerGame<double>>;
+
+ template class ModelInstantiator<storm::models::sparse::Dtmc<storm::RationalFunction>, storm::models::sparse::Dtmc<storm::RationalNumber>>;
+ template class ModelInstantiator<storm::models::sparse::Mdp<storm::RationalFunction>, storm::models::sparse::Mdp<storm::RationalNumber>>;
+ template class ModelInstantiator<storm::models::sparse::Ctmc<storm::RationalFunction>, storm::models::sparse::Ctmc<storm::RationalNumber>>;
+ template class ModelInstantiator<storm::models::sparse::MarkovAutomaton<storm::RationalFunction>, storm::models::sparse::MarkovAutomaton<storm::RationalNumber>>;
+ template class ModelInstantiator<storm::models::sparse::StochasticTwoPlayerGame<storm::RationalFunction>, storm::models::sparse::StochasticTwoPlayerGame<storm::RationalNumber>>;
#endif
} //namespace utility
} //namespace storm
diff --git a/src/storm/utility/constants.cpp b/src/storm/utility/constants.cpp
index 15b05caad..88ee8b355 100644
--- a/src/storm/utility/constants.cpp
+++ b/src/storm/utility/constants.cpp
@@ -414,6 +414,12 @@ namespace storm {
RationalFunction convertNumber(RationalNumber const& number) {
return RationalFunction(number);
}
+
+ template<>
+ RationalNumber convertNumber(RationalFunction const& number) {
+ STORM_LOG_ASSERT(isConstant(number), "Tried to convert a non-constant number to a constant type.");
+ return number.constantPart();
+ }
template<>
uint_fast64_t convertNumber(RationalFunction const& func) {
diff --git a/src/storm/utility/storm.h b/src/storm/utility/storm.h
index e0d1deff9..eb6dcf52d 100644
--- a/src/storm/utility/storm.h
+++ b/src/storm/utility/storm.h
@@ -67,7 +67,8 @@
#include "storm/modelchecker/reachability/SparseDtmcEliminationModelChecker.h"
#include "storm/modelchecker/abstraction/GameBasedMdpModelChecker.h"
#include "storm/modelchecker/exploration/SparseExplorationModelChecker.h"
-#include "storm/modelchecker/parametric/ParameterLifting.h"
+#include "storm/modelchecker/parametric/SparseDtmcParameterLifting.h"
+#include "storm/modelchecker/parametric/SparseMdpParameterLifting.h"
#include "storm/modelchecker/csl/SparseCtmcCslModelChecker.h"
#include "storm/modelchecker/csl/helper/SparseCtmcCslHelper.h"
@@ -333,20 +334,40 @@ namespace storm {
std::string resultVisualization;
if (markovModel->isOfType(storm::models::ModelType::Dtmc)) {
- storm::modelchecker::parametric::ParameterLifting <storm::models::sparse::Dtmc<storm::RationalFunction>, double> parameterLiftingContext(*markovModel->template as<storm::models::sparse::Dtmc<storm::RationalFunction>>());
- parameterLiftingContext.specifyFormula(task);
- result = parameterLiftingContext.performRegionRefinement(parameterSpace, refinementThreshold);
- parameterLiftingStopWatch.stop();
- if (modelParameters.size() == 2) {
- resultVisualization = parameterLiftingContext.visualizeResult(result, parameterSpace, *modelParameters.begin(), *(modelParameters.rbegin()));
+ if (storm::settings::getModule<storm::settings::modules::GeneralSettings>().isExactSet()) {
+ storm::modelchecker::parametric::SparseDtmcParameterLifting <storm::models::sparse::Dtmc<storm::RationalFunction>, storm::RationalNumber> parameterLiftingContext(*markovModel->template as<storm::models::sparse::Dtmc<storm::RationalFunction>>());
+ parameterLiftingContext.specifyFormula(task);
+ result = parameterLiftingContext.performRegionRefinement(parameterSpace, refinementThreshold);
+ parameterLiftingStopWatch.stop();
+ if (modelParameters.size() == 2) {
+ resultVisualization = parameterLiftingContext.visualizeResult(result, parameterSpace, *modelParameters.begin(), *(modelParameters.rbegin()));
+ }
+ } else {
+ storm::modelchecker::parametric::SparseDtmcParameterLifting <storm::models::sparse::Dtmc<storm::RationalFunction>, double> parameterLiftingContext(*markovModel->template as<storm::models::sparse::Dtmc<storm::RationalFunction>>());
+ parameterLiftingContext.specifyFormula(task);
+ result = parameterLiftingContext.performRegionRefinement(parameterSpace, refinementThreshold);
+ parameterLiftingStopWatch.stop();
+ if (modelParameters.size() == 2) {
+ resultVisualization = parameterLiftingContext.visualizeResult(result, parameterSpace, *modelParameters.begin(), *(modelParameters.rbegin()));
+ }
}
} else if (markovModel->isOfType(storm::models::ModelType::Mdp)) {
- storm::modelchecker::parametric::ParameterLifting<storm::models::sparse::Mdp<storm::RationalFunction>, double> parameterLiftingContext(*markovModel->template as<storm::models::sparse::Mdp<storm::RationalFunction>>());
- parameterLiftingContext.specifyFormula(task);
- result = parameterLiftingContext.performRegionRefinement(parameterSpace, refinementThreshold);
- parameterLiftingStopWatch.stop();
- if (modelParameters.size() == 2) {
- resultVisualization = parameterLiftingContext.visualizeResult(result, parameterSpace, *modelParameters.begin(), *(modelParameters.rbegin()));
+ if (storm::settings::getModule<storm::settings::modules::GeneralSettings>().isExactSet()) {
+ storm::modelchecker::parametric::SparseMdpParameterLifting<storm::models::sparse::Mdp<storm::RationalFunction>, storm::RationalNumber> parameterLiftingContext(*markovModel->template as<storm::models::sparse::Mdp<storm::RationalFunction>>());
+ parameterLiftingContext.specifyFormula(task);
+ result = parameterLiftingContext.performRegionRefinement(parameterSpace, refinementThreshold);
+ parameterLiftingStopWatch.stop();
+ if (modelParameters.size() == 2) {
+ resultVisualization = parameterLiftingContext.visualizeResult(result, parameterSpace, *modelParameters.begin(), *(modelParameters.rbegin()));
+ }
+ } else {
+ storm::modelchecker::parametric::SparseMdpParameterLifting<storm::models::sparse::Mdp<storm::RationalFunction>, double> parameterLiftingContext(*markovModel->template as<storm::models::sparse::Mdp<storm::RationalFunction>>());
+ parameterLiftingContext.specifyFormula(task);
+ result = parameterLiftingContext.performRegionRefinement(parameterSpace, refinementThreshold);
+ parameterLiftingStopWatch.stop();
+ if (modelParameters.size() == 2) {
+ resultVisualization = parameterLiftingContext.visualizeResult(result, parameterSpace, *modelParameters.begin(), *(modelParameters.rbegin()));
+ }
}
} else {
STORM_LOG_THROW(false, storm::exceptions::InvalidSettingsException, "Unable to perform parameterLifting on the provided model type.");
diff --git a/src/test/modelchecker/SparseDtmcParameterLiftingTest.cpp b/src/test/modelchecker/SparseDtmcParameterLiftingTest.cpp
index dd8fd422d..4de2b0c54 100644
--- a/src/test/modelchecker/SparseDtmcParameterLiftingTest.cpp
+++ b/src/test/modelchecker/SparseDtmcParameterLiftingTest.cpp
@@ -7,7 +7,7 @@
#include "utility/storm.h"
#include "storm/models/sparse/Model.h"
-#include "modelchecker/parametric/ParameterLifting.h"
+#include "modelchecker/parametric/SparseDtmcParameterLifting.h"
TEST(SparseDtmcParameterLiftingTest, Brp_Prob) {
@@ -25,7 +25,7 @@ TEST(SparseDtmcParameterLiftingTest, Brp_Prob) {
auto rewParameters = storm::models::sparse::getRewardParameters(*model);
modelParameters.insert(rewParameters.begin(), rewParameters.end());
- storm::modelchecker::parametric::ParameterLifting<storm::models::sparse::Dtmc<storm::RationalFunction>, double> parameterLiftingContext(*model);
+ storm::modelchecker::parametric::SparseDtmcParameterLifting<storm::models::sparse::Dtmc<storm::RationalFunction>, double> parameterLiftingContext(*model);
parameterLiftingContext.specifyFormula(storm::modelchecker::CheckTask<storm::logic::Formula, storm::RationalFunction>(*formulas[0], true));
//start testing
@@ -55,7 +55,7 @@ TEST(SparseDtmcParameterLiftingTest, Brp_Rew) {
auto rewParameters = storm::models::sparse::getRewardParameters(*model);
modelParameters.insert(rewParameters.begin(), rewParameters.end());
- storm::modelchecker::parametric::ParameterLifting<storm::models::sparse::Dtmc<storm::RationalFunction>, double> parameterLiftingContext(*model);
+ storm::modelchecker::parametric::SparseDtmcParameterLifting<storm::models::sparse::Dtmc<storm::RationalFunction>, double> parameterLiftingContext(*model);
parameterLiftingContext.specifyFormula(storm::modelchecker::CheckTask<storm::logic::Formula, storm::RationalFunction>(*formulas[0], true));
//start testing
@@ -85,7 +85,7 @@ TEST(SparseDtmcParameterLiftingTest, Brp_Rew_Bounded) {
auto rewParameters = storm::models::sparse::getRewardParameters(*model);
modelParameters.insert(rewParameters.begin(), rewParameters.end());
- storm::modelchecker::parametric::ParameterLifting<storm::models::sparse::Dtmc<storm::RationalFunction>, double> parameterLiftingContext(*model);
+ storm::modelchecker::parametric::SparseDtmcParameterLifting<storm::models::sparse::Dtmc<storm::RationalFunction>, double> parameterLiftingContext(*model);
parameterLiftingContext.specifyFormula(storm::modelchecker::CheckTask<storm::logic::Formula, storm::RationalFunction>(*formulas[0], true));
//start testing
@@ -115,7 +115,7 @@ TEST(SparseDtmcParameterLiftingTest, Brp_Rew_Infty) {
auto rewParameters = storm::models::sparse::getRewardParameters(*model);
modelParameters.insert(rewParameters.begin(), rewParameters.end());
- storm::modelchecker::parametric::ParameterLifting<storm::models::sparse::Dtmc<storm::RationalFunction>, double> parameterLiftingContext(*model);
+ storm::modelchecker::parametric::SparseDtmcParameterLifting<storm::models::sparse::Dtmc<storm::RationalFunction>, double> parameterLiftingContext(*model);
parameterLiftingContext.specifyFormula(storm::modelchecker::CheckTask<storm::logic::Formula, storm::RationalFunction>(*formulas[0], true));
//start testing
@@ -141,7 +141,7 @@ TEST(SparseDtmcParameterLiftingTest, Brp_Rew_4Par) {
auto rewParameters = storm::models::sparse::getRewardParameters(*model);
modelParameters.insert(rewParameters.begin(), rewParameters.end());
- storm::modelchecker::parametric::ParameterLifting<storm::models::sparse::Dtmc<storm::RationalFunction>, double> parameterLiftingContext(*model);
+ storm::modelchecker::parametric::SparseDtmcParameterLifting<storm::models::sparse::Dtmc<storm::RationalFunction>, double> parameterLiftingContext(*model);
parameterLiftingContext.specifyFormula(storm::modelchecker::CheckTask<storm::logic::Formula, storm::RationalFunction>(*formulas[0], true));
//start testing
@@ -172,7 +172,7 @@ TEST(SparseDtmcParameterLiftingTest, Crowds_Prob) {
auto rewParameters = storm::models::sparse::getRewardParameters(*model);
modelParameters.insert(rewParameters.begin(), rewParameters.end());
- storm::modelchecker::parametric::ParameterLifting<storm::models::sparse::Dtmc<storm::RationalFunction>, double> parameterLiftingContext(*model);
+ storm::modelchecker::parametric::SparseDtmcParameterLifting<storm::models::sparse::Dtmc<storm::RationalFunction>, double> parameterLiftingContext(*model);
parameterLiftingContext.specifyFormula(storm::modelchecker::CheckTask<storm::logic::Formula, storm::RationalFunction>(*formulas[0], true));
//start testing
@@ -205,7 +205,7 @@ TEST(SparseDtmcParameterLiftingTest, Crowds_Prob_stepBounded) {
auto rewParameters = storm::models::sparse::getRewardParameters(*model);
modelParameters.insert(rewParameters.begin(), rewParameters.end());
- storm::modelchecker::parametric::ParameterLifting<storm::models::sparse::Dtmc<storm::RationalFunction>, double> parameterLiftingContext(*model);
+ storm::modelchecker::parametric::SparseDtmcParameterLifting<storm::models::sparse::Dtmc<storm::RationalFunction>, double> parameterLiftingContext(*model);
parameterLiftingContext.specifyFormula(storm::modelchecker::CheckTask<storm::logic::Formula, storm::RationalFunction>(*formulas[0], true));
//start testing
@@ -239,7 +239,7 @@ TEST(SparseDtmcParameterLiftingTest, Crowds_Prob_1Par) {
auto rewParameters = storm::models::sparse::getRewardParameters(*model);
modelParameters.insert(rewParameters.begin(), rewParameters.end());
- storm::modelchecker::parametric::ParameterLifting<storm::models::sparse::Dtmc<storm::RationalFunction>, double> parameterLiftingContext(*model);
+ storm::modelchecker::parametric::SparseDtmcParameterLifting<storm::models::sparse::Dtmc<storm::RationalFunction>, double> parameterLiftingContext(*model);
parameterLiftingContext.specifyFormula(storm::modelchecker::CheckTask<storm::logic::Formula, storm::RationalFunction>(*formulas[0], true));
//start testing
@@ -270,7 +270,7 @@ TEST(SparseDtmcParameterLiftingTest, Crowds_Prob_Const) {
auto rewParameters = storm::models::sparse::getRewardParameters(*model);
modelParameters.insert(rewParameters.begin(), rewParameters.end());
- storm::modelchecker::parametric::ParameterLifting<storm::models::sparse::Dtmc<storm::RationalFunction>, double> parameterLiftingContext(*model);
+ storm::modelchecker::parametric::SparseDtmcParameterLifting<storm::models::sparse::Dtmc<storm::RationalFunction>, double> parameterLiftingContext(*model);
parameterLiftingContext.specifyFormula(storm::modelchecker::CheckTask<storm::logic::Formula, storm::RationalFunction>(*formulas[0], true));
//start testing
diff --git a/src/test/modelchecker/SparseMdpParameterLiftingTest.cpp b/src/test/modelchecker/SparseMdpParameterLiftingTest.cpp
index c31dbf66d..0da828493 100644
--- a/src/test/modelchecker/SparseMdpParameterLiftingTest.cpp
+++ b/src/test/modelchecker/SparseMdpParameterLiftingTest.cpp
@@ -7,7 +7,7 @@
#include "utility/storm.h"
#include "storm/models/sparse/Model.h"
-#include "storm/modelchecker/parametric/ParameterLifting.h"
+#include "storm/modelchecker/parametric/SparseMdpParameterLifting.h"
TEST(SparseMdpParameterLiftingTest, two_dice_Prob) {
@@ -24,7 +24,7 @@ TEST(SparseMdpParameterLiftingTest, two_dice_Prob) {
auto rewParameters = storm::models::sparse::getRewardParameters(*model);
modelParameters.insert(rewParameters.begin(), rewParameters.end());
- storm::modelchecker::parametric::ParameterLifting<storm::models::sparse::Mdp<storm::RationalFunction>, double> parameterLiftingContext(*model);
+ storm::modelchecker::parametric::SparseMdpParameterLifting<storm::models::sparse::Mdp<storm::RationalFunction>, double> parameterLiftingContext(*model);
parameterLiftingContext.specifyFormula(storm::modelchecker::CheckTask<storm::logic::Formula, storm::RationalFunction>(*formulas[0], true));
auto allSatRegion = storm::storage::ParameterRegion<storm::RationalFunction>::parseRegion("0.495<=p1<=0.5,0.5<=p2<=0.505", modelParameters);
@@ -54,7 +54,7 @@ TEST(SparseMdpParameterLiftingTest, two_dice_Prob_bounded) {
auto rewParameters = storm::models::sparse::getRewardParameters(*model);
modelParameters.insert(rewParameters.begin(), rewParameters.end());
- storm::modelchecker::parametric::ParameterLifting<storm::models::sparse::Mdp<storm::RationalFunction>, double> parameterLiftingContext(*model);
+ storm::modelchecker::parametric::SparseMdpParameterLifting<storm::models::sparse::Mdp<storm::RationalFunction>, double> parameterLiftingContext(*model);
parameterLiftingContext.specifyFormula(storm::modelchecker::CheckTask<storm::logic::Formula, storm::RationalFunction>(*formulas[0], true));
auto allSatRegion = storm::storage::ParameterRegion<storm::RationalFunction>::parseRegion("0.495<=p1<=0.5,0.5<=p2<=0.505", modelParameters);
@@ -82,7 +82,7 @@ TEST(SparseMdpParameterLiftingTest, coin_Prob) {
auto rewParameters = storm::models::sparse::getRewardParameters(*model);
modelParameters.insert(rewParameters.begin(), rewParameters.end());
- storm::modelchecker::parametric::ParameterLifting<storm::models::sparse::Mdp<storm::RationalFunction>, double> parameterLiftingContext(*model);
+ storm::modelchecker::parametric::SparseMdpParameterLifting<storm::models::sparse::Mdp<storm::RationalFunction>, double> parameterLiftingContext(*model);
parameterLiftingContext.specifyFormula(storm::modelchecker::CheckTask<storm::logic::Formula, storm::RationalFunction>(*formulas[0], true));
//start testing
@@ -112,7 +112,7 @@ TEST(SparseMdpParameterLiftingTest, brp_Prop) {
auto rewParameters = storm::models::sparse::getRewardParameters(*model);
modelParameters.insert(rewParameters.begin(), rewParameters.end());
- storm::modelchecker::parametric::ParameterLifting<storm::models::sparse::Mdp<storm::RationalFunction>, double> parameterLiftingContext(*model);
+ storm::modelchecker::parametric::SparseMdpParameterLifting<storm::models::sparse::Mdp<storm::RationalFunction>, double> parameterLiftingContext(*model);
parameterLiftingContext.specifyFormula(storm::modelchecker::CheckTask<storm::logic::Formula, storm::RationalFunction>(*formulas[0], true));
//start testing
@@ -143,7 +143,7 @@ TEST(SparseMdpParameterLiftingTest, brp_Rew) {
auto rewParameters = storm::models::sparse::getRewardParameters(*model);
modelParameters.insert(rewParameters.begin(), rewParameters.end());
- storm::modelchecker::parametric::ParameterLifting<storm::models::sparse::Mdp<storm::RationalFunction>, double> parameterLiftingContext(*model);
+ storm::modelchecker::parametric::SparseMdpParameterLifting<storm::models::sparse::Mdp<storm::RationalFunction>, double> parameterLiftingContext(*model);
parameterLiftingContext.specifyFormula(storm::modelchecker::CheckTask<storm::logic::Formula, storm::RationalFunction>(*formulas[0], true));
//start testing
@@ -173,7 +173,7 @@ TEST(SparseMdpParameterLiftingTest, brp_Rew_bounded) {
auto rewParameters = storm::models::sparse::getRewardParameters(*model);
modelParameters.insert(rewParameters.begin(), rewParameters.end());
- storm::modelchecker::parametric::ParameterLifting<storm::models::sparse::Mdp<storm::RationalFunction>, double> parameterLiftingContext(*model);
+ storm::modelchecker::parametric::SparseMdpParameterLifting<storm::models::sparse::Mdp<storm::RationalFunction>, double> parameterLiftingContext(*model);
parameterLiftingContext.specifyFormula(storm::modelchecker::CheckTask<storm::logic::Formula, storm::RationalFunction>(*formulas[0], true));
//start testing
@@ -204,7 +204,7 @@ TEST(SparseMdpParameterLiftingTest, Brp_Rew_Infty) {
auto rewParameters = storm::models::sparse::getRewardParameters(*model);
modelParameters.insert(rewParameters.begin(), rewParameters.end());
- storm::modelchecker::parametric::ParameterLifting<storm::models::sparse::Mdp<storm::RationalFunction>, double> parameterLiftingContext(*model);
+ storm::modelchecker::parametric::SparseMdpParameterLifting<storm::models::sparse::Mdp<storm::RationalFunction>, double> parameterLiftingContext(*model);
parameterLiftingContext.specifyFormula(storm::modelchecker::CheckTask<storm::logic::Formula, storm::RationalFunction>(*formulas[0], true));
//start testing
@@ -230,7 +230,7 @@ TEST(SparseMdpParameterLiftingTest, Brp_Rew_4Par) {
auto rewParameters = storm::models::sparse::getRewardParameters(*model);
modelParameters.insert(rewParameters.begin(), rewParameters.end());
- storm::modelchecker::parametric::ParameterLifting<storm::models::sparse::Mdp<storm::RationalFunction>, double> parameterLiftingContext(*model);
+ storm::modelchecker::parametric::SparseMdpParameterLifting<storm::models::sparse::Mdp<storm::RationalFunction>, double> parameterLiftingContext(*model);
parameterLiftingContext.specifyFormula(storm::modelchecker::CheckTask<storm::logic::Formula, storm::RationalFunction>(*formulas[0], true));
//start testing