From 0c2d906b09d085d1d9184b208a4c0677bb35dea4 Mon Sep 17 00:00:00 2001
From: sjunges <sebastian.junges@gmail.com>
Date: Sun, 12 Feb 2017 18:17:33 +0100
Subject: [PATCH] A more accurate version of having multiple levels; seems to
 fix at least one open issue.

---
 src/storm/storage/jani/Edge.cpp               | 1 +
 src/storm/storage/jani/OrderedAssignments.cpp | 2 +-
 src/storm/storage/jani/TemplateEdge.cpp       | 3 +++
 3 files changed, 5 insertions(+), 1 deletion(-)

diff --git a/src/storm/storage/jani/Edge.cpp b/src/storm/storage/jani/Edge.cpp
index 7efa96926..18fb35f4f 100644
--- a/src/storm/storage/jani/Edge.cpp
+++ b/src/storm/storage/jani/Edge.cpp
@@ -107,6 +107,7 @@ namespace storm {
             if(usesAssignmentLevels()) {
                 templateEdge = std::make_shared<TemplateEdge>(templateEdge->simplifyIndexedAssignments(!hasSilentAction(), localVars));
                 std::vector<EdgeDestination> newdestinations;
+                assert(templateEdge->getNumberOfDestinations() == destinations.size());
                 for (uint64_t i = 0; i < templateEdge->getNumberOfDestinations(); ++i) {
                     auto const& templateDestination = templateEdge->getDestination(i);
                     newdestinations.emplace_back(destinations[i].getLocationIndex(), destinations[i].getProbability(), templateDestination);
diff --git a/src/storm/storage/jani/OrderedAssignments.cpp b/src/storm/storage/jani/OrderedAssignments.cpp
index b9ea30beb..99eb415a8 100644
--- a/src/storm/storage/jani/OrderedAssignments.cpp
+++ b/src/storm/storage/jani/OrderedAssignments.cpp
@@ -74,7 +74,7 @@ namespace storm {
             if (allAssignments.empty()) {
                 return false;
             }
-            return getLowestLevel() != getHighestLevel();
+            return getLowestLevel() != 0 || getHighestLevel() != 0;
         }
         
         bool OrderedAssignments::empty() const {
diff --git a/src/storm/storage/jani/TemplateEdge.cpp b/src/storm/storage/jani/TemplateEdge.cpp
index a788685f8..959b7b7d1 100644
--- a/src/storm/storage/jani/TemplateEdge.cpp
+++ b/src/storm/storage/jani/TemplateEdge.cpp
@@ -133,6 +133,9 @@ namespace storm {
         }
         
         bool TemplateEdge::usesAssignmentLevels() const {
+            if (assignments.hasMultipleLevels()) {
+                return true;
+            }
             for (auto const& destination : this->getDestinations()) {
                 if (destination.usesAssignmentLevels()) {
                     return true;