From 2182beefcb019c4f82de813e6316fdf9b7bf2f22 Mon Sep 17 00:00:00 2001 From: dehnert Date: Thu, 8 Sep 2016 16:39:49 +0200 Subject: [PATCH] created storage class for JANI assignments that guarantees ordering Former-commit-id: 6cc43016a2605fbca29d4aef23f45b57faf1b9f8 [formerly aaa7b8a2131669ab8686ad68a740f829bfc4dfb2] Former-commit-id: 8eb1c8d54d417c3416fcc9ed88d68d6629c9bcbc --- src/adapters/DereferenceIteratorAdapter.h | 46 +++ src/generator/JaniNextStateGenerator.cpp | 10 +- src/generator/PrismNextStateGenerator.cpp | 3 +- src/storage/jani/Assignment.cpp | 31 +- src/storage/jani/Assignment.h | 22 +- src/storage/jani/Edge.cpp | 14 +- src/storage/jani/Edge.h | 23 +- src/storage/jani/EdgeDestination.cpp | 100 +---- src/storage/jani/EdgeDestination.h | 61 +-- src/storage/jani/Exporter.cpp | 438 ---------------------- src/storage/jani/Exporter.h | 48 --- src/storage/jani/Location.cpp | 14 +- src/storage/jani/Location.h | 8 +- src/storage/jani/OrderedAssignments.cpp | 116 ++++++ src/storage/jani/OrderedAssignments.h | 91 +++++ src/storage/jani/VariableSet.cpp | 90 ++--- src/storage/jani/VariableSet.h | 72 ++-- 17 files changed, 403 insertions(+), 784 deletions(-) create mode 100644 src/adapters/DereferenceIteratorAdapter.h delete mode 100644 src/storage/jani/Exporter.cpp delete mode 100644 src/storage/jani/Exporter.h create mode 100644 src/storage/jani/OrderedAssignments.cpp create mode 100644 src/storage/jani/OrderedAssignments.h diff --git a/src/adapters/DereferenceIteratorAdapter.h b/src/adapters/DereferenceIteratorAdapter.h new file mode 100644 index 000000000..ef1ab683d --- /dev/null +++ b/src/adapters/DereferenceIteratorAdapter.h @@ -0,0 +1,46 @@ +#pragma once + +#include + +#include + +namespace storm { + namespace adapters { + + template + struct Dereferencer { + decltype((*std::declval())) operator()(T const& t) const { + return *t; + } + }; + + template + class DereferenceIteratorAdapter { + public: + typedef typename ContainerType::value_type value_type; + typedef typename std::conditional::value, typename ContainerType::const_iterator, typename ContainerType::iterator>::type input_iterator; + typedef typename boost::transform_iterator, input_iterator> iterator; + + DereferenceIteratorAdapter(input_iterator it, input_iterator ite) : it(it), ite(ite) { + // Intentionally left empty. + } + + iterator begin() { + return boost::make_transform_iterator(it, Dereferencer()); + } + + iterator end() { + return boost::make_transform_iterator(ite, Dereferencer()); + } + + static iterator make_iterator(input_iterator it) { + return boost::make_transform_iterator(it, Dereferencer()); + } + + private: + input_iterator it; + input_iterator ite; + }; + + } +} \ No newline at end of file diff --git a/src/generator/JaniNextStateGenerator.cpp b/src/generator/JaniNextStateGenerator.cpp index f6dbfa618..510abbf5a 100644 --- a/src/generator/JaniNextStateGenerator.cpp +++ b/src/generator/JaniNextStateGenerator.cpp @@ -34,22 +34,22 @@ namespace storm { } } } else { + auto const& globalVariables = model.getGlobalVariables(); + // Extract the reward models from the program based on the names we were given. for (auto const& rewardModelName : this->options.getRewardModelNames()) { - auto const& globalVariables = model.getGlobalVariables(); if (globalVariables.hasVariable(rewardModelName)) { rewardVariables.push_back(globalVariables.getVariable(rewardModelName).getExpressionVariable()); } else { STORM_LOG_THROW(rewardModelName.empty(), storm::exceptions::InvalidArgumentException, "Cannot build unknown reward model '" << rewardModelName << "'."); STORM_LOG_THROW(globalVariables.getNumberOfTransientVariables() == 1, storm::exceptions::InvalidArgumentException, "Reference to standard reward model is ambiguous."); - STORM_LOG_THROW(this->program.getNumberOfRewardModels() > 0, storm::exceptions::InvalidArgumentException, "Reference to standard reward model is invalid, because there is no reward model."); } } - // If no reward model was yet added, but there was one that was given in the options, we try to build + // If no reward model was yet added, but there was one that was given in the options, we try to build the // standard reward model. - if (rewardModels.empty() && !this->options.getRewardModelNames().empty()) { - rewardModels.push_back(this->program.getRewardModel(0)); + if (rewardVariables.empty() && !this->options.getRewardModelNames().empty()) { + rewardVariables.push_back(globalVariables.getTransientVariables().front()->getExpressionVariable()); } } diff --git a/src/generator/PrismNextStateGenerator.cpp b/src/generator/PrismNextStateGenerator.cpp index 6e1aeafdb..1ecbec2ab 100644 --- a/src/generator/PrismNextStateGenerator.cpp +++ b/src/generator/PrismNextStateGenerator.cpp @@ -42,11 +42,10 @@ namespace storm { } else { STORM_LOG_THROW(rewardModelName.empty(), storm::exceptions::InvalidArgumentException, "Cannot build unknown reward model '" << rewardModelName << "'."); STORM_LOG_THROW(this->program.getNumberOfRewardModels() == 1, storm::exceptions::InvalidArgumentException, "Reference to standard reward model is ambiguous."); - STORM_LOG_THROW(this->program.getNumberOfRewardModels() > 0, storm::exceptions::InvalidArgumentException, "Reference to standard reward model is invalid, because there is no reward model."); } } - // If no reward model was yet added, but there was one that was given in the options, we try to build + // If no reward model was yet added, but there was one that was given in the options, we try to build the // standard reward model. if (rewardModels.empty() && !this->options.getRewardModelNames().empty()) { rewardModels.push_back(this->program.getRewardModel(0)); diff --git a/src/storage/jani/Assignment.cpp b/src/storage/jani/Assignment.cpp index 0e1720a8d..ddf65afe4 100644 --- a/src/storage/jani/Assignment.cpp +++ b/src/storage/jani/Assignment.cpp @@ -1,14 +1,18 @@ #include "src/storage/jani/Assignment.h" +#include "src/utility/macros.h" +#include "src/exceptions/NotImplementedException.h" + namespace storm { namespace jani { - Assignment::Assignment(storm::jani::Variable const& variable, storm::expressions::Expression const& expression) : variable(variable), expression(expression) { - // Intentionally left empty. + Assignment::Assignment(storm::jani::Variable const& variable, storm::expressions::Expression const& expression, uint64_t level) : variable(variable), expression(expression), level(level) { + STORM_LOG_THROW(level == 0, storm::exceptions::NotImplementedException, "Assignment levels other than 0 are currently not supported."); } bool Assignment::operator==(Assignment const& other) const { - return this->isTransientAssignment() == other.isTransientAssignment() && this->getExpressionVariable() == other.getExpressionVariable() && this->getAssignedExpression().isSyntacticallyEqual(other.getAssignedExpression()); + // FIXME: the level is currently ignored as we do not support it + return this->isTransient() == other.isTransient() && this->getExpressionVariable() == other.getExpressionVariable() && this->getAssignedExpression().isSyntacticallyEqual(other.getAssignedExpression()); } storm::jani::Variable const& Assignment::getVariable() const { @@ -27,7 +31,7 @@ namespace storm { this->expression = expression; } - bool Assignment::isTransientAssignment() const { + bool Assignment::isTransient() const { return this->variable.get().isTransient(); } @@ -35,10 +39,29 @@ namespace storm { this->setAssignedExpression(this->getAssignedExpression().substitute(substitution)); } + uint64_t Assignment::getLevel() const { + return level; + } + std::ostream& operator<<(std::ostream& stream, Assignment const& assignment) { stream << assignment.getVariable().getName() << " := " << assignment.getAssignedExpression(); return stream; } + bool AssignmentPartialOrderByVariable::operator()(Assignment const& left, Assignment const& right) const { + return left.getExpressionVariable() < right.getExpressionVariable(); + } + + bool AssignmentPartialOrderByVariable::operator()(Assignment const& left, std::shared_ptr const& right) const { + return left.getExpressionVariable() < right->getExpressionVariable(); + } + + bool AssignmentPartialOrderByVariable::operator()(std::shared_ptr const& left, std::shared_ptr const& right) const { + return left->getExpressionVariable() < right->getExpressionVariable(); + } + + bool AssignmentPartialOrderByVariable::operator()(std::shared_ptr const& left, Assignment const& right) const { + return left->getExpressionVariable() < right.getExpressionVariable(); + } } } \ No newline at end of file diff --git a/src/storage/jani/Assignment.h b/src/storage/jani/Assignment.h index 24cc9d10c..030c1f68f 100644 --- a/src/storage/jani/Assignment.h +++ b/src/storage/jani/Assignment.h @@ -13,7 +13,7 @@ namespace storm { /*! * Creates an assignment of the given expression to the given variable. */ - Assignment(storm::jani::Variable const& variable, storm::expressions::Expression const& expression); + Assignment(storm::jani::Variable const& variable, storm::expressions::Expression const& expression, uint64_t index = 0); bool operator==(Assignment const& other) const; @@ -45,7 +45,12 @@ namespace storm { /** * Retrieves whether the assignment assigns to a transient variable. */ - bool isTransientAssignment() const; + bool isTransient() const; + + /*! + * Retrieves the level of the assignment. + */ + uint64_t getLevel() const; friend std::ostream& operator<<(std::ostream& stream, Assignment const& assignment); @@ -55,7 +60,20 @@ namespace storm { // The expression that is being assigned to the variable. storm::expressions::Expression expression; + + // The level of the assignment. + uint64_t level; }; + /*! + * This functor enables ordering the assignments by variable. Note that this is a partial order. + */ + struct AssignmentPartialOrderByVariable { + bool operator()(Assignment const& left, Assignment const& right) const; + bool operator()(Assignment const& left, std::shared_ptr const& right) const; + bool operator()(std::shared_ptr const& left, std::shared_ptr const& right) const; + bool operator()(std::shared_ptr const& left, Assignment const& right) const; + }; + } } \ No newline at end of file diff --git a/src/storage/jani/Edge.cpp b/src/storage/jani/Edge.cpp index e1ac1a274..90b03fa16 100644 --- a/src/storage/jani/Edge.cpp +++ b/src/storage/jani/Edge.cpp @@ -2,6 +2,9 @@ #include "src/storage/jani/Model.h" +#include "src/utility/macros.h" +#include "src/exceptions/InvalidArgumentException.h" + namespace storm { namespace jani { @@ -49,11 +52,7 @@ namespace storm { destinations.push_back(destination); } - std::vector& Edge::getTransientAssignments() { - return transientAssignments; - } - - std::vector const& Edge::getTransientAssignments() const { + OrderedAssignments const& Edge::getTransientAssignments() const { return transientAssignments; } @@ -80,8 +79,9 @@ namespace storm { } } - void Edge::addTransientAssignment(Assignment const& assignment) { - transientAssignments.push_back(assignment); + bool Edge::addTransientAssignment(Assignment const& assignment) { + STORM_LOG_THROW(assignment.isTransient(), storm::exceptions::InvalidArgumentException, "Must not add non-transient assignment to location."); + return transientAssignments.add(assignment); } void Edge::liftTransientDestinationAssignments() { diff --git a/src/storage/jani/Edge.h b/src/storage/jani/Edge.h index 47358bb05..4e64b1b7f 100644 --- a/src/storage/jani/Edge.h +++ b/src/storage/jani/Edge.h @@ -4,6 +4,7 @@ #include #include "src/storage/jani/EdgeDestination.h" +#include "src/storage/jani/OrderedAssignments.h" namespace storm { namespace jani { @@ -64,16 +65,6 @@ namespace storm { */ void addDestination(EdgeDestination const& destination); - /*! - * Retrieves the transient assignments of this edge. - */ - std::vector& getTransientAssignments(); - - /*! - * Retrieves the transient assignments of this edge. - */ - std::vector const& getTransientAssignments() const; - /*! * Substitutes all variables in all expressions according to the given substitution. */ @@ -90,14 +81,20 @@ namespace storm { * that prior to calling this, the edge has to be finalized. */ boost::container::flat_set const& getWrittenGlobalVariables() const; - + /*! * Adds a transient assignment to this edge. * * @param assignment The transient assignment to add. + * @return True if the assignment was added. */ - void addTransientAssignment(Assignment const& assignment); + bool addTransientAssignment(Assignment const& assignment); + /*! + * Retrieves the transient assignments of this edge. + */ + OrderedAssignments const& getTransientAssignments() const; + /*! * Finds the transient assignments common to all destinations and lifts them to the edge. Afterwards, these * assignments are no longer contained in the destination. @@ -122,7 +119,7 @@ namespace storm { std::vector destinations; /// The transient assignments made when taking this edge. - std::vector transientAssignments; + OrderedAssignments transientAssignments; /// 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/storage/jani/EdgeDestination.cpp b/src/storage/jani/EdgeDestination.cpp index c59018e38..c20a5d520 100644 --- a/src/storage/jani/EdgeDestination.cpp +++ b/src/storage/jani/EdgeDestination.cpp @@ -7,33 +7,11 @@ namespace storm { namespace jani { EdgeDestination::EdgeDestination(uint64_t locationIndex, storm::expressions::Expression const& probability, std::vector const& assignments) : locationIndex(locationIndex), probability(probability), assignments(assignments) { - for (auto const& assignment : assignments) { - if (assignment.isTransientAssignment()) { - transientAssignments.push_back(assignment); - } else { - nonTransientAssignments.push_back(assignment); - } - } - sortAssignments(this->assignments); - sortAssignments(transientAssignments); - sortAssignments(nonTransientAssignments); + // Intentionally left empty. } void EdgeDestination::addAssignment(Assignment const& assignment) { - // We make sure that there are no two assignments to the same variable. - for (auto const& oldAssignment : assignments) { - STORM_LOG_THROW(oldAssignment.getExpressionVariable() != assignment.getExpressionVariable(), storm::exceptions::WrongFormatException, "Cannot add assignment '" << assignment << "', because another assignment '" << assignment << "' writes to the same target variable."); - } - assignments.push_back(assignment); - sortAssignments(assignments); - - if (assignment.isTransientAssignment()) { - transientAssignments.push_back(assignment); - sortAssignments(transientAssignments); - } else { - nonTransientAssignments.push_back(assignment); - sortAssignments(nonTransientAssignments); - } + assignments.add(assignment); } uint64_t EdgeDestination::getLocationIndex() const { @@ -48,84 +26,30 @@ namespace storm { this->probability = probability; } - std::vector& EdgeDestination::getAssignments() { - return assignments; + storm::jani::detail::ConstAssignments EdgeDestination::getAssignments() const { + return assignments.getAllAssignments(); } - - std::vector const& EdgeDestination::getAssignments() const { - return assignments; - } - - std::vector& EdgeDestination::getNonTransientAssignments() { - return nonTransientAssignments; - } - - std::vector const& EdgeDestination::getNonTransientAssignments() const { - return nonTransientAssignments; - } - - std::vector& EdgeDestination::getTransientAssignments() { - return transientAssignments; + + storm::jani::detail::ConstAssignments EdgeDestination::getTransientAssignments() const { + return assignments.getTransientAssignments(); } - std::vector const& EdgeDestination::getTransientAssignments() const { - return transientAssignments; + storm::jani::detail::ConstAssignments EdgeDestination::getNonTransientAssignments() const { + return assignments.getNonTransientAssignments(); } void EdgeDestination::substitute(std::map const& substitution) { this->setProbability(this->getProbability().substitute(substitution)); - for (auto& assignment : this->getAssignments()) { - assignment.substitute(substitution); - } - for (auto& assignment : this->getTransientAssignments()) { - assignment.substitute(substitution); - } - for (auto& assignment : this->getNonTransientAssignments()) { - assignment.substitute(substitution); - } + assignments.substitute(substitution); } bool EdgeDestination::hasAssignment(Assignment const& assignment) const { - for (auto const& containedAssignment : assignments) { - if (containedAssignment == assignment) { - return true; - } - } - return false; + return assignments.contains(assignment); } bool EdgeDestination::removeAssignment(Assignment const& assignment) { - bool toRemove = removeAssignment(assignment, assignments); - if (toRemove) { - if (assignment.isTransientAssignment()) { - removeAssignment(assignment, transientAssignments); - } else { - removeAssignment(assignment, nonTransientAssignments); - } - return true; - } - return false; - } - - void EdgeDestination::sortAssignments(std::vector& assignments) { - std::sort(assignments.begin(), assignments.end(), [] (storm::jani::Assignment const& assignment1, storm::jani::Assignment const& assignment2) { - bool smaller = assignment1.getExpressionVariable().getType().isBooleanType() && !assignment2.getExpressionVariable().getType().isBooleanType(); - if (!smaller) { - smaller = assignment1.getExpressionVariable() < assignment2.getExpressionVariable(); - } - return smaller; - }); + return assignments.remove(assignment); } - bool EdgeDestination::removeAssignment(Assignment const& assignment, std::vector& assignments) { - for (auto it = assignments.begin(), ite = assignments.end(); it != ite; ++it) { - if (assignment == *it) { - assignments.erase(it); - return true; - } - } - return false; - } - } } \ No newline at end of file diff --git a/src/storage/jani/EdgeDestination.h b/src/storage/jani/EdgeDestination.h index 02da155e1..a7e3fb672 100644 --- a/src/storage/jani/EdgeDestination.h +++ b/src/storage/jani/EdgeDestination.h @@ -4,7 +4,7 @@ #include "src/storage/expressions/Expression.h" -#include "src/storage/jani/Assignment.h" +#include "src/storage/jani/OrderedAssignments.h" namespace storm { namespace jani { @@ -39,81 +39,36 @@ namespace storm { /*! * Retrieves the assignments to make when choosing this destination. */ - std::vector& getAssignments(); + storm::jani::detail::ConstAssignments getAssignments() const; /*! - * Retrieves the assignments to make when choosing this destination. - */ - std::vector const& getAssignments() const; - - /*! - * Retrieves the non-transient assignments to make when choosing this destination. - */ - std::vector& getNonTransientAssignments(); - - /*! - * Retrieves the non-transient assignments to make when choosing this destination. + * Retrieves the transient assignments to make when choosing this destination. */ - std::vector const& getNonTransientAssignments() const; + storm::jani::detail::ConstAssignments getTransientAssignments() const; /*! * Retrieves the non-transient assignments to make when choosing this destination. */ - std::vector& getTransientAssignments(); - - /*! - * Retrieves the non-transient assignments to make when choosing this destination. - */ - std::vector const& getTransientAssignments() const; + storm::jani::detail::ConstAssignments getNonTransientAssignments() const; /*! * Substitutes all variables in all expressions according to the given substitution. */ void substitute(std::map const& substitution); - /*! - * Retrieves whether this assignment is made when choosing this destination. - * - * @return True iff the assignment is made. - */ + // Convenience methods to access the assignments. bool hasAssignment(Assignment const& assignment) const; - - /*! - * Removes the given assignment from this destination. - * - * @return True if the assignment was found and removed. - */ bool removeAssignment(Assignment const& assignment); private: - /*! - * Sorts the assignments to make all assignments to boolean variables precede all others and order the - * assignments within one variable group by the expression variables. - */ - static void sortAssignments(std::vector& assignments); - - /*! - * Removes the given assignment from the provided list of assignments if found. - * - * @return True if the assignment was removed. - */ - static bool removeAssignment(Assignment const& assignment, std::vector& assignments); - // The index of the destination location. uint64_t locationIndex; // The probability to go to the destination. storm::expressions::Expression probability; - // The assignments to make when choosing this destination. - std::vector assignments; - - // The assignments to make when choosing this destination. - std::vector nonTransientAssignments; - - // The assignments to make when choosing this destination. - std::vector transientAssignments; - + // The (ordered) assignments to make when choosing this destination. + OrderedAssignments assignments; }; } diff --git a/src/storage/jani/Exporter.cpp b/src/storage/jani/Exporter.cpp deleted file mode 100644 index 51635f10a..000000000 --- a/src/storage/jani/Exporter.cpp +++ /dev/null @@ -1,438 +0,0 @@ -#include "src/storage/jani/Exporter.h" - -#include - -namespace storm { - namespace jani { - - void appendIndent(std::stringstream& out, uint64_t indent) { - for (uint64_t i = 0; i < indent; ++i) { - out << "\t"; - } - } - - void appendField(std::stringstream& out, std::string const& name) { - out << "\"" << name << "\": "; - } - - void appendValue(std::stringstream& out, std::string const& value) { - out << "\"" << value << "\""; - } - - void clearLine(std::stringstream& out) { - out << std::endl; - } - - std::string expressionToString(storm::expressions::Expression const& expression) { - std::stringstream s; - s << expression; - return s.str(); - } - - void Exporter::appendVersion(std::stringstream& out, uint64_t janiVersion, uint64_t indent) const { - appendIndent(out, indent); - appendField(out, "jani-version"); - } - - void Exporter::appendModelName(std::stringstream& out, std::string const& name, uint64_t indent) const { - appendIndent(out, indent); - appendField(out, "name"); - appendValue(out, name); - } - - void Exporter::appendModelType(std::stringstream& out, storm::jani::ModelType const& modelType, uint64_t indent) const { - appendIndent(out, indent); - appendField(out, "type"); - } - - void Exporter::appendAction(std::stringstream& out, storm::jani::Action const& action, uint64_t indent) const { - appendIndent(out, indent); - out << "{" << std::endl; - appendIndent(out, indent + 1); - appendField(out, "name"); - appendValue(out, action.getName()); - clearLine(out); - appendIndent(out, indent); - out << "}"; - } - - void Exporter::appendActions(std::stringstream& out, storm::jani::Model const& model, uint64_t indent) const { - appendIndent(out, indent); - appendField(out, "actions"); - out << " [" << std::endl; - - for (uint64_t index = 0; index < model.actions.size(); ++index) { - appendAction(out, model.actions[index], indent + 1); - if (index < model.actions.size() - 1) { - out << ","; - } - clearLine(out); - } - - appendIndent(out, indent); - out << "]"; - } - - void Exporter::appendVariable(std::stringstream& out, storm::jani::BooleanVariable const& variable, uint64_t indent) const { - appendIndent(out, indent); - out << "{"; - clearLine(out); - appendIndent(out, indent + 1); - appendField(out, "name"); - appendValue(out, variable.getName()); - out << ","; - clearLine(out); - appendIndent(out, indent + 1); - appendField(out, "type"); - appendValue(out, "bool"); - out << ","; - clearLine(out); - appendIndent(out, indent); - out << "}"; - } - - void Exporter::appendBoundedIntegerVariableType(std::stringstream& out, storm::jani::BoundedIntegerVariable const& variable, uint64_t indent) const { - out << " {"; - clearLine(out); - - appendIndent(out, indent); - appendField(out, "kind"); - appendValue(out, "bounded"); - clearLine(out); - - appendIndent(out, indent); - appendField(out, "base"); - appendValue(out, "int"); - clearLine(out); - - appendIndent(out, indent); - appendField(out, "lower-bound"); - appendValue(out, expressionToString(variable.getLowerBound())); - clearLine(out); - - appendIndent(out, indent); - appendField(out, "upper-bound"); - appendValue(out, expressionToString(variable.getLowerBound())); - clearLine(out); - - appendIndent(out, indent - 1); - out << "}"; - } - - void Exporter::appendVariable(std::stringstream& out, storm::jani::BoundedIntegerVariable const& variable, uint64_t indent) const { - appendIndent(out, indent); - out << "{"; - clearLine(out); - appendIndent(out, indent + 1); - appendField(out, "name"); - appendValue(out, variable.getName()); - out << ","; - clearLine(out); - appendIndent(out, indent + 1); - appendField(out, "type"); - appendBoundedIntegerVariableType(out, variable, indent + 2); - out << ","; - clearLine(out); - appendIndent(out, indent); - out << "}"; - } - - void Exporter::appendVariable(std::stringstream& out, storm::jani::UnboundedIntegerVariable const& variable, uint64_t indent) const { - appendIndent(out, indent); - out << "{"; - clearLine(out); - appendIndent(out, indent + 1); - appendField(out, "name"); - appendValue(out, variable.getName()); - out << ","; - clearLine(out); - appendIndent(out, indent + 1); - appendField(out, "type"); - appendValue(out, "int"); - out << ","; - clearLine(out); - appendIndent(out, indent); - out << "}"; - } - - void Exporter::appendVariables(std::stringstream& out, storm::jani::VariableSet const& variables, uint64_t indent) const { - appendIndent(out, indent); - appendField(out, "variables"); - out << " ["; - clearLine(out); - - for (auto const& variable : variables.getBooleanVariables()) { - appendVariable(out, variable, indent + 1); - clearLine(out); - } - for (auto const& variable : variables.getBoundedIntegerVariables()) { - appendVariable(out, variable, indent + 1); - clearLine(out); - } - for (auto const& variable : variables.getUnboundedIntegerVariables()) { - appendVariable(out, variable, indent + 1); - clearLine(out); - } - - appendIndent(out, indent); - out << "]"; - } - - void Exporter::appendLocation(std::stringstream& out, storm::jani::Location const& location, uint64_t indent) const { - appendIndent(out, indent); - out << "{"; - clearLine(out); - - appendIndent(out, indent + 1); - appendField(out, "name"); - appendValue(out, location.getName()); - clearLine(out); - - appendIndent(out, indent); - out << "}"; - } - - void Exporter::appendLocations(std::stringstream& out, storm::jani::Automaton const& automaton, uint64_t indent) const { - appendIndent(out, indent); - appendField(out, "locations"); - out << " ["; - clearLine(out); - - for (auto const& location : automaton.getLocations()) { - appendLocation(out, location, indent + 1); - out << ","; - clearLine(out); - } - - appendIndent(out, indent); - out << "]"; - } - - void Exporter::appendAssignment(std::stringstream& out, storm::jani::Model const& model, storm::jani::Automaton const& automaton, storm::jani::Assignment const& assignment, uint64_t indent) const { - appendIndent(out, indent); - out << "{"; - clearLine(out); - - appendIndent(out, indent + 1); - appendField(out, "ref"); - storm::jani::Variable const& variable = model.getGlobalVariables().hasVariable(assignment.getExpressionVariable()) ? model.getGlobalVariables().getVariable(assignment.getExpressionVariable()) : automaton.getVariables().getVariable(assignment.getExpressionVariable()); - appendValue(out, variable.getName()); - out << ","; - clearLine(out); - - appendIndent(out, indent + 1); - appendField(out, "value"); - appendValue(out, expressionToString(assignment.getAssignedExpression())); - clearLine(out); - - appendIndent(out, indent); - out << "}"; - } - - void Exporter::appendEdgeDestination(std::stringstream& out, storm::jani::Model const& model, storm::jani::Automaton const& automaton, storm::jani::EdgeDestination const& destination, uint64_t indent) const { - appendIndent(out, indent); - out << "{"; - clearLine(out); - - appendIndent(out, indent + 1); - appendField(out, "probability"); - appendValue(out, expressionToString(destination.getProbability())); - out << ","; - clearLine(out); - - appendIndent(out, indent + 1); - appendField(out, "location"); - appendValue(out, automaton.getLocation(destination.getLocationIndex()).getName()); - out << ","; - clearLine(out); - - appendIndent(out, indent + 1); - appendField(out, "assignments"); - out << " ["; - clearLine(out); - - for (uint64_t index = 0; index < destination.getAssignments().size(); ++index) { - appendAssignment(out, model, automaton, destination.getAssignments()[index], indent + 2); - if (index < destination.getAssignments().size() - 1) { - out << ","; - } - clearLine(out); - } - - appendIndent(out, indent + 1); - out << "]"; - clearLine(out); - - appendIndent(out, indent); - out << "}"; - clearLine(out); - } - - void Exporter::appendEdge(std::stringstream& out, storm::jani::Model const& model, storm::jani::Automaton const& automaton, storm::jani::Edge const& edge, uint64_t indent) const { - appendIndent(out, indent); - out << "{"; - clearLine(out); - - appendIndent(out, indent + 1); - appendField(out, "location"); - appendValue(out, automaton.getLocation(edge.getSourceLocationIndex()).getName()); - out << ","; - clearLine(out); - - appendIndent(out, indent + 1); - appendField(out, "action"); - appendValue(out, model.getAction(edge.getActionIndex()).getName()); - out << ","; - clearLine(out); - - appendIndent(out, indent + 1); - appendField(out, "guard"); - appendValue(out, expressionToString(edge.getGuard())); - out << ","; - clearLine(out); - - appendIndent(out, indent + 1); - appendField(out, "destinations"); - out << " ["; - clearLine(out); - - for (auto const& destination : edge.getDestinations()) { - appendEdgeDestination(out, model, automaton, destination, indent + 2); - } - - appendIndent(out, indent + 1); - out << "]"; - clearLine(out); - - appendIndent(out, indent); - out << "}"; - } - - void Exporter::appendEdges(std::stringstream& out, storm::jani::Model const& model, storm::jani::Automaton const& automaton, uint64_t indent) const { - appendIndent(out, indent); - appendField(out, "edges"); - out << " ["; - clearLine(out); - - for (uint64_t location = 0; location < automaton.getNumberOfLocations(); ++location) { - for (auto const& edge : automaton.getEdgesFromLocation(location)) { - appendEdge(out, model, automaton, edge, indent + 1); - out << ","; - clearLine(out); - } - } - - appendIndent(out, indent); - out << "]"; - clearLine(out); - } - - void Exporter::appendAutomaton(std::stringstream& out, storm::jani::Model const& model, storm::jani::Automaton const& automaton, uint64_t indent) const { - appendIndent(out, indent); - out << "{"; - clearLine(out); - - appendIndent(out, indent + 1); - appendField(out, "name"); - appendValue(out, automaton.getName()); - clearLine(out); - appendVariables(out, automaton.getVariables(), indent + 1); - out << ","; - clearLine(out); - - appendLocations(out, automaton, indent + 1); - out << ","; - clearLine(out); - appendIndent(out, indent + 1); - appendField(out, "initial-locations"); - out << " ["; - clearLine(out); - for (auto const& index : automaton.getInitialLocationIndices()) { - appendIndent(out, indent + 2); - appendValue(out, automaton.getLocation(index).getName()); - clearLine(out); - } - appendIndent(out, indent + 1); - out << "]"; - clearLine(out); - if (automaton.hasInitialStatesRestriction()) { - appendIndent(out, indent + 1); - appendField(out, "initial-states"); - clearLine(out); - appendIndent(out, indent + 2); - out << "{"; - clearLine(out); - appendIndent(out, indent + 3); - appendField(out, "exp"); - appendValue(out, expressionToString(automaton.getInitialStatesExpression())); - clearLine(out); - appendIndent(out, indent + 2); - out << "}"; - clearLine(out); - } - - appendEdges(out, model, automaton, indent + 1); - - appendIndent(out, indent); - out << "}"; - } - - void Exporter::appendAutomata(std::stringstream& out, storm::jani::Model const& model, uint64_t indent) const { - appendIndent(out, indent); - appendField(out, "automata"); - out << " ["; - clearLine(out); - - for (uint64_t index = 0; index < model.automata.size(); ++index) { - appendAutomaton(out, model, model.automata[index], indent + 1); - if (index < model.automata.size() - 1) { - out << ","; - } - clearLine(out); - } - - appendIndent(out, indent); - out << "]"; - } - - std::string Exporter::toJaniString(storm::jani::Model const& model) const { - std::stringstream out; - - out << "{" << std::endl; - appendVersion(out, model.getJaniVersion(), 1); - out << ","; - clearLine(out); - appendModelName(out, model.getName(), 1); - out << ","; - clearLine(out); - appendModelType(out, model.getModelType(), 1); - out << ","; - clearLine(out); - appendActions(out, model, 1); - clearLine(out); - appendVariables(out, model.getGlobalVariables(), 1); - clearLine(out); - - appendIndent(out, 1); - appendField(out, "initial-states"); - clearLine(out); - appendIndent(out, 2); - out << "{"; - clearLine(out); - appendIndent(out, 3); - appendField(out, "exp"); - appendValue(out, expressionToString(model.getInitialStatesRestriction())); - clearLine(out); - appendIndent(out, 2); - out << "}"; - clearLine(out); - - appendAutomata(out, model, 1); - clearLine(out); - out << "}" << std::endl; - - return out.str(); - } - - } -} \ No newline at end of file diff --git a/src/storage/jani/Exporter.h b/src/storage/jani/Exporter.h deleted file mode 100644 index 7b0a1990b..000000000 --- a/src/storage/jani/Exporter.h +++ /dev/null @@ -1,48 +0,0 @@ -#pragma once - -#include -#include - -#include "src/storage/jani/Model.h" - -namespace storm { - namespace jani { - - class Exporter { - public: - Exporter() = default; - - std::string toJaniString(storm::jani::Model const& model) const; - - private: - void appendVersion(std::stringstream& out, uint64_t janiVersion, uint64_t indent) const; - - void appendModelName(std::stringstream& out, std::string const& name, uint64_t indent) const; - - void appendModelType(std::stringstream& out, storm::jani::ModelType const& modelType, uint64_t indent) const; - - void appendAction(std::stringstream& out, storm::jani::Action const& action, uint64_t indent) const; - - void appendActions(std::stringstream& out, storm::jani::Model const& model, uint64_t indent) const; - - void appendVariables(std::stringstream& out, storm::jani::VariableSet const& variables, uint64_t indent) const; - - void appendVariable(std::stringstream& out, storm::jani::BooleanVariable const& variable, uint64_t indent) const; - void appendVariable(std::stringstream& out, storm::jani::BoundedIntegerVariable const& variable, uint64_t indent) const; - void appendBoundedIntegerVariableType(std::stringstream& out, storm::jani::BoundedIntegerVariable const& variable, uint64_t indent) const; - void appendVariable(std::stringstream& out, storm::jani::UnboundedIntegerVariable const& variable, uint64_t indent) const; - - void appendAutomata(std::stringstream& out, storm::jani::Model const& model, uint64_t indent) const; - void appendAutomaton(std::stringstream& out, storm::jani::Model const& model, storm::jani::Automaton const& automaton, uint64_t indent) const; - - void appendLocation(std::stringstream& out, storm::jani::Location const& location, uint64_t indent) const; - void appendLocations(std::stringstream& out, storm::jani::Automaton const& automaton, uint64_t indent) const; - - void appendAssignment(std::stringstream& out, storm::jani::Model const& model, storm::jani::Automaton const& automaton, storm::jani::Assignment const& assignment, uint64_t indent) const; - void appendEdgeDestination(std::stringstream& out, storm::jani::Model const& model, storm::jani::Automaton const& automaton, storm::jani::EdgeDestination const& destination, uint64_t indent) const; - void appendEdge(std::stringstream& out, storm::jani::Model const& model, storm::jani::Automaton const& automaton, storm::jani::Edge const& edge, uint64_t indent) const; - void appendEdges(std::stringstream& out, storm::jani::Model const& model, storm::jani::Automaton const& automaton, uint64_t indent) const; - }; - - } -} \ No newline at end of file diff --git a/src/storage/jani/Location.cpp b/src/storage/jani/Location.cpp index 32d17531e..18e91f720 100644 --- a/src/storage/jani/Location.cpp +++ b/src/storage/jani/Location.cpp @@ -1,7 +1,8 @@ #include "src/storage/jani/Location.h" -#include "src/storage/jani/Assignment.h" -#include "src/exceptions/InvalidJaniException.h" + #include "src/utility/macros.h" +#include "src/exceptions/InvalidJaniException.h" +#include "src/exceptions/InvalidArgumentException.h" namespace storm { namespace jani { @@ -14,18 +15,17 @@ namespace storm { return name; } - std::vector const& Location::getTransientAssignments() const { + OrderedAssignments const& Location::getTransientAssignments() const { return transientAssignments; } void Location::addTransientAssignment(storm::jani::Assignment const& assignment) { - transientAssignments.push_back(assignment); + STORM_LOG_THROW(assignment.isTransient(), storm::exceptions::InvalidArgumentException, "Must not add non-transient assignment to location."); + transientAssignments.add(assignment); } void Location::checkValid() const { - for(auto const& assignment : transientAssignments) { - STORM_LOG_THROW(assignment.isTransientAssignment(), storm::exceptions::InvalidJaniException, "Only transient assignments are allowed in locations."); - } + // Intentionally left empty. } } diff --git a/src/storage/jani/Location.h b/src/storage/jani/Location.h index e80faedf9..050129972 100644 --- a/src/storage/jani/Location.h +++ b/src/storage/jani/Location.h @@ -1,8 +1,8 @@ #pragma once #include -#include -#include "src/storage/jani/Assignment.h" + +#include "src/storage/jani/OrderedAssignments.h" namespace storm { namespace jani { @@ -27,7 +27,7 @@ namespace storm { /*! * Retrieves the transient assignments of this location. */ - std::vector const& getTransientAssignments() const; + OrderedAssignments const& getTransientAssignments() const; /*! * Adds the given transient assignment to this location. @@ -44,7 +44,7 @@ namespace storm { std::string name; /// The transient assignments made in this location. - std::vector transientAssignments; + OrderedAssignments transientAssignments; }; } diff --git a/src/storage/jani/OrderedAssignments.cpp b/src/storage/jani/OrderedAssignments.cpp new file mode 100644 index 000000000..2b7ee613f --- /dev/null +++ b/src/storage/jani/OrderedAssignments.cpp @@ -0,0 +1,116 @@ +#include "src/storage/jani/OrderedAssignments.h" + +#include "src/utility/macros.h" +#include "src/exceptions/InvalidArgumentException.h" + +namespace storm { + namespace jani { + + OrderedAssignments::OrderedAssignments(std::vector const& assignments) { + for (auto const& assignment : assignments) { + add(assignment); + } + } + + bool OrderedAssignments::add(Assignment const& assignment) { + // If the element is contained in this set of assignment, nothing needs to be added. + if (this->contains(assignment)) { + return false; + } + + // Otherwise, we find the spot to insert it. + auto it = lowerBound(assignment, allAssignments); + + if (it != allAssignments.end()) { + STORM_LOG_THROW(assignment.getExpressionVariable() != (*it)->getExpressionVariable(), storm::exceptions::InvalidArgumentException, "Cannot add assignment as an assignment to this variable already exists."); + } + + // Finally, insert the new element in the correct vectors. + auto elementToInsert = std::make_shared(assignment); + allAssignments.emplace(it, elementToInsert); + if (assignment.isTransient()) { + auto transientIt = lowerBound(assignment, transientAssignments); + transientAssignments.emplace(transientIt, elementToInsert); + } else { + auto nonTransientIt = lowerBound(assignment, nonTransientAssignments); + nonTransientAssignments.emplace(nonTransientIt, elementToInsert); + } + + return true; + } + + bool OrderedAssignments::remove(Assignment const& assignment) { + // If the element is contained in this set of assignment, nothing needs to be removed. + if (!this->contains(assignment)) { + return false; + } + + // Otherwise, we find the element to delete. + auto it = lowerBound(assignment, allAssignments); + STORM_LOG_ASSERT(it != allAssignments.end(), "Invalid iterator, expected existing element."); + STORM_LOG_ASSERT(assignment == **it, "Wrong iterator position."); + allAssignments.erase(it); + + if (assignment.isTransient()) { + auto transientIt = lowerBound(assignment, transientAssignments); + STORM_LOG_ASSERT(transientIt != transientAssignments.end(), "Invalid iterator, expected existing element."); + STORM_LOG_ASSERT(assignment == **transientIt, "Wrong iterator position."); + transientAssignments.erase(transientIt); + } else { + auto nonTransientIt = lowerBound(assignment, nonTransientAssignments); + STORM_LOG_ASSERT(nonTransientIt != nonTransientAssignments.end(), "Invalid iterator, expected existing element."); + STORM_LOG_ASSERT(assignment == **nonTransientIt, "Wrong iterator position."); + nonTransientAssignments.erase(nonTransientIt); + } + return true; + } + + bool OrderedAssignments::contains(Assignment const& assignment) const { + auto it = lowerBound(assignment, allAssignments); + if (it != allAssignments.end() && assignment == **it) { + return true; + } else { + return false; + } + } + + detail::ConstAssignments OrderedAssignments::getAllAssignments() const { + return detail::ConstAssignments(allAssignments.begin(), allAssignments.end()); + } + + detail::ConstAssignments OrderedAssignments::getTransientAssignments() const { + return detail::ConstAssignments(transientAssignments.begin(), transientAssignments.end()); + } + + detail::ConstAssignments OrderedAssignments::getNonTransientAssignments() const { + return detail::ConstAssignments(nonTransientAssignments.begin(), nonTransientAssignments.end()); + } + + detail::Assignments::iterator OrderedAssignments::begin() { + return detail::Assignments::make_iterator(allAssignments.begin()); + } + + detail::ConstAssignments::iterator OrderedAssignments::begin() const { + return detail::ConstAssignments::make_iterator(allAssignments.begin()); + } + + detail::Assignments::iterator OrderedAssignments::end() { + return detail::Assignments::make_iterator(allAssignments.end()); + } + + detail::ConstAssignments::iterator OrderedAssignments::end() const { + return detail::ConstAssignments::make_iterator(allAssignments.end()); + } + + void OrderedAssignments::substitute(std::map const& substitution) { + for (auto& assignment : allAssignments) { + assignment->substitute(substitution); + } + } + + std::vector>::const_iterator OrderedAssignments::lowerBound(Assignment const& assignment, std::vector> const& assignments) { + return std::lower_bound(assignments.begin(), assignments.end(), assignment, storm::jani::AssignmentPartialOrderByVariable()); + } + + } +} \ No newline at end of file diff --git a/src/storage/jani/OrderedAssignments.h b/src/storage/jani/OrderedAssignments.h new file mode 100644 index 000000000..c9e07a34d --- /dev/null +++ b/src/storage/jani/OrderedAssignments.h @@ -0,0 +1,91 @@ +#pragma once + +#include "src/adapters/DereferenceIteratorAdapter.h" + +#include "src/storage/jani/Assignment.h" + +namespace storm { + namespace jani { + + namespace detail { + using Assignments = storm::adapters::DereferenceIteratorAdapter>>; + using ConstAssignments = storm::adapters::DereferenceIteratorAdapter> const>; + } + + class OrderedAssignments { + public: + /*! + * Creates an ordered set of assignments. + */ + OrderedAssignments(std::vector const& assignments = std::vector()); + + /*! + * Adds the given assignment to the set of assignments. + * + * @return True iff the assignment was added. + */ + bool add(Assignment const& assignment); + + /*! + * Removes the given assignment from this set of assignments. + * + * @return True if the assignment was found and removed. + */ + bool remove(Assignment const& assignment); + + /*! + * Retrieves whether the given assignment is contained in this set of assignments. + */ + bool contains(Assignment const& assignment) const; + + /*! + * Returns all assignments in this set of assignments. + */ + detail::ConstAssignments getAllAssignments() const; + + /*! + * Returns all transient assignments in this set of assignments. + */ + detail::ConstAssignments getTransientAssignments() const; + + /*! + * Returns all non-transient assignments in this set of assignments. + */ + detail::ConstAssignments getNonTransientAssignments() const; + + /*! + * Returns an iterator to the assignments. + */ + detail::Assignments::iterator begin(); + + /*! + * Returns an iterator to the assignments. + */ + detail::ConstAssignments::iterator begin() const; + + /*! + * Returns an iterator past the end of the assignments. + */ + detail::Assignments::iterator end(); + + /*! + * Returns an iterator past the end of the assignments. + */ + detail::ConstAssignments::iterator end() const; + + /*! + * Substitutes all variables in all expressions according to the given substitution. + */ + void substitute(std::map const& substitution); + + private: + 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; + std::vector> nonTransientAssignments; + }; + + } +} \ No newline at end of file diff --git a/src/storage/jani/VariableSet.cpp b/src/storage/jani/VariableSet.cpp index c138686e8..4caae4269 100644 --- a/src/storage/jani/VariableSet.cpp +++ b/src/storage/jani/VariableSet.cpp @@ -6,46 +6,7 @@ namespace storm { namespace jani { - - namespace detail { - - template - VariableType& Dereferencer::operator()(std::shared_ptr const& d) const { - return *d; - } - - template - Variables::Variables(input_iterator it, input_iterator ite) : it(it), ite(ite) { - // Intentionally left empty. - } - template - typename Variables::iterator Variables::begin() { - return boost::make_transform_iterator(it, Dereferencer()); - } - - template - typename Variables::iterator Variables::end() { - return boost::make_transform_iterator(ite, Dereferencer()); - } - - template - ConstVariables::ConstVariables(const_input_iterator it, const_input_iterator ite) : it(it), ite(ite) { - // Intentionally left empty. - } - - template - typename ConstVariables::const_iterator ConstVariables::begin() { - return boost::make_transform_iterator(it, Dereferencer()); - } - - template - typename ConstVariables::const_iterator ConstVariables::end() { - return boost::make_transform_iterator(ite, Dereferencer()); - } - - } - VariableSet::VariableSet() { // Intentionally left empty. } @@ -132,20 +93,20 @@ namespace storm { return getVariable(it->second); } - VariableSet::iterator VariableSet::begin() { - return boost::make_transform_iterator(variables.begin(), detail::Dereferencer()); + typename detail::Variables::iterator VariableSet::begin() { + return detail::Variables::make_iterator(variables.begin()); } - VariableSet::const_iterator VariableSet::begin() const { - return boost::make_transform_iterator(variables.begin(), detail::Dereferencer()); + typename detail::ConstVariables::iterator VariableSet::begin() const { + return detail::ConstVariables::make_iterator(variables.begin()); } - VariableSet::iterator VariableSet::end() { - return boost::make_transform_iterator(variables.end(), detail::Dereferencer()); + typename detail::Variables::iterator VariableSet::end() { + return detail::Variables::make_iterator(variables.end()); } - VariableSet::const_iterator VariableSet::end() const { - return boost::make_transform_iterator(variables.end(), detail::Dereferencer()); + detail::ConstVariables::iterator VariableSet::end() const { + return detail::ConstVariables::make_iterator(variables.end()); } Variable const& VariableSet::getVariable(storm::expressions::Variable const& variable) const { @@ -197,20 +158,25 @@ namespace storm { return !(containsBooleanVariable() || containsBoundedIntegerVariable() || containsUnboundedIntegerVariables()); } - template class detail::Dereferencer; - template class detail::Dereferencer; - template class detail::Dereferencer; - template class detail::Dereferencer; - template class detail::Dereferencer; - template class detail::Dereferencer; - template class detail::Dereferencer; - template class detail::Dereferencer; - template class detail::Variables; - template class detail::Variables; - template class detail::Variables; - template class detail::ConstVariables; - template class detail::ConstVariables; - template class detail::ConstVariables; - + uint_fast64_t VariableSet::getNumberOfTransientVariables() const { + uint_fast64_t result = 0; + for (auto const& variable : variables) { + if (variable->isTransient()) { + ++result; + } + } + return result; + } + + std::vector> VariableSet::getTransientVariables() const { + std::vector> result; + for (auto const& variable : variables) { + if (variable->isTransient()) { + result.push_back(variable); + } + } + return result; + } + } } diff --git a/src/storage/jani/VariableSet.h b/src/storage/jani/VariableSet.h index 777292ba9..78275de0b 100644 --- a/src/storage/jani/VariableSet.h +++ b/src/storage/jani/VariableSet.h @@ -3,7 +3,7 @@ #include #include -#include +#include "src/adapters/DereferenceIteratorAdapter.h" #include "src/storage/jani/BooleanVariable.h" #include "src/storage/jani/UnboundedIntegerVariable.h" @@ -12,57 +12,17 @@ namespace storm { namespace jani { - - class VariableSet; - - namespace detail { - - template - class Dereferencer { - public: - VariableType& operator()(std::shared_ptr const& d) const; - }; - - template - class Variables { - public: - typedef typename std::vector>::iterator input_iterator; - typedef boost::transform_iterator, input_iterator> iterator; - - Variables(input_iterator it, input_iterator ite); - - iterator begin(); - iterator end(); - - private: - input_iterator it; - input_iterator ite; - }; - - template - class ConstVariables { - public: - typedef typename std::vector>::const_iterator const_input_iterator; - typedef boost::transform_iterator, const_input_iterator> const_iterator; - - ConstVariables(const_input_iterator it, const_input_iterator ite); - - const_iterator begin(); - const_iterator end(); - private: - const_input_iterator it; - const_input_iterator ite; - }; + namespace detail { + template + using Variables = storm::adapters::DereferenceIteratorAdapter>>; + + template + using ConstVariables = storm::adapters::DereferenceIteratorAdapter> const>; } class VariableSet { public: - typedef typename std::vector>::iterator input_iterator; - typedef typename std::vector>::const_iterator const_input_iterator; - typedef boost::transform_iterator, input_iterator> iterator; - typedef boost::transform_iterator, const_input_iterator> const_iterator; - /*! * Creates an empty variable set. */ @@ -156,22 +116,22 @@ namespace storm { /*! * Retrieves an iterator to the variables in this set. */ - iterator begin(); + typename detail::Variables::iterator begin(); /*! * Retrieves an iterator to the variables in this set. */ - const_iterator begin() const; + typename detail::ConstVariables::iterator begin() const; /*! * Retrieves the end iterator to the variables in this set. */ - iterator end(); + typename detail::Variables::iterator end(); /*! * Retrieves the end iterator to the variables in this set. */ - const_iterator end() const; + typename detail::ConstVariables::iterator end() const; /*! * Retrieves whether the set of variables contains a boolean variable. @@ -203,6 +163,16 @@ namespace storm { */ bool empty() const; + /*! + * Retrieves the number of transient variables in this variable set. + */ + uint_fast64_t getNumberOfTransientVariables() const; + + /*! + * Retrieves a vector of transient variables in this variable set. + */ + std::vector> getTransientVariables() const; + private: /// The vector of all variables. std::vector> variables;