From 49cc789ca257e4bf76faac7b1ec14e605f5de166 Mon Sep 17 00:00:00 2001
From: dehnert <dehnert@cs.rwth-aachen.de>
Date: Thu, 12 Oct 2017 15:05:49 +0200
Subject: [PATCH] symbolic minmax solver respecting linear equation solver
problem format; fixed parsing bug pointed out by Dr. Nils Jansen
---
src/storm/parser/ExpressionParser.cpp | 2 +-
.../solver/SymbolicEliminationLinearEquationSolver.cpp | 2 +-
src/storm/solver/SymbolicMinMaxLinearEquationSolver.cpp | 6 +++++-
3 files changed, 7 insertions(+), 3 deletions(-)
diff --git a/src/storm/parser/ExpressionParser.cpp b/src/storm/parser/ExpressionParser.cpp
index cd3ccd595..6306f5da9 100644
--- a/src/storm/parser/ExpressionParser.cpp
+++ b/src/storm/parser/ExpressionParser.cpp
@@ -120,7 +120,7 @@ namespace storm {
}
orExpression.name("or expression");
- iteExpression = orExpression[qi::_val = qi::_1] > -(qi::lit("?") > orExpression > qi::lit(":") > orExpression)[qi::_val = phoenix::bind(&ExpressionCreator::createIteExpression, phoenix::ref(*expressionCreator), qi::_val, qi::_1, qi::_2, qi::_pass)];
+ iteExpression = orExpression[qi::_val = qi::_1] > -(qi::lit("?") > iteExpression > qi::lit(":") > iteExpression)[qi::_val = phoenix::bind(&ExpressionCreator::createIteExpression, phoenix::ref(*expressionCreator), qi::_val, qi::_1, qi::_2, qi::_pass)];
iteExpression.name("if-then-else expression");
expression %= iteExpression;
diff --git a/src/storm/solver/SymbolicEliminationLinearEquationSolver.cpp b/src/storm/solver/SymbolicEliminationLinearEquationSolver.cpp
index 7443ecdcf..eed002c27 100644
--- a/src/storm/solver/SymbolicEliminationLinearEquationSolver.cpp
+++ b/src/storm/solver/SymbolicEliminationLinearEquationSolver.cpp
@@ -24,7 +24,7 @@ namespace storm {
SymbolicEliminationLinearEquationSolver<DdType, ValueType>::SymbolicEliminationLinearEquationSolver(storm::dd::Bdd<DdType> const& allRows, std::set<storm::expressions::Variable> const& rowMetaVariables, std::set<storm::expressions::Variable> const& columnMetaVariables, std::vector<std::pair<storm::expressions::Variable, storm::expressions::Variable>> const& rowColumnMetaVariablePairs) : SymbolicLinearEquationSolver<DdType, ValueType>(allRows, rowMetaVariables, columnMetaVariables, rowColumnMetaVariablePairs) {
this->createInternalData(allRows, rowMetaVariables, columnMetaVariables, rowColumnMetaVariablePairs);
}
-
+
template<storm::dd::DdType DdType, typename ValueType>
storm::dd::Add<DdType, ValueType> SymbolicEliminationLinearEquationSolver<DdType, ValueType>::solveEquations(storm::dd::Add<DdType, ValueType> const& x, storm::dd::Add<DdType, ValueType> const& b) const {
storm::dd::DdManager<DdType>& ddManager = x.getDdManager();
diff --git a/src/storm/solver/SymbolicMinMaxLinearEquationSolver.cpp b/src/storm/solver/SymbolicMinMaxLinearEquationSolver.cpp
index 904458646..e2d8f931b 100644
--- a/src/storm/solver/SymbolicMinMaxLinearEquationSolver.cpp
+++ b/src/storm/solver/SymbolicMinMaxLinearEquationSolver.cpp
@@ -303,6 +303,7 @@ namespace storm {
std::unique_ptr<SymbolicLinearEquationSolver<DdType, ValueType>> solver = linearEquationSolverFactory->create(this->allRows, this->rowMetaVariables, this->columnMetaVariables, this->rowColumnMetaVariablePairs);
this->forwardBounds(*solver);
+
storm::dd::Add<DdType, ValueType> diagonal = (storm::utility::dd::getRowColumnDiagonal<DdType>(x.getDdManager(), this->rowColumnMetaVariablePairs) && this->allRows).template toAdd<ValueType>();
return solveEquationsWithScheduler(*solver, scheduler, x, b, diagonal);
}
@@ -311,7 +312,10 @@ namespace storm {
storm::dd::Add<DdType, ValueType> SymbolicMinMaxLinearEquationSolver<DdType, ValueType>::solveEquationsWithScheduler(SymbolicLinearEquationSolver<DdType, ValueType>& solver, storm::dd::Bdd<DdType> const& scheduler, storm::dd::Add<DdType, ValueType> const& x, storm::dd::Add<DdType, ValueType> const& b, storm::dd::Add<DdType, ValueType> const& diagonal) const {
// Apply scheduler to the matrix and vector.
- storm::dd::Add<DdType, ValueType> schedulerA = diagonal - scheduler.ite(this->A, scheduler.getDdManager().template getAddZero<ValueType>()).sumAbstract(this->choiceVariables);
+ storm::dd::Add<DdType, ValueType> schedulerA = scheduler.ite(this->A, scheduler.getDdManager().template getAddZero<ValueType>()).sumAbstract(this->choiceVariables);
+ if (solver.getEquationProblemFormat() == storm::solver::LinearEquationSolverProblemFormat::EquationSystem) {
+ schedulerA = diagonal - schedulerA;
+ }
storm::dd::Add<DdType, ValueType> schedulerB = scheduler.ite(b, scheduler.getDdManager().template getAddZero<ValueType>()).sumAbstract(this->choiceVariables);
// Set the matrix for the solver.