From 6564abd434a7082654585b408814a46e17fc5400 Mon Sep 17 00:00:00 2001 From: TimQu Date: Mon, 3 Sep 2018 13:06:50 +0200 Subject: [PATCH] jani expression substitution now also works for array expressions --- .../storage/SymbolicModelDescription.cpp | 3 --- src/storm/storage/jani/Assignment.cpp | 5 ++-- src/storm/storage/jani/Automaton.cpp | 3 ++- .../storage/jani/BoundedIntegerVariable.cpp | 5 ++-- src/storm/storage/jani/Edge.cpp | 3 ++- src/storm/storage/jani/EdgeDestination.cpp | 4 +++- .../storage/jani/JaniLocationExpander.cpp | 8 ++++--- src/storm/storage/jani/Model.cpp | 24 +++++++++++++------ src/storm/storage/jani/Model.h | 7 +++--- src/storm/storage/jani/TemplateEdge.cpp | 3 ++- src/storm/storage/jani/Variable.cpp | 3 ++- .../JaniExpressionSubstitutionVisitor.cpp | 11 +++++++++ .../JaniExpressionSubstitutionVisitor.h | 6 +++++ 13 files changed, 60 insertions(+), 25 deletions(-) diff --git a/src/storm/storage/SymbolicModelDescription.cpp b/src/storm/storage/SymbolicModelDescription.cpp index 77c1a897d..60708af6e 100644 --- a/src/storm/storage/SymbolicModelDescription.cpp +++ b/src/storm/storage/SymbolicModelDescription.cpp @@ -150,9 +150,6 @@ namespace storm { SymbolicModelDescription SymbolicModelDescription::preprocess(std::map const& constantDefinitions) const { if (this->isJaniModel()) { storm::jani::Model preparedModel = this->asJaniModel().defineUndefinedConstants(constantDefinitions).substituteConstants(); - if (preparedModel.hasArrayVariables()) { - preparedModel = preparedModel.convertArrays(); - } return SymbolicModelDescription(preparedModel); } else if (this->isPrismProgram()) { return SymbolicModelDescription(this->asPrismProgram().defineUndefinedConstants(constantDefinitions).substituteConstants()); diff --git a/src/storm/storage/jani/Assignment.cpp b/src/storm/storage/jani/Assignment.cpp index 003e48762..74f801906 100644 --- a/src/storm/storage/jani/Assignment.cpp +++ b/src/storm/storage/jani/Assignment.cpp @@ -1,6 +1,7 @@ #include "storm/storage/jani/Assignment.h" #include "storm/storage/jani/LValue.h" +#include "storm/storage/jani/expressions/JaniExpressionSubstitutionVisitor.h" #include "storm/storage/expressions/LinearityCheckVisitor.h" @@ -51,9 +52,9 @@ namespace storm { } void Assignment::substitute(std::map const& substitution) { - this->setAssignedExpression(this->getAssignedExpression().substitute(substitution).simplify()); + this->setAssignedExpression(substituteJaniExpression(this->getAssignedExpression(), substitution).simplify()); if (lValue.isArrayAccess()) { - lValue = LValue(LValue(lValue.getArray()), lValue.getArrayIndex().substitute(substitution).simplify()); + lValue = LValue(LValue(lValue.getArray()), substituteJaniExpression(lValue.getArrayIndex(), substitution).simplify()); } } diff --git a/src/storm/storage/jani/Automaton.cpp b/src/storm/storage/jani/Automaton.cpp index 58404e9a7..9737d768f 100644 --- a/src/storm/storage/jani/Automaton.cpp +++ b/src/storm/storage/jani/Automaton.cpp @@ -3,6 +3,7 @@ #include "storm/storage/jani/Edge.h" #include "storm/storage/jani/TemplateEdge.h" #include "storm/storage/jani/Location.h" +#include "storm/storage/jani/expressions/JaniExpressionSubstitutionVisitor.h" #include "storm/utility/macros.h" #include "storm/exceptions/WrongFormatException.h" @@ -387,7 +388,7 @@ namespace storm { location.substitute(substitution); } - this->setInitialStatesRestriction(this->getInitialStatesRestriction().substitute(substitution)); + this->setInitialStatesRestriction(substituteJaniExpression(this->getInitialStatesRestriction(), substitution)); edges.substitute(substitution); } diff --git a/src/storm/storage/jani/BoundedIntegerVariable.cpp b/src/storm/storage/jani/BoundedIntegerVariable.cpp index 5b851b127..79bce1eda 100644 --- a/src/storm/storage/jani/BoundedIntegerVariable.cpp +++ b/src/storm/storage/jani/BoundedIntegerVariable.cpp @@ -1,5 +1,6 @@ #include "storm/storage/jani/BoundedIntegerVariable.h" #include "storm/exceptions/NotImplementedException.h" +#include "storm/storage/jani/expressions/JaniExpressionSubstitutionVisitor.h" #include "storm/utility/macros.h" namespace storm { @@ -47,8 +48,8 @@ namespace storm { void BoundedIntegerVariable::substitute(std::map const& substitution) { Variable::substitute(substitution); - this->setLowerBound(this->getLowerBound().substitute(substitution)); - this->setUpperBound(this->getUpperBound().substitute(substitution)); + this->setLowerBound(substituteJaniExpression(this->getLowerBound(), substitution)); + this->setUpperBound(substituteJaniExpression(this->getUpperBound(), substitution)); } std::shared_ptr makeBoundedIntegerVariable(std::string const& name, storm::expressions::Variable const& variable, boost::optional initValue, bool transient, boost::optional lowerBound, boost::optional upperBound) { diff --git a/src/storm/storage/jani/Edge.cpp b/src/storm/storage/jani/Edge.cpp index 4460b2a65..33834b2c4 100644 --- a/src/storm/storage/jani/Edge.cpp +++ b/src/storm/storage/jani/Edge.cpp @@ -1,6 +1,7 @@ #include "storm/storage/jani/Edge.h" #include "storm/storage/jani/Model.h" +#include "storm/storage/jani/expressions/JaniExpressionSubstitutionVisitor.h" #include "storm/utility/macros.h" #include "storm/exceptions/InvalidArgumentException.h" @@ -76,7 +77,7 @@ namespace storm { void Edge::substitute(std::map const& substitution) { if (this->hasRate()) { - this->setRate(this->getRate().substitute(substitution)); + this->setRate(substituteJaniExpression(this->getRate(), substitution)); } for (auto& destination : destinations) { destination.substitute(substitution); diff --git a/src/storm/storage/jani/EdgeDestination.cpp b/src/storm/storage/jani/EdgeDestination.cpp index 62b92c1f0..0a9dd4b32 100644 --- a/src/storm/storage/jani/EdgeDestination.cpp +++ b/src/storm/storage/jani/EdgeDestination.cpp @@ -1,6 +1,8 @@ #include "storm/storage/jani/EdgeDestination.h" #include "storm/utility/macros.h" +#include "storm/storage/jani/expressions/JaniExpressionSubstitutionVisitor.h" + #include "storm/exceptions/WrongFormatException.h" namespace storm { @@ -37,7 +39,7 @@ namespace storm { } void EdgeDestination::substitute(std::map const& substitution) { - this->setProbability(this->getProbability().substitute(substitution)); + this->setProbability(substituteJaniExpression(this->getProbability(), substitution)); } bool EdgeDestination::hasAssignment(Assignment const& assignment) const { diff --git a/src/storm/storage/jani/JaniLocationExpander.cpp b/src/storm/storage/jani/JaniLocationExpander.cpp index d955a7754..8c06fb3c1 100644 --- a/src/storm/storage/jani/JaniLocationExpander.cpp +++ b/src/storm/storage/jani/JaniLocationExpander.cpp @@ -1,5 +1,7 @@ #include "storm/storage/jani/JaniLocationExpander.h" +#include "storm/storage/jani/expressions/JaniExpressionSubstitutionVisitor.h" + #include "storm/storage/expressions/ExpressionManager.h" #include "storm/exceptions/NotSupportedException.h" #include "storm/exceptions/IllegalArgumentException.h" @@ -83,7 +85,7 @@ namespace storm { substitutionMap[eliminatedExpressionVariable] = original.getExpressionManager().integer(newValueAndLocation.first); uint64_t newSourceIndex = newValueAndLocation.second; - storm::expressions::Expression newGuard = edge.getGuard().substitute(substitutionMap).simplify(); + storm::expressions::Expression newGuard = substituteJaniExpression(edge.getGuard(), substitutionMap).simplify(); if (!newGuard.containsVariables() && !newGuard.evaluateAsBool()) { continue; } @@ -105,9 +107,9 @@ namespace storm { } TemplateEdgeDestination ted(oa); templateEdge->addDestination(ted); - destinationLocationsAndProbabilities.emplace_back(locationVariableValueMap[destination.getLocationIndex()][value], destination.getProbability().substitute((substitutionMap))); + destinationLocationsAndProbabilities.emplace_back(locationVariableValueMap[destination.getLocationIndex()][value], substituteJaniExpression(destination.getProbability(), substitutionMap)); } - newAutomaton.addEdge(storm::jani::Edge(newSourceIndex, edge.getActionIndex(), edge.hasRate() ? boost::optional(edge.getRate().substitute(substitutionMap)) : boost::none, templateEdge, destinationLocationsAndProbabilities)); + newAutomaton.addEdge(storm::jani::Edge(newSourceIndex, edge.getActionIndex(), edge.hasRate() ? boost::optional(substituteJaniExpression(edge.getRate(), substitutionMap)) : boost::none, templateEdge, destinationLocationsAndProbabilities)); } } diff --git a/src/storm/storage/jani/Model.cpp b/src/storm/storage/jani/Model.cpp index 9f5f19915..3f34b72d4 100644 --- a/src/storm/storage/jani/Model.cpp +++ b/src/storm/storage/jani/Model.cpp @@ -16,6 +16,8 @@ #include "storm/storage/jani/CompositionInformationVisitor.h" #include "storm/storage/jani/Compositions.h" #include "storm/storage/jani/JSONExporter.h" +#include "storm/storage/jani/traverser/ArrayEliminator.h" +#include "storm/storage/jani/expressions/JaniExpressionSubstitutionVisitor.h" #include "storm/storage/expressions/LinearityCheckVisitor.h" @@ -896,7 +898,7 @@ namespace storm { std::map constantSubstitution; for (auto& constant : result.getConstants()) { if (constant.isDefined()) { - constant.define(constant.getExpression().substitute(constantSubstitution)); + constant.define(substituteJaniExpression(constant.getExpression(), constantSubstitution)); constantSubstitution[constant.getExpressionVariable()] = constant.getExpression(); } } @@ -910,7 +912,7 @@ namespace storm { } // Substitute constants in initial states expression. - result.setInitialStatesRestriction(this->getInitialStatesRestriction().substitute(constantSubstitution)); + result.setInitialStatesRestriction(substituteJaniExpression(this->getInitialStatesRestriction(), constantSubstitution)); // Substitute constants in variables of automata and their edges. for (auto& automaton : result.getAutomata()) { @@ -932,13 +934,21 @@ namespace storm { return result; } - bool Model::hasArrayVariables() const { - return getExpressionManager().getNumberOfArrayVariables() != 0; + bool Model::containsArrayVariables() const { + if (getGlobalVariables().containsArrayVariables()) { + return true; + } + for (auto const& a : getAutomata()) { + if (a.getVariables().containsArrayVariables()) { + return true; + } + } + return false; } - Model Model::convertArrays() const { - std::cout << "TODO"; - return *this; + void Model::eliminateArrays(bool keepNonTrivialArrayAccess) { + ArrayEliminator arrayEliminator; + arrayEliminator.eliminate(*this); } void Model::setInitialStatesRestriction(storm::expressions::Expression const& initialStatesRestriction) { diff --git a/src/storm/storage/jani/Model.h b/src/storm/storage/jani/Model.h index 452a3e4c5..ed0d0638a 100644 --- a/src/storm/storage/jani/Model.h +++ b/src/storm/storage/jani/Model.h @@ -360,12 +360,13 @@ namespace storm { /*! * Returns true if at least one array variable occurs in the model. */ - bool hasArrayVariables() const; + bool containsArrayVariables() const; /*! - * Converts occurring (fixed size) arrays into multiple variables. + * Eliminates occurring array variables and expressions by replacing array variables by multiple basic variables. + * @param keepNonTrivialArrayAccess if set, array access expressions in LValues and expressions are only replaced, if the index expression is constant. */ - Model convertArrays() const; + void eliminateArrays(bool keepNonTrivialArrayAccess = false); /*! * Retrieves whether there is an expression restricting the legal initial values of the global variables. diff --git a/src/storm/storage/jani/TemplateEdge.cpp b/src/storm/storage/jani/TemplateEdge.cpp index 460e6add3..889d25214 100644 --- a/src/storm/storage/jani/TemplateEdge.cpp +++ b/src/storm/storage/jani/TemplateEdge.cpp @@ -4,6 +4,7 @@ #include "storm/storage/jani/LValue.h" #include "storm/storage/expressions/LinearityCheckVisitor.h" +#include "storm/storage/jani/expressions/JaniExpressionSubstitutionVisitor.h" namespace storm { namespace jani { @@ -61,7 +62,7 @@ namespace storm { } void TemplateEdge::substitute(std::map const& substitution) { - guard = guard.substitute(substitution); + guard = substituteJaniExpression(guard, substitution); for (auto& assignment : assignments) { assignment.substitute(substitution); diff --git a/src/storm/storage/jani/Variable.cpp b/src/storm/storage/jani/Variable.cpp index d6a67996c..50fae165b 100644 --- a/src/storm/storage/jani/Variable.cpp +++ b/src/storm/storage/jani/Variable.cpp @@ -5,6 +5,7 @@ #include "storm/storage/jani/UnboundedIntegerVariable.h" #include "storm/storage/jani/RealVariable.h" #include "storm/storage/jani/ArrayVariable.h" +#include "storm/storage/jani/expressions/JaniExpressionSubstitutionVisitor.h" namespace storm { namespace jani { @@ -111,7 +112,7 @@ namespace storm { void Variable::substitute(std::map const& substitution) { if (this->hasInitExpression()) { - this->setInitExpression(this->getInitExpression().substitute(substitution)); + this->setInitExpression(substituteJaniExpression(this->getInitExpression(), substitution)); } } diff --git a/src/storm/storage/jani/expressions/JaniExpressionSubstitutionVisitor.cpp b/src/storm/storage/jani/expressions/JaniExpressionSubstitutionVisitor.cpp index 101f53472..a75a7cfed 100644 --- a/src/storm/storage/jani/expressions/JaniExpressionSubstitutionVisitor.cpp +++ b/src/storm/storage/jani/expressions/JaniExpressionSubstitutionVisitor.cpp @@ -3,6 +3,17 @@ #include "storm/exceptions/InvalidArgumentException.h" namespace storm { + + namespace jani { + storm::expressions::Expression substituteJaniExpression(storm::expressions::Expression const& expression, std::map const& identifierToExpressionMap) { + return JaniExpressionSubstitutionVisitor>(identifierToExpressionMap).substitute(expression); + } + + storm::expressions::Expression substituteJaniExpression(storm::expressions::Expression const& expression, std::unordered_map const& identifierToExpressionMap) { + return JaniExpressionSubstitutionVisitor>(identifierToExpressionMap).substitute(expression); + } + } + namespace expressions { template boost::any JaniExpressionSubstitutionVisitor::visit(ValueArrayExpression const& expression, boost::any const& data) { diff --git a/src/storm/storage/jani/expressions/JaniExpressionSubstitutionVisitor.h b/src/storm/storage/jani/expressions/JaniExpressionSubstitutionVisitor.h index ca82d7df1..ab196acee 100644 --- a/src/storm/storage/jani/expressions/JaniExpressionSubstitutionVisitor.h +++ b/src/storm/storage/jani/expressions/JaniExpressionSubstitutionVisitor.h @@ -5,6 +5,12 @@ #include "storm/storage/jani/expressions/JaniExpressionVisitor.h" namespace storm { + + namespace jani { + storm::expressions::Expression substituteJaniExpression(storm::expressions::Expression const& expression, std::map const& identifierToExpressionMap); + storm::expressions::Expression substituteJaniExpression(storm::expressions::Expression const& expression, std::unordered_map const& identifierToExpressionMap); + } + namespace expressions { template class JaniExpressionSubstitutionVisitor : public SubstitutionVisitor, public JaniExpressionVisitor {