diff --git a/src/storm/modelchecker/parametric/SparseDtmcParameterLiftingModelChecker.cpp b/src/storm/modelchecker/parametric/SparseDtmcParameterLiftingModelChecker.cpp
index 89010a988..175ffc0fe 100644
--- a/src/storm/modelchecker/parametric/SparseDtmcParameterLiftingModelChecker.cpp
+++ b/src/storm/modelchecker/parametric/SparseDtmcParameterLiftingModelChecker.cpp
@@ -24,9 +24,14 @@ namespace storm {
template <typename SparseModelType, typename ConstantType>
SparseDtmcParameterLiftingModelChecker<SparseModelType, ConstantType>::SparseDtmcParameterLiftingModelChecker(SparseModelType const& parametricModel, std::unique_ptr<storm::solver::MinMaxLinearEquationSolverFactory<ConstantType>>&& solverFactory) : SparseParameterLiftingModelChecker<SparseModelType, ConstantType>(parametricModel), solverFactory(std::move(solverFactory)) {
}
-
+
+ template <typename SparseModelType, typename ConstantType>
+ bool SparseDtmcParameterLiftingModelChecker<SparseModelType, ConstantType>::canHandle(CheckTask<storm::logic::Formula, ConstantType> const& checkTask) const {
+ return checkTask.getFormula().isInFragment(storm::logic::reachability().setReachabilityRewardFormulasAllowed(true).setBoundedUntilFormulasAllowed(true).setCumulativeRewardFormulasAllowed(true));
+ }
+
template <typename SparseModelType, typename ConstantType>
- void SparseDtmcParameterLiftingModelChecker<SparseModelType, ConstantType>::specifyBoundedUntilFormula(CheckTask<logic::BoundedUntilFormula, ConstantType> const& checkTask) {
+ void SparseDtmcParameterLiftingModelChecker<SparseModelType, ConstantType>::specifyBoundedUntilFormula(CheckTask<storm::logic::BoundedUntilFormula, ConstantType> const& checkTask) {
// get the step bound
STORM_LOG_THROW(!checkTask.getFormula().hasLowerBound(), storm::exceptions::NotSupportedException, "Lower step bounds are not supported.");
@@ -68,7 +73,7 @@ namespace storm {
}
template <typename SparseModelType, typename ConstantType>
- void SparseDtmcParameterLiftingModelChecker<SparseModelType, ConstantType>::specifyUntilFormula(CheckTask<logic::UntilFormula, ConstantType> const& checkTask) {
+ void SparseDtmcParameterLiftingModelChecker<SparseModelType, ConstantType>::specifyUntilFormula(CheckTask<storm::logic::UntilFormula, ConstantType> const& checkTask) {
// get the results for the subformulas
storm::modelchecker::SparsePropositionalModelChecker<SparseModelType> propositionalChecker(this->parametricModel);
@@ -98,7 +103,7 @@ namespace storm {
}
template <typename SparseModelType, typename ConstantType>
- void SparseDtmcParameterLiftingModelChecker<SparseModelType, ConstantType>::specifyReachabilityRewardFormula(CheckTask<logic::EventuallyFormula, ConstantType> const& checkTask) {
+ void SparseDtmcParameterLiftingModelChecker<SparseModelType, ConstantType>::specifyReachabilityRewardFormula(CheckTask<storm::logic::EventuallyFormula, ConstantType> const& checkTask) {
// get the results for the subformula
storm::modelchecker::SparsePropositionalModelChecker<SparseModelType> propositionalChecker(this->parametricModel);
@@ -132,7 +137,7 @@ namespace storm {
}
template <typename SparseModelType, typename ConstantType>
- void SparseDtmcParameterLiftingModelChecker<SparseModelType, ConstantType>::specifyCumulativeRewardFormula(CheckTask<logic::CumulativeRewardFormula, ConstantType> const& checkTask) {
+ void SparseDtmcParameterLiftingModelChecker<SparseModelType, ConstantType>::specifyCumulativeRewardFormula(CheckTask<storm::logic::CumulativeRewardFormula, ConstantType> const& checkTask) {
// Obtain the stepBound
stepBound = checkTask.getFormula().getBound().evaluateAsInt();
diff --git a/src/storm/modelchecker/parametric/SparseDtmcParameterLiftingModelChecker.h b/src/storm/modelchecker/parametric/SparseDtmcParameterLiftingModelChecker.h
index 8ad36bd6e..0384e839f 100644
--- a/src/storm/modelchecker/parametric/SparseDtmcParameterLiftingModelChecker.h
+++ b/src/storm/modelchecker/parametric/SparseDtmcParameterLiftingModelChecker.h
@@ -9,6 +9,8 @@
#include "storm/storage/TotalScheduler.h"
#include "storm/solver/MinMaxLinearEquationSolver.h"
#include "storm/transformer/ParameterLifter.h"
+#include "storm/logic/FragmentSpecification.h"
+
namespace storm {
namespace modelchecker {
@@ -20,6 +22,8 @@ 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;
+
protected:
virtual void specifyBoundedUntilFormula(CheckTask<storm::logic::BoundedUntilFormula, ConstantType> const& checkTask) override;
diff --git a/src/storm/modelchecker/parametric/SparseMdpParameterLiftingModelChecker.cpp b/src/storm/modelchecker/parametric/SparseMdpParameterLiftingModelChecker.cpp
index 33dfbadb4..463637d2a 100644
--- a/src/storm/modelchecker/parametric/SparseMdpParameterLiftingModelChecker.cpp
+++ b/src/storm/modelchecker/parametric/SparseMdpParameterLiftingModelChecker.cpp
@@ -9,6 +9,7 @@
#include "storm/utility/vector.h"
#include "storm/utility/graph.h"
#include "storm/solver/GameSolver.h"
+#include "storm/logic/FragmentSpecification.h"
#include "storm/exceptions/InvalidArgumentException.h"
#include "storm/exceptions/InvalidPropertyException.h"
@@ -27,7 +28,12 @@ namespace storm {
}
template <typename SparseModelType, typename ConstantType>
- void SparseMdpParameterLiftingModelChecker<SparseModelType, ConstantType>::specifyBoundedUntilFormula(CheckTask<logic::BoundedUntilFormula, ConstantType> const& checkTask) {
+ bool SparseMdpParameterLiftingModelChecker<SparseModelType, ConstantType>::canHandle(CheckTask<storm::logic::Formula, ConstantType> const& checkTask) const {
+ return checkTask.getFormula().isInFragment(storm::logic::reachability().setReachabilityRewardFormulasAllowed(true).setBoundedUntilFormulasAllowed(true).setCumulativeRewardFormulasAllowed(true));
+ }
+
+ template <typename SparseModelType, typename ConstantType>
+ void SparseMdpParameterLiftingModelChecker<SparseModelType, ConstantType>::specifyBoundedUntilFormula(CheckTask<storm::logic::BoundedUntilFormula, ConstantType> const& checkTask) {
// get the step bound
STORM_LOG_THROW(!checkTask.getFormula().hasLowerBound(), storm::exceptions::NotSupportedException, "Lower step bounds are not supported.");
@@ -74,7 +80,7 @@ namespace storm {
}
template <typename SparseModelType, typename ConstantType>
- void SparseMdpParameterLiftingModelChecker<SparseModelType, ConstantType>::specifyUntilFormula(CheckTask<logic::UntilFormula, ConstantType> const& checkTask) {
+ void SparseMdpParameterLiftingModelChecker<SparseModelType, ConstantType>::specifyUntilFormula(CheckTask<storm::logic::UntilFormula, ConstantType> const& checkTask) {
// get the results for the subformulas
storm::modelchecker::SparsePropositionalModelChecker<SparseModelType> propositionalChecker(this->parametricModel);
@@ -111,7 +117,7 @@ namespace storm {
}
template <typename SparseModelType, typename ConstantType>
- void SparseMdpParameterLiftingModelChecker<SparseModelType, ConstantType>::specifyReachabilityRewardFormula(CheckTask<logic::EventuallyFormula, ConstantType> const& checkTask) {
+ void SparseMdpParameterLiftingModelChecker<SparseModelType, ConstantType>::specifyReachabilityRewardFormula(CheckTask<storm::logic::EventuallyFormula, ConstantType> const& checkTask) {
// get the results for the subformula
storm::modelchecker::SparsePropositionalModelChecker<SparseModelType> propositionalChecker(this->parametricModel);
@@ -164,7 +170,7 @@ namespace storm {
}
template <typename SparseModelType, typename ConstantType>
- void SparseMdpParameterLiftingModelChecker<SparseModelType, ConstantType>::specifyCumulativeRewardFormula(CheckTask<logic::CumulativeRewardFormula, ConstantType> const& checkTask) {
+ void SparseMdpParameterLiftingModelChecker<SparseModelType, ConstantType>::specifyCumulativeRewardFormula(CheckTask<storm::logic::CumulativeRewardFormula, ConstantType> const& checkTask) {
// Obtain the stepBound
stepBound = checkTask.getFormula().getBound().evaluateAsInt();
diff --git a/src/storm/modelchecker/parametric/SparseMdpParameterLiftingModelChecker.h b/src/storm/modelchecker/parametric/SparseMdpParameterLiftingModelChecker.h
index b2bb4d893..a1e73a78b 100644
--- a/src/storm/modelchecker/parametric/SparseMdpParameterLiftingModelChecker.h
+++ b/src/storm/modelchecker/parametric/SparseMdpParameterLiftingModelChecker.h
@@ -22,6 +22,8 @@ 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;
+
protected:
virtual void specifyBoundedUntilFormula(CheckTask<storm::logic::BoundedUntilFormula, ConstantType> const& checkTask) override;
diff --git a/src/storm/modelchecker/parametric/SparseParameterLiftingModelChecker.h b/src/storm/modelchecker/parametric/SparseParameterLiftingModelChecker.h
index 5c4a059af..f93ab84e6 100644
--- a/src/storm/modelchecker/parametric/SparseParameterLiftingModelChecker.h
+++ b/src/storm/modelchecker/parametric/SparseParameterLiftingModelChecker.h
@@ -22,11 +22,14 @@ namespace storm {
public:
SparseParameterLiftingModelChecker(SparseModelType const& parametricModel);
+ virtual bool canHandle(CheckTask<storm::logic::Formula, ConstantType> const& checkTask) const = 0;
+
void specifyFormula(CheckTask<storm::logic::Formula, typename SparseModelType::ValueType> const& checkTask);
/*!
* Checks the specified formula on the given region by applying parameter lifting (Parameter choices are lifted to nondeterministic choices)
- *
+ * This yields a (sound) approximative model checking result.
+
* @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.
*/