From 339b598694622e43b0cb4ae7a4294fdbff88bfdf Mon Sep 17 00:00:00 2001 From: dehnert Date: Tue, 26 Nov 2013 21:36:41 +0100 Subject: [PATCH] Enabled computation of LRA for individual maximal end components. It remains to compute the overall LRA value using the values for the individual MECs. Former-commit-id: 47eb90e62c009ecb29cdc2e85727a8afbdb9fd16 --- .../SparseMarkovAutomatonCslModelChecker.h | 67 ++++++++++++++++++- src/models/MarkovAutomaton.h | 4 ++ src/storm.cpp | 1 + 3 files changed, 71 insertions(+), 1 deletion(-) diff --git a/src/modelchecker/csl/SparseMarkovAutomatonCslModelChecker.h b/src/modelchecker/csl/SparseMarkovAutomatonCslModelChecker.h index 1a3fe138f..8a3b594ff 100644 --- a/src/modelchecker/csl/SparseMarkovAutomatonCslModelChecker.h +++ b/src/modelchecker/csl/SparseMarkovAutomatonCslModelChecker.h @@ -8,6 +8,8 @@ #include "src/storage/BitVector.h" #include "src/storage/MaximalEndComponentDecomposition.h" #include "src/solver/AbstractNondeterministicLinearEquationSolver.h" +#include "src/solver/LpSolver.h" +#include "src/utility/solver.h" #include "src/utility/graph.h" #include "src/exceptions/NotImplementedException.h" @@ -69,12 +71,75 @@ namespace storm { std::vector checkLongRunAverage(bool min, storm::storage::BitVector const& goalStates) const { // Start by decomposing the Markov automaton into its MECs. - storm::storage::MaximalEndComponentDecomposition mecDecomposition(this->getModel(), ~goalStates); + storm::storage::MaximalEndComponentDecomposition mecDecomposition(this->getModel()); + + // Get some data members for convenience. + typename storm::storage::SparseMatrix const& transitionMatrix = this->getModel().getTransitionMatrix(); + std::vector const& nondeterministicChoiceIndices = this->getModel().getNondeterministicChoiceIndices(); // Now compute the long-run average for all end components in isolation. + std::vector lraValuesForEndComponents; for (storm::storage::MaximalEndComponent const& mec : mecDecomposition) { + std::unique_ptr solver = storm::utility::solver::getLpSolver("Long-Run Average"); + solver->setModelSense(storm::solver::LpSolver::MAXIMIZE); + + // First, we need to create the variables for the problem. + std::map stateToVariableIndexMap; + for (auto const& stateChoicesPair : mec) { + stateToVariableIndexMap[stateChoicesPair.first] = solver->createContinuousVariable("x" + std::to_string(stateChoicesPair.first), storm::solver::LpSolver::UNBOUNDED, 0, 0, 0); + } + uint_fast64_t lraValueVariableIndex = solver->createContinuousVariable("k", storm::solver::LpSolver::UNBOUNDED, 0, 0, 1); + // Now we encode the problem as constraints. + std::vector variables; + std::vector coefficients; + for (auto const& stateChoicesPair : mec) { + uint_fast64_t state = stateChoicesPair.first; + + // Now, based on the type of the state, create a suitable constraint. + if (this->getModel().isMarkovianState(state)) { + variables.clear(); + coefficients.clear(); + + variables.push_back(stateToVariableIndexMap.at(state)); + coefficients.push_back(1); + + typename storm::storage::SparseMatrix::Rows row = transitionMatrix.getRow(nondeterministicChoiceIndices[state]); + for (auto element : row) { + variables.push_back(stateToVariableIndexMap.at(element.column())); + coefficients.push_back(-element.value()); + } + + variables.push_back(lraValueVariableIndex); + coefficients.push_back(this->getModel().getExitRate(state)); + + solver->addConstraint("state" + std::to_string(state), variables, coefficients, storm::solver::LpSolver::LESS_EQUAL, storm::utility::constGetOne() / this->getModel().getExitRate(state)); + } else { + // For probabilistic states, we want to add the constraint x_s <= sum P(s, a, s') * x_s' where a is the current action + // and the sum ranges over all states s'. + for (auto choice : stateChoicesPair.second) { + variables.clear(); + coefficients.clear(); + + variables.push_back(stateToVariableIndexMap.at(state)); + coefficients.push_back(1); + + typename storm::storage::SparseMatrix::Rows row = transitionMatrix.getRow(choice); + for (auto element : row) { + variables.push_back(stateToVariableIndexMap.at(element.column())); + coefficients.push_back(-element.value()); + } + + solver->addConstraint("state" + std::to_string(state), variables, coefficients, storm::solver::LpSolver::LESS_EQUAL, storm::utility::constGetZero()); + } + } + } + + solver->optimize(); + lraValuesForEndComponents.push_back(solver->getContinuousValue(lraValueVariableIndex)); } + + return lraValuesForEndComponents; } std::vector checkExpectedTime(bool min, storm::storage::BitVector const& goalStates) const { diff --git a/src/models/MarkovAutomaton.h b/src/models/MarkovAutomaton.h index b6273181a..9ea225f59 100644 --- a/src/models/MarkovAutomaton.h +++ b/src/models/MarkovAutomaton.h @@ -96,6 +96,10 @@ namespace storm { return this->exitRates; } + T const& getExitRate(uint_fast64_t state) const { + return this->exitRates[state]; + } + storm::storage::BitVector const& getMarkovianStates() const { return this->markovianStates; } diff --git a/src/storm.cpp b/src/storm.cpp index 68df53112..e70721b4a 100644 --- a/src/storm.cpp +++ b/src/storm.cpp @@ -476,6 +476,7 @@ int main(const int argc, const char* argv[]) { storm::modelchecker::csl::SparseMarkovAutomatonCslModelChecker mc(*markovAutomaton, new storm::solver::AbstractNondeterministicLinearEquationSolver()); std::cout << mc.checkExpectedTime(true, markovAutomaton->getLabeledStates("goal")) << std::endl; std::cout << mc.checkExpectedTime(false, markovAutomaton->getLabeledStates("goal")) << std::endl; + std::cout << mc.checkLongRunAverage(false, markovAutomaton->getLabeledStates("goal")) << std::endl; break; }