From d1f99e0548ea939f222151e8b2ef7570ceb3419c Mon Sep 17 00:00:00 2001
From: Stefan Pranger <stefan.pranger@student.tugraz.at>
Date: Wed, 20 Jan 2021 10:42:00 +0100
Subject: [PATCH] refactored canHandle check in rpatl model checker
According to/stolen from 6c0cbe622
---
src/storm/modelchecker/rpatl/SparseSmgRpatlModelChecker.cpp | 6 +-----
1 file changed, 1 insertion(+), 5 deletions(-)
diff --git a/src/storm/modelchecker/rpatl/SparseSmgRpatlModelChecker.cpp b/src/storm/modelchecker/rpatl/SparseSmgRpatlModelChecker.cpp
index cedc64ae7..35464513d 100644
--- a/src/storm/modelchecker/rpatl/SparseSmgRpatlModelChecker.cpp
+++ b/src/storm/modelchecker/rpatl/SparseSmgRpatlModelChecker.cpp
@@ -41,11 +41,7 @@ namespace storm {
template<typename SparseSmgModelType>
bool SparseSmgRpatlModelChecker<SparseSmgModelType>::canHandleStatic(CheckTask<storm::logic::Formula, ValueType> const& checkTask, bool* requiresSingleInitialState) {
storm::logic::Formula const& formula = checkTask.getFormula();
- if (formula.isInFragment(storm::logic::rpatl().setGameFormulasAllowed(true).setRewardOperatorsAllowed(true).setLongRunAverageRewardFormulasAllowed(true).setLongRunAverageProbabilitiesAllowed(true).setLongRunAverageOperatorsAllowed(true))) {
- return true;
- } else {
- return false;
- }
+ return formula.isInFragment(storm::logic::rpatl());
}
template<typename SparseSmgModelType>