Browse Source

fixed 'canHandle' method in pla checker

tempestpy_adaptions
TimQu 7 years ago
parent
commit
b10dcce21a
  1. 2
      src/storm-pars/modelchecker/region/SparseDtmcParameterLiftingModelChecker.cpp
  2. 2
      src/storm-pars/modelchecker/region/SparseMdpParameterLiftingModelChecker.cpp

2
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;
}

2
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;
}

Loading…
Cancel
Save