fixes for step bounded properties

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

src/storm/modelchecker/parametric/SparseDtmcParameterLiftingModelChecker.cpp

@@ -27,7 +27,7 @@ namespace storm {
             
             template <typename SparseModelType, typename ConstantType>
             bool SparseDtmcParameterLiftingModelChecker<SparseModelType, ConstantType>::canHandle(CheckTask<storm::logic::Formula, typename SparseModelType::ValueType> 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 <typename SparseModelType, typename ConstantType>

src/storm/modelchecker/parametric/SparseMdpParameterLiftingModelChecker.cpp

@@ -29,7 +29,7 @@ namespace storm {
     
             template <typename SparseModelType, typename ConstantType>
             bool SparseMdpParameterLiftingModelChecker<SparseModelType, ConstantType>::canHandle(CheckTask<storm::logic::Formula, typename SparseModelType::ValueType> 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 <typename SparseModelType, typename ConstantType>
@@ -190,7 +190,8 @@ namespace storm {
                 std::vector<typename SparseModelType::ValueType> b = rewardModel.getTotalRewardVector(this->parametricModel.getTransitionMatrix());
                     
                 parameterLifter = std::make_unique<storm::transformer::ParameterLifter<typename SparseModelType::ValueType, ConstantType>>(this->parametricModel.getTransitionMatrix(), b, maybeStates, maybeStates);
-                
+                computePlayer1Matrix();
+
                 applyPreviousResultAsHint = false;
                 
                 // We only know a lower bound for the result