From d80586b4aa4ae090c17dc42e3827d7d9f7745086 Mon Sep 17 00:00:00 2001 From: dehnert Date: Sun, 11 May 2014 20:39:41 +0200 Subject: [PATCH] Adapted MA model checker to new LP solver interface (LRA computation). Former-commit-id: b23b72c8510ca956a9c80a80bf448a0a4289f630 --- .../SparseMarkovAutomatonCslModelChecker.cpp | 14 ++--- .../SparseMarkovAutomatonCslModelChecker.h | 52 +++++++++---------- 2 files changed, 33 insertions(+), 33 deletions(-) diff --git a/src/modelchecker/csl/SparseMarkovAutomatonCslModelChecker.cpp b/src/modelchecker/csl/SparseMarkovAutomatonCslModelChecker.cpp index 580ea9c69..b5fa4bad4 100644 --- a/src/modelchecker/csl/SparseMarkovAutomatonCslModelChecker.cpp +++ b/src/modelchecker/csl/SparseMarkovAutomatonCslModelChecker.cpp @@ -1,8 +1,8 @@ -// #include "src/modelchecker/csl/SparseMarkovAutomatonCslModelChecker.h" +#include "src/modelchecker/csl/SparseMarkovAutomatonCslModelChecker.h" -//bool SparseMarkovAutomatonCslModelCheckerOptionsRegistered = storm::settings::Settings::registerNewModule([] (storm::settings::Settings* instance) -> bool { -// -// instance->addOption(storm::settings::OptionBuilder("GmmxxLinearEquationSolver", "digiprecision", "", "Precision used for iterative solving of linear equation systems").addArgument(storm::settings::ArgumentBuilder::createDoubleArgument("precision value", "Precision").setDefaultValueDouble(1e-4).addValidationFunctionDouble(storm::settings::ArgumentValidators::doubleRangeValidatorExcluding(0.0, 1.0)).build()).build()); -// -// return true; -//}); +bool SparseMarkovAutomatonCslModelCheckerOptionsRegistered = storm::settings::Settings::registerNewModule([] (storm::settings::Settings* instance) -> bool { + + instance->addOption(storm::settings::OptionBuilder("GmmxxLinearEquationSolver", "digiprecision", "", "Precision used for iterative solving of linear equation systems").addArgument(storm::settings::ArgumentBuilder::createDoubleArgument("precision value", "Precision").setDefaultValueDouble(1e-4).addValidationFunctionDouble(storm::settings::ArgumentValidators::doubleRangeValidatorExcluding(0.0, 1.0)).build()).build()); + + return true; +}); diff --git a/src/modelchecker/csl/SparseMarkovAutomatonCslModelChecker.h b/src/modelchecker/csl/SparseMarkovAutomatonCslModelChecker.h index 8a924ba47..dbcf4d8b1 100644 --- a/src/modelchecker/csl/SparseMarkovAutomatonCslModelChecker.h +++ b/src/modelchecker/csl/SparseMarkovAutomatonCslModelChecker.h @@ -431,58 +431,58 @@ namespace storm { solver->setModelSense(min ? storm::solver::LpSolver::ModelSense::Maximize : storm::solver::LpSolver::ModelSense::Minimize); // First, we need to create the variables for the problem. - std::map stateToVariableIndexMap; + std::map stateToVariableNameMap; for (auto const& stateChoicesPair : mec) { - stateToVariableIndexMap[stateChoicesPair.first] = solver->createContinuousVariable("x" + std::to_string(stateChoicesPair.first), storm::solver::LpSolver::UNBOUNDED, 0, 0, 0); + std::string variableName = "x" + std::to_string(stateChoicesPair.first); + stateToVariableNameMap[stateChoicesPair.first] = variableName; + solver->addUnboundedContinuousVariable(variableName); } - uint_fast64_t lraValueVariableIndex = solver->createContinuousVariable("k", storm::solver::LpSolver::UNBOUNDED, 0, 0, 1); + solver->addUnboundedContinuousVariable("k", 1); solver->update(); // 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 (markovianStates.get(state)) { - variables.clear(); - coefficients.clear(); - - variables.push_back(stateToVariableIndexMap.at(state)); - coefficients.push_back(1); + storm::expressions::Expression constraint = storm::expressions::Expression::createDoubleVariable(stateToVariableNameMap.at(state)); for (auto element : transitionMatrix.getRow(nondeterministicChoiceIndices[state])) { - variables.push_back(stateToVariableIndexMap.at(element.getColumn())); - coefficients.push_back(-element.getValue()); + constraint = constraint - storm::expressions::Expression::createDoubleVariable(stateToVariableNameMap.at(element.getColumn())); } - variables.push_back(lraValueVariableIndex); - coefficients.push_back(storm::utility::constantOne() / exitRates[state]); - - solver->addConstraint("state" + std::to_string(state), variables, coefficients, min ? storm::solver::LpSolver::LESS_EQUAL : storm::solver::LpSolver::GREATER_EQUAL, goalStates.get(state) ? storm::utility::constantOne() / exitRates[state] : storm::utility::constantZero()); + constraint = constraint + storm::expressions::Expression::createDoubleLiteral(storm::utility::constantOne() / exitRates[state]) * storm::expressions::Expression::createDoubleVariable("k"); + storm::expressions::Expression rightHandSide = goalStates.get(state) ? storm::expressions::Expression::createDoubleLiteral(storm::utility::constantOne() / exitRates[state]) : storm::expressions::Expression::createDoubleLiteral(storm::utility::constantZero()); + if (min) { + constraint = constraint <= rightHandSide; + } else { + constraint = constraint >= rightHandSide; + } + solver->addConstraint("state" + std::to_string(state), constraint); } 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); - + storm::expressions::Expression constraint = storm::expressions::Expression::createDoubleVariable(stateToVariableNameMap.at(state)); + for (auto element : transitionMatrix.getRow(choice)) { - variables.push_back(stateToVariableIndexMap.at(element.getColumn())); - coefficients.push_back(-element.getValue()); + constraint = constraint - storm::expressions::Expression::createDoubleVariable(stateToVariableNameMap.at(element.getColumn())); } - solver->addConstraint("state" + std::to_string(state), variables, coefficients, min ? storm::solver::LpSolver::LESS_EQUAL : storm::solver::LpSolver::GREATER_EQUAL, storm::utility::constantZero()); + storm::expressions::Expression rightHandSide = storm::expressions::Expression::createDoubleLiteral(storm::utility::constantZero()); + if (min) { + constraint = constraint <= rightHandSide; + } else { + constraint = constraint >= rightHandSide; + } + solver->addConstraint("state" + std::to_string(state), constraint); } } } solver->optimize(); - return solver->getContinuousValue(lraValueVariableIndex); + return solver->getContinuousValue("k"); } /*!