diff --git a/src/storm-parsers/parser/JaniParser.cpp b/src/storm-parsers/parser/JaniParser.cpp index 97e7a80ad..ddd518fb9 100644 --- a/src/storm-parsers/parser/JaniParser.cpp +++ b/src/storm-parsers/parser/JaniParser.cpp @@ -24,7 +24,7 @@ #include #include #include -#include +#include "storm/storage/jani/ArrayVariable.h" #include "storm/utility/macros.h" #include "storm/utility/file.h" @@ -1299,8 +1299,7 @@ namespace storm { for (auto const& assignmentEntry : destEntry.at("assignments")) { // ref STORM_LOG_THROW(assignmentEntry.count("ref") == 1, storm::exceptions::InvalidJaniException, "Assignment in edge from '" << sourceLoc << "' to '" << targetLoc << "' in automaton '" << name << "' must have one ref field"); - std::string refstring = getString(assignmentEntry.at("ref"), "assignment in edge from '" + sourceLoc + "' to '" + targetLoc + "' in automaton '" + name + "'"); - storm::jani::LValue lValue = parseLValue(refstring, "Assignment variable in edge from '" + sourceLoc + "' to '" + targetLoc + "' in automaton '" + name + "'", globalVars, constants, localVars); + storm::jani::LValue lValue = parseLValue(assignmentEntry.at("ref"), "Assignment variable in edge from '" + sourceLoc + "' to '" + targetLoc + "' in automaton '" + name + "'", globalVars, constants, localVars); // value STORM_LOG_THROW(assignmentEntry.count("value") == 1, storm::exceptions::InvalidJaniException, "Assignment in edge from '" << sourceLoc << "' to '" << targetLoc << "' in automaton '" << name << "' must have one value field"); storm::expressions::Expression assignmentExpr = parseExpression(assignmentEntry.at("value"), "assignment in edge from '" + sourceLoc + "' to '" + targetLoc + "' in automaton '" + name + "'", globalVars, constants, localVars); diff --git a/src/storm/storage/jani/Assignment.cpp b/src/storm/storage/jani/Assignment.cpp index 6830abb6f..003e48762 100644 --- a/src/storm/storage/jani/Assignment.cpp +++ b/src/storm/storage/jani/Assignment.cpp @@ -15,7 +15,7 @@ namespace storm { } bool Assignment::operator==(Assignment const& other) const { - return this->isTransient() == other.isTransient() && this->getExpressionVariable() == other.getExpressionVariable() && this->getAssignedExpression().isSyntacticallyEqual(other.getAssignedExpression()) && this->getLevel() == other.getLevel(); + return this->isTransient() == other.isTransient() && this->getLValue() == other.getLValue() && this->getAssignedExpression().isSyntacticallyEqual(other.getAssignedExpression()) && this->getLevel() == other.getLevel(); } bool Assignment::lValueIsVariable() const { diff --git a/src/storm/storage/jani/Automaton.cpp b/src/storm/storage/jani/Automaton.cpp index 62d2576cf..58404e9a7 100644 --- a/src/storm/storage/jani/Automaton.cpp +++ b/src/storm/storage/jani/Automaton.cpp @@ -33,6 +33,8 @@ namespace storm { return addVariable(variable.asUnboundedIntegerVariable()); } else if (variable.isRealVariable()) { return addVariable(variable.asRealVariable()); + } else if (variable.isArrayVariable()) { + return addVariable(variable.asArrayVariable()); } else { STORM_LOG_THROW(false, storm::exceptions::InvalidTypeException, "Variable has invalid type."); } @@ -53,6 +55,10 @@ namespace storm { RealVariable const& Automaton::addVariable(RealVariable const& variable) { return variables.addVariable(variable); } + + ArrayVariable const& Automaton::addVariable(ArrayVariable const& variable) { + return variables.addVariable(variable); + } bool Automaton::hasVariable(std::string const& name) const { return variables.hasVariable(name); diff --git a/src/storm/storage/jani/Automaton.h b/src/storm/storage/jani/Automaton.h index 869f5cd09..6e51d6440 100644 --- a/src/storm/storage/jani/Automaton.h +++ b/src/storm/storage/jani/Automaton.h @@ -70,6 +70,11 @@ namespace storm { */ RealVariable const& addVariable(RealVariable const& variable); + /*! + * Adds the given array variable to this automaton. + */ + ArrayVariable const& addVariable(ArrayVariable const& variable); + /*! * Retrieves the variables of this automaton. */ diff --git a/src/storm/storage/jani/LValue.cpp b/src/storm/storage/jani/LValue.cpp index f8ba7eef4..27788db78 100644 --- a/src/storm/storage/jani/LValue.cpp +++ b/src/storm/storage/jani/LValue.cpp @@ -62,9 +62,9 @@ namespace storm { return false; } STORM_LOG_ASSERT(other.isArrayAccess(), "Unhandled LValue."); - if (variable->getExpressionVariable() < other.getVariable().getExpressionVariable()) { + if (getArray().getExpressionVariable() < other.getArray().getExpressionVariable()) { return true; - } else if (other.getVariable().getExpressionVariable() < variable->getExpressionVariable()) { + } else if (other.getArray().getExpressionVariable() < getArray().getExpressionVariable()) { return false; } else { return std::less()(arrayIndex, other.getArrayIndex()); diff --git a/src/storm/storage/jani/Model.cpp b/src/storm/storage/jani/Model.cpp index bd6e59c0c..d484b6cb7 100644 --- a/src/storm/storage/jani/Model.cpp +++ b/src/storm/storage/jani/Model.cpp @@ -634,6 +634,8 @@ namespace storm { return addVariable(variable.asUnboundedIntegerVariable()); } else if (variable.isRealVariable()) { return addVariable(variable.asRealVariable()); + } else if (variable.isArrayVariable()) { + return addVariable(variable.asArrayVariable()); } else { STORM_LOG_THROW(false, storm::exceptions::InvalidTypeException, "Variable has invalid type."); } @@ -654,6 +656,10 @@ namespace storm { RealVariable const& Model::addVariable(RealVariable const& variable) { return globalVariables.addVariable(variable); } + + ArrayVariable const& Model::addVariable(ArrayVariable const& variable) { + return globalVariables.addVariable(variable); + } VariableSet& Model::getGlobalVariables() { return globalVariables; @@ -899,6 +905,9 @@ namespace storm { for (auto& variable : result.getGlobalVariables().getBoundedIntegerVariables()) { variable.substitute(constantSubstitution); } + for (auto& variable : result.getGlobalVariables().getArrayVariables()) { + variable.substitute(constantSubstitution); + } // Substitute constants in initial states expression. result.setInitialStatesRestriction(this->getInitialStatesRestriction().substitute(constantSubstitution)); @@ -993,6 +1002,7 @@ namespace storm { for (auto const& variable : this->getGlobalVariables().getBoundedIntegerVariables()) { result.push_back(variable.getRangeExpression()); } + STORM_LOG_ASSERT(this->getGlobalVariables().getArrayVariables().empty(), "This operation is unsupported if array variables are present."); if (automata.empty()) { for (auto const& automaton : this->getAutomata()) { diff --git a/src/storm/storage/jani/Model.h b/src/storm/storage/jani/Model.h index 2bcf13504..4235b904b 100644 --- a/src/storm/storage/jani/Model.h +++ b/src/storm/storage/jani/Model.h @@ -190,6 +190,11 @@ namespace storm { */ RealVariable const& addVariable(RealVariable const& variable); + /*! + * Adds the given array variable to this model. + */ + ArrayVariable const& addVariable(ArrayVariable const& variable); + /*! * Retrieves the variables of this automaton. */ diff --git a/src/storm/storage/jani/OrderedAssignments.cpp b/src/storm/storage/jani/OrderedAssignments.cpp index bce6a0fc8..27ccd2761 100644 --- a/src/storm/storage/jani/OrderedAssignments.cpp +++ b/src/storm/storage/jani/OrderedAssignments.cpp @@ -35,8 +35,8 @@ namespace storm { auto it = lowerBound(assignment, allAssignments); // Check if an assignment to this variable is already present - if (it != allAssignments.end() && assignment.getExpressionVariable() == (*it)->getExpressionVariable()) { - STORM_LOG_THROW(addToExisting && assignment.getExpressionVariable().hasNumericalType(), storm::exceptions::InvalidArgumentException, "Cannot add assignment ('" << assignment.getAssignedExpression() << "') as an assignment ('" << (*it)->getAssignedExpression() << "') to variable '" << (*it)->getVariable().getName() << "' already exists."); + if (it != allAssignments.end() && assignment.getLValue() == (*it)->getLValue()) { + STORM_LOG_THROW(addToExisting && assignment.getLValue().isVariable() && assignment.getExpressionVariable().hasNumericalType(), storm::exceptions::InvalidArgumentException, "Cannot add assignment ('" << assignment.getAssignedExpression() << "') as an assignment ('" << (*it)->getAssignedExpression() << "') to LValue '" << (*it)->getLValue() << "' already exists."); (*it)->setAssignedExpression((*it)->getAssignedExpression() + assignment.getAssignedExpression()); } else { // Finally, insert the new element in the correct vectors. @@ -125,18 +125,19 @@ namespace storm { if (first) { std::vector newAssignments; for (uint64_t i = 0; i < allAssignments.size(); ++i) { - if (synchronous && !localVars.hasVariable(allAssignments.at(i)->getVariable())) { + auto const& iLValue = allAssignments.at(i)->getLValue(); + if (synchronous && !localVars.hasVariable(iLValue.isVariable() ? iLValue.getVariable() : iLValue.getArray())) { newAssignments.push_back(*(allAssignments.at(i))); continue; } bool readBeforeWrite = true; for (uint64_t j = i + 1; j < allAssignments.size(); ++j) { if (allAssignments.at(j)->getAssignedExpression().containsVariable( - {allAssignments.at(i)->getVariable().getExpressionVariable()})) { + {iLValue.isVariable() ? iLValue.getVariable().getExpressionVariable() : iLValue.getArray().getExpressionVariable()})) { // is read. break; } - if (allAssignments.at(j)->getVariable() == allAssignments.at(i)->getVariable()) { + if (iLValue == allAssignments.at(j)->getLValue()) { // is written, has not been read before readBeforeWrite = false; break; @@ -158,15 +159,15 @@ namespace storm { std::vector newAssignments; for (auto const& assignment : allAssignments) { newAssignments.push_back(*assignment); - if (synchronous && !localVars.hasVariable(assignment->getVariable())) { + if (synchronous && !localVars.hasVariable(assignment->getLValue().isVariable() ? assignment->getLValue().getVariable() : assignment->getLValue().getArray())) { continue; } if (assignment->getLevel() == 0) { continue; } uint64_t assNr = upperBound(assignment->getLevel() - 1); - if (assNr == isWrittenBeforeAssignment(assignment->getVariable(), assNr)) { - if (assNr == isReadBeforeAssignment(assignment->getVariable(), assNr)) { + if (assNr == isWrittenBeforeAssignment(assignment->getLValue(), assNr)) { + if (assNr == isReadBeforeAssignment(assignment->getLValue(), assNr)) { newAssignments.back().setLevel(0); changed = true; } @@ -230,7 +231,10 @@ namespace storm { return std::lower_bound(assignments.begin(), assignments.end(), assignment, storm::jani::AssignmentPartialOrderByLevelAndLValue()); } - uint64_t OrderedAssignments::isReadBeforeAssignment(Variable const& var, uint64_t assignmentNumber, uint64_t start) const { + uint64_t OrderedAssignments::isReadBeforeAssignment(LValue const& lValue, uint64_t assignmentNumber, uint64_t start) const { + Variable const& var = lValue.isVariable() ? lValue.getVariable() : lValue.getArray(); + // TODO: do this more carefully + STORM_LOG_WARN_COND(lValue.isVariable(), "Called a method that is not optimized for arrays."); for (uint64_t i = start; i < assignmentNumber; i++) { if (allAssignments.at(i)->getAssignedExpression().containsVariable({ var.getExpressionVariable() })) { return i; @@ -239,9 +243,9 @@ namespace storm { return assignmentNumber; } - uint64_t OrderedAssignments::isWrittenBeforeAssignment(Variable const& var, uint64_t assignmentNumber, uint64_t start) const { + uint64_t OrderedAssignments::isWrittenBeforeAssignment(LValue const& lValue, uint64_t assignmentNumber, uint64_t start) const { for (uint64_t i = start; i < assignmentNumber; i++) { - if (allAssignments.at(i)->getVariable() == var) { + if (allAssignments.at(i)->getLValue() == lValue) { return i; } } diff --git a/src/storm/storage/jani/OrderedAssignments.h b/src/storm/storage/jani/OrderedAssignments.h index 45e769920..aa81f59a3 100644 --- a/src/storm/storage/jani/OrderedAssignments.h +++ b/src/storm/storage/jani/OrderedAssignments.h @@ -146,8 +146,8 @@ namespace storm { OrderedAssignments clone() const; private: - uint64_t isReadBeforeAssignment(Variable const& var, uint64_t assignmentNumber, uint64_t start = 0) const; - uint64_t isWrittenBeforeAssignment(Variable const& var, uint64_t assignmentNumber, uint64_t start = 0) const; + uint64_t isReadBeforeAssignment(LValue const& lValue, uint64_t assignmentNumber, uint64_t start = 0) const; + uint64_t isWrittenBeforeAssignment(LValue const& LValue, uint64_t assignmentNumber, uint64_t start = 0) const; /*! * Gets the number of assignments number with an assignment not higher than index. diff --git a/src/storm/storage/jani/TemplateEdge.cpp b/src/storm/storage/jani/TemplateEdge.cpp index 6e5af6695..460e6add3 100644 --- a/src/storm/storage/jani/TemplateEdge.cpp +++ b/src/storm/storage/jani/TemplateEdge.cpp @@ -1,6 +1,7 @@ #include "storm/storage/jani/TemplateEdge.h" #include "storm/storage/jani/Model.h" +#include "storm/storage/jani/LValue.h" #include "storm/storage/expressions/LinearityCheckVisitor.h" @@ -27,8 +28,9 @@ namespace storm { void TemplateEdge::finalize(Model const& containingModel) { for (auto const& destination : getDestinations()) { for (auto const& assignment : destination.getOrderedAssignments().getAllAssignments()) { - if (containingModel.getGlobalVariables().hasVariable(assignment.getExpressionVariable())) { - writtenGlobalVariables.insert(assignment.getExpressionVariable()); + Variable const& var = assignment.getLValue().isVariable() ? assignment.getLValue().getVariable() : assignment.getLValue().getArray(); + if (containingModel.getGlobalVariables().hasVariable(var.getExpressionVariable())) { + writtenGlobalVariables.insert(var.getExpressionVariable()); } } } diff --git a/src/storm/storage/jani/VariableSet.cpp b/src/storm/storage/jani/VariableSet.cpp index ac692c637..973630a2c 100644 --- a/src/storm/storage/jani/VariableSet.cpp +++ b/src/storm/storage/jani/VariableSet.cpp @@ -44,6 +44,14 @@ namespace storm { return detail::ConstVariables(realVariables.begin(), realVariables.end()); } + detail::Variables VariableSet::getArrayVariables() { + return detail::Variables(arrayVariables.begin(), arrayVariables.end()); + } + + detail::ConstVariables VariableSet::getArrayVariables() const { + return detail::ConstVariables(arrayVariables.begin(), arrayVariables.end()); + } + Variable const& VariableSet::addVariable(Variable const& variable) { if (variable.isBooleanVariable()) { return addVariable(variable.asBooleanVariable()); @@ -53,6 +61,8 @@ namespace storm { return addVariable(variable.asUnboundedIntegerVariable()); } else if (variable.isRealVariable()) { return addVariable(variable.asRealVariable()); + } else if (variable.isArrayVariable()) { + return addVariable(variable.asArrayVariable()); } STORM_LOG_THROW(false, storm::exceptions::InvalidTypeException, "Cannot add variable of unknown type."); } @@ -109,6 +119,19 @@ namespace storm { return *newVariable; } + ArrayVariable const& VariableSet::addVariable(ArrayVariable const& variable) { + STORM_LOG_THROW(!this->hasVariable(variable.getName()), storm::exceptions::WrongFormatException, "Cannot add variable with name '" << variable.getName() << "', because a variable with that name already exists."); + std::shared_ptr newVariable = std::make_shared(variable); + variables.push_back(newVariable); + arrayVariables.push_back(newVariable); + if (variable.isTransient()) { + transientVariables.push_back(newVariable); + } + nameToVariable.emplace(variable.getName(), variable.getExpressionVariable()); + variableToVariable.emplace(variable.getExpressionVariable(), newVariable); + return *newVariable; + } + bool VariableSet::hasVariable(std::string const& name) const { return nameToVariable.find(name) != nameToVariable.end(); } @@ -174,6 +197,10 @@ namespace storm { return !realVariables.empty(); } + bool VariableSet::containsArrayVariables() const { + return !arrayVariables.empty(); + } + bool VariableSet::containsNonTransientRealVariables() const { for (auto const& variable : realVariables) { if (!variable->isTransient()) { @@ -193,7 +220,7 @@ namespace storm { } bool VariableSet::empty() const { - return !(containsBooleanVariable() || containsBoundedIntegerVariable() || containsUnboundedIntegerVariables()); + return !(containsBooleanVariable() || containsBoundedIntegerVariable() || containsUnboundedIntegerVariables() || containsRealVariables() || containsArrayVariables()); } uint_fast64_t VariableSet::getNumberOfTransientVariables() const { @@ -251,6 +278,22 @@ namespace storm { return true; } } + for (auto const& arrayVariable : this->getArrayVariables()) { + if (arrayVariable.hasInitExpression()) { + if (arrayVariable.getInitExpression().containsVariable(variables)) { + return true; + } + } + if (arrayVariable.hasElementTypeBounds()) { + auto const& bounds = arrayVariable.getElementTypeBounds(); + if (bounds.first.containsVariable(variables)) { + return true; + } + if (bounds.second.containsVariable(variables)) { + return true; + } + } + } return false; } diff --git a/src/storm/storage/jani/VariableSet.h b/src/storm/storage/jani/VariableSet.h index 6d101ad7a..9940d37a2 100644 --- a/src/storm/storage/jani/VariableSet.h +++ b/src/storm/storage/jani/VariableSet.h @@ -9,6 +9,7 @@ #include "storm/storage/jani/UnboundedIntegerVariable.h" #include "storm/storage/jani/BoundedIntegerVariable.h" #include "storm/storage/jani/RealVariable.h" +#include "storm/storage/jani/ArrayVariable.h" namespace storm { namespace jani { @@ -67,6 +68,16 @@ namespace storm { * Retrieves the real variables in this set. */ detail::ConstVariables getRealVariables() const; + + /*! + * Retrieves the Array variables in this set. + */ + detail::Variables getArrayVariables(); + + /*! + * Retrieves the Array variables in this set. + */ + detail::ConstVariables getArrayVariables() const; /*! * Adds the given variable to this set. @@ -93,6 +104,11 @@ namespace storm { */ RealVariable const& addVariable(RealVariable const& variable); + /*! + * Adds the given real variable to this set. + */ + ArrayVariable const& addVariable(ArrayVariable const& variable); + /*! * Retrieves whether this variable set contains a variable with the given name. */ @@ -162,6 +178,11 @@ namespace storm { */ bool containsRealVariables() const; + /*! + * Retrieves whether the set of variables contains a Array variable. + */ + bool containsArrayVariables() const; + /*! * Retrieves whether the set of variables contains a non-transient real variable. */ @@ -224,6 +245,9 @@ namespace storm { /// The real variables in this set. std::vector> realVariables; + /// The array variables in this set. + std::vector> arrayVariables; + /// The transient variables in this set. std::vector> transientVariables; diff --git a/src/storm/storage/jani/traverser/ArrayEliminator.cpp b/src/storm/storage/jani/traverser/ArrayEliminator.cpp new file mode 100644 index 000000000..2acce661b --- /dev/null +++ b/src/storm/storage/jani/traverser/ArrayEliminator.cpp @@ -0,0 +1,100 @@ +#include "storm/storage/jani/traverser/ArrayEliminator.h" + + +#include "storm/storage/expressions/ExpressionVisitor.h" +#include "storm/storage/jani/expressions/JaniExpressionVisitor.h" + +namespace storm { + namespace jani { + namespace detail { +/* + + + class MaxArraySizeVisitor : public ExpressionVisitor, public JaniExpressionVisitor { + virtual MaxArraySizeVisitor() = default; + virtual ~MaxArraySizeVisitor() = default; + + std::size_t getMaxSize(Expression const& expression) { + return boost::any_cast expression.accept(*this); + } + + virtual boost::any visit(IfThenElseExpression const& expression, boost::any const& data) override { + + } + + virtual boost::any visit(BinaryBooleanFunctionExpression const& expression, boost::any const& data) override { + + } + + virtual boost::any visit(BinaryNumericalFunctionExpression const& expression, boost::any const& data) override { + + } + + virtual boost::any visit(BinaryRelationExpression const& expression, boost::any const& data) override { + + } + + virtual boost::any visit(VariableExpression const& expression, boost::any const& data) override { + + } + + virtual boost::any visit(UnaryBooleanFunctionExpression const& expression, boost::any const& data) override { + + } + + virtual boost::any visit(UnaryNumericalFunctionExpression const& expression, boost::any const& data) override { + + } + + virtual boost::any visit(BooleanLiteralExpression const& expression, boost::any const& data) override { + + } + + virtual boost::any visit(IntegerLiteralExpression const& expression, boost::any const& data) override { + + } + + virtual boost::any visit(RationalLiteralExpression const& expression, boost::any const& data) override { + + } + + + virtual boost::any visit(ValueArrayExpression const& expression, boost::any const& data) override { + + } + + virtual boost::any visit(ConstructorArrayExpression const& expression, boost::any const& data) override { + + } + + virtual boost::any visit(ArrayAccessExpression const& expression, boost::any const& data) override { + + } + }; + + class ArrayVariableReplacer : public JaniTraverser { + public: + + ArrayVariableReplacer() = default; + virtual ~ArrayVariableReplacer() = default; + std::unordered_map> replace(); + + virtual void traverse(Assignment const& assignment, boost::any const& data) const override; + + private: + void std::unordered_map::getMaxSizes(Model& model); + + }; + + class ArrayAccessLValueReplacer : public JaniTraverser { + } + */ + } + + ArrayEliminator::eliminate(Model& model) { + //auto variableReplacements ArrayVariableReplacer().replace(model) + + } + } +} + diff --git a/src/storm/storage/jani/traverser/ArrayEliminator.h b/src/storm/storage/jani/traverser/ArrayEliminator.h index fcff57b45..775909e1c 100644 --- a/src/storm/storage/jani/traverser/ArrayEliminator.h +++ b/src/storm/storage/jani/traverser/ArrayEliminator.h @@ -8,48 +8,14 @@ namespace storm { namespace jani { class ArrayEliminator { -/* public: + ArrayEliminator() = default; + void eliminate(Model& model); private: - class ArrayVariableReplacer : public JaniTraverser { - public: - - ArrayVariableReplacer() = default; - virtual ~ArrayVariableReplacer() = default; - std::unordered_map> replace(); - - virtual void traverse(Assignment const& assignment, boost::any const& data) const override; - - private: - void std::unordered_map::getMaxSizes(Model& model); - - }; - - - - }; - - : public JaniTraverser { - public: - - struct ResultType { - bool hasLocationAssignment, hasEdgeAssignment, hasEdgeDestinationAssignment; - }; - - AssignmentsFinder() = default; - - ResultType find(Model const& model, Variable const& variable); - - virtual ~AssignmentsFinder() = default; - - virtual void traverse(Location const& location, boost::any const& data) const override; - virtual void traverse(TemplateEdge const& templateEdge, boost::any const& data) const override; - virtual void traverse(TemplateEdgeDestination const& templateEdgeDestination, boost::any const& data) const override; - */ }; } }