support for negative assignment levels

src/storm-parsers/parser/JaniParser.cpp

@@ -61,6 +61,12 @@ namespace storm {
             return static_cast<uint64_t>(num);
         }
 
+        int64_t getSignedInt(json const& structure, std::string const& errorInfo) {
+            STORM_LOG_THROW(structure.is_number(), storm::exceptions::InvalidJaniException, "Expected a number in " << errorInfo << ", got '" << structure.dump() << "'");
+            int num = structure.front();
+            return static_cast<int64_t>(num);
+        }
+
 
         std::pair<storm::jani::Model, std::map<std::string, storm::jani::Property>> JaniParser::parse(std::string const& path) {
             JaniParser parser;
@@ -1313,9 +1319,9 @@ namespace storm {
                             storm::expressions::Expression assignmentExpr = parseExpression(assignmentEntry.at("value"), "assignment in edge from '" + sourceLoc + "' to '" + targetLoc + "' in automaton '" + name + "'",  globalVars, constants, localVars);
                             // TODO check types
                             // index
-                            uint64_t assignmentIndex = 0; // default.
+                            int64_t assignmentIndex = 0; // default.
                             if(assignmentEntry.count("index") > 0) {
-                                assignmentIndex = getUnsignedInt(assignmentEntry.at("index"), "assignment index in edge from '" + sourceLoc + "' to '" + targetLoc + "' in automaton '" + name + "'");
+                                assignmentIndex = getSignedInt(assignmentEntry.at("index"), "assignment index in edge from '" + sourceLoc + "' to '" + targetLoc + "' in automaton '" + name + "'");
                             }
                             assignments.emplace_back(lValue, assignmentExpr, assignmentIndex);
                         }

src/storm/generator/JaniNextStateGenerator.cpp

@@ -53,7 +53,7 @@ namespace storm {
             STORM_LOG_THROW(features.empty(), storm::exceptions::InvalidSettingsException, "The explicit next-state generator does not support the following model feature(s): " << features.toString() << ".");
 
             // Lift the transient edge destinations of the first assignment level.
-            uint64_t lowestAssignmentLevel = storm::jani::AssignmentLevelFinder().getLowestAssignmentLevel(this->model);
+            int64_t lowestAssignmentLevel = storm::jani::AssignmentLevelFinder().getLowestAssignmentLevel(this->model);
             if (this->model.hasTransientEdgeDestinationAssignments()) {
                 this->model.liftTransientEdgeDestinationAssignments(lowestAssignmentLevel);
                 if (this->model.hasTransientEdgeDestinationAssignments()) {
@@ -251,25 +251,20 @@ namespace storm {
         }
         
         template<typename ValueType, typename StateType>
-        CompressedState JaniNextStateGenerator<ValueType, StateType>::applyUpdate(CompressedState const& state, storm::jani::EdgeDestination const& destination, storm::generator::LocationVariableInformation const& locationVariable, uint64_t assignmentLevel, storm::expressions::ExpressionEvaluator<ValueType> const& expressionEvaluator) {
+        CompressedState JaniNextStateGenerator<ValueType, StateType>::applyUpdate(CompressedState const& state, storm::jani::EdgeDestination const& destination, storm::generator::LocationVariableInformation const& locationVariable, int64_t assignmentLevel, storm::expressions::ExpressionEvaluator<ValueType> const& expressionEvaluator) {
             CompressedState newState(state);
             
             // Update the location of the state.
             setLocation(newState, locationVariable, destination.getLocationIndex());
             
             // Then perform the assignments.
-            auto assignmentIt = destination.getOrderedAssignments().getNonTransientAssignments().begin();
-            auto assignmentIte = destination.getOrderedAssignments().getNonTransientAssignments().end();
-            
-            if (assignmentLevel > 0) {
-                while (assignmentIt != assignmentIte && assignmentIt->getLevel() < assignmentLevel) {
-                    ++assignmentIt;
-                }
-            }
+            auto const& assignments = destination.getOrderedAssignments().getNonTransientAssignments(assignmentLevel);
+            auto assignmentIt = assignments.begin();
+            auto assignmentIte = assignments.end();
             
             // Iterate over all boolean assignments and carry them out.
             auto boolIt = this->variableInformation.booleanVariables.begin();
-            for (; assignmentIt != assignmentIte && assignmentIt->getAssignedExpression().hasBooleanType() && assignmentIt->getLevel() == assignmentLevel && assignmentIt->getLValue().isVariable(); ++assignmentIt) {
+            for (; assignmentIt != assignmentIte && assignmentIt->getAssignedExpression().hasBooleanType() && assignmentIt->getLValue().isVariable(); ++assignmentIt) {
                 while (assignmentIt->getExpressionVariable() != boolIt->variable) {
                     ++boolIt;
                 }
@@ -278,7 +273,7 @@ namespace storm {
             
             // Iterate over all integer assignments and carry them out.
             auto integerIt = this->variableInformation.integerVariables.begin();
-            for (; assignmentIt != assignmentIte && assignmentIt->getAssignedExpression().hasIntegerType() && assignmentIt->getLevel() == assignmentLevel && assignmentIt->getLValue().isVariable(); ++assignmentIt) {
+            for (; assignmentIt != assignmentIte && assignmentIt->getAssignedExpression().hasIntegerType() && assignmentIt->getLValue().isVariable(); ++assignmentIt) {
                 while (assignmentIt->getExpressionVariable() != integerIt->variable) {
                     ++integerIt;
                 }
@@ -296,7 +291,7 @@ namespace storm {
                 STORM_LOG_ASSERT(static_cast<int_fast64_t>(newState.getAsInt(integerIt->bitOffset, integerIt->bitWidth)) + integerIt->lowerBound == assignedValue, "Writing to the bit vector bucket failed (read " << newState.getAsInt(integerIt->bitOffset, integerIt->bitWidth) << " but wrote " << assignedValue << ").");
             }
             // Iterate over all array access assignments and carry them out.
-            for (; assignmentIt != assignmentIte && assignmentIt->getLValue().isArrayAccess() && assignmentIt->getLevel() == assignmentLevel; ++assignmentIt) {
+            for (; assignmentIt != assignmentIte && assignmentIt->getLValue().isArrayAccess(); ++assignmentIt) {
                 int_fast64_t arrayIndex = expressionEvaluator.asInt(assignmentIt->getLValue().getArrayIndex());
                 if (assignmentIt->getAssignedExpression().hasIntegerType()) {
                     IntegerVariableInformation const& intInfo = this->variableInformation.getIntegerArrayVariableReplacement(assignmentIt->getLValue().getArray().getExpressionVariable(), arrayIndex);
@@ -320,7 +315,7 @@ namespace storm {
             }
             
             // Check that we processed all assignments.
-            STORM_LOG_ASSERT(assignmentIt == assignmentIte || assignmentIt->getLevel() > assignmentLevel, "Not all assignments were consumed.");
+            STORM_LOG_ASSERT(assignmentIt == assignmentIte, "Not all assignments were consumed.");
             return newState;
         }
         
@@ -439,8 +434,8 @@ namespace storm {
                 if (probability != storm::utility::zero<ValueType>()) {
                     // Obtain target state index and add it to the list of known states. If it has not yet been
                     // seen, we also add it to the set of states that have yet to be explored.
-                    uint64_t assignmentLevel = edge.getLowestAssignmentLevel(); // Might be the largest possible integer, if there is no assignment
-                    uint64_t const& highestLevel = edge.getHighestAssignmentLevel();
+                    int64_t assignmentLevel = edge.getLowestAssignmentLevel(); // Might be the largest possible integer, if there is no assignment
+                    int64_t const& highestLevel = edge.getHighestAssignmentLevel();
                     bool hasTransientRewardAssignments = destination.hasTransientAssignment();
                     CompressedState newState = applyUpdate(state, destination, this->variableInformation.locationVariables[automatonIndex], assignmentLevel, *this->evaluator);
                     if (hasTransientRewardAssignments) {
@@ -514,8 +509,8 @@ namespace storm {
                 nextDistribution.clear();
                 
                 EdgeIndexSet edgeIndices;
-                uint64_t assignmentLevel = std::numeric_limits<uint64_t>::max();
-                uint64_t highestLevel = 0;
+                int64_t assignmentLevel = std::numeric_limits<uint64_t>::max();
+                int64_t highestLevel = std::numeric_limits<uint64_t>::min();
                 for (uint_fast64_t i = 0; i < iteratorList.size(); ++i) {
                     if (this->getOptions().isBuildChoiceOriginsSet()) {
                         edgeIndices.insert(model.encodeAutomatonAndEdgeIndices(edgeCombination[i].first, iteratorList[i]->first));

src/storm/generator/JaniNextStateGenerator.h

@@ -70,7 +70,7 @@ namespace storm {
              * @params assignmentLevel The assignmentLevel that is to be considered for the update.
              * @return The resulting state.
              */
-            CompressedState applyUpdate(CompressedState const& state, storm::jani::EdgeDestination const& update, storm::generator::LocationVariableInformation const& locationVariable, uint64_t assignmentlevel, storm::expressions::ExpressionEvaluator<ValueType> const& expressionEvaluator);
+            CompressedState applyUpdate(CompressedState const& state, storm::jani::EdgeDestination const& update, storm::generator::LocationVariableInformation const& locationVariable, int64_t assignmentlevel, storm::expressions::ExpressionEvaluator<ValueType> const& expressionEvaluator);
             
             /*!
              * Retrieves all choices possible from the given state.

src/storm/storage/jani/Assignment.cpp

@@ -11,7 +11,7 @@
 namespace storm  {
     namespace jani {
         
-        Assignment::Assignment(storm::jani::LValue const& lValue, storm::expressions::Expression const& expression, uint64_t level) : lValue(lValue), expression(expression), level(level) {
+        Assignment::Assignment(storm::jani::LValue const& lValue, storm::expressions::Expression const& expression, int64_t level) : lValue(lValue), expression(expression), level(level) {
             // Intentionally left empty
         }
         

src/storm/storage/jani/Assignment.h

@@ -13,7 +13,7 @@ namespace storm {
             /*!
              * Creates an assignment of the given expression to the given LValue.
              */
-            Assignment(storm::jani::LValue const& lValue, storm::expressions::Expression const& expression, uint64_t index = 0);
+            Assignment(storm::jani::LValue const& lValue, storm::expressions::Expression const& expression, int64_t level = 0);
 
             Assignment(Assignment const&) = default;
             bool operator==(Assignment const& other) const;
@@ -96,7 +96,7 @@ namespace storm {
             storm::expressions::Expression expression;
             
             // The level of the assignment.
-            uint64_t level;
+            int64_t level;
         };
         
         /*!

src/storm/storage/jani/Automaton.cpp

@@ -478,7 +478,7 @@ namespace storm {
             return false;
         }
         
-        void Automaton::liftTransientEdgeDestinationAssignments(uint64_t maxLevel) {
+        void Automaton::liftTransientEdgeDestinationAssignments(int64_t maxLevel) {
             edges.liftTransientDestinationAssignments(maxLevel);
         }
 

src/storm/storage/jani/Automaton.h

@@ -325,7 +325,7 @@ namespace storm {
             /*!
              * Lifts the common edge destination assignments to edge assignments.
              */
-            void liftTransientEdgeDestinationAssignments(uint64_t maxLevel = 0);
+            void liftTransientEdgeDestinationAssignments(int64_t maxLevel = 0);
             
             /*!
              * Retrieves whether the automaton uses an assignment level other than zero.

src/storm/storage/jani/Edge.cpp

@@ -121,11 +121,11 @@ namespace storm {
             }
         }
 
-        uint64_t const& Edge::getLowestAssignmentLevel() const {
+        int64_t const& Edge::getLowestAssignmentLevel() const {
             return templateEdge->getLowestAssignmentLevel();
         }
 
-        uint64_t const& Edge::getHighestAssignmentLevel() const {
+        int64_t const& Edge::getHighestAssignmentLevel() const {
             return templateEdge->getHighestAssignmentLevel();
         }
         

src/storm/storage/jani/Edge.h

@@ -123,13 +123,13 @@ namespace storm {
              * Retrieves the lowest assignment level occurring in each assignment.
              * If no assignment exists, this value is the highest possible integer
              */
-            uint64_t const& getLowestAssignmentLevel() const;
+            int64_t const& getLowestAssignmentLevel() const;
             
             /*!
              * Retrieves the highest assignment level occurring in each assignment
              * If no assignment exists, this value is always zero
              */
-            uint64_t const& getHighestAssignmentLevel() const;
+            int64_t const& getHighestAssignmentLevel() const;
             
 
             void assertValid() const;

src/storm/storage/jani/EdgeContainer.cpp

@@ -86,7 +86,7 @@ namespace storm {
             edges.clear();
         }
 
-        void EdgeContainer::liftTransientDestinationAssignments(uint64_t maxLevel) {
+        void EdgeContainer::liftTransientDestinationAssignments(int64_t maxLevel) {
             for (auto& templateEdge : templates) {
                 templateEdge->liftTransientDestinationAssignments(maxLevel);
             }

src/storm/storage/jani/EdgeContainer.h

@@ -107,7 +107,7 @@ namespace storm {
             std::set<uint64_t> getActionIndices() const;
 
             void substitute(std::map<storm::expressions::Variable, storm::expressions::Expression> const& substitution);
-            void liftTransientDestinationAssignments(uint64_t maxLevel = 0);
+            void liftTransientDestinationAssignments(int64_t maxLevel = 0);
             void pushAssignmentsToDestinations();
             void insertEdge(Edge const& e, uint64_t locStart, uint64_t locEnd);
             void insertTemplateEdge(std::shared_ptr<TemplateEdge> const& te);

src/storm/storage/jani/Model.cpp

@@ -1180,7 +1180,7 @@ namespace storm {
             }
         }
         
-        void Model::liftTransientEdgeDestinationAssignments(uint64_t maxLevel) {
+        void Model::liftTransientEdgeDestinationAssignments(int64_t maxLevel) {
             for (auto& automaton : this->getAutomata()) {
                 automaton.liftTransientEdgeDestinationAssignments(maxLevel);
             }

src/storm/storage/jani/Model.h

@@ -478,7 +478,7 @@ namespace storm {
              * Lifts the common edge destination assignments to edge assignments.
              * @param maxLevel the maximum level of assignments that are to be lifted.
              */
-            void liftTransientEdgeDestinationAssignments(uint64_t maxLevel = 0);
+            void liftTransientEdgeDestinationAssignments(int64_t maxLevel = 0);
             
             /*!
              * Retrieves whether there is any transient edge destination assignment in the model.

src/storm/storage/jani/OrderedAssignments.cpp

@@ -101,13 +101,13 @@ namespace storm {
             return allAssignments.size();
         }
         
-        int_fast64_t OrderedAssignments::getLowestLevel(bool onlyTransient) const {
+        int64_t OrderedAssignments::getLowestLevel(bool onlyTransient) const {
             auto const& as = onlyTransient ? transientAssignments : allAssignments;
             assert(!as.empty());
             return as.front()->getLevel();
         }
         
-        int_fast64_t OrderedAssignments::getHighestLevel(bool onlyTransient) const {
+        int64_t OrderedAssignments::getHighestLevel(bool onlyTransient) const {
             auto const& as = onlyTransient ? transientAssignments : allAssignments;
             assert(!as.empty());
             return as.back()->getLevel();
@@ -198,15 +198,24 @@ namespace storm {
             return detail::ConstAssignments(nonTransientAssignments.begin(), nonTransientAssignments.end());
         }
         
-        detail::ConstAssignments OrderedAssignments::getTransientAssignments(int_fast64_t assignmentLevel) const {
-            auto begin = transientAssignments.begin();
-            while (begin != transientAssignments.end() && (*begin)->getLevel() < assignmentLevel) {
-                ++begin;
+        struct AssignmentLevelToLevelComparator {
+            bool operator()(std::shared_ptr<Assignment> const& left, int64_t const& right) const {
+                return left->getLevel() < right;
             }
-            auto end = begin;
-            while (end != transientAssignments.end() && (*begin)->getLevel() == assignmentLevel) {
-                ++end;
+            bool operator()(int64_t const& left, std::shared_ptr<Assignment> const& right) const {
+                return left < right->getLevel();
             }
+        };
+        
+        detail::ConstAssignments OrderedAssignments::getTransientAssignments(int64_t assignmentLevel) const {
+            auto begin = std::lower_bound(transientAssignments.begin(), transientAssignments.end(), assignmentLevel, AssignmentLevelToLevelComparator());
+            auto end = std::upper_bound(begin, transientAssignments.end(), assignmentLevel, AssignmentLevelToLevelComparator());
+            return detail::ConstAssignments(begin, end);
+        }
+        
+        detail::ConstAssignments OrderedAssignments::getNonTransientAssignments(int64_t assignmentLevel) const {
+            auto begin = std::lower_bound(nonTransientAssignments.begin(), nonTransientAssignments.end(), assignmentLevel, AssignmentLevelToLevelComparator());
+            auto end = std::upper_bound(begin, nonTransientAssignments.end(), assignmentLevel, AssignmentLevelToLevelComparator());
             return detail::ConstAssignments(begin, end);
         }
         
@@ -247,7 +256,7 @@ 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::AssignmentPartialOrderByLevelAndLValue());
         }
-
+        
         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

src/storm/storage/jani/OrderedAssignments.h

@@ -73,13 +73,13 @@ namespace storm {
              * Retrieves the lowest level among all assignments. Note that this may only be called if there is at least
              * one assignment.
              */
-            int_fast64_t getLowestLevel(bool onlyTransient = false) const;
+            int64_t getLowestLevel(bool onlyTransient = false) const;
 
             /*!
              * Retrieves the highest level among all assignments. Note that this may only be called if there is at least
              * one assignment.
              */
-            int_fast64_t getHighestLevel(bool onlyTransient = false) const;
+            int64_t getHighestLevel(bool onlyTransient = false) const;
 
             /*!
              * Retrieves whether the given assignment is contained in this set of assignments.
@@ -99,12 +99,17 @@ namespace storm {
             /*!
              * Returns all transient assignments in this set of assignments.
              */
-            detail::ConstAssignments getTransientAssignments(int_fast64_t assignmentLevel) const;
+            detail::ConstAssignments getTransientAssignments(int64_t assignmentLevel) const;
 
             /*!
              * Returns all non-transient assignments in this set of assignments.
              */
             detail::ConstAssignments getNonTransientAssignments() const;
+            
+            /*!
+             * Returns all non-transient assignments in this set of assignments.
+             */
+            detail::ConstAssignments getNonTransientAssignments(int64_t assignmentLevel) const;
 
             /*!
              * Retrieves whether the set of assignments has at least one transient assignment.
@@ -167,7 +172,7 @@ namespace storm {
             uint64_t upperBound(int64_t index) const;
 
             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.
             std::vector<std::shared_ptr<Assignment>> allAssignments;
             std::vector<std::shared_ptr<Assignment>> transientAssignments;

src/storm/storage/jani/TemplateEdge.cpp

@@ -9,12 +9,12 @@
 namespace storm {
     namespace jani {
         
-        TemplateEdge::TemplateEdge(storm::expressions::Expression const& guard) : guard(guard), lowestAssignmentLevel(std::numeric_limits<uint64_t>::max()), highestAssignmentLevel(0) {
+        TemplateEdge::TemplateEdge(storm::expressions::Expression const& guard) : guard(guard), lowestAssignmentLevel(std::numeric_limits<int64_t>::max()), highestAssignmentLevel(std::numeric_limits<int64_t>::min()) {
             // Intentionally left empty.
         }
 
         TemplateEdge::TemplateEdge(storm::expressions::Expression const& guard, OrderedAssignments const& assignments, std::vector<TemplateEdgeDestination> const& destinations)
-                : guard(guard), destinations(destinations), assignments(assignments), lowestAssignmentLevel(std::numeric_limits<uint64_t>::max()), highestAssignmentLevel(0) {
+                : guard(guard), destinations(destinations), assignments(assignments), lowestAssignmentLevel(std::numeric_limits<int64_t>::max()), highestAssignmentLevel(std::numeric_limits<int64_t>::min()) {
             // Intentionally left empty.
         }
         
@@ -28,16 +28,16 @@ namespace storm {
         
         void TemplateEdge::finalize(Model const& containingModel) {
             if (assignments.empty()) {
-                lowestAssignmentLevel = std::numeric_limits<uint64_t>::max();
-                highestAssignmentLevel = 0;
+                lowestAssignmentLevel = std::numeric_limits<int64_t>::max();
+                highestAssignmentLevel = std::numeric_limits<int64_t>::min();
             } else {
                 lowestAssignmentLevel = assignments.getLowestLevel();
                 highestAssignmentLevel = assignments.getHighestLevel();
             }
             for (auto const& destination : getDestinations()) {
                 if (!destination.getOrderedAssignments().empty()) {
-                    lowestAssignmentLevel = std::min<uint64_t>(lowestAssignmentLevel, destination.getOrderedAssignments().getLowestLevel());
-                    highestAssignmentLevel = std::max<uint64_t>(highestAssignmentLevel, destination.getOrderedAssignments().getHighestLevel());
+                    lowestAssignmentLevel = std::min(lowestAssignmentLevel, destination.getOrderedAssignments().getLowestLevel());
+                    highestAssignmentLevel = std::max(highestAssignmentLevel, destination.getOrderedAssignments().getHighestLevel());
                 }
                 for (auto const& assignment : destination.getOrderedAssignments().getAllAssignments()) {
                     Variable const& var = assignment.getLValue().isVariable() ? assignment.getLValue().getVariable() : assignment.getLValue().getArray();
@@ -103,7 +103,7 @@ namespace storm {
             assignments.changeAssignmentVariables(remapping);
         }
 
-        void TemplateEdge::liftTransientDestinationAssignments(uint64_t maxLevel) {
+        void TemplateEdge::liftTransientDestinationAssignments(int64_t maxLevel) {
             if (!destinations.empty()) {
                 auto const& destination = *destinations.begin();
                 
@@ -180,11 +180,11 @@ namespace storm {
             return false;
         }
         
-        uint64_t const& TemplateEdge::getLowestAssignmentLevel() const {
+        int64_t const& TemplateEdge::getLowestAssignmentLevel() const {
             return lowestAssignmentLevel;
         }
         
-        uint64_t const& TemplateEdge::getHighestAssignmentLevel() const {
+        int64_t const& TemplateEdge::getHighestAssignmentLevel() const {
             return highestAssignmentLevel;
         }
 

src/storm/storage/jani/TemplateEdge.h

@@ -69,7 +69,7 @@ namespace storm {
              * assignments are no longer contained in the destination. Note that this may modify the semantics of the
              * model if assignment levels are being used somewhere in the model.
              */
-            void liftTransientDestinationAssignments(uint64_t maxLevel = 0);
+            void liftTransientDestinationAssignments(int64_t maxLevel = 0);
             
             /**
              * Shifts the assingments from the edges to the destinations.
@@ -95,13 +95,13 @@ namespace storm {
              * Retrieves the lowest assignment level occurring in each assignment.
              * If no assignment exists, this value is the highest possible integer
              */
-            uint64_t const& getLowestAssignmentLevel() const;
+            int64_t const& getLowestAssignmentLevel() const;
             
             /*!
              * Retrieves the highest assignment level occurring in each assignment
              * If no assignment exists, this value is always zero
              */
-            uint64_t const& getHighestAssignmentLevel() const;
+            int64_t const& getHighestAssignmentLevel() const;
             
             /*!
              * Checks the template edge for linearity.
@@ -125,7 +125,7 @@ namespace storm {
             /// The assignments made when taking this edge.
             OrderedAssignments assignments;
             
-            uint64_t lowestAssignmentLevel, highestAssignmentLevel;
+            int64_t lowestAssignmentLevel, highestAssignmentLevel;
             
             /// A set of global variables that is written by at least one of the edge's destinations. This set is
             /// initialized by the call to <code>finalize</code>.

src/storm/storage/jani/traverser/AssignmentLevelFinder.cpp

@@ -4,15 +4,15 @@
 namespace storm {
     namespace jani {
         
-        uint64_t AssignmentLevelFinder::getLowestAssignmentLevel(Model const& model) {
-            uint64_t res = std::numeric_limits<uint64_t>::max();
+        int64_t AssignmentLevelFinder::getLowestAssignmentLevel(Model const& model) {
+            int64_t res = std::numeric_limits<int64_t>::max();
             ConstJaniTraverser::traverse(model, &res);
             return res;
         }
         
         void AssignmentLevelFinder::traverse(Assignment const& assignment, boost::any const& data) {
-            auto& res = *boost::any_cast<uint64_t*>(data);
-            res = std::min<uint64_t>(res, assignment.getLevel());
+            auto& res = *boost::any_cast<int64_t*>(data);
+            res = std::min<int64_t>(res, assignment.getLevel());
         }
     }
 }

src/storm/storage/jani/traverser/AssignmentLevelFinder.h

@@ -10,7 +10,7 @@ namespace storm {
             AssignmentLevelFinder() = default;
             virtual ~AssignmentLevelFinder() = default;
             
-            uint64_t getLowestAssignmentLevel(Model const& model);
+            int64_t getLowestAssignmentLevel(Model const& model);
             
             virtual void traverse(Assignment const& assignment, boost::any const& data) override;
         };