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 <type_traits>
+
+#include <boost/iterator/transform_iterator.hpp>
+
+namespace storm {
+ namespace adapters {
+
+ template<typename T>
+ struct Dereferencer {
+ decltype((*std::declval<T>())) operator()(T const& t) const {
+ return *t;
+ }
+ };
+
+ template<typename ContainerType>
+ class DereferenceIteratorAdapter {
+ public:
+ typedef typename ContainerType::value_type value_type;
+ typedef typename std::conditional<std::is_const<ContainerType>::value, typename ContainerType::const_iterator, typename ContainerType::iterator>::type input_iterator;
+ typedef typename boost::transform_iterator<Dereferencer<value_type>, 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<value_type>());
+ }
+
+ iterator end() {
+ return boost::make_transform_iterator(ite, Dereferencer<value_type>());
+ }
+
+ static iterator make_iterator(input_iterator it) {
+ return boost::make_transform_iterator(it, Dereferencer<value_type>());
+ }
+
+ 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<Assignment> const& right) const {
+ return left.getExpressionVariable() < right->getExpressionVariable();
+ }
+
+ bool AssignmentPartialOrderByVariable::operator()(std::shared_ptr<Assignment> const& left, std::shared_ptr<Assignment> const& right) const {
+ return left->getExpressionVariable() < right->getExpressionVariable();
+ }
+
+ bool AssignmentPartialOrderByVariable::operator()(std::shared_ptr<Assignment> 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<Assignment> const& right) const;
+ bool operator()(std::shared_ptr<Assignment> const& left, std::shared_ptr<Assignment> const& right) const;
+ bool operator()(std::shared_ptr<Assignment> 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<Assignment>& Edge::getTransientAssignments() {
- return transientAssignments;
- }
-
- std::vector<Assignment> 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 <boost/container/flat_set.hpp>
#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<Assignment>& getTransientAssignments();
-
- /*!
- * Retrieves the transient assignments of this edge.
- */
- std::vector<Assignment> 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<storm::expressions::Variable> 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<EdgeDestination> destinations;
/// The transient assignments made when taking this edge.
- std::vector<Assignment> 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 <code>finalize</code>.
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<Assignment> 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<Assignment>& EdgeDestination::getAssignments() {
- return assignments;
+ storm::jani::detail::ConstAssignments EdgeDestination::getAssignments() const {
+ return assignments.getAllAssignments();
}
-
- std::vector<Assignment> const& EdgeDestination::getAssignments() const {
- return assignments;
- }
-
- std::vector<Assignment>& EdgeDestination::getNonTransientAssignments() {
- return nonTransientAssignments;
- }
-
- std::vector<Assignment> const& EdgeDestination::getNonTransientAssignments() const {
- return nonTransientAssignments;
- }
-
- std::vector<Assignment>& EdgeDestination::getTransientAssignments() {
- return transientAssignments;
+
+ storm::jani::detail::ConstAssignments EdgeDestination::getTransientAssignments() const {
+ return assignments.getTransientAssignments();
}
- std::vector<Assignment> const& EdgeDestination::getTransientAssignments() const {
- return transientAssignments;
+ storm::jani::detail::ConstAssignments EdgeDestination::getNonTransientAssignments() const {
+ return assignments.getNonTransientAssignments();
}
void EdgeDestination::substitute(std::map<storm::expressions::Variable, storm::expressions::Expression> 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<Assignment>& 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<Assignment>& 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<Assignment>& getAssignments();
+ storm::jani::detail::ConstAssignments getAssignments() const;
/*!
- * Retrieves the assignments to make when choosing this destination.
- */
- std::vector<Assignment> const& getAssignments() const;
-
- /*!
- * Retrieves the non-transient assignments to make when choosing this destination.
- */
- std::vector<Assignment>& getNonTransientAssignments();
-
- /*!
- * Retrieves the non-transient assignments to make when choosing this destination.
+ * Retrieves the transient assignments to make when choosing this destination.
*/
- std::vector<Assignment> const& getNonTransientAssignments() const;
+ storm::jani::detail::ConstAssignments getTransientAssignments() const;
/*!
* Retrieves the non-transient assignments to make when choosing this destination.
*/
- std::vector<Assignment>& getTransientAssignments();
-
- /*!
- * Retrieves the non-transient assignments to make when choosing this destination.
- */
- std::vector<Assignment> const& getTransientAssignments() const;
+ storm::jani::detail::ConstAssignments getNonTransientAssignments() const;
/*!
* Substitutes all variables in all expressions according to the given substitution.
*/
void substitute(std::map<storm::expressions::Variable, storm::expressions::Expression> 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<Assignment>& 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<Assignment>& 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<Assignment> assignments;
-
- // The assignments to make when choosing this destination.
- std::vector<Assignment> nonTransientAssignments;
-
- // The assignments to make when choosing this destination.
- std::vector<Assignment> 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 <iostream>
-
-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 <sstream>
-#include <cstdint>
-
-#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<Assignment> 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 <string>
-#include <vector>
-#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<Assignment> 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<Assignment> 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<Assignment> 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>(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<storm::expressions::Variable, storm::expressions::Expression> const& substitution) {
+ for (auto& assignment : allAssignments) {
+ assignment->substitute(substitution);
+ }
+ }
+
+ 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::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<std::vector<std::shared_ptr<Assignment>>>;
+ using ConstAssignments = storm::adapters::DereferenceIteratorAdapter<std::vector<std::shared_ptr<Assignment>> const>;
+ }
+
+ class OrderedAssignments {
+ public:
+ /*!
+ * Creates an ordered set of assignments.
+ */
+ OrderedAssignments(std::vector<Assignment> const& assignments = std::vector<Assignment>());
+
+ /*!
+ * 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<storm::expressions::Variable, storm::expressions::Expression> const& substitution);
+
+ private:
+ 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;
+ std::vector<std::shared_ptr<Assignment>> 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<typename VariableType>
- VariableType& Dereferencer<VariableType>::operator()(std::shared_ptr<VariableType> const& d) const {
- return *d;
- }
-
- template<typename VariableType>
- Variables<VariableType>::Variables(input_iterator it, input_iterator ite) : it(it), ite(ite) {
- // Intentionally left empty.
- }
- template<typename VariableType>
- typename Variables<VariableType>::iterator Variables<VariableType>::begin() {
- return boost::make_transform_iterator(it, Dereferencer<VariableType>());
- }
-
- template<typename VariableType>
- typename Variables<VariableType>::iterator Variables<VariableType>::end() {
- return boost::make_transform_iterator(ite, Dereferencer<VariableType>());
- }
-
- template<typename VariableType>
- ConstVariables<VariableType>::ConstVariables(const_input_iterator it, const_input_iterator ite) : it(it), ite(ite) {
- // Intentionally left empty.
- }
-
- template<typename VariableType>
- typename ConstVariables<VariableType>::const_iterator ConstVariables<VariableType>::begin() {
- return boost::make_transform_iterator(it, Dereferencer<VariableType const>());
- }
-
- template<typename VariableType>
- typename ConstVariables<VariableType>::const_iterator ConstVariables<VariableType>::end() {
- return boost::make_transform_iterator(ite, Dereferencer<VariableType const>());
- }
-
- }
-
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<Variable>());
+ typename detail::Variables<Variable>::iterator VariableSet::begin() {
+ return detail::Variables<Variable>::make_iterator(variables.begin());
}
- VariableSet::const_iterator VariableSet::begin() const {
- return boost::make_transform_iterator(variables.begin(), detail::Dereferencer<Variable const>());
+ typename detail::ConstVariables<Variable>::iterator VariableSet::begin() const {
+ return detail::ConstVariables<Variable>::make_iterator(variables.begin());
}
- VariableSet::iterator VariableSet::end() {
- return boost::make_transform_iterator(variables.end(), detail::Dereferencer<Variable>());
+ typename detail::Variables<Variable>::iterator VariableSet::end() {
+ return detail::Variables<Variable>::make_iterator(variables.end());
}
- VariableSet::const_iterator VariableSet::end() const {
- return boost::make_transform_iterator(variables.end(), detail::Dereferencer<Variable const>());
+ detail::ConstVariables<Variable>::iterator VariableSet::end() const {
+ return detail::ConstVariables<Variable>::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<Variable>;
- template class detail::Dereferencer<BooleanVariable>;
- template class detail::Dereferencer<BoundedIntegerVariable>;
- template class detail::Dereferencer<UnboundedIntegerVariable>;
- template class detail::Dereferencer<Variable const>;
- template class detail::Dereferencer<BooleanVariable const>;
- template class detail::Dereferencer<BoundedIntegerVariable const>;
- template class detail::Dereferencer<UnboundedIntegerVariable const>;
- template class detail::Variables<BooleanVariable>;
- template class detail::Variables<BoundedIntegerVariable>;
- template class detail::Variables<UnboundedIntegerVariable>;
- template class detail::ConstVariables<BooleanVariable>;
- template class detail::ConstVariables<BoundedIntegerVariable>;
- template class detail::ConstVariables<UnboundedIntegerVariable>;
-
+ uint_fast64_t VariableSet::getNumberOfTransientVariables() const {
+ uint_fast64_t result = 0;
+ for (auto const& variable : variables) {
+ if (variable->isTransient()) {
+ ++result;
+ }
+ }
+ return result;
+ }
+
+ std::vector<std::shared_ptr<Variable const>> VariableSet::getTransientVariables() const {
+ std::vector<std::shared_ptr<Variable const>> 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 <vector>
#include <set>
-#include <boost/iterator/transform_iterator.hpp>
+#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<typename VariableType>
- class Dereferencer {
- public:
- VariableType& operator()(std::shared_ptr<VariableType> const& d) const;
- };
-
- template<typename VariableType>
- class Variables {
- public:
- typedef typename std::vector<std::shared_ptr<VariableType>>::iterator input_iterator;
- typedef boost::transform_iterator<Dereferencer<VariableType>, input_iterator> iterator;
-
- Variables(input_iterator it, input_iterator ite);
-
- iterator begin();
- iterator end();
-
- private:
- input_iterator it;
- input_iterator ite;
- };
-
- template<typename VariableType>
- class ConstVariables {
- public:
- typedef typename std::vector<std::shared_ptr<VariableType>>::const_iterator const_input_iterator;
- typedef boost::transform_iterator<Dereferencer<VariableType const>, 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 <typename VariableType>
+ using Variables = storm::adapters::DereferenceIteratorAdapter<std::vector<std::shared_ptr<VariableType>>>;
+
+ template <typename VariableType>
+ using ConstVariables = storm::adapters::DereferenceIteratorAdapter<std::vector<std::shared_ptr<VariableType>> const>;
}
class VariableSet {
public:
- typedef typename std::vector<std::shared_ptr<Variable>>::iterator input_iterator;
- typedef typename std::vector<std::shared_ptr<Variable>>::const_iterator const_input_iterator;
- typedef boost::transform_iterator<detail::Dereferencer<Variable>, input_iterator> iterator;
- typedef boost::transform_iterator<detail::Dereferencer<Variable const>, 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<Variable>::iterator begin();
/*!
* Retrieves an iterator to the variables in this set.
*/
- const_iterator begin() const;
+ typename detail::ConstVariables<Variable>::iterator begin() const;
/*!
* Retrieves the end iterator to the variables in this set.
*/
- iterator end();
+ typename detail::Variables<Variable>::iterator end();
/*!
* Retrieves the end iterator to the variables in this set.
*/
- const_iterator end() const;
+ typename detail::ConstVariables<Variable>::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<std::shared_ptr<Variable const>> getTransientVariables() const;
+
private:
/// The vector of all variables.
std::vector<std::shared_ptr<Variable>> variables;