From d0461f168b13491c39a852ed561cc6f75da16778 Mon Sep 17 00:00:00 2001 From: TimQu Date: Thu, 13 Sep 2018 10:01:54 +0200 Subject: [PATCH] support for negative assignment levels --- src/storm-parsers/parser/JaniParser.cpp | 10 ++++-- .../generator/JaniNextStateGenerator.cpp | 31 ++++++++----------- src/storm/generator/JaniNextStateGenerator.h | 2 +- src/storm/storage/jani/Assignment.cpp | 2 +- src/storm/storage/jani/Assignment.h | 4 +-- src/storm/storage/jani/Automaton.cpp | 2 +- src/storm/storage/jani/Automaton.h | 2 +- src/storm/storage/jani/Edge.cpp | 4 +-- src/storm/storage/jani/Edge.h | 4 +-- src/storm/storage/jani/EdgeContainer.cpp | 2 +- src/storm/storage/jani/EdgeContainer.h | 2 +- src/storm/storage/jani/Model.cpp | 2 +- src/storm/storage/jani/Model.h | 2 +- src/storm/storage/jani/OrderedAssignments.cpp | 29 +++++++++++------ src/storm/storage/jani/OrderedAssignments.h | 13 +++++--- src/storm/storage/jani/TemplateEdge.cpp | 18 +++++------ src/storm/storage/jani/TemplateEdge.h | 8 ++--- .../jani/traverser/AssignmentLevelFinder.cpp | 8 ++--- .../jani/traverser/AssignmentLevelFinder.h | 2 +- 19 files changed, 81 insertions(+), 66 deletions(-) diff --git a/src/storm-parsers/parser/JaniParser.cpp b/src/storm-parsers/parser/JaniParser.cpp index c21add9e7..63423299d 100644 --- a/src/storm-parsers/parser/JaniParser.cpp +++ b/src/storm-parsers/parser/JaniParser.cpp @@ -61,6 +61,12 @@ namespace storm { return static_cast(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(num); + } + std::pair> 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); } diff --git a/src/storm/generator/JaniNextStateGenerator.cpp b/src/storm/generator/JaniNextStateGenerator.cpp index 8575f3a7d..bd034ece7 100644 --- a/src/storm/generator/JaniNextStateGenerator.cpp +++ b/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 - CompressedState JaniNextStateGenerator::applyUpdate(CompressedState const& state, storm::jani::EdgeDestination const& destination, storm::generator::LocationVariableInformation const& locationVariable, uint64_t assignmentLevel, storm::expressions::ExpressionEvaluator const& expressionEvaluator) { + CompressedState JaniNextStateGenerator::applyUpdate(CompressedState const& state, storm::jani::EdgeDestination const& destination, storm::generator::LocationVariableInformation const& locationVariable, int64_t assignmentLevel, storm::expressions::ExpressionEvaluator 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(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()) { // 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::max(); - uint64_t highestLevel = 0; + int64_t assignmentLevel = std::numeric_limits::max(); + int64_t highestLevel = std::numeric_limits::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)); diff --git a/src/storm/generator/JaniNextStateGenerator.h b/src/storm/generator/JaniNextStateGenerator.h index e9bd01a07..f84665db1 100644 --- a/src/storm/generator/JaniNextStateGenerator.h +++ b/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 const& expressionEvaluator); + CompressedState applyUpdate(CompressedState const& state, storm::jani::EdgeDestination const& update, storm::generator::LocationVariableInformation const& locationVariable, int64_t assignmentlevel, storm::expressions::ExpressionEvaluator const& expressionEvaluator); /*! * Retrieves all choices possible from the given state. diff --git a/src/storm/storage/jani/Assignment.cpp b/src/storm/storage/jani/Assignment.cpp index 0632f294d..3235eacfe 100644 --- a/src/storm/storage/jani/Assignment.cpp +++ b/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 } diff --git a/src/storm/storage/jani/Assignment.h b/src/storm/storage/jani/Assignment.h index f2a18c8a9..ac616cd39 100644 --- a/src/storm/storage/jani/Assignment.h +++ b/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; }; /*! diff --git a/src/storm/storage/jani/Automaton.cpp b/src/storm/storage/jani/Automaton.cpp index b9c1e6449..14a1e7b2f 100644 --- a/src/storm/storage/jani/Automaton.cpp +++ b/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); } diff --git a/src/storm/storage/jani/Automaton.h b/src/storm/storage/jani/Automaton.h index abd459735..c6422fb1a 100644 --- a/src/storm/storage/jani/Automaton.h +++ b/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. diff --git a/src/storm/storage/jani/Edge.cpp b/src/storm/storage/jani/Edge.cpp index cbe78c699..240317817 100644 --- a/src/storm/storage/jani/Edge.cpp +++ b/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(); } diff --git a/src/storm/storage/jani/Edge.h b/src/storm/storage/jani/Edge.h index d47edf14f..c6ab6d28d 100644 --- a/src/storm/storage/jani/Edge.h +++ b/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; diff --git a/src/storm/storage/jani/EdgeContainer.cpp b/src/storm/storage/jani/EdgeContainer.cpp index 83db856ad..f2e3b9855 100644 --- a/src/storm/storage/jani/EdgeContainer.cpp +++ b/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); } diff --git a/src/storm/storage/jani/EdgeContainer.h b/src/storm/storage/jani/EdgeContainer.h index 550fc80e0..bf1e0cbe9 100644 --- a/src/storm/storage/jani/EdgeContainer.h +++ b/src/storm/storage/jani/EdgeContainer.h @@ -107,7 +107,7 @@ namespace storm { std::set getActionIndices() const; void substitute(std::map 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 const& te); diff --git a/src/storm/storage/jani/Model.cpp b/src/storm/storage/jani/Model.cpp index a02a919eb..d84762fc7 100644 --- a/src/storm/storage/jani/Model.cpp +++ b/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); } diff --git a/src/storm/storage/jani/Model.h b/src/storm/storage/jani/Model.h index 6bce3603d..274d17490 100644 --- a/src/storm/storage/jani/Model.h +++ b/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. diff --git a/src/storm/storage/jani/OrderedAssignments.cpp b/src/storm/storage/jani/OrderedAssignments.cpp index 8b46a3d7a..747fbcecd 100644 --- a/src/storm/storage/jani/OrderedAssignments.cpp +++ b/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 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 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>::const_iterator OrderedAssignments::lowerBound(Assignment const& assignment, std::vector> 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 diff --git a/src/storm/storage/jani/OrderedAssignments.h b/src/storm/storage/jani/OrderedAssignments.h index 4d15268e7..de914b738 100644 --- a/src/storm/storage/jani/OrderedAssignments.h +++ b/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>::const_iterator lowerBound(Assignment const& assignment, std::vector> const& assignments); - + // The vectors to store the assignments. These need to be ordered at all times. std::vector> allAssignments; std::vector> transientAssignments; diff --git a/src/storm/storage/jani/TemplateEdge.cpp b/src/storm/storage/jani/TemplateEdge.cpp index a1ea3f7b5..51fee6578 100644 --- a/src/storm/storage/jani/TemplateEdge.cpp +++ b/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::max()), highestAssignmentLevel(0) { + TemplateEdge::TemplateEdge(storm::expressions::Expression const& guard) : guard(guard), lowestAssignmentLevel(std::numeric_limits::max()), highestAssignmentLevel(std::numeric_limits::min()) { // Intentionally left empty. } TemplateEdge::TemplateEdge(storm::expressions::Expression const& guard, OrderedAssignments const& assignments, std::vector const& destinations) - : guard(guard), destinations(destinations), assignments(assignments), lowestAssignmentLevel(std::numeric_limits::max()), highestAssignmentLevel(0) { + : guard(guard), destinations(destinations), assignments(assignments), lowestAssignmentLevel(std::numeric_limits::max()), highestAssignmentLevel(std::numeric_limits::min()) { // Intentionally left empty. } @@ -28,16 +28,16 @@ namespace storm { void TemplateEdge::finalize(Model const& containingModel) { if (assignments.empty()) { - lowestAssignmentLevel = std::numeric_limits::max(); - highestAssignmentLevel = 0; + lowestAssignmentLevel = std::numeric_limits::max(); + highestAssignmentLevel = std::numeric_limits::min(); } else { lowestAssignmentLevel = assignments.getLowestLevel(); highestAssignmentLevel = assignments.getHighestLevel(); } for (auto const& destination : getDestinations()) { if (!destination.getOrderedAssignments().empty()) { - lowestAssignmentLevel = std::min(lowestAssignmentLevel, destination.getOrderedAssignments().getLowestLevel()); - highestAssignmentLevel = std::max(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; } diff --git a/src/storm/storage/jani/TemplateEdge.h b/src/storm/storage/jani/TemplateEdge.h index 0928c50e0..1606bec85 100644 --- a/src/storm/storage/jani/TemplateEdge.h +++ b/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 finalize. diff --git a/src/storm/storage/jani/traverser/AssignmentLevelFinder.cpp b/src/storm/storage/jani/traverser/AssignmentLevelFinder.cpp index 442ba4bd4..0872c1f4f 100644 --- a/src/storm/storage/jani/traverser/AssignmentLevelFinder.cpp +++ b/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::max(); + int64_t AssignmentLevelFinder::getLowestAssignmentLevel(Model const& model) { + int64_t res = std::numeric_limits::max(); ConstJaniTraverser::traverse(model, &res); return res; } void AssignmentLevelFinder::traverse(Assignment const& assignment, boost::any const& data) { - auto& res = *boost::any_cast(data); - res = std::min(res, assignment.getLevel()); + auto& res = *boost::any_cast(data); + res = std::min(res, assignment.getLevel()); } } } diff --git a/src/storm/storage/jani/traverser/AssignmentLevelFinder.h b/src/storm/storage/jani/traverser/AssignmentLevelFinder.h index 7a5a4a4fc..c8887df7a 100644 --- a/src/storm/storage/jani/traverser/AssignmentLevelFinder.h +++ b/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; };