diff --git a/src/storm/modelchecker/parametric/SparseDtmcInstantiationModelChecker.cpp b/src/storm/modelchecker/parametric/SparseDtmcInstantiationModelChecker.cpp index 1370f48cc..830113f77 100644 --- a/src/storm/modelchecker/parametric/SparseDtmcInstantiationModelChecker.cpp +++ b/src/storm/modelchecker/parametric/SparseDtmcInstantiationModelChecker.cpp @@ -26,7 +26,6 @@ namespace storm { if(!this->currentCheckTask->isQualitativeSet() && this->currentCheckTask->getFormula().isInFragment(storm::logic::reachability().setRewardOperatorsAllowed(true).setReachabilityRewardFormulasAllowed(true))) { return checkWithHint(modelChecker); } else { - STORM_LOG_WARN("Checking without hint"); // todo:remove this warning return modelChecker.check(*this->currentCheckTask); } } diff --git a/src/storm/modelchecker/parametric/SparseDtmcParameterLiftingModelChecker.cpp b/src/storm/modelchecker/parametric/SparseDtmcParameterLiftingModelChecker.cpp index 2833a5142..b98774d2b 100644 --- a/src/storm/modelchecker/parametric/SparseDtmcParameterLiftingModelChecker.cpp +++ b/src/storm/modelchecker/parametric/SparseDtmcParameterLiftingModelChecker.cpp @@ -27,7 +27,7 @@ namespace storm { template bool SparseDtmcParameterLiftingModelChecker::canHandle(CheckTask const& checkTask) const { - return checkTask.getFormula().isInFragment(storm::logic::reachability().setRewardOperatorsAllowed(true).setReachabilityRewardFormulasAllowed(true).setBoundedUntilFormulasAllowed(true).setCumulativeRewardFormulasAllowed(true)); + return checkTask.getFormula().isInFragment(storm::logic::reachability().setRewardOperatorsAllowed(true).setReachabilityRewardFormulasAllowed(true).setBoundedUntilFormulasAllowed(true).setCumulativeRewardFormulasAllowed(true).setStepBoundedUntilFormulasAllowed(true)); } template diff --git a/src/storm/modelchecker/parametric/SparseMdpParameterLiftingModelChecker.cpp b/src/storm/modelchecker/parametric/SparseMdpParameterLiftingModelChecker.cpp index e2130cc2f..5b8c0457d 100644 --- a/src/storm/modelchecker/parametric/SparseMdpParameterLiftingModelChecker.cpp +++ b/src/storm/modelchecker/parametric/SparseMdpParameterLiftingModelChecker.cpp @@ -29,7 +29,7 @@ namespace storm { template bool SparseMdpParameterLiftingModelChecker::canHandle(CheckTask const& checkTask) const { - return checkTask.getFormula().isInFragment(storm::logic::reachability().setRewardOperatorsAllowed(true).setReachabilityRewardFormulasAllowed(true).setBoundedUntilFormulasAllowed(true).setCumulativeRewardFormulasAllowed(true)); + return checkTask.getFormula().isInFragment(storm::logic::reachability().setRewardOperatorsAllowed(true).setReachabilityRewardFormulasAllowed(true).setBoundedUntilFormulasAllowed(true).setStepBoundedUntilFormulasAllowed(true).setCumulativeRewardFormulasAllowed(true)); } template @@ -190,7 +190,8 @@ namespace storm { std::vector b = rewardModel.getTotalRewardVector(this->parametricModel.getTransitionMatrix()); parameterLifter = std::make_unique>(this->parametricModel.getTransitionMatrix(), b, maybeStates, maybeStates); - + computePlayer1Matrix(); + applyPreviousResultAsHint = false; // We only know a lower bound for the result