Browse Source

Fixing steady state distribution computation.

tempestpy_adaptions
Tim Quatmann 4 years ago
parent
commit
b73e2e5d1c
  1. 14
      src/storm/modelchecker/helper/infinitehorizon/SparseDeterministicInfiniteHorizonHelper.cpp

14
src/storm/modelchecker/helper/infinitehorizon/SparseDeterministicInfiniteHorizonHelper.cpp

@ -522,21 +522,25 @@ namespace storm {
storm::solver::GeneralLinearEquationSolverFactory<ValueType> linearEquationSolverFactory; storm::solver::GeneralLinearEquationSolverFactory<ValueType> linearEquationSolverFactory;
bool isEqSysFormat = linearEquationSolverFactory.getEquationProblemFormat(env) == storm::solver::LinearEquationSolverProblemFormat::EquationSystem; bool isEqSysFormat = linearEquationSolverFactory.getEquationProblemFormat(env) == storm::solver::LinearEquationSolverProblemFormat::EquationSystem;
auto eqSysMatrix = this->_transitionMatrix.getSubmatrix(false, statesNotInComponent, statesNotInComponent, isEqSysFormat); auto eqSysMatrix = this->_transitionMatrix.getSubmatrix(false, statesNotInComponent, statesNotInComponent, isEqSysFormat);
std::unique_ptr<storm::solver::LinearEquationSolver<ValueType>> solver = linearEquationSolverFactory.create(env, eqSysMatrix);
solver->setLowerBound(storm::utility::zero<ValueType>());
boost::optional<std::vector<ValueType>> upperBounds;
// Check solver requirements // Check solver requirements
auto requirements = solver->getRequirements(env);
auto requirements = linearEquationSolverFactory.getRequirements(env);
requirements.clearLowerBounds(); requirements.clearLowerBounds();
if (requirements.upperBounds()) { if (requirements.upperBounds()) {
auto toBsccProbabilities = this->_transitionMatrix.getConstrainedRowSumVector(statesNotInComponent, ~statesNotInComponent); auto toBsccProbabilities = this->_transitionMatrix.getConstrainedRowSumVector(statesNotInComponent, ~statesNotInComponent);
solver->setUpperBounds(computeUpperBoundsForExpectedVisitingTimes(eqSysMatrix, toBsccProbabilities));
upperBounds = computeUpperBoundsForExpectedVisitingTimes(eqSysMatrix, toBsccProbabilities);
requirements.clearUpperBounds(); requirements.clearUpperBounds();
} }
STORM_LOG_THROW(!requirements.hasEnabledCriticalRequirement(), storm::exceptions::UnmetRequirementException, "Solver requirements " + requirements.getEnabledRequirementsAsString() + " not checked."); STORM_LOG_THROW(!requirements.hasEnabledCriticalRequirement(), storm::exceptions::UnmetRequirementException, "Solver requirements " + requirements.getEnabledRequirementsAsString() + " not checked.");
eqSysMatrix.transpose(false, true); // Transpose so that each row considers the predecessors
eqSysMatrix = eqSysMatrix.transpose(false, true); // Transpose so that each row considers the predecessors
if (isEqSysFormat) { if (isEqSysFormat) {
eqSysMatrix.convertToEquationSystem(); eqSysMatrix.convertToEquationSystem();
} }
std::unique_ptr<storm::solver::LinearEquationSolver<ValueType>> solver = linearEquationSolverFactory.create(env, eqSysMatrix);
solver->setLowerBound(storm::utility::zero<ValueType>());
if (upperBounds) {
solver->setUpperBounds(std::move(upperBounds.get()));
}
std::vector<ValueType> eqSysRhs; std::vector<ValueType> eqSysRhs;
eqSysRhs.reserve(eqSysMatrix.getRowCount()); eqSysRhs.reserve(eqSysMatrix.getRowCount());
for (auto state : statesNotInComponent) { for (auto state : statesNotInComponent) {

Loading…
Cancel
Save