diff --git a/src/storm/modelchecker/parametric/ParameterLifting.cpp b/src/storm/modelchecker/parametric/ParameterLifting.cpp
new file mode 100644
index 000000000..0e2eebab9
--- /dev/null
+++ b/src/storm/modelchecker/parametric/ParameterLifting.cpp
@@ -0,0 +1,187 @@
+#include "storm/modelchecker/parametric/ParameterLifting.h"
+
+#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/models/sparse/StandardRewardModel.h"
+#include "storm/models/sparse/Dtmc.h"
+#include "storm/models/sparse/Mdp.h"
+
+#include "storm/exceptions/NotSupportedException.h"
+#include "storm/exceptions/InvalidStateException.h"
+
+namespace storm {
+ namespace modelchecker {
+ namespace parametric {
+
+
+ template <typename SparseModelType, typename ConstantType>
+ ParameterLifting<SparseModelType, ConstantType>::ParameterLifting(SparseModelType const& parametricModel) : parametricModel(parametricModel){
+ STORM_LOG_THROW(parametricModel.getInitialStates().getNumberOfSetBits() == 1, storm::exceptions::NotSupportedException, "Parameter lifting requires models with only one initial state");
+ }
+
+ template <typename SparseModelType, typename ConstantType>
+ void ParameterLifting<SparseModelType, ConstantType>::specifyFormula(CheckTask<storm::logic::Formula, typename SparseModelType::ValueType> const& checkTask) {
+ STORM_LOG_THROW(checkTask.isBoundSet(), storm::exceptions::NotSupportedException, "Parameter lifting requires a bounded property.");
+ STORM_LOG_THROW(parameterLiftingChecker->canHandle(checkTask), storm::exceptions::NotSupportedException, "Parameter lifting is not supported for this property.");
+
+ simplifyParametricModel(checkTask);
+ initializeUnderlyingCheckers();
+ currentCheckTask = std::make_unique<storm::modelchecker::CheckTask<storm::logic::Formula, typename SparseModelType::ValueType>>(checkTask.substituteFormula(*currentFormula));
+
+ instantiationChecker->specifyFormula(*currentCheckTask);
+ parameterLiftingChecker->specifyFormula(*currentCheckTask);
+ }
+
+ template <typename SparseModelType, typename ConstantType>
+ RegionCheckResult ParameterLifting<SparseModelType, ConstantType>::analyzeRegion(storm::storage::ParameterRegion<typename SparseModelType::ValueType> const& region, bool sampleVerticesOfRegion) const {
+ // First sample for one point to decide whether we should try to prove AllSat or AllViolated
+ if(instantiationChecker->check(region.getCenterPoint())->asExplicitQualitativeCheckResult()[*getConsideredParametricModel().getInitialStates().begin()]) {
+ // try to prove AllSat
+ if(parameterLiftingChecker->check(region, this->currentCheckTask->getOptimizationDirection())->asExplicitQualitativeCheckResult()[*getConsideredParametricModel().getInitialStates().begin()]) {
+ return RegionCheckResult::AllSat;
+ } else if (sampleVerticesOfRegion) {
+ // Check if there is a point in the region for which the property is violated
+ auto vertices = region.getVerticesOfRegion(region.getVariables());
+ for (auto const& v : vertices) {
+ if (!instantiationChecker->check(v)->asExplicitQualitativeCheckResult()[*getConsideredParametricModel().getInitialStates().begin()]) {
+ return RegionCheckResult::ExistsBoth;
+ }
+ }
+ }
+ // Reaching this point means that we only know that there is (at least) one point in the region for which the property is satisfied
+ return RegionCheckResult::ExistsSat;
+ } else {
+ // try to prove AllViolated
+ if(!parameterLiftingChecker->check(region, storm::solver::invert(this->currentCheckTask->getOptimizationDirection()))->asExplicitQualitativeCheckResult()[*getConsideredParametricModel().getInitialStates().begin()]) {
+ return RegionCheckResult::AllViolated;
+ } else if (sampleVerticesOfRegion) {
+ // Check if there is a point in the region for which the property is satisfied
+ auto vertices = region.getVerticesOfRegion(region.getVariables());
+ for (auto const& v : vertices) {
+ if (instantiationChecker->check(v)->asExplicitQualitativeCheckResult()[*getConsideredParametricModel().getInitialStates().begin()]) {
+ return RegionCheckResult::ExistsBoth;
+ }
+ }
+ }
+ // Reaching this point means that we only know that there is (at least) one point in the region for which the property is violated
+ return RegionCheckResult::ExistsViolated;
+ }
+ }
+
+ 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 {
+ 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>();
+
+ std::vector<std::pair<storm::storage::ParameterRegion<typename SparseModelType::ValueType>, RegionCheckResult>> regions;
+ regions.emplace_back(region, RegionCheckResult::Unknown);
+ storm::storage::BitVector resultRegions(1, true);
+ uint_fast64_t indexOfCurrentRegion = 0;
+
+ while (fractionOfUndiscoveredArea > threshold) {
+ STORM_LOG_THROW(indexOfCurrentRegion < regions.size(), storm::exceptions::InvalidStateException, "Threshold for undiscovered area not reached but no unprocessed regions left.");
+ auto & currentRegion = regions[indexOfCurrentRegion];
+ RegionCheckResult res = analyzeRegion(currentRegion.first, currentRegion.second, false);
+ switch (res) {
+ case RegionCheckResult::AllSat:
+ fractionOfUndiscoveredArea -= currentRegion.area() / areaOfParameterSpace;
+ fractionOfAllSatArea += currentRegion.area() / areaOfParameterSpace;
+ break;
+ case RegionCheckResult::AllViolated:
+ fractionOfUndiscoveredArea -= currentRegion.area() / areaOfParameterSpace;
+ fractionOfAllViolatedArea += currentRegion.area() / areaOfParameterSpace;
+ break;
+ default:
+ uint_fast64_t oldNumOfRegions = regions.size();
+ std::vector<storm::storage::ParameterRegion<typename SparseModelType::ValueType>> newRegions;
+ currentRegion.split(currentRegion.getCenterPoint(), regions);
+ resultRegions.grow(regions.size());
+ resultRegions.set(resultRegions.begin() + oldNumOfRegions-1?, resultRegions.begin() + regions.size()-1? );
+ resultRegions.set(indexOfCurrentRegion, false);
+ break;
+ }
+ ++indexOfCurrentRegion;
+ }
+ std::cout << " done! " << std::endl << "Fraction of ALLSAT;ALLVIOLATED;UNDISCOVERED area:" << std::endl;
+ std::cout << "REFINEMENTRESULT;" <<storm::utility::convertNumber<double>(fractionOfAllSatArea) << ";" << storm::utility::convertNumber<double>(fractionOfAllViolatedArea) << ";" << storm::utility::convertNumber<double>(fractionOfUndiscoveredArea) << std::endl;
+
+ ()
+ return ;
+ }
+
+ 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) {
+ return *simplifiedModel;
+ } else {
+ 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();
+ }
+ }
+
+
+#ifdef STORM_HAVE_CARL
+ template class ParameterLifting<storm::models::sparse::Dtmc<storm::RationalFunction>, double>;
+ template class ParameterLifting<storm::models::sparse::Mdp<storm::RationalFunction>, double>;
+#endif
+ } // namespace parametric
+ } //namespace modelchecker
+} //namespace storm
+
diff --git a/src/storm/modelchecker/parametric/ParameterLifting.h b/src/storm/modelchecker/parametric/ParameterLifting.h
new file mode 100644
index 000000000..2685b8551
--- /dev/null
+++ b/src/storm/modelchecker/parametric/ParameterLifting.h
@@ -0,0 +1,64 @@
+#pragma once
+
+#include <memory>
+
+#include "storm/modelchecker/parametric/RegionCheckResult.h"
+#include "storm/modelchecker/parametric/SparseInstantiationModelChecker.h"
+#include "storm/modelchecker/parametric/SparseParameterLiftingModelChecker.h"
+#include "storm/storage/ParameterRegion.h"
+
+#include "storm/modelchecker/CheckTask.h"
+
+namespace storm {
+ namespace modelchecker{
+ namespace parametric{
+
+ template<typename SparseModelType, typename ConstantType>
+ class ParameterLifting {
+
+ public:
+
+ ParameterLifting(SparseModelType const& parametricModel);
+
+ ~ParameterLifting() = default;
+
+ void specifyFormula(CheckTask<storm::logic::Formula, typename SparseModelType::ValueType> const& checkTask);
+
+ /*!
+ * Analyzes the given region by applying parameter lifting.
+ * We first 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, bool sampleVerticesOfRegion) const;
+
+ /*!
+ * 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;
+
+ private:
+ SparseModelType const& getConsideredParametricModel() const;
+
+ void initializeUnderlyingCheckers();
+ void simplifyParametricModel(CheckTask<storm::logic::Formula, typename SparseModelType::ValueType> const& checkTask);
+
+
+ SparseModelType const& parametricModel;
+ 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<SparseInstantiationModelChecker<SparseModelType, ConstantType>> instantiationChecker;
+
+
+ };
+
+ } //namespace parametric
+ } //namespace modelchecker
+} //namespace storm
diff --git a/src/storm/modelchecker/region/RegionCheckResult.cpp b/src/storm/modelchecker/parametric/RegionCheckResult.cpp
similarity index 67%
rename from src/storm/modelchecker/region/RegionCheckResult.cpp
rename to src/storm/modelchecker/parametric/RegionCheckResult.cpp
index 896cc4644..910de6efe 100644
--- a/src/storm/modelchecker/region/RegionCheckResult.cpp
+++ b/src/storm/modelchecker/parametric/RegionCheckResult.cpp
@@ -1,35 +1,29 @@
-/*
- * File: RegionCheckResult.cpp
- * Author: tim
- *
- * Created on September 9, 2015, 1:56 PM
- */
+#include "storm/modelchecker/parametric/RegionCheckResult.h"
-#include "RegionCheckResult.h"
#include "storm/utility/macros.h"
#include "storm/exceptions/NotImplementedException.h"
namespace storm {
namespace modelchecker {
- namespace region {
+ namespace parametric {
std::ostream& operator<<(std::ostream& os, RegionCheckResult const& regionCheckResult) {
switch (regionCheckResult) {
- case RegionCheckResult::UNKNOWN:
+ case RegionCheckResult::Unknown:
os << "Unknown";
break;
- case RegionCheckResult::EXISTSSAT:
+ case RegionCheckResult::ExistsSat:
os << "ExistsSat";
break;
- case RegionCheckResult::EXISTSVIOLATED:
+ case RegionCheckResult::ExistsViolated:
os << "ExistsViolated";
break;
- case RegionCheckResult::EXISTSBOTH:
+ case RegionCheckResult::ExistsBoth:
os << "ExistsBoth";
break;
- case RegionCheckResult::ALLSAT:
+ case RegionCheckResult::AllSat:
os << "AllSat";
break;
- case RegionCheckResult::ALLVIOLATED:
+ case RegionCheckResult::AllViolated:
os << "AllViolated";
break;
default:
diff --git a/src/storm/modelchecker/parametric/RegionCheckResult.h b/src/storm/modelchecker/parametric/RegionCheckResult.h
new file mode 100644
index 000000000..98ee3bc9c
--- /dev/null
+++ b/src/storm/modelchecker/parametric/RegionCheckResult.h
@@ -0,0 +1,24 @@
+#pragma once
+
+#include <ostream>
+
+namespace storm {
+ namespace modelchecker {
+ namespace parametric {
+ /*!
+ * The results for a single Parameter region
+ */
+ enum class RegionCheckResult {
+ Unknown, /*!< the result is unknown */
+ ExistsSat, /*!< the formula is satisfied for at least one parameter evaluation that lies in the given region */
+ ExistsViolated, /*!< the formula is violated for at least one parameter evaluation that lies in the given region */
+ ExistsBoth, /*!< the formula is satisfied for some parameters but also violated for others */
+ AllSat, /*!< the formula is satisfied for all parameters in the given region */
+ AllViolated /*!< the formula is violated for all parameters in the given region */
+ };
+
+ std::ostream& operator<<(std::ostream& os, RegionCheckResult const& regionCheckResult);
+ }
+ }
+}
+
diff --git a/src/storm/modelchecker/parametric/SparseDtmcParameterLiftingModelChecker.cpp b/src/storm/modelchecker/parametric/SparseDtmcParameterLiftingModelChecker.cpp
index 175ffc0fe..a682fb089 100644
--- a/src/storm/modelchecker/parametric/SparseDtmcParameterLiftingModelChecker.cpp
+++ b/src/storm/modelchecker/parametric/SparseDtmcParameterLiftingModelChecker.cpp
@@ -26,7 +26,7 @@ namespace storm {
}
template <typename SparseModelType, typename ConstantType>
- bool SparseDtmcParameterLiftingModelChecker<SparseModelType, ConstantType>::canHandle(CheckTask<storm::logic::Formula, ConstantType> const& checkTask) const {
+ bool SparseDtmcParameterLiftingModelChecker<SparseModelType, ConstantType>::canHandle(CheckTask<storm::logic::Formula, typename SparseModelType::ValueType> const& checkTask) const {
return checkTask.getFormula().isInFragment(storm::logic::reachability().setReachabilityRewardFormulasAllowed(true).setBoundedUntilFormulasAllowed(true).setCumulativeRewardFormulasAllowed(true));
}
@@ -160,7 +160,7 @@ namespace storm {
}
template <typename SparseModelType, typename ConstantType>
- std::unique_ptr<CheckResult> SparseDtmcParameterLiftingModelChecker<SparseModelType, ConstantType>::computeQuantitativeValues(ParameterRegion<typename SparseModelType::ValueType> const& region, storm::solver::OptimizationDirection const& dirForParameters) {
+ std::unique_ptr<CheckResult> SparseDtmcParameterLiftingModelChecker<SparseModelType, ConstantType>::computeQuantitativeValues(storm::storage::ParameterRegion<typename SparseModelType::ValueType> const& region, storm::solver::OptimizationDirection const& dirForParameters) {
if(maybeStates.empty()) {
return std::make_unique<storm::modelchecker::ExplicitQuantitativeCheckResult<ConstantType>>(resultsForNonMaybeStates);
diff --git a/src/storm/modelchecker/parametric/SparseDtmcParameterLiftingModelChecker.h b/src/storm/modelchecker/parametric/SparseDtmcParameterLiftingModelChecker.h
index 0384e839f..4d810cd48 100644
--- a/src/storm/modelchecker/parametric/SparseDtmcParameterLiftingModelChecker.h
+++ b/src/storm/modelchecker/parametric/SparseDtmcParameterLiftingModelChecker.h
@@ -22,7 +22,7 @@ namespace storm {
SparseDtmcParameterLiftingModelChecker(SparseModelType const& parametricModel);
SparseDtmcParameterLiftingModelChecker(SparseModelType const& parametricModel, std::unique_ptr<storm::solver::MinMaxLinearEquationSolverFactory<ConstantType>>&& solverFactory);
- virtual bool canHandle(CheckTask<storm::logic::Formula, ConstantType> const& checkTask) const override;
+ virtual bool canHandle(CheckTask<storm::logic::Formula, typename SparseModelType::ValueType> const& checkTask) const override;
protected:
@@ -31,7 +31,7 @@ namespace storm {
virtual void specifyReachabilityRewardFormula(CheckTask<storm::logic::EventuallyFormula, ConstantType> const& checkTask) override;
virtual void specifyCumulativeRewardFormula(CheckTask<storm::logic::CumulativeRewardFormula, ConstantType> const& checkTask) override;
- virtual std::unique_ptr<CheckResult> computeQuantitativeValues(ParameterRegion<typename SparseModelType::ValueType> const& region, storm::solver::OptimizationDirection const& dirForParameters) override;
+ virtual std::unique_ptr<CheckResult> computeQuantitativeValues(storm::storage::ParameterRegion<typename SparseModelType::ValueType> const& region, storm::solver::OptimizationDirection const& dirForParameters) override;
virtual void reset() override;
diff --git a/src/storm/modelchecker/parametric/SparseMdpParameterLiftingModelChecker.cpp b/src/storm/modelchecker/parametric/SparseMdpParameterLiftingModelChecker.cpp
index 463637d2a..bb862cd0a 100644
--- a/src/storm/modelchecker/parametric/SparseMdpParameterLiftingModelChecker.cpp
+++ b/src/storm/modelchecker/parametric/SparseMdpParameterLiftingModelChecker.cpp
@@ -28,7 +28,7 @@ namespace storm {
}
template <typename SparseModelType, typename ConstantType>
- bool SparseMdpParameterLiftingModelChecker<SparseModelType, ConstantType>::canHandle(CheckTask<storm::logic::Formula, ConstantType> const& checkTask) const {
+ bool SparseMdpParameterLiftingModelChecker<SparseModelType, ConstantType>::canHandle(CheckTask<storm::logic::Formula, typename SparseModelType::ValueType> const& checkTask) const {
return checkTask.getFormula().isInFragment(storm::logic::reachability().setReachabilityRewardFormulasAllowed(true).setBoundedUntilFormulasAllowed(true).setCumulativeRewardFormulasAllowed(true));
}
@@ -194,7 +194,7 @@ namespace storm {
}
template <typename SparseModelType, typename ConstantType>
- std::unique_ptr<CheckResult> SparseMdpParameterLiftingModelChecker<SparseModelType, ConstantType>::computeQuantitativeValues(ParameterRegion<typename SparseModelType::ValueType> const& region, storm::solver::OptimizationDirection const& dirForParameters) {
+ std::unique_ptr<CheckResult> SparseMdpParameterLiftingModelChecker<SparseModelType, ConstantType>::computeQuantitativeValues(storm::storage::ParameterRegion<typename SparseModelType::ValueType> const& region, storm::solver::OptimizationDirection const& dirForParameters) {
if(maybeStates.empty()) {
return std::make_unique<storm::modelchecker::ExplicitQuantitativeCheckResult<ConstantType>>(resultsForNonMaybeStates);
diff --git a/src/storm/modelchecker/parametric/SparseMdpParameterLiftingModelChecker.h b/src/storm/modelchecker/parametric/SparseMdpParameterLiftingModelChecker.h
index a1e73a78b..76d66bbd7 100644
--- a/src/storm/modelchecker/parametric/SparseMdpParameterLiftingModelChecker.h
+++ b/src/storm/modelchecker/parametric/SparseMdpParameterLiftingModelChecker.h
@@ -22,7 +22,7 @@ namespace storm {
SparseMdpParameterLiftingModelChecker(SparseModelType const& parametricModel);
SparseMdpParameterLiftingModelChecker(SparseModelType const& parametricModel, std::unique_ptr<storm::utility::solver::GameSolverFactory<ConstantType>>&& solverFactory);
- virtual bool canHandle(CheckTask<storm::logic::Formula, ConstantType> const& checkTask) const override;
+ virtual bool canHandle(CheckTask<storm::logic::Formula, typename SparseModelType::ValueType> const& checkTask) const override;
protected:
@@ -31,7 +31,7 @@ namespace storm {
virtual void specifyReachabilityRewardFormula(CheckTask<storm::logic::EventuallyFormula, ConstantType> const& checkTask) override;
virtual void specifyCumulativeRewardFormula(CheckTask<storm::logic::CumulativeRewardFormula, ConstantType> const& checkTask) override;
- virtual std::unique_ptr<CheckResult> computeQuantitativeValues(ParameterRegion<typename SparseModelType::ValueType> const& region, storm::solver::OptimizationDirection const& dirForParameters) override;
+ virtual std::unique_ptr<CheckResult> computeQuantitativeValues(storm::storage::ParameterRegion<typename SparseModelType::ValueType> const& region, storm::solver::OptimizationDirection const& dirForParameters) override;
virtual void reset() override;
diff --git a/src/storm/modelchecker/parametric/SparseParameterLiftingModelChecker.cpp b/src/storm/modelchecker/parametric/SparseParameterLiftingModelChecker.cpp
index d56936397..93fce21f7 100644
--- a/src/storm/modelchecker/parametric/SparseParameterLiftingModelChecker.cpp
+++ b/src/storm/modelchecker/parametric/SparseParameterLiftingModelChecker.cpp
@@ -49,7 +49,7 @@ namespace storm {
}
template <typename SparseModelType, typename ConstantType>
- std::unique_ptr<CheckResult> SparseParameterLiftingModelChecker<SparseModelType, ConstantType>::check(ParameterRegion<typename SparseModelType::ValueType> const& region, storm::solver::OptimizationDirection const& dirForParameters) {
+ std::unique_ptr<CheckResult> SparseParameterLiftingModelChecker<SparseModelType, ConstantType>::check(storm::storage::ParameterRegion<typename SparseModelType::ValueType> const& region, storm::solver::OptimizationDirection const& dirForParameters) {
auto quantitativeResult = computeQuantitativeValues(region, dirForParameters);
if(currentCheckTask->getFormula().hasQuantitativeResult()) {
return quantitativeResult;
diff --git a/src/storm/modelchecker/parametric/SparseParameterLiftingModelChecker.h b/src/storm/modelchecker/parametric/SparseParameterLiftingModelChecker.h
index f93ab84e6..59fd8458b 100644
--- a/src/storm/modelchecker/parametric/SparseParameterLiftingModelChecker.h
+++ b/src/storm/modelchecker/parametric/SparseParameterLiftingModelChecker.h
@@ -22,7 +22,7 @@ namespace storm {
public:
SparseParameterLiftingModelChecker(SparseModelType const& parametricModel);
- virtual bool canHandle(CheckTask<storm::logic::Formula, ConstantType> const& checkTask) const = 0;
+ virtual bool canHandle(CheckTask<storm::logic::Formula, typename SparseModelType::ValueType> const& checkTask) const = 0;
void specifyFormula(CheckTask<storm::logic::Formula, typename SparseModelType::ValueType> const& checkTask);
@@ -33,7 +33,7 @@ namespace storm {
* @param region the region on which parameter lifting is applied
* @param dirForParameters The optimization direction for the parameter choices. If this is, e.g., minimize, then the returned result will be a lower bound for all results induced by the parameter evaluations inside the region.
*/
- std::unique_ptr<CheckResult> check(ParameterRegion<typename SparseModelType::ValueType> const& region, storm::solver::OptimizationDirection const& dirForParameters);
+ std::unique_ptr<CheckResult> check(storm::storage::ParameterRegion<typename SparseModelType::ValueType> const& region, storm::solver::OptimizationDirection const& dirForParameters);
protected:
@@ -43,7 +43,7 @@ namespace storm {
virtual void specifyReachabilityRewardFormula(CheckTask<storm::logic::EventuallyFormula, ConstantType> const& checkTask);
virtual void specifyCumulativeRewardFormula(CheckTask<storm::logic::CumulativeRewardFormula, ConstantType> const& checkTask);
- virtual std::unique_ptr<CheckResult> computeQuantitativeValues(ParameterRegion<typename SparseModelType::ValueType> const& region, storm::solver::OptimizationDirection const& dirForParameters) = 0;
+ virtual std::unique_ptr<CheckResult> computeQuantitativeValues(storm::storage::ParameterRegion<typename SparseModelType::ValueType> const& region, storm::solver::OptimizationDirection const& dirForParameters) = 0;
virtual void reset() = 0;
diff --git a/src/storm/modelchecker/region/RegionCheckResult.h b/src/storm/modelchecker/region/RegionCheckResult.h
deleted file mode 100644
index 4c4a95364..000000000
--- a/src/storm/modelchecker/region/RegionCheckResult.h
+++ /dev/null
@@ -1,34 +0,0 @@
-/*
- * File: RegionCheckResult.h
- * Author: tim
- *
- * Created on September 9, 2015, 1:56 PM
- */
-
-#ifndef STORM_MODELCHECKER_REGION_REGIONCHECKRESULT_H
-#define STORM_MODELCHECKER_REGION_REGIONCHECKRESULT_H
-
-#include <ostream>
-
-namespace storm {
- namespace modelchecker {
- namespace region {
- /*!
- * The possible results for a single Parameter region
- */
- enum class RegionCheckResult {
- UNKNOWN, /*!< the result is unknown */
- EXISTSSAT, /*!< the formula is satisfied for at least one parameter evaluation that lies in the given region */
- EXISTSVIOLATED, /*!< the formula is violated for at least one parameter evaluation that lies in the given region */
- EXISTSBOTH, /*!< the formula is satisfied for some parameters but also violated for others */
- ALLSAT, /*!< the formula is satisfied for all parameters in the given region */
- ALLVIOLATED /*!< the formula is violated for all parameters in the given region */
- };
-
- std::ostream& operator<<(std::ostream& os, RegionCheckResult const& regionCheckResult);
- }
- }
-}
-
-#endif /* STORM_MODELCHECKER_REGION_REGIONCHECKRESULT_H */
-
diff --git a/src/storm/storage/ParameterRegion.cpp b/src/storm/storage/ParameterRegion.cpp
index 85921b6c5..d3f2a3909 100644
--- a/src/storm/storage/ParameterRegion.cpp
+++ b/src/storm/storage/ParameterRegion.cpp
@@ -11,241 +11,235 @@
#include "storm/utility/file.h"
namespace storm {
- namespace modelchecker {
- namespace parametric {
+ namespace storage {
- template<typename ParametricType>
- ParameterRegion<ParametricType>::ParameterRegion(Valuation const& lowerBoundaries, Valuation const& upperBoundaries) : lowerBoundaries(lowerBoundaries), upperBoundaries(upperBoundaries) {
- init();
- }
+ template<typename ParametricType>
+ ParameterRegion<ParametricType>::ParameterRegion(Valuation const& lowerBoundaries, Valuation const& upperBoundaries) : lowerBoundaries(lowerBoundaries), upperBoundaries(upperBoundaries) {
+ init();
+ }
- template<typename ParametricType>
- ParameterRegion<ParametricType>::ParameterRegion(Valuation&& lowerBoundaries, Valuation&& upperBoundaries) : lowerBoundaries(lowerBoundaries), upperBoundaries(upperBoundaries) {
- init();
- }
+ template<typename ParametricType>
+ ParameterRegion<ParametricType>::ParameterRegion(Valuation&& lowerBoundaries, Valuation&& upperBoundaries) : lowerBoundaries(lowerBoundaries), upperBoundaries(upperBoundaries) {
+ init();
+ }
- template<typename ParametricType>
- void ParameterRegion<ParametricType>::init() {
- //check whether both mappings map the same variables, check that lower boundary <= upper boundary, and pre-compute the set of variables
- for (auto const& variableWithLowerBoundary : this->lowerBoundaries) {
- auto variableWithUpperBoundary = this->upperBoundaries.find(variableWithLowerBoundary.first);
- STORM_LOG_THROW((variableWithUpperBoundary != upperBoundaries.end()), storm::exceptions::InvalidArgumentException, "Could not create region. No upper boundary specified for Variable " << variableWithLowerBoundary.first);
- STORM_LOG_THROW((variableWithLowerBoundary.second<=variableWithUpperBoundary->second), storm::exceptions::InvalidArgumentException, "Could not create region. The lower boundary for " << variableWithLowerBoundary.first << " is larger then the upper boundary");
- this->variables.insert(variableWithLowerBoundary.first);
- }
- for (auto const& variableWithBoundary : this->upperBoundaries) {
- STORM_LOG_THROW((this->variables.find(variableWithBoundary.first) != this->variables.end()), storm::exceptions::InvalidArgumentException, "Could not create region. No lower boundary specified for Variable " << variableWithBoundary.first);
- }
+ template<typename ParametricType>
+ void ParameterRegion<ParametricType>::init() {
+ //check whether both mappings map the same variables, check that lower boundary <= upper boundary, and pre-compute the set of variables
+ for (auto const& variableWithLowerBoundary : this->lowerBoundaries) {
+ auto variableWithUpperBoundary = this->upperBoundaries.find(variableWithLowerBoundary.first);
+ STORM_LOG_THROW((variableWithUpperBoundary != upperBoundaries.end()), storm::exceptions::InvalidArgumentException, "Could not create region. No upper boundary specified for Variable " << variableWithLowerBoundary.first);
+ STORM_LOG_THROW((variableWithLowerBoundary.second<=variableWithUpperBoundary->second), storm::exceptions::InvalidArgumentException, "Could not create region. The lower boundary for " << variableWithLowerBoundary.first << " is larger then the upper boundary");
+ this->variables.insert(variableWithLowerBoundary.first);
}
-
- template<typename ParametricType>
- std::set<typename ParameterRegion<ParametricType>::VariableType> const& ParameterRegion<ParametricType>::getVariables() const {
- return this->variables;
+ for (auto const& variableWithBoundary : this->upperBoundaries) {
+ STORM_LOG_THROW((this->variables.find(variableWithBoundary.first) != this->variables.end()), storm::exceptions::InvalidArgumentException, "Could not create region. No lower boundary specified for Variable " << variableWithBoundary.first);
}
+ }
- template<typename ParametricType>
- typename ParameterRegion<ParametricType>::CoefficientType const& ParameterRegion<ParametricType>::getLowerBoundary(VariableType const& variable) const {
- auto const& result = lowerBoundaries.find(variable);
- STORM_LOG_THROW(result != lowerBoundaries.end(), storm::exceptions::InvalidArgumentException, "Tried to find a lower boundary for variable " << variable << " which is not specified by this region");
- return (*result).second;
- }
+ template<typename ParametricType>
+ std::set<typename ParameterRegion<ParametricType>::VariableType> const& ParameterRegion<ParametricType>::getVariables() const {
+ return this->variables;
+ }
- template<typename ParametricType>
- typename ParameterRegion<ParametricType>::CoefficientType const& ParameterRegion<ParametricType>::getUpperBoundary(VariableType const& variable) const {
- auto const& result = upperBoundaries.find(variable);
- STORM_LOG_THROW(result != upperBoundaries.end(), storm::exceptions::InvalidArgumentException, "Tried to find an upper boundary for variable " << variable << " which is not specified by this region");
- return (*result).second;
- }
+ template<typename ParametricType>
+ typename ParameterRegion<ParametricType>::CoefficientType const& ParameterRegion<ParametricType>::getLowerBoundary(VariableType const& variable) const {
+ auto const& result = lowerBoundaries.find(variable);
+ STORM_LOG_THROW(result != lowerBoundaries.end(), storm::exceptions::InvalidArgumentException, "Tried to find a lower boundary for variable " << variable << " which is not specified by this region");
+ return (*result).second;
+ }
- template<typename ParametricType>
- typename ParameterRegion<ParametricType>::Valuation const& ParameterRegion<ParametricType>::getUpperBoundaries() const {
- return upperBoundaries;
- }
+ template<typename ParametricType>
+ typename ParameterRegion<ParametricType>::CoefficientType const& ParameterRegion<ParametricType>::getUpperBoundary(VariableType const& variable) const {
+ auto const& result = upperBoundaries.find(variable);
+ STORM_LOG_THROW(result != upperBoundaries.end(), storm::exceptions::InvalidArgumentException, "Tried to find an upper boundary for variable " << variable << " which is not specified by this region");
+ return (*result).second;
+ }
- template<typename ParametricType>
- typename ParameterRegion<ParametricType>::Valuation const& ParameterRegion<ParametricType>::getLowerBoundaries() const {
- return lowerBoundaries;
- }
+ template<typename ParametricType>
+ typename ParameterRegion<ParametricType>::Valuation const& ParameterRegion<ParametricType>::getUpperBoundaries() const {
+ return upperBoundaries;
+ }
+
+ template<typename ParametricType>
+ typename ParameterRegion<ParametricType>::Valuation const& ParameterRegion<ParametricType>::getLowerBoundaries() const {
+ return lowerBoundaries;
+ }
- template<typename ParametricType>
- std::vector<typename ParameterRegion<ParametricType>::Valuation> ParameterRegion<ParametricType>::getVerticesOfRegion(std::set<VariableType> const& consideredVariables) const {
- std::size_t const numOfVariables = consideredVariables.size();
- std::size_t const numOfVertices = std::pow(2, numOfVariables);
- std::vector<Valuation> resultingVector(numOfVertices);
-
- for (uint_fast64_t vertexId = 0; vertexId < numOfVertices; ++vertexId) {
- //interprete vertexId as a bit sequence
- //the consideredVariables.size() least significant bits of vertex will always represent the next vertex
- //(00...0 = lower boundaries for all variables, 11...1 = upper boundaries for all variables)
- uint_fast64_t variableIndex = 0;
- for (auto const& variable : consideredVariables) {
- if ((vertexId >> variableIndex) % 2 == 0) {
- resultingVector[vertexId].insert(std::pair<VariableType, CoefficientType>(variable, getLowerBoundary(variable)));
- } else {
- resultingVector[vertexId].insert(std::pair<VariableType, CoefficientType>(variable, getUpperBoundary(variable)));
- }
- ++variableIndex;
+ template<typename ParametricType>
+ std::vector<typename ParameterRegion<ParametricType>::Valuation> ParameterRegion<ParametricType>::getVerticesOfRegion(std::set<VariableType> const& consideredVariables) const {
+ std::size_t const numOfVariables = consideredVariables.size();
+ std::size_t const numOfVertices = std::pow(2, numOfVariables);
+ std::vector<Valuation> resultingVector(numOfVertices);
+
+ for (uint_fast64_t vertexId = 0; vertexId < numOfVertices; ++vertexId) {
+ //interprete vertexId as a bit sequence
+ //the consideredVariables.size() least significant bits of vertex will always represent the next vertex
+ //(00...0 = lower boundaries for all variables, 11...1 = upper boundaries for all variables)
+ uint_fast64_t variableIndex = 0;
+ for (auto const& variable : consideredVariables) {
+ if ((vertexId >> variableIndex) % 2 == 0) {
+ resultingVector[vertexId].insert(std::pair<VariableType, CoefficientType>(variable, getLowerBoundary(variable)));
+ } else {
+ resultingVector[vertexId].insert(std::pair<VariableType, CoefficientType>(variable, getUpperBoundary(variable)));
}
+ ++variableIndex;
}
- return resultingVector;
}
+ return resultingVector;
+ }
- template<typename ParametricType>
- typename ParameterRegion<ParametricType>::Valuation ParameterRegion<ParametricType>::getSomePoint() const {
- return this->getLowerBoundaries();
- }
+ template<typename ParametricType>
+ typename ParameterRegion<ParametricType>::Valuation ParameterRegion<ParametricType>::getSomePoint() const {
+ return this->getLowerBoundaries();
+ }
- template<typename ParametricType>
- typename ParameterRegion<ParametricType>::Valuation ParameterRegion<ParametricType>::getCenterPoint() const {
- Valuation result;
- for (auto const& variable : this->variables) {
- result.insert(typename Valuation::value_type(variable, (this->getLowerBoundary(variable) + this->getUpperBoundary(variable))/2));
- }
- return result;
+ template<typename ParametricType>
+ typename ParameterRegion<ParametricType>::Valuation ParameterRegion<ParametricType>::getCenterPoint() const {
+ Valuation result;
+ for (auto const& variable : this->variables) {
+ result.insert(typename Valuation::value_type(variable, (this->getLowerBoundary(variable) + this->getUpperBoundary(variable))/2));
}
+ return result;
+ }
- template<typename ParametricType>
- typename ParameterRegion<ParametricType>::CoefficientType ParameterRegion<ParametricType>::area() const {
- CoefficientType result = storm::utility::one<CoefficientType>();
- for( auto const& variable : this->variables){
- result *= (this->getUpperBoundary(variable) - this->getLowerBoundary(variable));
- }
- return result;
+ template<typename ParametricType>
+ typename ParameterRegion<ParametricType>::CoefficientType ParameterRegion<ParametricType>::area() const {
+ CoefficientType result = storm::utility::one<CoefficientType>();
+ for( auto const& variable : this->variables){
+ result *= (this->getUpperBoundary(variable) - this->getLowerBoundary(variable));
}
+ return result;
+ }
- template<typename ParametricType>
- void ParameterRegion<ParametricType>::split(Valuation const& splittingPoint, std::vector<ParameterRegion<ParametricType> >& regionVector) const{
- //Check if splittingPoint is valid.
- STORM_LOG_THROW(splittingPoint.size() == this->variables.size(), storm::exceptions::InvalidArgumentException, "Tried to split a region w.r.t. a point, but the point considers a different number of variables.");
- for(auto const& variable : this->variables){
+ template<typename ParametricType>
+ void ParameterRegion<ParametricType>::split(Valuation const& splittingPoint, std::vector<ParameterRegion<ParametricType> >& regionVector) const{
+ //Check if splittingPoint is valid.
+ STORM_LOG_THROW(splittingPoint.size() == this->variables.size(), storm::exceptions::InvalidArgumentException, "Tried to split a region w.r.t. a point, but the point considers a different number of variables.");
+ for(auto const& variable : this->variables){
+ auto splittingPointEntry=splittingPoint.find(variable);
+ STORM_LOG_THROW(splittingPointEntry != splittingPoint.end(), storm::exceptions::InvalidArgumentException, "Tried to split a region but a variable of this region is not defined by the splitting point.");
+ STORM_LOG_THROW(this->getLowerBoundary(variable) <=splittingPointEntry->second, storm::exceptions::InvalidArgumentException, "Tried to split a region but the splitting point is not contained in the region.");
+ STORM_LOG_THROW(this->getUpperBoundary(variable) >=splittingPointEntry->second, storm::exceptions::InvalidArgumentException, "Tried to split a region but the splitting point is not contained in the region.");
+ }
+
+ //Now compute the subregions.
+ std::vector<Valuation> vertices(this->getVerticesOfRegion(this->variables));
+ for(auto const& vertex : vertices){
+ //The resulting subregion is the smallest region containing vertex and splittingPoint.
+ Valuation subLower, subUpper;
+ for(auto variableBound : this->lowerBoundaries){
+ VariableType variable = variableBound.first;
+ auto vertexEntry=vertex.find(variable);
auto splittingPointEntry=splittingPoint.find(variable);
- STORM_LOG_THROW(splittingPointEntry != splittingPoint.end(), storm::exceptions::InvalidArgumentException, "Tried to split a region but a variable of this region is not defined by the splitting point.");
- STORM_LOG_THROW(this->getLowerBoundary(variable) <=splittingPointEntry->second, storm::exceptions::InvalidArgumentException, "Tried to split a region but the splitting point is not contained in the region.");
- STORM_LOG_THROW(this->getUpperBoundary(variable) >=splittingPointEntry->second, storm::exceptions::InvalidArgumentException, "Tried to split a region but the splitting point is not contained in the region.");
+ subLower.insert(typename Valuation::value_type(variable, std::min(vertexEntry->second, splittingPointEntry->second)));
+ subUpper.insert(typename Valuation::value_type(variable, std::max(vertexEntry->second, splittingPointEntry->second)));
}
-
- //Now compute the subregions.
- std::vector<Valuation> vertices(this->getVerticesOfRegion(this->variables));
- for(auto const& vertex : vertices){
- //The resulting subregion is the smallest region containing vertex and splittingPoint.
- Valuation subLower, subUpper;
- for(auto variableBound : this->lowerBoundaries){
- VariableType variable = variableBound.first;
- auto vertexEntry=vertex.find(variable);
- auto splittingPointEntry=splittingPoint.find(variable);
- subLower.insert(typename Valuation::value_type(variable, std::min(vertexEntry->second, splittingPointEntry->second)));
- subUpper.insert(typename Valuation::value_type(variable, std::max(vertexEntry->second, splittingPointEntry->second)));
- }
- ParameterRegion<ParametricType> subRegion(std::move(subLower), std::move(subUpper));
- if(!storm::utility::isZero(subRegion.area())){
- regionVector.push_back(std::move(subRegion));
- }
+ ParameterRegion<ParametricType> subRegion(std::move(subLower), std::move(subUpper));
+ if(!storm::utility::isZero(subRegion.area())){
+ regionVector.push_back(std::move(subRegion));
}
}
+ }
- template<typename ParametricType>
- std::string ParameterRegion<ParametricType>::toString(bool boundariesAsDouble) const {
- std::stringstream regionstringstream;
- if(boundariesAsDouble) {
- for (auto var : this->getVariables()) {
- regionstringstream << storm::utility::convertNumber<double>(this->getLowerBoundary(var));
- regionstringstream << "<=";
- regionstringstream << var;
- regionstringstream << "<=";
- regionstringstream << storm::utility::convertNumber<double>(this->getUpperBoundary(var));
- regionstringstream << ",";
- }
- } else {
- for (auto var : this->getVariables()) {
- regionstringstream << this->getLowerBoundary(var);
- regionstringstream << "<=";
- regionstringstream << var;
- regionstringstream << "<=";
- regionstringstream << this->getUpperBoundary(var);
- regionstringstream << ",";
- }
+ template<typename ParametricType>
+ std::string ParameterRegion<ParametricType>::toString(bool boundariesAsDouble) const {
+ std::stringstream regionstringstream;
+ if(boundariesAsDouble) {
+ for (auto var : this->getVariables()) {
+ regionstringstream << storm::utility::convertNumber<double>(this->getLowerBoundary(var));
+ regionstringstream << "<=";
+ regionstringstream << var;
+ regionstringstream << "<=";
+ regionstringstream << storm::utility::convertNumber<double>(this->getUpperBoundary(var));
+ regionstringstream << ",";
+ }
+ } else {
+ for (auto var : this->getVariables()) {
+ regionstringstream << this->getLowerBoundary(var);
+ regionstringstream << "<=";
+ regionstringstream << var;
+ regionstringstream << "<=";
+ regionstringstream << this->getUpperBoundary(var);
+ regionstringstream << ",";
}
- std::string regionstring = regionstringstream.str();
- //the last comma should actually be a semicolon
- regionstring = regionstring.substr(0, regionstring.length() - 1) + ";";
- return regionstring;
}
+ std::string regionstring = regionstringstream.str();
+ //the last comma should actually be a semicolon
+ regionstring = regionstring.substr(0, regionstring.length() - 1) + ";";
+ return regionstring;
+ }
- template<typename ParametricType>
- void ParameterRegion<ParametricType>::parseParameterBoundaries(
- Valuation& lowerBoundaries,
- Valuation& upperBoundaries,
- std::string const& parameterBoundariesString){
-
- std::string::size_type positionOfFirstRelation = parameterBoundariesString.find("<=");
- STORM_LOG_THROW(positionOfFirstRelation!=std::string::npos, storm::exceptions::InvalidArgumentException, "When parsing the region" << parameterBoundariesString << " I could not find a '<=' after the first number");
- std::string::size_type positionOfSecondRelation = parameterBoundariesString.find("<=", positionOfFirstRelation+2);
- STORM_LOG_THROW(positionOfSecondRelation!=std::string::npos, storm::exceptions::InvalidArgumentException, "When parsing the region" << parameterBoundariesString << " I could not find a '<=' after the parameter");
-
- std::string parameter=parameterBoundariesString.substr(positionOfFirstRelation+2,positionOfSecondRelation-(positionOfFirstRelation+2));
- //removes all whitespaces from the parameter string:
- parameter.erase(std::remove_if(parameter.begin(), parameter.end(), ::isspace), parameter.end());
- STORM_LOG_THROW(parameter.length()>0, storm::exceptions::InvalidArgumentException, "When parsing the region" << parameterBoundariesString << " I could not find a parameter");
-
- VariableType var = storm::utility::region::getVariableFromString<VariableType>(parameter);
- CoefficientType lb = storm::utility::convertNumber<CoefficientType>(parameterBoundariesString.substr(0,positionOfFirstRelation));
- CoefficientType ub = storm::utility::convertNumber<CoefficientType>(parameterBoundariesString.substr(positionOfSecondRelation+2));
- lowerBoundaries.emplace(std::make_pair(var, lb));
- upperBoundaries.emplace(std::make_pair(var, ub));
- }
+ template<typename ParametricType>
+ void ParameterRegion<ParametricType>::parseParameterBoundaries(Valuation& lowerBoundaries, Valuation& upperBoundaries, std::string const& parameterBoundariesString){
+
+ std::string::size_type positionOfFirstRelation = parameterBoundariesString.find("<=");
+ STORM_LOG_THROW(positionOfFirstRelation!=std::string::npos, storm::exceptions::InvalidArgumentException, "When parsing the region" << parameterBoundariesString << " I could not find a '<=' after the first number");
+ std::string::size_type positionOfSecondRelation = parameterBoundariesString.find("<=", positionOfFirstRelation+2);
+ STORM_LOG_THROW(positionOfSecondRelation!=std::string::npos, storm::exceptions::InvalidArgumentException, "When parsing the region" << parameterBoundariesString << " I could not find a '<=' after the parameter");
+
+ std::string parameter=parameterBoundariesString.substr(positionOfFirstRelation+2,positionOfSecondRelation-(positionOfFirstRelation+2));
+ //removes all whitespaces from the parameter string:
+ parameter.erase(std::remove_if(parameter.begin(), parameter.end(), ::isspace), parameter.end());
+ STORM_LOG_THROW(parameter.length()>0, storm::exceptions::InvalidArgumentException, "When parsing the region" << parameterBoundariesString << " I could not find a parameter");
+
+ VariableType var = storm::utility::region::getVariableFromString<VariableType>(parameter);
+ CoefficientType lb = storm::utility::convertNumber<CoefficientType>(parameterBoundariesString.substr(0,positionOfFirstRelation));
+ CoefficientType ub = storm::utility::convertNumber<CoefficientType>(parameterBoundariesString.substr(positionOfSecondRelation+2));
+ lowerBoundaries.emplace(std::make_pair(var, lb));
+ upperBoundaries.emplace(std::make_pair(var, ub));
+ }
- template<typename ParametricType>
- ParameterRegion<ParametricType> ParameterRegion<ParametricType>::parseRegion(
- std::string const& regionString){
- Valuation lowerBoundaries;
- Valuation upperBoundaries;
- std::vector<std::string> parameterBoundaries;
- boost::split(parameterBoundaries, regionString, boost::is_any_of(","));
- for(auto const& parameterBoundary : parameterBoundaries){
- if(!std::all_of(parameterBoundary.begin(),parameterBoundary.end(), ::isspace)){ //skip this string if it only consists of space
- parseParameterBoundaries(lowerBoundaries, upperBoundaries, parameterBoundary);
- }
- }
- return ParameterRegion(std::move(lowerBoundaries), std::move(upperBoundaries));
+ template<typename ParametricType>
+ ParameterRegion<ParametricType> ParameterRegion<ParametricType>::parseRegion(
+ std::string const& regionString){
+ Valuation lowerBoundaries;
+ Valuation upperBoundaries;
+ std::vector<std::string> parameterBoundaries;
+ boost::split(parameterBoundaries, regionString, boost::is_any_of(","));
+ for(auto const& parameterBoundary : parameterBoundaries){
+ if(!std::all_of(parameterBoundary.begin(),parameterBoundary.end(), ::isspace)){ //skip this string if it only consists of space
+ parseParameterBoundaries(lowerBoundaries, upperBoundaries, parameterBoundary);
}
+ }
+ return ParameterRegion(std::move(lowerBoundaries), std::move(upperBoundaries));
+ }
- template<typename ParametricType>
- std::vector<ParameterRegion<ParametricType>> ParameterRegion<ParametricType>::parseMultipleRegions(
- std::string const& regionsString){
- std::vector<ParameterRegion> result;
- std::vector<std::string> regionsStrVec;
- boost::split(regionsStrVec, regionsString, boost::is_any_of(";"));
- for(auto const& regionStr : regionsStrVec){
- if(!std::all_of(regionStr.begin(),regionStr.end(), ::isspace)){ //skip this string if it only consists of space
- result.emplace_back(parseRegion(regionStr));
- }
- }
- return result;
+ template<typename ParametricType>
+ std::vector<ParameterRegion<ParametricType>> ParameterRegion<ParametricType>::parseMultipleRegions(std::string const& regionsString) {
+ std::vector<ParameterRegion> result;
+ std::vector<std::string> regionsStrVec;
+ boost::split(regionsStrVec, regionsString, boost::is_any_of(";"));
+ for(auto const& regionStr : regionsStrVec){
+ if(!std::all_of(regionStr.begin(),regionStr.end(), ::isspace)){ //skip this string if it only consists of space
+ result.emplace_back(parseRegion(regionStr));
}
+ }
+ return result;
+ }
- template<typename ParametricType>
- std::vector<ParameterRegion<ParametricType>> ParameterRegion<ParametricType>::getRegionsFromSettings(){
- STORM_LOG_THROW(storm::settings::getModule<storm::settings::modules::RegionSettings>().isRegionsSet() ||storm::settings::getModule<storm::settings::modules::RegionSettings>().isRegionFileSet(), storm::exceptions::InvalidSettingsException, "Tried to obtain regions from the settings but no regions are specified.");
- STORM_LOG_THROW(!(storm::settings::getModule<storm::settings::modules::RegionSettings>().isRegionsSet() && storm::settings::getModule<storm::settings::modules::RegionSettings>().isRegionFileSet()), storm::exceptions::InvalidSettingsException, "Regions are specified via file AND cmd line. Only one option is allowed.");
+ template<typename ParametricType>
+ std::vector<ParameterRegion<ParametricType>> ParameterRegion<ParametricType>::getRegionsFromSettings(){
+ STORM_LOG_THROW(storm::settings::getModule<storm::settings::modules::RegionSettings>().isRegionsSet() ||storm::settings::getModule<storm::settings::modules::RegionSettings>().isRegionFileSet(), storm::exceptions::InvalidSettingsException, "Tried to obtain regions from the settings but no regions are specified.");
+ STORM_LOG_THROW(!(storm::settings::getModule<storm::settings::modules::RegionSettings>().isRegionsSet() && storm::settings::getModule<storm::settings::modules::RegionSettings>().isRegionFileSet()), storm::exceptions::InvalidSettingsException, "Regions are specified via file AND cmd line. Only one option is allowed.");
- std::string regionsString;
- if(storm::settings::getModule<storm::settings::modules::RegionSettings>().isRegionsSet()){
- regionsString = storm::settings::getModule<storm::settings::modules::RegionSettings>().getRegionsFromCmdLine();
- }
- else{
- //if we reach this point we can assume that the region is given as a file.
- STORM_LOG_THROW(storm::utility::fileExistsAndIsReadable(storm::settings::getModule<storm::settings::modules::RegionSettings>().getRegionFilePath()), storm::exceptions::InvalidSettingsException, "The path to the file in which the regions are specified is not valid.");
- storm::parser::MappedFile mf(storm::settings::getModule<storm::settings::modules::RegionSettings>().getRegionFilePath().c_str());
- regionsString = std::string(mf.getData(),mf.getDataSize());
- }
- return parseMultipleRegions(regionsString);
- }
+ std::string regionsString;
+ if(storm::settings::getModule<storm::settings::modules::RegionSettings>().isRegionsSet()){
+ regionsString = storm::settings::getModule<storm::settings::modules::RegionSettings>().getRegionsFromCmdLine();
+ }
+ else{
+ //if we reach this point we can assume that the region is given as a file.
+ STORM_LOG_THROW(storm::utility::fileExistsAndIsReadable(storm::settings::getModule<storm::settings::modules::RegionSettings>().getRegionFilePath()), storm::exceptions::InvalidSettingsException, "The path to the file in which the regions are specified is not valid.");
+ storm::parser::MappedFile mf(storm::settings::getModule<storm::settings::modules::RegionSettings>().getRegionFilePath().c_str());
+ regionsString = std::string(mf.getData(),mf.getDataSize());
+ }
+ return parseMultipleRegions(regionsString);
+ }
#ifdef STORM_HAVE_CARL
template class ParameterRegion<storm::RationalFunction>;
#endif
- }
}
}
diff --git a/src/storm/storage/ParameterRegion.h b/src/storm/storage/ParameterRegion.h
index 2c07abbdb..246ad5971 100644
--- a/src/storm/storage/ParameterRegion.h
+++ b/src/storm/storage/ParameterRegion.h
@@ -5,109 +5,98 @@
#include "storm/utility/parametric.h"
namespace storm {
- namespace modelchecker{
- namespace parametric {
- template<typename ParametricType>
- class ParameterRegion{
- public:
- typedef typename storm::utility::parametric::VariableType<ParametricType>::type VariableType;
- typedef typename storm::utility::parametric::CoefficientType<ParametricType>::type CoefficientType;
- typedef typename storm::utility::parametric::Valuation<ParametricType> Valuation;
-
- ParameterRegion(Valuation const& lowerBoundaries, Valuation const& upperBoundaries);
- ParameterRegion(Valuation&& lowerBoundaries, Valuation&& upperBoundaries);
- ParameterRegion(ParameterRegion const& other) = default;
- ParameterRegion(ParameterRegion&& other) = default;
+ namespace storage {
+ template<typename ParametricType>
+ class ParameterRegion{
+ public:
+ typedef typename storm::utility::parametric::VariableType<ParametricType>::type VariableType;
+ typedef typename storm::utility::parametric::CoefficientType<ParametricType>::type CoefficientType;
+ typedef typename storm::utility::parametric::Valuation<ParametricType> Valuation;
+
+ ParameterRegion(Valuation const& lowerBoundaries, Valuation const& upperBoundaries);
+ ParameterRegion(Valuation&& lowerBoundaries, Valuation&& upperBoundaries);
+ ParameterRegion(ParameterRegion const& other) = default;
+ ParameterRegion(ParameterRegion&& other) = default;
+
+ virtual ~ParameterRegion() = default;
+
+ std::set<VariableType> const& getVariables() const;
+ CoefficientType const& getLowerBoundary(VariableType const& variable) const;
+ CoefficientType const& getUpperBoundary(VariableType const& variable) const;
+ Valuation const& getLowerBoundaries() const;
+ Valuation const& getUpperBoundaries() const;
+
+ /*!
+ * Returns a vector of all possible combinations of lower and upper bounds of the given variables.
+ * The first entry of the returned vector will map every variable to its lower bound
+ * The second entry will map every variable to its lower bound, except the first one (i.e. *getVariables.begin())
+ * ...
+ * The last entry will map every variable to its upper bound
+ *
+ * If the given set of variables is empty, the returned vector will contain an empty map
+ */
+ std::vector<Valuation> getVerticesOfRegion(std::set<VariableType> const& consideredVariables) const;
+
+ /*!
+ * Returns some point that lies within this region
+ */
+ Valuation getSomePoint() const;
+
+ /*!
+ * Returns the center point of this region
+ */
+ Valuation getCenterPoint() const;
- virtual ~ParameterRegion() = default;
-
- std::set<VariableType> const& getVariables() const;
- CoefficientType const& getLowerBoundary(VariableType const& variable) const;
- CoefficientType const& getUpperBoundary(VariableType const& variable) const;
- Valuation const& getLowerBoundaries() const;
- Valuation const& getUpperBoundaries() const;
-
- /*!
- * Returns a vector of all possible combinations of lower and upper bounds of the given variables.
- * The first entry of the returned vector will map every variable to its lower bound
- * The second entry will map every variable to its lower bound, except the first one (i.e. *getVariables.begin())
- * ...
- * The last entry will map every variable to its upper bound
- *
- * If the given set of variables is empty, the returned vector will contain an empty map
- */
- std::vector<Valuation> getVerticesOfRegion(std::set<VariableType> const& consideredVariables) const;
-
- /*!
- * Returns some point that lies within this region
- */
- Valuation getSomePoint() const;
-
- /*!
- * Returns the center point of this region
- */
- Valuation getCenterPoint() const;
-
- /*!
- * Returns the area of this region
- */
- CoefficientType area() const;
-
- /*!
- * Splits the region at the given point and inserts the resulting subregions at the end of the given vector.
- * It is assumed that the point lies within this region.
- * Subregions with area()==0 are not inserted in the vector.
- */
- void split(Valuation const& splittingPoint, std::vector<ParameterRegion<ParametricType>>& regionVector) const;
-
- //returns the region as string in the format 0.3<=p<=0.4,0.2<=q<=0.5;
- std::string toString(bool boundariesAsDouble = false) const;
-
- /*
- * Can be used to parse a single parameter with its boundaries from a string of the form "0.3<=p<=0.5".
- * The numbers are parsed as doubles and then converted to SparseDtmcRegionModelChecker::CoefficientType.
- * The results will be inserted in the given maps
- *
- */
- static void parseParameterBoundaries(
- Valuation& lowerBoundaries,
- Valuation& upperBoundaries,
- std::string const& parameterBoundariesString
- );
-
- /*
- * Can be used to parse a single region from a string of the form "0.3<=p<=0.5,0.4<=q<=0.7".
- * The numbers are parsed as doubles and then converted to SparseDtmcRegionModelChecker::CoefficientType.
- *
- */
- static ParameterRegion parseRegion(
- std::string const& regionString
- );
-
- /*
- * Can be used to parse a vector of region from a string of the form "0.3<=p<=0.5,0.4<=q<=0.7;0.1<=p<=0.3,0.2<=q<=0.4".
- * The numbers are parsed as doubles and then converted to SparseDtmcRegionModelChecker::CoefficientType.
- *
- */
- static std::vector<ParameterRegion> parseMultipleRegions(
- std::string const& regionsString
- );
-
-
- /*
- * Retrieves the regions that are specified in the settings.
- */
- static std::vector<ParameterRegion> getRegionsFromSettings();
-
- private:
-
- void init();
-
- Valuation lowerBoundaries;
- Valuation upperBoundaries;
- std::set<VariableType> variables;
- };
- }
+ /*!
+ * Returns the area of this region
+ */
+ CoefficientType area() const;
+
+ /*!
+ * Splits the region at the given point and inserts the resulting subregions at the end of the given vector.
+ * It is assumed that the point lies within this region.
+ * Subregions with area()==0 are not inserted in the vector.
+ */
+ void split(Valuation const& splittingPoint, std::vector<ParameterRegion<ParametricType>>& regionVector) const;
+
+ //returns the region as string in the format 0.3<=p<=0.4,0.2<=q<=0.5;
+ std::string toString(bool boundariesAsDouble = false) const;
+
+ /*
+ * Can be used to parse a single parameter with its boundaries from a string of the form "0.3<=p<=0.5".
+ * The numbers are parsed as doubles and then converted to SparseDtmcRegionModelChecker::CoefficientType.
+ * The results will be inserted in the given maps
+ *
+ */
+ static void parseParameterBoundaries( Valuation& lowerBoundaries, Valuation& upperBoundaries, std::string const& parameterBoundariesString);
+
+ /*
+ * Can be used to parse a single region from a string of the form "0.3<=p<=0.5,0.4<=q<=0.7".
+ * The numbers are parsed as doubles and then converted to SparseDtmcRegionModelChecker::CoefficientType.
+ *
+ */
+ static ParameterRegion parseRegion(std::string const& regionString);
+
+ /*
+ * Can be used to parse a vector of region from a string of the form "0.3<=p<=0.5,0.4<=q<=0.7;0.1<=p<=0.3,0.2<=q<=0.4".
+ * The numbers are parsed as doubles and then converted to SparseDtmcRegionModelChecker::CoefficientType.
+ *
+ */
+ static std::vector<ParameterRegion> parseMultipleRegions(std::string const& regionsString);
+
+ /*
+ * Retrieves the regions that are specified in the settings.
+ */
+ static std::vector<ParameterRegion> getRegionsFromSettings();
+
+ private:
+
+ void init();
+
+ Valuation lowerBoundaries;
+ Valuation upperBoundaries;
+ std::set<VariableType> variables;
+ };
}
}
diff --git a/src/storm/transformer/ParameterLifter.cpp b/src/storm/transformer/ParameterLifter.cpp
index 8d33919f8..21e949ce2 100644
--- a/src/storm/transformer/ParameterLifter.cpp
+++ b/src/storm/transformer/ParameterLifter.cpp
@@ -124,7 +124,7 @@ namespace storm {
}
template<typename ParametricType, typename ConstantType>
- void ParameterLifter<ParametricType, ConstantType>::specifyRegion(storm::modelchecker::parametric::ParameterRegion<ParametricType> const& region, storm::solver::OptimizationDirection const& dirForParameters) {
+ void ParameterLifter<ParametricType, ConstantType>::specifyRegion(storm::storage::ParameterRegion<ParametricType> const& region, storm::solver::OptimizationDirection const& dirForParameters) {
// write the evaluation result of each function,evaluation pair into the placeholders
functionValuationCollector.evaluateCollectedFunctions(region, dirForParameters);
@@ -223,7 +223,7 @@ namespace storm {
}
template<typename ParametricType, typename ConstantType>
- std::vector<storm::utility::parametric::Valuation<ParametricType>> ParameterLifter<ParametricType, ConstantType>::AbstractValuation::getConcreteValuations(storm::modelchecker::parametric::ParameterRegion<ParametricType> const& region) const {
+ std::vector<storm::utility::parametric::Valuation<ParametricType>> ParameterLifter<ParametricType, ConstantType>::AbstractValuation::getConcreteValuations(storm::storage::ParameterRegion<ParametricType> const& region) const {
auto result = region.getVerticesOfRegion(unspecifiedPars);
for(auto& valuation : result) {
for (auto const& lowerPar : lowerPars) {
@@ -253,7 +253,7 @@ namespace storm {
}
template<typename ParametricType, typename ConstantType>
- void ParameterLifter<ParametricType, ConstantType>::FunctionValuationCollector::evaluateCollectedFunctions(storm::modelchecker::parametric::ParameterRegion<ParametricType> const& region, storm::solver::OptimizationDirection const& dirForUnspecifiedParameters) {
+ void ParameterLifter<ParametricType, ConstantType>::FunctionValuationCollector::evaluateCollectedFunctions(storm::storage::ParameterRegion<ParametricType> const& region, storm::solver::OptimizationDirection const& dirForUnspecifiedParameters) {
for (auto& collectedFunctionValuationPlaceholder : collectedFunctions) {
ParametricType const& function = collectedFunctionValuationPlaceholder.first.first;
AbstractValuation const& abstrValuation = collectedFunctionValuationPlaceholder.first.second;
diff --git a/src/storm/transformer/ParameterLifter.h b/src/storm/transformer/ParameterLifter.h
index 580d83204..e29e648a6 100644
--- a/src/storm/transformer/ParameterLifter.h
+++ b/src/storm/transformer/ParameterLifter.h
@@ -41,7 +41,7 @@ namespace storm {
*/
ParameterLifter(storm::storage::SparseMatrix<ParametricType> const& pMatrix, std::vector<ParametricType> const& pVector, storm::storage::BitVector const& selectedRows, storm::storage::BitVector const& selectedColumns);
- void specifyRegion(storm::modelchecker::parametric::ParameterRegion<ParametricType> const& region, storm::solver::OptimizationDirection const& dirForParameters);
+ void specifyRegion(storm::storage::ParameterRegion<ParametricType> const& region, storm::solver::OptimizationDirection const& dirForParameters);
// Returns the resulting matrix. Should only be called AFTER specifying a region
storm::storage::SparseMatrix<ConstantType> const& getMatrix() const;
@@ -77,7 +77,7 @@ namespace storm {
* Returns the concrete valuation(s) (w.r.t. the provided region) represented by this abstract valuation.
* Note that an abstract valuation represents 2^(#unspecified parameters) many concrete valuations.
*/
- std::vector<storm::utility::parametric::Valuation<ParametricType>> getConcreteValuations(storm::modelchecker::parametric::ParameterRegion<ParametricType> const& region) const;
+ std::vector<storm::utility::parametric::Valuation<ParametricType>> getConcreteValuations(storm::storage::ParameterRegion<ParametricType> const& region) const;
private:
std::set<VariableType> lowerPars, upperPars, unspecifiedPars;
@@ -97,7 +97,7 @@ namespace storm {
*/
ConstantType& add(ParametricType const& function, AbstractValuation const& valuation);
- void evaluateCollectedFunctions(storm::modelchecker::parametric::ParameterRegion<ParametricType> const& region, storm::solver::OptimizationDirection const& dirForUnspecifiedParameters);
+ void evaluateCollectedFunctions(storm::storage::ParameterRegion<ParametricType> const& region, storm::solver::OptimizationDirection const& dirForUnspecifiedParameters);
private:
// Stores a function and a valuation. The valuation is stored as an index of the collectedValuations-vector.