From a03a7a4ea833d3adc649c1e7ce32fec58582ae83 Mon Sep 17 00:00:00 2001
From: sjunges <sebastian.junges@gmail.com>
Date: Thu, 9 Feb 2017 09:43:07 +0100
Subject: [PATCH] towards simplifying levels by preliminary support in ordered
 assignments

---
 src/storm/storage/jani/OrderedAssignments.cpp | 53 ++++++++++++++++++-
 src/storm/storage/jani/OrderedAssignments.h   | 20 +++++++
 2 files changed, 71 insertions(+), 2 deletions(-)

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<Assignment> 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<std::shared_ptr<Assignment>>::const_iterator OrderedAssignments::lowerBound(Assignment const& assignment, std::vector<std::shared_ptr<Assignment>> 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<std::vector<std::shared_ptr<Assignment>>>;
@@ -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<std::shared_ptr<Assignment>>::const_iterator lowerBound(Assignment const& assignment, std::vector<std::shared_ptr<Assignment>> const& assignments);
                         
             // The vectors to store the assignments. These need to be ordered at all times.