sp
/
tempest
1
0
Fork 0
Code Issues Pull Requests Projects Releases Wiki Activity
Browse Source

Adapted MA model checker to new LP solver interface (LRA computation). 

Former-commit-id: b23b72c851
main
dehnert 11 years ago
parent
29d8111991
commit
d80586b4aa
2 changed files with 33 additions and 33 deletions
Unified View
  1. 14
      src/modelchecker/csl/SparseMarkovAutomatonCslModelChecker.cpp
  2. 52
      src/modelchecker/csl/SparseMarkovAutomatonCslModelChecker.h

14
src/modelchecker/csl/SparseMarkovAutomatonCslModelChecker.cpp
View File

@ -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 { 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());
// 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;
// });
// return true;
//});

52
src/modelchecker/csl/SparseMarkovAutomatonCslModelChecker.h
View File

@ -431,58 +431,58 @@ namespace storm {
solver->setModelSense(min ? storm::solver::LpSolver::ModelSense::Maximize : storm::solver::LpSolver::ModelSense::Minimize); solver->setModelSense(min ? storm::solver::LpSolver::ModelSense::Maximize : storm::solver::LpSolver::ModelSense::Minimize);
// First, we need to create the variables for the problem. // First, we need to create the variables for the problem.
std::map<uint_fast64_t, uint_fast64_t> stateToVariableIndexMap; std::map<uint_fast64_t, std::string> stateToVariableNameMap;
for (auto const& stateChoicesPair : mec) { 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(); solver->update();
// Now we encode the problem as constraints. // Now we encode the problem as constraints.
std::vector<uint_fast64_t> variables;
std::vector<double> coefficients;
for (auto const& stateChoicesPair : mec) { for (auto const& stateChoicesPair : mec) {
uint_fast64_t state = stateChoicesPair.first; uint_fast64_t state = stateChoicesPair.first;
// Now, based on the type of the state, create a suitable constraint. // Now, based on the type of the state, create a suitable constraint.
if (markovianStates.get(state)) { if (markovianStates.get(state)) {
variables.clear(); storm::expressions::Expression constraint = storm::expressions::Expression::createDoubleVariable(stateToVariableNameMap.at(state));
coefficients.clear();
variables.push_back(stateToVariableIndexMap.at(state));
coefficients.push_back(1);
for (auto element : transitionMatrix.getRow(nondeterministicChoiceIndices[state])) { for (auto element : transitionMatrix.getRow(nondeterministicChoiceIndices[state])) {
variables.push_back(stateToVariableIndexMap.at(element.getColumn())); constraint = constraint - storm::expressions::Expression::createDoubleVariable(stateToVariableNameMap.at(element.getColumn()));
coefficients.push_back(-element.getValue());
} }
variables.push_back(lraValueVariableIndex); constraint = constraint + storm::expressions::Expression::createDoubleLiteral(storm::utility::constantOne<ValueType>() / exitRates[state]) * storm::expressions::Expression::createDoubleVariable("k");
coefficients.push_back(storm::utility::constantOne<ValueType>() / exitRates[state]); storm::expressions::Expression rightHandSide = goalStates.get(state) ? storm::expressions::Expression::createDoubleLiteral(storm::utility::constantOne<ValueType>() / exitRates[state]) : storm::expressions::Expression::createDoubleLiteral(storm::utility::constantZero<ValueType>());
if (min) {
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<ValueType>() / exitRates[state] : storm::utility::constantZero<ValueType>()); constraint = constraint <= rightHandSide;
} else {
constraint = constraint >= rightHandSide;
}
solver->addConstraint("state" + std::to_string(state), constraint);
} else { } 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 // 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'. // and the sum ranges over all states s'.
for (auto choice : stateChoicesPair.second) { for (auto choice : stateChoicesPair.second) {
variables.clear(); storm::expressions::Expression constraint = storm::expressions::Expression::createDoubleVariable(stateToVariableNameMap.at(state));
coefficients.clear();
variables.push_back(stateToVariableIndexMap.at(state));
coefficients.push_back(1);
for (auto element : transitionMatrix.getRow(choice)) { for (auto element : transitionMatrix.getRow(choice)) {
variables.push_back(stateToVariableIndexMap.at(element.getColumn())); constraint = constraint - storm::expressions::Expression::createDoubleVariable(stateToVariableNameMap.at(element.getColumn()));
coefficients.push_back(-element.getValue());
} }
solver->addConstraint("state" + std::to_string(state), variables, coefficients, min ? storm::solver::LpSolver::LESS_EQUAL : storm::solver::LpSolver::GREATER_EQUAL, storm::utility::constantZero<ValueType>()); storm::expressions::Expression rightHandSide = storm::expressions::Expression::createDoubleLiteral(storm::utility::constantZero<ValueType>());
if (min) {
constraint = constraint <= rightHandSide;
} else {
constraint = constraint >= rightHandSide;
}
solver->addConstraint("state" + std::to_string(state), constraint);
} }
} }
} }
solver->optimize(); solver->optimize();
return solver->getContinuousValue(lraValueVariableIndex); return solver->getContinuousValue("k");
} }
/*! /*!

Write Preview
|||||||
100:0
Loading…
Cancel
Save