Browse Source

refactored canHandle check in rpatl model checker

According to/stolen from 6c0cbe622
tempestpy_adaptions
Stefan Pranger 4 years ago
parent
commit
d1f99e0548
  1. 6
      src/storm/modelchecker/rpatl/SparseSmgRpatlModelChecker.cpp

6
src/storm/modelchecker/rpatl/SparseSmgRpatlModelChecker.cpp

@ -41,11 +41,7 @@ namespace storm {
template<typename SparseSmgModelType> template<typename SparseSmgModelType>
bool SparseSmgRpatlModelChecker<SparseSmgModelType>::canHandleStatic(CheckTask<storm::logic::Formula, ValueType> const& checkTask, bool* requiresSingleInitialState) { bool SparseSmgRpatlModelChecker<SparseSmgModelType>::canHandleStatic(CheckTask<storm::logic::Formula, ValueType> const& checkTask, bool* requiresSingleInitialState) {
storm::logic::Formula const& formula = checkTask.getFormula(); 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> template<typename SparseSmgModelType>

Loading…
Cancel
Save