diff --git a/src/storm/storage/jani/OrderedAssignments.cpp b/src/storm/storage/jani/OrderedAssignments.cpp index 56657e2ce..3e432dfc8 100644 --- a/src/storm/storage/jani/OrderedAssignments.cpp +++ b/src/storm/storage/jani/OrderedAssignments.cpp @@ -106,7 +106,30 @@ namespace storm { return false; } } - + + OrderedAssignments OrderedAssignments::simplifyLevels(bool synchronous, VariableSet const& localVars) const { + if (!synchronous) { + bool changed = false; + std::vector newAssignments; + for (auto const& assignment : allAssignments) { + newAssignments.push_back(*assignment); + if (!isReadBeforeAssignment(assignment->getVariable(), upperBound(assignment->getLevel() - 1))) { + if (!isWrittenBeforeAssignment(assignment->getVariable(), upperBound(assignment->getLevel()-1))) { + newAssignments.back().setLevel(0); + changed = true; + } + } + } + if (changed) { + return OrderedAssignments(newAssignments).simplifyLevels(synchronous, localVars); + } else { + return *this; + } + } else { + return *this; + } + } + detail::ConstAssignments OrderedAssignments::getAllAssignments() const { return detail::ConstAssignments(allAssignments.begin(), allAssignments.end()); } @@ -156,7 +179,33 @@ namespace storm { std::vector>::const_iterator OrderedAssignments::lowerBound(Assignment const& assignment, std::vector> const& assignments) { return std::lower_bound(assignments.begin(), assignments.end(), assignment, storm::jani::AssignmentPartialOrderByLevelAndVariable()); } - + + bool OrderedAssignments::isReadBeforeAssignment(Variable const& var, uint64_t assignmentNumber, uint64_t start) const { + for (uint64_t i = start; i < assignmentNumber; i++) { + if (allAssignments.at(i)->getAssignedExpression().containsVariable(var.getExpressionVariable())) { + return true; + } + } + } + + bool OrderedAssignments::isWrittenBeforeAssignment(Variable const& var, uint64_t assignmentNumber, uint64_t start) const { + for (uint64_t i = start; i < assignmentNumber; i++) { + if (allAssignments.at(i)->getVariable() == var) { + return true; + } + } + } + + uint64_t OrderedAssignments::upperBound(int64_t index) const { + uint64_t result = 0; + for(auto const& assignment : allAssignments) { + if(assignment->getLevel() > index) { + return result; + } + ++result; + } + } + bool OrderedAssignments::areLinear() const { bool result = true; for (auto const& assignment : getAllAssignments()) { diff --git a/src/storm/storage/jani/OrderedAssignments.h b/src/storm/storage/jani/OrderedAssignments.h index f45206461..97d7e732d 100644 --- a/src/storm/storage/jani/OrderedAssignments.h +++ b/src/storm/storage/jani/OrderedAssignments.h @@ -6,6 +6,8 @@ namespace storm { namespace jani { + + class VariableSet; namespace detail { using Assignments = storm::adapters::DereferenceIteratorAdapter>>; @@ -41,6 +43,14 @@ namespace storm { * @return True if more than one level occurs in the assignment set. */ bool hasMultipleLevels() const; + + /** + * Produces a new OrderedAssignments object with simplified leveling + * @param synchronous + * @param localVars + * @return + */ + OrderedAssignments simplifyLevels(bool synchronous, VariableSet const& localVars) const; /*! * Retrieves whether this set of assignments is empty. @@ -132,6 +142,16 @@ namespace storm { friend std::ostream& operator<<(std::ostream& stream, OrderedAssignments const& assignments); private: + bool isReadBeforeAssignment(Variable const& var, uint64_t assignmentNumber, uint64_t start = 0) const; + bool isWrittenBeforeAssignment(Variable const& var, uint64_t assignmentNumber, uint64_t start = 0) const; + + /*! + * Gets the number of assignments number with an assignment not higher than index. + * @param index The index we are interested in + * @return + */ + uint64_t upperBound(int64_t index); + static std::vector>::const_iterator lowerBound(Assignment const& assignment, std::vector> const& assignments); // The vectors to store the assignments. These need to be ordered at all times.