From b10dcce21ab69fc30e7d9b3c510f31a805f00371 Mon Sep 17 00:00:00 2001
From: TimQu <tim.quatmann@cs.rwth-aachen.de>
Date: Wed, 15 Nov 2017 19:28:00 +0100
Subject: [PATCH] fixed 'canHandle' method in pla checker

---
 .../region/SparseDtmcParameterLiftingModelChecker.cpp           | 2 +-
 .../region/SparseMdpParameterLiftingModelChecker.cpp            | 2 +-
 2 files changed, 2 insertions(+), 2 deletions(-)

diff --git a/src/storm-pars/modelchecker/region/SparseDtmcParameterLiftingModelChecker.cpp b/src/storm-pars/modelchecker/region/SparseDtmcParameterLiftingModelChecker.cpp
index e76b2b3af..374f6c3b2 100644
--- a/src/storm-pars/modelchecker/region/SparseDtmcParameterLiftingModelChecker.cpp
+++ b/src/storm-pars/modelchecker/region/SparseDtmcParameterLiftingModelChecker.cpp
@@ -42,7 +42,7 @@ namespace storm {
             result &= parametricModel->supportsParameters();
             auto dtmc = parametricModel->template as<SparseModelType>();
             result &= static_cast<bool>(dtmc);
-            result &= checkTask.getFormula().isInFragment(storm::logic::reachability().setRewardOperatorsAllowed(true).setReachabilityRewardFormulasAllowed(true).setBoundedUntilFormulasAllowed(true).setCumulativeRewardFormulasAllowed(true).setStepBoundedCumulativeRewardFormulasAllowed(true).setTimeBoundedUntilFormulasAllowed(true).setStepBoundedUntilFormulasAllowed(true).setTimeBoundedUntilFormulasAllowed(true));
+            result &= checkTask.getFormula().isInFragment(storm::logic::reachability().setRewardOperatorsAllowed(true).setReachabilityRewardFormulasAllowed(true).setBoundedUntilFormulasAllowed(true).setCumulativeRewardFormulasAllowed(true).setStepBoundedCumulativeRewardFormulasAllowed(true).setTimeBoundedCumulativeRewardFormulasAllowed(true).setTimeBoundedUntilFormulasAllowed(true).setStepBoundedUntilFormulasAllowed(true).setTimeBoundedUntilFormulasAllowed(true));
             return result;
         }
         
diff --git a/src/storm-pars/modelchecker/region/SparseMdpParameterLiftingModelChecker.cpp b/src/storm-pars/modelchecker/region/SparseMdpParameterLiftingModelChecker.cpp
index c21ef3d5b..95d79bd1f 100644
--- a/src/storm-pars/modelchecker/region/SparseMdpParameterLiftingModelChecker.cpp
+++ b/src/storm-pars/modelchecker/region/SparseMdpParameterLiftingModelChecker.cpp
@@ -40,7 +40,7 @@ namespace storm {
             result &= parametricModel->supportsParameters();
             auto mdp = parametricModel->template as<SparseModelType>();
             result &= static_cast<bool>(mdp);
-            result &= checkTask.getFormula().isInFragment(storm::logic::reachability().setRewardOperatorsAllowed(true).setReachabilityRewardFormulasAllowed(true).setBoundedUntilFormulasAllowed(true).setCumulativeRewardFormulasAllowed(true).setStepBoundedUntilFormulasAllowed(true).setTimeBoundedUntilFormulasAllowed(true));
+            result &= checkTask.getFormula().isInFragment(storm::logic::reachability().setRewardOperatorsAllowed(true).setReachabilityRewardFormulasAllowed(true).setBoundedUntilFormulasAllowed(true).setCumulativeRewardFormulasAllowed(true).setStepBoundedUntilFormulasAllowed(true).setTimeBoundedCumulativeRewardFormulasAllowed(true).setStepBoundedCumulativeRewardFormulasAllowed(true).setTimeBoundedUntilFormulasAllowed(true));
             return result;
         }