From dae55eeb29291e54312636f62e97c16a207747e0 Mon Sep 17 00:00:00 2001 From: dehnert Date: Wed, 16 Mar 2016 16:12:22 +0100 Subject: [PATCH 1/3] fixed some bugs and enabled markov automaton model checking from cli Former-commit-id: 91b689d81744ca75d6c7fb374ad2ef3aedbe4ce4 --- .../SparseMarkovAutomatonCslModelChecker.cpp | 12 ++++++- .../helper/SparseMarkovAutomatonCslHelper.cpp | 3 +- src/models/sparse/MarkovAutomaton.cpp | 32 ++++++++++++------- src/models/sparse/MarkovAutomaton.h | 5 +++ .../MarkovAutomatonSparseTransitionParser.cpp | 26 +++++++++++++++ src/utility/storm.h | 11 +++++++ 6 files changed, 75 insertions(+), 14 deletions(-) diff --git a/src/modelchecker/csl/SparseMarkovAutomatonCslModelChecker.cpp b/src/modelchecker/csl/SparseMarkovAutomatonCslModelChecker.cpp index 77535cdbe..7cd7e12ac 100644 --- a/src/modelchecker/csl/SparseMarkovAutomatonCslModelChecker.cpp +++ b/src/modelchecker/csl/SparseMarkovAutomatonCslModelChecker.cpp @@ -46,7 +46,17 @@ namespace storm { std::unique_ptr rightResultPointer = this->check(pathFormula.getRightSubformula()); ExplicitQualitativeCheckResult const& rightResult = rightResultPointer->asExplicitQualitativeCheckResult(); - std::vector result = storm::modelchecker::helper::SparseMarkovAutomatonCslHelper::computeBoundedUntilProbabilities(checkTask.getOptimizationDirection(), this->getModel().getTransitionMatrix(), this->getModel().getExitRates(), this->getModel().getMarkovianStates(), rightResult.getTruthValuesVector(), pathFormula.getIntervalBounds(), *minMaxLinearEquationSolverFactory); + double lowerBound = 0; + double upperBound = 0; + if (!pathFormula.hasDiscreteTimeBound()) { + std::pair const& intervalBounds = pathFormula.getIntervalBounds(); + lowerBound = intervalBounds.first; + upperBound = intervalBounds.second; + } else { + upperBound = pathFormula.getDiscreteTimeBound(); + } + + std::vector result = storm::modelchecker::helper::SparseMarkovAutomatonCslHelper::computeBoundedUntilProbabilities(checkTask.getOptimizationDirection(), this->getModel().getTransitionMatrix(), this->getModel().getExitRates(), this->getModel().getMarkovianStates(), rightResult.getTruthValuesVector(), std::make_pair(lowerBound, upperBound), *minMaxLinearEquationSolverFactory); return std::unique_ptr(new ExplicitQuantitativeCheckResult(std::move(result))); } diff --git a/src/modelchecker/csl/helper/SparseMarkovAutomatonCslHelper.cpp b/src/modelchecker/csl/helper/SparseMarkovAutomatonCslHelper.cpp index c03b01871..71564b929 100644 --- a/src/modelchecker/csl/helper/SparseMarkovAutomatonCslHelper.cpp +++ b/src/modelchecker/csl/helper/SparseMarkovAutomatonCslHelper.cpp @@ -32,6 +32,7 @@ namespace storm { template void SparseMarkovAutomatonCslHelper::computeBoundedReachabilityProbabilities(OptimizationDirection dir, storm::storage::SparseMatrix const& transitionMatrix, std::vector const& exitRates, storm::storage::BitVector const& markovianStates, storm::storage::BitVector const& goalStates, storm::storage::BitVector const& markovianNonGoalStates, storm::storage::BitVector const& probabilisticNonGoalStates, std::vector& markovianNonGoalValues, std::vector& probabilisticNonGoalValues, ValueType delta, uint_fast64_t numberOfSteps, storm::utility::solver::MinMaxLinearEquationSolverFactory const& minMaxLinearEquationSolverFactory) { + // Start by computing four sparse matrices: // * a matrix aMarkovian with all (discretized) transitions from Markovian non-goal states to all Markovian non-goal states. // * a matrix aMarkovianToProbabilistic with all (discretized) transitions from Markovian non-goal states to all probabilistic non-goal states. @@ -116,10 +117,10 @@ namespace storm { storm::utility::vector::addVectors(bProbabilistic, bProbabilisticFixed, bProbabilistic); solver->solveEquationSystem(dir, probabilisticNonGoalValues, bProbabilistic, &multiplicationResultScratchMemory, &aProbabilisticScratchMemory); } - template std::vector SparseMarkovAutomatonCslHelper::computeBoundedUntilProbabilities(OptimizationDirection dir, storm::storage::SparseMatrix const& transitionMatrix, std::vector const& exitRateVector, storm::storage::BitVector const& markovianStates, storm::storage::BitVector const& psiStates, std::pair const& boundsPair, storm::utility::solver::MinMaxLinearEquationSolverFactory const& minMaxLinearEquationSolverFactory) { + uint_fast64_t numberOfStates = transitionMatrix.getRowGroupCount(); // 'Unpack' the bounds to make them more easily accessible. diff --git a/src/models/sparse/MarkovAutomaton.cpp b/src/models/sparse/MarkovAutomaton.cpp index 983bda12e..993cc4aa9 100644 --- a/src/models/sparse/MarkovAutomaton.cpp +++ b/src/models/sparse/MarkovAutomaton.cpp @@ -15,7 +15,7 @@ namespace storm { std::vector const& exitRates, std::unordered_map const& rewardModels, boost::optional> const& optionalChoiceLabeling) - : NondeterministicModel(storm::models::ModelType::MarkovAutomaton, transitionMatrix, stateLabeling, rewardModels, optionalChoiceLabeling), markovianStates(markovianStates), exitRates(exitRates), closed(false) { + : NondeterministicModel(storm::models::ModelType::MarkovAutomaton, transitionMatrix, stateLabeling, rewardModels, optionalChoiceLabeling), markovianStates(markovianStates), exitRates(exitRates), closed(this->checkIsClosed()) { this->turnRatesToProbabilities(); } @@ -26,7 +26,7 @@ namespace storm { std::vector const& exitRates, std::unordered_map&& rewardModels, boost::optional>&& optionalChoiceLabeling) - : NondeterministicModel(storm::models::ModelType::MarkovAutomaton, std::move(transitionMatrix), std::move(stateLabeling), std::move(rewardModels), std::move(optionalChoiceLabeling)), markovianStates(markovianStates), exitRates(std::move(exitRates)), closed(false) { + : NondeterministicModel(storm::models::ModelType::MarkovAutomaton, std::move(transitionMatrix), std::move(stateLabeling), std::move(rewardModels), std::move(optionalChoiceLabeling)), markovianStates(markovianStates), exitRates(std::move(exitRates)), closed(this->checkIsClosed()) { this->turnRatesToProbabilities(); } @@ -97,21 +97,19 @@ namespace storm { // Now copy over all choices that need to be kept. uint_fast64_t currentChoice = 0; for (uint_fast64_t state = 0; state < this->getNumberOfStates(); ++state) { - // If the state is a hybrid state, closing it will make it a probabilistic state, so we remove the Markovian marking. - if (this->isHybridState(state)) { - this->markovianStates.set(state, false); - } - // Record the new beginning of choices of this state. newTransitionMatrixBuilder.newRowGroup(currentChoice); - - // If we are currently treating a hybrid state, we need to skip its first choice. + + // If the state is a hybrid state, closing it will make it a probabilistic state, so we remove the Markovian marking. + // Additionally, we need to remember whether we need to skip the first choice of the state when + // we assemble the new transition matrix. + uint_fast64_t offset = 0; if (this->isHybridState(state)) { - // Remove the Markovian state marking. this->markovianStates.set(state, false); + offset = 1; } - for (uint_fast64_t row = this->getTransitionMatrix().getRowGroupIndices()[state] + (this->isHybridState(state) ? 1 : 0); row < this->getTransitionMatrix().getRowGroupIndices()[state + 1]; ++row) { + for (uint_fast64_t row = this->getTransitionMatrix().getRowGroupIndices()[state] + offset; row < this->getTransitionMatrix().getRowGroupIndices()[state + 1]; ++row) { for (auto const& entry : this->getTransitionMatrix().getRow(row)) { newTransitionMatrixBuilder.addNextValue(currentChoice, entry.getColumn(), entry.getValue()); } @@ -216,12 +214,22 @@ namespace storm { template void MarkovAutomaton::turnRatesToProbabilities() { for (auto state : this->markovianStates) { - for (auto& transition : this->getTransitionMatrix().getRowGroup(state)) { + for (auto& transition : this->getTransitionMatrix().getRow(this->getTransitionMatrix().getRowGroupIndices()[state])) { transition.setValue(transition.getValue() / this->exitRates[state]); } } } + template + bool MarkovAutomaton::checkIsClosed() const { + for (auto state : markovianStates) { + if (this->getTransitionMatrix().getRowGroupSize(state) > 1) { + return false; + } + } + return true; + } + template class MarkovAutomaton; // template class MarkovAutomaton; diff --git a/src/models/sparse/MarkovAutomaton.h b/src/models/sparse/MarkovAutomaton.h index 0556ffa9b..3ffb59e70 100644 --- a/src/models/sparse/MarkovAutomaton.h +++ b/src/models/sparse/MarkovAutomaton.h @@ -140,6 +140,11 @@ namespace storm { */ void turnRatesToProbabilities(); + /*! + * Checks whether the automaton is closed by actually looking at the transition information. + */ + bool checkIsClosed() const; + // A bit vector representing the set of Markovian states. storm::storage::BitVector markovianStates; diff --git a/src/parser/MarkovAutomatonSparseTransitionParser.cpp b/src/parser/MarkovAutomatonSparseTransitionParser.cpp index 18d87d314..a49fa3996 100644 --- a/src/parser/MarkovAutomatonSparseTransitionParser.cpp +++ b/src/parser/MarkovAutomatonSparseTransitionParser.cpp @@ -6,6 +6,7 @@ #include "src/exceptions/FileIoException.h" #include "src/parser/MappedFile.h" #include "src/utility/cstring.h" +#include "src/utility/constants.h" #include "src/utility/macros.h" namespace storm { @@ -152,6 +153,16 @@ namespace storm { } } while (!encounteredEOF && !encounteredNewDistribution); } + + // If there are some states with indices that are behind the last source for which no transition was specified, + // we need to reserve some space for introducing self-loops later. + if (!dontFixDeadlocks) { + result.numberOfNonzeroEntries += result.highestStateIndex - lastsource; + result.numberOfChoices += result.highestStateIndex - lastsource; + } else { + STORM_LOG_ERROR("Found deadlock states (e.g. " << lastsource + 1 << ") during parsing. Please fix them or set the appropriate flag."); + throw storm::exceptions::WrongFormatException() << "Found deadlock states (e.g. " << lastsource + 1 << ") during parsing. Please fix them or set the appropriate flag."; + } return result; } @@ -259,6 +270,21 @@ namespace storm { ++currentChoice; } + + // If there are some states with indices that are behind the last source for which no transition was specified, + // we need to insert the self-loops now. Note that we assume all these states to be Markovian. + if (!dontFixDeadlocks) { + for (uint_fast64_t index = lastsource + 1; index <= firstPassResult.highestStateIndex; ++index) { + result.markovianStates.set(index, true); + result.exitRates[index] = storm::utility::one(); + result.transitionMatrixBuilder.newRowGroup(currentChoice); + result.transitionMatrixBuilder.addNextValue(currentChoice, index, storm::utility::one()); + ++currentChoice; + } + } else { + STORM_LOG_ERROR("Found deadlock states (e.g. " << lastsource + 1 << ") during parsing. Please fix them or set the appropriate flag."); + throw storm::exceptions::WrongFormatException() << "Found deadlock states (e.g. " << lastsource + 1 << ") during parsing. Please fix them or set the appropriate flag."; + } return result; } diff --git a/src/utility/storm.h b/src/utility/storm.h index d2963a0f5..1a5cee872 100644 --- a/src/utility/storm.h +++ b/src/utility/storm.h @@ -59,6 +59,7 @@ #include "src/modelchecker/reachability/SparseDtmcEliminationModelChecker.h" #include "src/modelchecker/csl/SparseCtmcCslModelChecker.h" #include "src/modelchecker/csl/HybridCtmcCslModelChecker.h" +#include "src/modelchecker/csl/SparseMarkovAutomatonCslModelChecker.h" #include "src/modelchecker/results/ExplicitQualitativeCheckResult.h" #include "src/modelchecker/results/SymbolicQualitativeCheckResult.h" @@ -295,6 +296,16 @@ namespace storm { storm::modelchecker::SparseCtmcCslModelChecker> modelchecker(*ctmc); result = modelchecker.check(task); + } else if (model->getType() == storm::models::ModelType::MarkovAutomaton) { + std::shared_ptr> ma = model->template as>(); + + // Close the MA, if it is not already closed. + if (!ma->isClosed()) { + ma->close(); + } + + storm::modelchecker::SparseMarkovAutomatonCslModelChecker> modelchecker(*ma); + result = modelchecker.check(task); } return result; From 4bb4e29e43c0dc866deb1eee32e648d0fb4f47d4 Mon Sep 17 00:00:00 2001 From: TimQu Date: Fri, 18 Mar 2016 16:47:06 +0100 Subject: [PATCH 2/3] Added a test case where model checking expected rewards on MDPs currently fails Former-commit-id: 35dbe908c8c3cc6a59225832200e28c315803434 --- .../GmmxxMdpPrctlModelCheckerTest.cpp | 33 +++++++++++++++++++ test/functional/modelchecker/tiny_rewards.nm | 17 ++++++++++ 2 files changed, 50 insertions(+) create mode 100644 test/functional/modelchecker/tiny_rewards.nm 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; From 67cc067f35035770ebf7596a3faa956b26a5e8eb Mon Sep 17 00:00:00 2001 From: TimQu Date: Thu, 31 Mar 2016 17:07:52 +0200 Subject: [PATCH 3/3] fixed computeSchedulerProbGreater0E. Previously, it did not enforce that psiStates are actually reached. For instance, it was ok to chose a probability 1 selfloop. Former-commit-id: 518a3b33a96b8550b481d68906bf0161c3328991 --- src/utility/graph.cpp | 44 ++++++++++++++++++++++++++++++++++++++++--- src/utility/graph.h | 19 +++++++++++++++---- 2 files changed, 56 insertions(+), 7 deletions(-) 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);