diff --git a/src/modelchecker/prctl/helper/SparseDtmcPrctlHelper.cpp b/src/modelchecker/prctl/helper/SparseDtmcPrctlHelper.cpp index 9e1b6ef14..98cbcf2ea 100644 --- a/src/modelchecker/prctl/helper/SparseDtmcPrctlHelper.cpp +++ b/src/modelchecker/prctl/helper/SparseDtmcPrctlHelper.cpp @@ -367,6 +367,7 @@ namespace storm { // Now compute reachability probabilities in the transformed model. storm::storage::SparseMatrix const& newTransitionMatrix = transformedModel.transitionMatrix.get(); std::vector conditionalProbabilities = computeUntilProbabilities(newTransitionMatrix, newTransitionMatrix.transpose(), storm::storage::BitVector(newTransitionMatrix.getRowCount(), true), transformedModel.targetStates.get(), qualitative, linearEquationSolverFactory); + storm::utility::vector::setVectorValues(result, transformedModel.beforeStates, conditionalProbabilities); } } diff --git a/src/modelchecker/prctl/helper/SparseDtmcPrctlHelper.h b/src/modelchecker/prctl/helper/SparseDtmcPrctlHelper.h index 637c30cb5..0be762298 100644 --- a/src/modelchecker/prctl/helper/SparseDtmcPrctlHelper.h +++ b/src/modelchecker/prctl/helper/SparseDtmcPrctlHelper.h @@ -45,6 +45,10 @@ namespace storm { static std::vector computeReachabilityRewards(storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, std::function(uint_fast64_t, storm::storage::SparseMatrix const&, storm::storage::BitVector const&)> const& totalStateRewardVectorGetter, storm::storage::BitVector const& targetStates, bool qualitative, storm::utility::solver::LinearEquationSolverFactory const& linearEquationSolverFactory); struct BaierTransformedModel { + BaierTransformedModel() : noTargetStates(false) { + // Intentionally left empty. + } + storm::storage::BitVector beforeStates; boost::optional> transitionMatrix; boost::optional targetStates; diff --git a/src/utility/graph.cpp b/src/utility/graph.cpp index de920ad21..bd10cfd03 100644 --- a/src/utility/graph.cpp +++ b/src/utility/graph.cpp @@ -310,8 +310,46 @@ namespace storm { } template - storm::storage::PartialScheduler computeSchedulerProbGreater0E(storm::storage::BitVector const& probGreater0EStates, storm::storage::SparseMatrix const& transitionMatrix) { - return computeSchedulerWithOneSuccessorInStates(probGreater0EStates, transitionMatrix); + storm::storage::PartialScheduler computeSchedulerProbGreater0E(storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, boost::optional const& rowFilter) { + //Perform backwards DFS from psiStates and find a valid choice for each visited state. + + storm::storage::PartialScheduler result; + std::vector stack; + storm::storage::BitVector currentStates(psiStates); //the states that are either psiStates or for which we have found a valid choice. + stack.insert(stack.end(), currentStates.begin(), currentStates.end()); + uint_fast64_t currentState = 0; + + while (!stack.empty()) { + currentState = stack.back(); + stack.pop_back(); + + for (typename storm::storage::SparseMatrix::const_iterator predecessorEntryIt = backwardTransitions.begin(currentState), predecessorEntryIte = backwardTransitions.end(currentState); predecessorEntryIt != predecessorEntryIte; ++predecessorEntryIt) { + uint_fast64_t const& predecessor = predecessorEntryIt->getColumn(); + if (phiStates.get(predecessor) && !currentStates.get(predecessor)) { + //The predecessor is a probGreater0E state that has not been considered yet. Let's find the right choice that leads to a state in currentStates. + bool foundValidChoice = false; + for (uint_fast64_t row = transitionMatrix.getRowGroupIndices()[predecessor]; row < transitionMatrix.getRowGroupIndices()[predecessor + 1]; ++row) { + if(rowFilter && !rowFilter->get(row)){ + continue; + } + for (typename storm::storage::SparseMatrix::const_iterator successorEntryIt = transitionMatrix.begin(row), successorEntryIte = transitionMatrix.end(row); successorEntryIt != successorEntryIte; ++successorEntryIt) { + if(currentStates.get(successorEntryIt->getColumn())){ + foundValidChoice = true; + break; + } + } + if(foundValidChoice){ + result.setChoice(predecessor, row - transitionMatrix.getRowGroupIndices()[predecessor]); + currentStates.set(predecessor, true); + stack.push_back(predecessor); + break; + } + } + STORM_LOG_INFO_COND(foundValidChoice, "Could not find a valid choice for ProbGreater0E state " << predecessor << "."); + } + } + } + return result; } template @@ -972,7 +1010,7 @@ namespace storm { - template storm::storage::PartialScheduler computeSchedulerProbGreater0E(storm::storage::BitVector const& probGreater0EStates, storm::storage::SparseMatrix const& transitionMatrix); + template storm::storage::PartialScheduler computeSchedulerProbGreater0E(storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, boost::optional const& rowFilter); template storm::storage::PartialScheduler computeSchedulerProb0E(storm::storage::BitVector const& prob0EStates, storm::storage::SparseMatrix const& transitionMatrix); diff --git a/src/utility/graph.h b/src/utility/graph.h index 913a8aaab..54e541ac9 100644 --- a/src/utility/graph.h +++ b/src/utility/graph.h @@ -234,13 +234,20 @@ namespace storm { storm::storage::PartialScheduler computeSchedulerWithOneSuccessorInStates(storm::storage::BitVector const& states, storm::storage::SparseMatrix const& transitionMatrix); /*! - * Computes a scheduler for the given states that have a scheduler that has a probability greater 0. + * Computes a scheduler for the ProbGreater0E-States such that in the induced system the given psiStates are reachable via phiStates * - * @param probGreater0EStates The states that have a scheduler achieving a probablity greater 0. * @param transitionMatrix The transition matrix of the system. + * @param backwardTransitions The reversed transition relation. + * @param phiStates The set of states satisfying phi. + * @param psiStates The set of states satisfying psi. + * @param rowFilter If given, the returned scheduler will only pick choices such that rowFilter is true for the corresponding matrixrow. + * @return A Scheduler for the ProbGreater0E-States + * + * @note No choice is defined for ProbGreater0E-States if all the probGreater0-choices violate the row filter. + * This also holds for states that only reach psi via such states. */ template - storm::storage::PartialScheduler computeSchedulerProbGreater0E(storm::storage::BitVector const& probGreater0EStates, storm::storage::SparseMatrix const& transitionMatrix); + storm::storage::PartialScheduler computeSchedulerProbGreater0E(storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, boost::optional const& rowFilter = boost::none); /*! * Computes a scheduler for the given states that have a scheduler that has a probability 0. @@ -252,10 +259,14 @@ namespace storm { storm::storage::PartialScheduler computeSchedulerProb0E(storm::storage::BitVector const& prob0EStates, storm::storage::SparseMatrix const& transitionMatrix); /*! - * Computes a scheduler for the given states that have a scheduler that has a probability 0. + * Computes a scheduler for the given prob1EStates such that in the induced system the given psiStates are reached with probability 1. * * @param prob1EStates The states that have a scheduler achieving probablity 1. * @param transitionMatrix The transition matrix of the system. + * @param backwardTransitions The reversed transition relation. + * @param phiStates The set of states satisfying phi. + * @param psiStates The set of states satisfying psi. + * @return A scheduler for the Prob1E-States */ template storm::storage::PartialScheduler computeSchedulerProb1E(storm::storage::BitVector const& prob1EStates, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates); diff --git a/test/functional/modelchecker/GmmxxMdpPrctlModelCheckerTest.cpp b/test/functional/modelchecker/GmmxxMdpPrctlModelCheckerTest.cpp index 93643fd52..22e7d8464 100644 --- a/test/functional/modelchecker/GmmxxMdpPrctlModelCheckerTest.cpp +++ b/test/functional/modelchecker/GmmxxMdpPrctlModelCheckerTest.cpp @@ -240,3 +240,36 @@ TEST(GmmxxMdpPrctlModelCheckerTest, SchedulerGeneration) { EXPECT_EQ(0, scheduler2.getChoice(2)); EXPECT_EQ(0, scheduler2.getChoice(3)); } + +TEST(GmmxxMdpPrctlModelCheckerTest, tiny_rewards) { + storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/modelchecker/tiny_rewards.nm"); + + // A parser that we use for conveniently constructing the formulas. + storm::parser::FormulaParser formulaParser; + + std::shared_ptr> model = storm::builder::ExplicitPrismModelBuilder(program).translate(); + EXPECT_EQ(3ul, model->getNumberOfStates()); + EXPECT_EQ(4ul, model->getNumberOfTransitions()); + + ASSERT_EQ(model->getType(), storm::models::ModelType::Mdp); + + std::shared_ptr> mdp = model->as>(); + + EXPECT_EQ(4ul, mdp->getNumberOfChoices()); + + auto solverFactory = std::make_unique>(storm::solver::EquationSolverTypeSelection::Gmmxx); + solverFactory->setPreferredTechnique(storm::solver::MinMaxTechniqueSelection::ValueIteration); + storm::modelchecker::SparseMdpPrctlModelChecker> checker(*mdp, std::move(solverFactory)); + + std::shared_ptr formula = formulaParser.parseSingleFormulaFromString("Rmin=? [F \"target\"]"); + + storm::modelchecker::CheckTask checkTask(*formula); + + std::unique_ptr result = checker.check(checkTask); + + ASSERT_TRUE(result->isExplicitQuantitativeCheckResult()); + EXPECT_NEAR(1,result->asExplicitQuantitativeCheckResult().getValueVector()[0], storm::settings::nativeEquationSolverSettings().getPrecision()); + EXPECT_NEAR(1,result->asExplicitQuantitativeCheckResult().getValueVector()[1], storm::settings::nativeEquationSolverSettings().getPrecision()); + EXPECT_NEAR(0,result->asExplicitQuantitativeCheckResult().getValueVector()[2], storm::settings::nativeEquationSolverSettings().getPrecision()); + +} diff --git a/test/functional/modelchecker/tiny_rewards.nm b/test/functional/modelchecker/tiny_rewards.nm new file mode 100644 index 000000000..5119f6306 --- /dev/null +++ b/test/functional/modelchecker/tiny_rewards.nm @@ -0,0 +1,17 @@ +mdp + +module mod1 + +s : [0..2] init 0; +[] s=0 -> true; +[] s=0 -> (s'=1); +[] s=1 -> (s'=2); +[] s=2 -> (s'=2); + +endmodule + +rewards + [] s=1 : 1; +endrewards + +label "target" = s=2;