Browse Source

symbolic minmax solver respecting linear equation solver problem format; fixed parsing bug pointed out by Dr. Nils Jansen

tempestpy_adaptions
dehnert 7 years ago
parent
commit
49cc789ca2
  1. 2
      src/storm/parser/ExpressionParser.cpp
  2. 6
      src/storm/solver/SymbolicMinMaxLinearEquationSolver.cpp

2
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;

6
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.

Loading…
Cancel
Save