added a canHandle method to the parameter lifting model checker

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();

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;

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();

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;

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.
                  */