From dae55eeb29291e54312636f62e97c16a207747e0 Mon Sep 17 00:00:00 2001 From: dehnert Date: Wed, 16 Mar 2016 16:12:22 +0100 Subject: [PATCH] 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;