From d38e7d5eb9babb122d393fdbb0deccd188eb27d2 Mon Sep 17 00:00:00 2001
From: dehnert <dehnert@cs.rwth-aachen.de>
Date: Fri, 20 May 2016 16:50:22 +0200
Subject: [PATCH] started working on jani data structures
Former-commit-id: 30deb6d38d44bdf6e1499496771b356bbf1a3c90
---
src/storage/jani/Assignment.cpp | 24 ++++
src/storage/jani/Assignment.h | 37 ++++++
src/storage/jani/Automaton.cpp | 78 +++++++++++++
src/storage/jani/Automaton.h | 105 ++++++++++++++++++
src/storage/jani/AutomatonComposition.cpp | 0
src/storage/jani/AutomatonComposition.h | 0
src/storage/jani/BooleanVariable.cpp | 11 ++
src/storage/jani/BooleanVariable.h | 17 +++
src/storage/jani/BoundedIntegerVariable.cpp | 19 ++++
src/storage/jani/BoundedIntegerVariable.h | 35 ++++++
src/storage/jani/Composition.cpp | 0
src/storage/jani/Composition.h | 0
src/storage/jani/Edge.cpp | 39 +++++++
src/storage/jani/Edge.h | 68 ++++++++++++
src/storage/jani/EdgeDestination.cpp | 42 +++++++
src/storage/jani/EdgeDestination.h | 65 +++++++++++
src/storage/jani/EdgeSet.cpp | 27 +++++
src/storage/jani/EdgeSet.h | 31 ++++++
src/storage/jani/Location.cpp | 15 +++
src/storage/jani/Location.h | 26 +++++
src/storage/jani/Model.cpp | 0
src/storage/jani/ParallelComposition.cpp | 0
src/storage/jani/ParallelComposition.h | 0
src/storage/jani/RenameComposition.cpp | 0
src/storage/jani/RenameComposition.h | 0
src/storage/jani/RewardIncrement.cpp | 11 ++
src/storage/jani/RewardIncrement.h | 29 +++++
src/storage/jani/UnboundedIntegerVariable.cpp | 11 ++
src/storage/jani/UnboundedIntegerVariable.h | 17 +++
src/storage/jani/Variable.cpp | 19 ++++
src/storage/jani/Variable.h | 46 ++++++++
src/storage/jani/VariableSet.cpp | 55 +++++++++
src/storage/jani/VariableSet.h | 75 +++++++++++++
.../functional/builder/system_composition2.nm | 30 +++++
34 files changed, 932 insertions(+)
create mode 100644 src/storage/jani/Assignment.cpp
create mode 100644 src/storage/jani/Assignment.h
create mode 100644 src/storage/jani/Automaton.cpp
create mode 100644 src/storage/jani/AutomatonComposition.cpp
create mode 100644 src/storage/jani/AutomatonComposition.h
create mode 100644 src/storage/jani/BooleanVariable.cpp
create mode 100644 src/storage/jani/BooleanVariable.h
create mode 100644 src/storage/jani/BoundedIntegerVariable.cpp
create mode 100644 src/storage/jani/BoundedIntegerVariable.h
create mode 100644 src/storage/jani/Composition.cpp
create mode 100644 src/storage/jani/Composition.h
create mode 100644 src/storage/jani/Edge.cpp
create mode 100644 src/storage/jani/Edge.h
create mode 100644 src/storage/jani/EdgeDestination.cpp
create mode 100644 src/storage/jani/EdgeDestination.h
create mode 100644 src/storage/jani/EdgeSet.cpp
create mode 100644 src/storage/jani/EdgeSet.h
create mode 100644 src/storage/jani/Location.cpp
create mode 100644 src/storage/jani/Location.h
create mode 100644 src/storage/jani/Model.cpp
create mode 100644 src/storage/jani/ParallelComposition.cpp
create mode 100644 src/storage/jani/ParallelComposition.h
create mode 100644 src/storage/jani/RenameComposition.cpp
create mode 100644 src/storage/jani/RenameComposition.h
create mode 100644 src/storage/jani/RewardIncrement.cpp
create mode 100644 src/storage/jani/RewardIncrement.h
create mode 100644 src/storage/jani/UnboundedIntegerVariable.cpp
create mode 100644 src/storage/jani/UnboundedIntegerVariable.h
create mode 100644 src/storage/jani/Variable.cpp
create mode 100644 src/storage/jani/Variable.h
create mode 100644 src/storage/jani/VariableSet.cpp
create mode 100644 src/storage/jani/VariableSet.h
create mode 100644 test/functional/builder/system_composition2.nm
diff --git a/src/storage/jani/Assignment.cpp b/src/storage/jani/Assignment.cpp
new file mode 100644
index 000000000..a73c40d93
--- /dev/null
+++ b/src/storage/jani/Assignment.cpp
@@ -0,0 +1,24 @@
+#include "src/storage/jani/Assignment.h"
+
+namespace storm {
+ namespace jani {
+
+ Assignment::Assignment(storm::expressions::Variable const& variable, storm::expressions::Expression const& expression) : variable(variable), expression(expression) {
+ // Intentionally left empty.
+ }
+
+ storm::expressions::Variable const& Assignment::getExpressionVariable() const {
+ return variable;
+ }
+
+ storm::expressions::Expression const& Assignment::getAssignedExpression() const {
+ return expression;
+ }
+
+ std::ostream& operator<<(std::ostream& stream, Assignment const& assignment) {
+ stream << assignment.getExpressionVariable().getName() << " := " << assignment.getAssignedExpression();
+ return stream;
+ }
+
+ }
+}
\ No newline at end of file
diff --git a/src/storage/jani/Assignment.h b/src/storage/jani/Assignment.h
new file mode 100644
index 000000000..4fc0a5330
--- /dev/null
+++ b/src/storage/jani/Assignment.h
@@ -0,0 +1,37 @@
+#pragma once
+
+#include "src/storage/expressions/Variable.h"
+#include "src/storage/expressions/Expression.h"
+
+namespace storm {
+ namespace jani {
+
+ class Assignment {
+ public:
+ /*!
+ * Creates an assignment of the given expression to the given variable.
+ */
+ Assignment(storm::expressions::Variable const& variable, storm::expressions::Expression const& expression);
+
+ /*!
+ * Retrieves the expression variable that is written in this assignment.
+ */
+ storm::expressions::Variable const& getExpressionVariable() const;
+
+ /*!
+ * Retrieves the expression whose value is assigned to the target variable.
+ */
+ storm::expressions::Expression const& getAssignedExpression() const;
+
+ friend std::ostream& operator<<(std::ostream& stream, Assignment const& assignment);
+
+ private:
+ // The variable being assigned.
+ storm::expressions::Variable variable;
+
+ // The expression that is being assigned to the variable.
+ storm::expressions::Expression expression;
+ };
+
+ }
+}
\ No newline at end of file
diff --git a/src/storage/jani/Automaton.cpp b/src/storage/jani/Automaton.cpp
new file mode 100644
index 000000000..d3958b6d8
--- /dev/null
+++ b/src/storage/jani/Automaton.cpp
@@ -0,0 +1,78 @@
+#include "src/storage/jani/Automaton.h"
+
+#include "src/utility/macros.h"
+#include "src/exceptions/WrongFormatException.h"
+#include "src/exceptions/InvalidArgumentException.h"
+
+namespace storm {
+ namespace jani {
+
+ Automaton::Automaton(std::string const& name) : name(name) {
+ // Intentionally left empty.
+ }
+
+ std::string const& Automaton::getName() const {
+ return name;
+ }
+
+ void Automaton::addBooleanVariable(BooleanVariable const& variable) {
+ variables.addBooleanVariable(variable);
+ }
+
+ void Automaton::addBoundedIntegerVariable(BoundedIntegerVariable const& variable) {
+ variables.addBoundedIntegerVariable(variable);
+ }
+
+ void Automaton::addUnboundedIntegerVariable(UnboundedIntegerVariable const& variable) {
+ variables.addUnboundedIntegerVariable(variable);
+ }
+
+ VariableSet const& Automaton::getVariableSet() const {
+ return variables;
+ }
+
+ bool Automaton::hasLocation(std::string const& name) const {
+ return locationToIndex.find(name) != locationToIndex.end();
+ }
+
+ std::vector<Location> const& Automaton::getLocations() const {
+ return locations;
+ }
+
+ void Automaton::addLocation(Location const& location) {
+ STORM_LOG_THROW(!this->hasLocation(location.getName()), storm::exceptions::WrongFormatException, "Cannot add location with name '" << location.getName() << "', because a location with this name already exists.");
+ locationToIndex.emplace(location.getName(), locations.size());
+ locations.push_back(location);
+ }
+
+ void Automaton::setInitialLocation(std::string const& name) {
+ auto it = locationToIndex.find(name);
+ STORM_LOG_THROW(it != locationToIndex.end(), storm::exceptions::InvalidArgumentException, "Cannot make unknown location '" << name << "' the initial location.");
+ return setInitialLocation(it->second);
+ }
+
+ void Automaton::setInitialLocation(uint64_t index) {
+ STORM_LOG_THROW(index < locations.size(), storm::exceptions::InvalidArgumentException, "Cannot make location with index " << index << " initial: out of bounds.");
+ initialLocationIndex = index;
+ }
+
+ Location const& Automaton::getInitialLocation() const {
+ return locations[getInitialLocationIndex()];
+ }
+
+ uint64_t Automaton::getInitialLocationIndex() const {
+ return initialLocationIndex;
+ }
+
+ EdgeSet const& Automaton::getEdgesFromLocation(std::string const& name) const {
+ auto it = locationToIndex.find(name);
+ STORM_LOG_THROW(it != locationToIndex.end(), storm::exceptions::InvalidArgumentException, "Cannot retrieve edges from unknown location '" << name << ".");
+ return getEdgesFromLocation(it->second);
+ }
+
+ EdgeSet const& Automaton::getEdgesFromLocation(uint64_t index) const {
+ return edges[index];
+ }
+
+ }
+}
\ No newline at end of file
diff --git a/src/storage/jani/Automaton.h b/src/storage/jani/Automaton.h
index 766b23eb3..270f0921c 100644
--- a/src/storage/jani/Automaton.h
+++ b/src/storage/jani/Automaton.h
@@ -1,7 +1,112 @@
#pragma once
+#include <string>
+#include <cstdint>
+#include <unordered_map>
+
+#include "src/storage/jani/VariableSet.h"
+#include "src/storage/jani/EdgeSet.h"
+#include "src/storage/jani/Location.h"
+
namespace storm {
namespace jani {
+ class Automaton {
+ public:
+ /*!
+ * Creates an empty automaton.
+ */
+ Automaton(std::string const& name);
+
+ /*!
+ * Retrieves the name of the automaton.
+ */
+ std::string const& getName() const;
+
+ /*!
+ * Adds the given boolean variable to this automaton.
+ */
+ void addBooleanVariable(BooleanVariable const& variable);
+
+ /*!
+ * Adds the given bounded integer variable to this automaton.
+ */
+ void addBoundedIntegerVariable(BoundedIntegerVariable const& variable);
+
+ /*!
+ * Adds the given unbounded integer variable to this automaton.
+ */
+ void addUnboundedIntegerVariable(UnboundedIntegerVariable const& variable);
+
+ /*!
+ * Retrieves the variables of this automaton.
+ */
+ VariableSet const& getVariableSet() const;
+
+ /*!
+ * Retrieves whether the automaton has a location with the given name.
+ */
+ bool hasLocation(std::string const& name) const;
+
+ /*!
+ * Retrieves the locations of the automaton.
+ */
+ std::vector<Location> const& getLocations() const;
+
+ /*!
+ * Adds the given location to the automaton.
+ */
+ void addLocation(Location const& location);
+
+ /*!
+ * Uses the location with the given name as the initial location.
+ */
+ void setInitialLocation(std::string const& name);
+
+ /*!
+ * Uses the location with the given index as the initial location.
+ */
+ void setInitialLocation(uint64_t index);
+
+ /*!
+ * Retrieves the initial location of the automaton.
+ */
+ Location const& getInitialLocation() const;
+
+ /*!
+ * Retrieves the index of the initial location.
+ */
+ uint64_t getInitialLocationIndex() const;
+
+ /*!
+ * Retrieves the edges of the location with the given name.
+ */
+ EdgeSet const& getEdgesFromLocation(std::string const& name) const;
+
+ /*!
+ * Retrieves the edges of the location with the given index.
+ */
+ EdgeSet const& getEdgesFromLocation(uint64_t index) const;
+
+ private:
+ // The name of the automaton.
+ std::string name;
+
+ // The set of variables of this automaton.
+ VariableSet variables;
+
+ // The locations of the automaton.
+ std::vector<Location> locations;
+
+ // A mapping of location names to their indices.
+ std::unordered_map<std::string, uint64_t> locationToIndex;
+
+ // All edges of the automaton. The edges at index i are the edges of the location with index i.
+ std::vector<EdgeSet> edges;
+
+ // The index of the initial location.
+ uint64_t initialLocationIndex;
+ };
+
}
}
\ No newline at end of file
diff --git a/src/storage/jani/AutomatonComposition.cpp b/src/storage/jani/AutomatonComposition.cpp
new file mode 100644
index 000000000..e69de29bb
diff --git a/src/storage/jani/AutomatonComposition.h b/src/storage/jani/AutomatonComposition.h
new file mode 100644
index 000000000..e69de29bb
diff --git a/src/storage/jani/BooleanVariable.cpp b/src/storage/jani/BooleanVariable.cpp
new file mode 100644
index 000000000..d3d37f64e
--- /dev/null
+++ b/src/storage/jani/BooleanVariable.cpp
@@ -0,0 +1,11 @@
+#include "src/storage/jani/BooleanVariable.h"
+
+namespace storm {
+ namespace jani {
+
+ BooleanVariable::BooleanVariable(std::string const& name, storm::expressions::Variable const& variable, storm::expressions::Expression const& initialValue) : Variable(name, variable, initialValue) {
+ // Intentionally left empty.
+ }
+
+ }
+}
\ No newline at end of file
diff --git a/src/storage/jani/BooleanVariable.h b/src/storage/jani/BooleanVariable.h
new file mode 100644
index 000000000..733dd027a
--- /dev/null
+++ b/src/storage/jani/BooleanVariable.h
@@ -0,0 +1,17 @@
+#pragma once
+
+#include "src/storage/jani/Variable.h"
+
+namespace storm {
+ namespace jani {
+
+ class BooleanVariable : public Variable {
+ public:
+ /*!
+ * Creates a boolean variable.
+ */
+ BooleanVariable(std::string const& name, storm::expressions::Variable const& variable, storm::expressions::Expression const& initialValue);
+ };
+
+ }
+}
\ No newline at end of file
diff --git a/src/storage/jani/BoundedIntegerVariable.cpp b/src/storage/jani/BoundedIntegerVariable.cpp
new file mode 100644
index 000000000..879f9a165
--- /dev/null
+++ b/src/storage/jani/BoundedIntegerVariable.cpp
@@ -0,0 +1,19 @@
+#include "src/storage/jani/BoundedIntegerVariable.h"
+
+namespace storm {
+ namespace jani {
+
+ BoundedIntegerVariable::BoundedIntegerVariable(std::string const& name, storm::expressions::Variable const& variable, storm::expressions::Expression const& lowerBound, storm::expressions::Expression const& upperBound, storm::expressions::Expression const& initialValue) : Variable(name, variable, initialValue), lowerBound(lowerBound), upperBound(upperBound) {
+ // Intentionally left empty.
+ }
+
+ storm::expressions::Expression const& BoundedIntegerVariable::getLowerBound() const {
+ return lowerBound;
+ }
+
+ storm::expressions::Expression const& BoundedIntegerVariable::getUpperBound() const {
+ return upperBound;
+ }
+
+ }
+}
\ No newline at end of file
diff --git a/src/storage/jani/BoundedIntegerVariable.h b/src/storage/jani/BoundedIntegerVariable.h
new file mode 100644
index 000000000..12577867c
--- /dev/null
+++ b/src/storage/jani/BoundedIntegerVariable.h
@@ -0,0 +1,35 @@
+#pragma once
+
+#include "src/storage/jani/Variable.h"
+#include "src/storage/expressions/Expression.h"
+
+namespace storm {
+ namespace jani {
+
+ class BoundedIntegerVariable : public Variable {
+ public:
+ /*!
+ * Creates a bounded integer variable.
+ */
+ BoundedIntegerVariable(std::string const& name, storm::expressions::Variable const& variable, storm::expressions::Expression const& lowerBound, storm::expressions::Expression const& upperBound, storm::expressions::Expression const& initialValue);
+
+ /*!
+ * Retrieves the expression defining the lower bound of the variable.
+ */
+ storm::expressions::Expression const& getLowerBound() const;
+
+ /*!
+ * Retrieves the expression defining the upper bound of the variable.
+ */
+ storm::expressions::Expression const& getUpperBound() const;
+
+ private:
+ // The expression defining the lower bound of the variable.
+ storm::expressions::Expression lowerBound;
+
+ // The expression defining the upper bound of the variable.
+ storm::expressions::Expression upperBound;
+ };
+
+ }
+}
\ No newline at end of file
diff --git a/src/storage/jani/Composition.cpp b/src/storage/jani/Composition.cpp
new file mode 100644
index 000000000..e69de29bb
diff --git a/src/storage/jani/Composition.h b/src/storage/jani/Composition.h
new file mode 100644
index 000000000..e69de29bb
diff --git a/src/storage/jani/Edge.cpp b/src/storage/jani/Edge.cpp
new file mode 100644
index 000000000..5b8003815
--- /dev/null
+++ b/src/storage/jani/Edge.cpp
@@ -0,0 +1,39 @@
+#include "src/storage/jani/Edge.h"
+
+namespace storm {
+ namespace jani {
+
+ Edge::Edge(uint64_t sourceLocationId, uint64_t actionId, boost::optional<storm::expressions::Expression> const& rate, storm::expressions::Expression const& guard, std::vector<EdgeDestination> destinations) : sourceLocationId(sourceLocationId), actionId(actionId), rate(rate), guard(guard), destinations(destinations) {
+ // Intentionally left empty.
+ }
+
+ uint64_t Edge::getSourceLocationId() const {
+ return sourceLocationId;
+ }
+
+ uint64_t Edge::getActionId() const {
+ return actionId;
+ }
+
+ bool Edge::hasRate() const {
+ return static_cast<bool>(rate);
+ }
+
+ storm::expressions::Expression const& Edge::getRate() const {
+ return rate.get();
+ }
+
+ storm::expressions::Expression const& Edge::getGuard() const {
+ return guard;
+ }
+
+ std::vector<EdgeDestination> const& Edge::getDestinations() const {
+ return destinations;
+ }
+
+ void Edge::addDestination(EdgeDestination const& destination) {
+ destinations.push_back(destination);
+ }
+
+ }
+}
\ No newline at end of file
diff --git a/src/storage/jani/Edge.h b/src/storage/jani/Edge.h
new file mode 100644
index 000000000..ff5def7ee
--- /dev/null
+++ b/src/storage/jani/Edge.h
@@ -0,0 +1,68 @@
+#pragma once
+
+#include <boost/optional.hpp>
+
+#include "src/storage/jani/EdgeDestination.h"
+
+namespace storm {
+ namespace jani {
+
+ class Edge {
+ public:
+ Edge(uint64_t sourceLocationId, uint64_t actionId, boost::optional<storm::expressions::Expression> const& rate, storm::expressions::Expression const& guard, std::vector<EdgeDestination> destinations = {});
+
+ /*!
+ * Retrieves the id of the source location.
+ */
+ uint64_t getSourceLocationId() const;
+
+ /*!
+ * Retrieves the id of the action with which this edge is labeled.
+ */
+ uint64_t getActionId() const;
+
+ /*!
+ * Retrieves whether this edge has an associated rate.
+ */
+ bool hasRate() const;
+
+ /*!
+ * Retrieves the rate of this edge. Note that calling this is only valid if the edge has an associated rate.
+ */
+ storm::expressions::Expression const& getRate() const;
+
+ /*!
+ * Retrieves the guard of this edge.
+ */
+ storm::expressions::Expression const& getGuard() const;
+
+ /*!
+ * Retrieves the destinations of this edge.
+ */
+ std::vector<EdgeDestination> const& getDestinations() const;
+
+ /*!
+ * Adds the given destination to the destinations of this edge.
+ */
+ void addDestination(EdgeDestination const& destination);
+
+ private:
+ // The id of the source location.
+ uint64_t sourceLocationId;
+
+ // The id of the action with which this edge is labeled.
+ uint64_t actionId;
+
+ // The rate with which this edge is taken. This only applies to continuous-time models. For discrete-time
+ // models, this must be set to none.
+ boost::optional<storm::expressions::Expression> rate;
+
+ // The guard that defines when this edge is enabled.
+ storm::expressions::Expression guard;
+
+ // The destinations of this edge.
+ std::vector<EdgeDestination> destinations;
+ };
+
+ }
+}
\ No newline at end of file
diff --git a/src/storage/jani/EdgeDestination.cpp b/src/storage/jani/EdgeDestination.cpp
new file mode 100644
index 000000000..35554545d
--- /dev/null
+++ b/src/storage/jani/EdgeDestination.cpp
@@ -0,0 +1,42 @@
+#include "src/storage/jani/EdgeDestination.h"
+
+#include "src/utility/macros.h"
+#include "src/exceptions/WrongFormatException.h"
+
+namespace storm {
+ namespace jani {
+
+ EdgeDestination::EdgeDestination(uint64_t locationId, storm::expressions::Expression const& probability, std::vector<Assignment> const& assignments, std::vector<RewardIncrement> const& rewardIncrements) : locationId(locationId), probability(probability), assignments(assignments), rewardIncrements(rewardIncrements) {
+ // 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);
+ }
+
+ void EdgeDestination::addRewardIncrement(RewardIncrement const& rewardIncrement) {
+ rewardIncrements.push_back(rewardIncrement);
+ }
+
+ uint64_t EdgeDestination::getLocationId() const {
+ return locationId;
+ }
+
+ storm::expressions::Expression const& EdgeDestination::getProbability() const {
+ return probability;
+ }
+
+ std::vector<Assignment> const& EdgeDestination::getAssignments() const {
+ return assignments;
+ }
+
+ std::vector<RewardIncrement> const& EdgeDestination::getRewardIncrements() const {
+ return rewardIncrements;
+ }
+
+ }
+}
\ No newline at end of file
diff --git a/src/storage/jani/EdgeDestination.h b/src/storage/jani/EdgeDestination.h
new file mode 100644
index 000000000..07efeece1
--- /dev/null
+++ b/src/storage/jani/EdgeDestination.h
@@ -0,0 +1,65 @@
+#pragma once
+
+#include <cstdint>
+
+#include "src/storage/expressions/Expression.h"
+
+#include "src/storage/jani/Assignment.h"
+#include "src/storage/jani/RewardIncrement.h"
+
+namespace storm {
+ namespace jani {
+
+ class EdgeDestination {
+ public:
+ /*!
+ * Creates a new edge destination.
+ */
+ EdgeDestination(uint64_t locationId, storm::expressions::Expression const& probability, std::vector<Assignment> const& assignments = {}, std::vector<RewardIncrement> const& rewardIncrements = {});
+
+ /*!
+ * Additionally performs the given assignment when choosing this destination.
+ */
+ void addAssignment(Assignment const& assignment);
+
+ /*!
+ * Additionally performs the given reward increment when choosing this destination.
+ */
+ void addRewardIncrement(RewardIncrement const& rewardIncrement);
+
+ /*!
+ * Retrieves the id of the destination location.
+ */
+ uint64_t getLocationId() const;
+
+ /*!
+ * Retrieves the probability of choosing this destination.
+ */
+ storm::expressions::Expression const& getProbability() const;
+
+ /*!
+ * Retrieves the assignments to make when choosing this destination.
+ */
+ std::vector<Assignment> const& getAssignments() const;
+
+ /*!
+ * Retrieves the reward increments to make when choosing this destination.
+ */
+ std::vector<RewardIncrement> const& getRewardIncrements() const;
+
+ private:
+ // The id of the destination location.
+ uint64_t locationId;
+
+ // The probability to go to the destination.
+ storm::expressions::Expression probability;
+
+ // The assignments to make when choosing this destination.
+ std::vector<Assignment> assignments;
+
+ // The increments to rewards to make when choosing this destination.
+ std::vector<RewardIncrement> rewardIncrements;
+ };
+
+ }
+}
\ No newline at end of file
diff --git a/src/storage/jani/EdgeSet.cpp b/src/storage/jani/EdgeSet.cpp
new file mode 100644
index 000000000..fbdac5a39
--- /dev/null
+++ b/src/storage/jani/EdgeSet.cpp
@@ -0,0 +1,27 @@
+#include "src/storage/jani/EdgeSet.h"
+
+namespace storm {
+ namespace jani {
+
+ EdgeSet::EdgeSet(std::vector<Edge> const& edges) : edges(edges) {
+ // Intentionally left empty.
+ }
+
+ EdgeSet::iterator EdgeSet::begin() {
+ return edges.begin();
+ }
+
+ EdgeSet::iterator EdgeSet::end() {
+ return edges.end();
+ }
+
+ EdgeSet::const_iterator EdgeSet::begin() const {
+ return edges.cbegin();
+ }
+
+ EdgeSet::const_iterator EdgeSet::end() const {
+ return edges.cend();
+ }
+
+ }
+}
\ No newline at end of file
diff --git a/src/storage/jani/EdgeSet.h b/src/storage/jani/EdgeSet.h
new file mode 100644
index 000000000..df61d7722
--- /dev/null
+++ b/src/storage/jani/EdgeSet.h
@@ -0,0 +1,31 @@
+#pragma once
+
+#include "src/storage/jani/Edge.h"
+
+namespace storm {
+ namespace jani {
+
+ class EdgeSet {
+ public:
+ typedef std::vector<Edge> container_type;
+ typedef container_type::iterator iterator;
+ typedef container_type::const_iterator const_iterator;
+
+ /*!
+ * Creates a new set of edges.
+ */
+ EdgeSet(std::vector<Edge> const& edges);
+
+ // Methods to get an iterator to the edges.
+ iterator begin();
+ iterator end();
+ const_iterator begin() const;
+ const_iterator end() const;
+
+ private:
+ // The set of edges.
+ container_type edges;
+ };
+
+ }
+}
\ No newline at end of file
diff --git a/src/storage/jani/Location.cpp b/src/storage/jani/Location.cpp
new file mode 100644
index 000000000..84b45ebaf
--- /dev/null
+++ b/src/storage/jani/Location.cpp
@@ -0,0 +1,15 @@
+#include "src/storage/jani/Location.h"
+
+namespace storm {
+ namespace jani {
+
+ Location::Location(std::string const& name) : name(name) {
+ // Intentionally left empty.
+ }
+
+ std::string const& Location::getName() const {
+ return name;
+ }
+
+ }
+}
\ No newline at end of file
diff --git a/src/storage/jani/Location.h b/src/storage/jani/Location.h
new file mode 100644
index 000000000..56a08ab2c
--- /dev/null
+++ b/src/storage/jani/Location.h
@@ -0,0 +1,26 @@
+#pragma once
+
+#include <string>
+
+namespace storm {
+ namespace jani {
+
+ class Location {
+ public:
+ /*!
+ * Creates a new location.
+ */
+ Location(std::string const& name);
+
+ /*!
+ * Retrieves the name of the location.
+ */
+ std::string const& getName() const;
+
+ private:
+ // The name of the location.
+ std::string name;
+ };
+
+ }
+}
\ No newline at end of file
diff --git a/src/storage/jani/Model.cpp b/src/storage/jani/Model.cpp
new file mode 100644
index 000000000..e69de29bb
diff --git a/src/storage/jani/ParallelComposition.cpp b/src/storage/jani/ParallelComposition.cpp
new file mode 100644
index 000000000..e69de29bb
diff --git a/src/storage/jani/ParallelComposition.h b/src/storage/jani/ParallelComposition.h
new file mode 100644
index 000000000..e69de29bb
diff --git a/src/storage/jani/RenameComposition.cpp b/src/storage/jani/RenameComposition.cpp
new file mode 100644
index 000000000..e69de29bb
diff --git a/src/storage/jani/RenameComposition.h b/src/storage/jani/RenameComposition.h
new file mode 100644
index 000000000..e69de29bb
diff --git a/src/storage/jani/RewardIncrement.cpp b/src/storage/jani/RewardIncrement.cpp
new file mode 100644
index 000000000..500cc9b33
--- /dev/null
+++ b/src/storage/jani/RewardIncrement.cpp
@@ -0,0 +1,11 @@
+#include "src/storage/jani/RewardIncrement.h"
+
+namespace storm {
+ namespace jani {
+
+ RewardIncrement::RewardIncrement(uint64_t rewardId, storm::expressions::Expression const& value) : rewardId(rewardId), value(value) {
+ // Intentionally left empty.
+ }
+
+ }
+}
\ No newline at end of file
diff --git a/src/storage/jani/RewardIncrement.h b/src/storage/jani/RewardIncrement.h
new file mode 100644
index 000000000..43b2211c1
--- /dev/null
+++ b/src/storage/jani/RewardIncrement.h
@@ -0,0 +1,29 @@
+#pragma once
+
+#include <cstdint>
+
+#include "src/storage/expressions/Expression.h"
+
+namespace storm {
+ namespace jani {
+
+ class RewardIncrement {
+ public:
+ /*!
+ * Creates an increment of a reward (given by its id) by the given expression.
+ *
+ * @param rewardId The id of the reward to increment.
+ * @param value The expression defining the amount the reward is the incremented.
+ */
+ RewardIncrement(uint64_t rewardId, storm::expressions::Expression const& value);
+
+ private:
+ // The id of the reward that is to be incremented.
+ uint64_t rewardId;
+
+ // The expression defining the amount the reward is to be incremented.
+ storm::expressions::Expression value;
+ };
+
+ }
+}
\ No newline at end of file
diff --git a/src/storage/jani/UnboundedIntegerVariable.cpp b/src/storage/jani/UnboundedIntegerVariable.cpp
new file mode 100644
index 000000000..9a2497a1b
--- /dev/null
+++ b/src/storage/jani/UnboundedIntegerVariable.cpp
@@ -0,0 +1,11 @@
+#include "src/storage/jani/UnboundedIntegerVariable.h"
+
+namespace storm {
+ namespace jani {
+
+ UnboundedIntegerVariable::UnboundedIntegerVariable(std::string const& name, storm::expressions::Variable const& variable, storm::expressions::Expression const& initialValue) : Variable(name, variable, initialValue) {
+ // Intentionally left empty.
+ }
+
+ }
+}
\ No newline at end of file
diff --git a/src/storage/jani/UnboundedIntegerVariable.h b/src/storage/jani/UnboundedIntegerVariable.h
new file mode 100644
index 000000000..c6fdf2405
--- /dev/null
+++ b/src/storage/jani/UnboundedIntegerVariable.h
@@ -0,0 +1,17 @@
+#pragma once
+
+#include "src/storage/jani/Variable.h"
+
+namespace storm {
+ namespace jani {
+
+ class UnboundedIntegerVariable : public Variable {
+ public:
+ /*!
+ * Creates an unbounded integer variable.
+ */
+ UnboundedIntegerVariable(std::string const& name, storm::expressions::Variable const& variable, storm::expressions::Expression const& initialValue);
+ };
+
+ }
+}
\ No newline at end of file
diff --git a/src/storage/jani/Variable.cpp b/src/storage/jani/Variable.cpp
new file mode 100644
index 000000000..93e419804
--- /dev/null
+++ b/src/storage/jani/Variable.cpp
@@ -0,0 +1,19 @@
+#include "src/storage/jani/Variable.h"
+
+namespace storm {
+ namespace jani {
+
+ Variable::Variable(std::string const& name, storm::expressions::Variable const& variable, storm::expressions::Expression const& initialValue) : name(name), variable(variable), initialValue(initialValue) {
+ // Intentionally left empty.
+ }
+
+ storm::expressions::Variable const& Variable::getExpressionVariable() const {
+ return variable;
+ }
+
+ std::string const& Variable::getName() const {
+ return name;
+ }
+
+ }
+}
\ No newline at end of file
diff --git a/src/storage/jani/Variable.h b/src/storage/jani/Variable.h
new file mode 100644
index 000000000..2bb5326af
--- /dev/null
+++ b/src/storage/jani/Variable.h
@@ -0,0 +1,46 @@
+#pragma once
+
+#include <cstdint>
+#include <string>
+
+#include "src/storage/expressions/Variable.h"
+#include "src/storage/expressions/Expression.h"
+
+namespace storm {
+ namespace jani {
+
+ class Variable {
+ public:
+ /*!
+ * Creates a new variable.
+ */
+ Variable(std::string const& name, storm::expressions::Variable const& variable, storm::expressions::Expression const& initialValue);
+
+ /*!
+ * Retrieves the associated expression variable
+ */
+ storm::expressions::Variable const& getExpressionVariable() const;
+
+ /*!
+ * Retrieves the name of the variable.
+ */
+ std::string const& getName() const;
+
+ /*!
+ * Retrieves the initial value of the variable.
+ */
+ storm::expressions::Expression const& getInitialValue() const;
+
+ private:
+ // The name of the variable.
+ std::string name;
+
+ // The expression variable associated with this variable.
+ storm::expressions::Variable variable;
+
+ // The expression defining the initial value of the variable.
+ storm::expressions::Expression initialValue;
+ };
+
+ }
+}
\ No newline at end of file
diff --git a/src/storage/jani/VariableSet.cpp b/src/storage/jani/VariableSet.cpp
new file mode 100644
index 000000000..8f387cde9
--- /dev/null
+++ b/src/storage/jani/VariableSet.cpp
@@ -0,0 +1,55 @@
+#include "src/storage/jani/VariableSet.h"
+
+#include "src/utility/macros.h"
+#include "src/exceptions/WrongFormatException.h"
+#include "src/exceptions/InvalidArgumentException.h"
+
+namespace storm {
+ namespace jani {
+
+ VariableSet::VariableSet() {
+ // Intentionally left empty.
+ }
+
+ std::vector<BooleanVariable> const& VariableSet::getBooleanVariables() const {
+ return booleanVariables;
+ }
+
+ std::vector<BoundedIntegerVariable> const& VariableSet::getBoundedIntegerVariables() const {
+ return boundedIntegerVariables;
+ }
+
+ std::vector<UnboundedIntegerVariable> const& VariableSet::getUnboundedIntegerVariables() const {
+ return unboundedIntegerVariables;
+ }
+
+ void VariableSet::addBooleanVariable(BooleanVariable const& variable) {
+ STORM_LOG_THROW(!this->hasVariable(variable.getName()), storm::exceptions::WrongFormatException, "Cannot add variable with name '" << variable.getName() << "', because a variable with that name already exists.");
+ booleanVariables.push_back(variable);
+ variables.emplace(variable.getName(), booleanVariables.back());
+ }
+
+ void VariableSet::addBoundedIntegerVariable(BoundedIntegerVariable const& variable) {
+ STORM_LOG_THROW(!this->hasVariable(variable.getName()), storm::exceptions::WrongFormatException, "Cannot add variable with name '" << variable.getName() << "', because a variable with that name already exists.");
+ boundedIntegerVariables.push_back(variable);
+ variables.emplace(variable.getName(), boundedIntegerVariables.back());
+ }
+
+ void VariableSet::addUnboundedIntegerVariable(UnboundedIntegerVariable const& variable) {
+ STORM_LOG_THROW(!this->hasVariable(variable.getName()), storm::exceptions::WrongFormatException, "Cannot add variable with name '" << variable.getName() << "', because a variable with that name already exists.");
+ unboundedIntegerVariables.push_back(variable);
+ variables.emplace(variable.getName(), unboundedIntegerVariables.back());
+ }
+
+ bool VariableSet::hasVariable(std::string const& name) const {
+ return variables.find(name) != variables.end();
+ }
+
+ Variable const& VariableSet::getVariable(std::string const& name) const {
+ auto it = variables.find(name);
+ STORM_LOG_THROW(it != variables.end(), storm::exceptions::InvalidArgumentException, "Unable to retrieve unknown variable '" << name << "'.");
+ return it->second.get();
+ }
+
+ }
+}
\ No newline at end of file
diff --git a/src/storage/jani/VariableSet.h b/src/storage/jani/VariableSet.h
new file mode 100644
index 000000000..25628426d
--- /dev/null
+++ b/src/storage/jani/VariableSet.h
@@ -0,0 +1,75 @@
+#pragma once
+
+#include <vector>
+#include <set>
+
+#include "src/storage/jani/BooleanVariable.h"
+#include "src/storage/jani/UnboundedIntegerVariable.h"
+#include "src/storage/jani/BoundedIntegerVariable.h"
+
+namespace storm {
+ namespace jani {
+
+ class VariableSet {
+ public:
+ /*!
+ * Creates an empty variable set.
+ */
+ VariableSet();
+
+ /*!
+ * Retrieves the boolean variables in this set.
+ */
+ std::vector<BooleanVariable> const& getBooleanVariables() const;
+
+ /*!
+ * Retrieves the bounded integer variables in this set.
+ */
+ std::vector<BoundedIntegerVariable> const& getBoundedIntegerVariables() const;
+
+ /*!
+ * Retrieves the unbounded integer variables in this set.
+ */
+ std::vector<UnboundedIntegerVariable> const& getUnboundedIntegerVariables() const;
+
+ /*!
+ * Adds the given boolean variable to this set.
+ */
+ void addBooleanVariable(BooleanVariable const& variable);
+
+ /*!
+ * Adds the given bounded integer variable to this set.
+ */
+ void addBoundedIntegerVariable(BoundedIntegerVariable const& variable);
+
+ /*!
+ * Adds the given unbounded integer variable to this set.
+ */
+ void addUnboundedIntegerVariable(UnboundedIntegerVariable const& variable);
+
+ /*!
+ * Retrieves whether this variable set contains a variable with the given name.
+ */
+ bool hasVariable(std::string const& name) const;
+
+ /*!
+ * Retrieves the variable with the given name.
+ */
+ Variable const& getVariable(std::string const& name) const;
+
+ private:
+ // The boolean variables in this set.
+ std::vector<BooleanVariable> booleanVariables;
+
+ // The bounded integer variables in this set.
+ std::vector<BoundedIntegerVariable> boundedIntegerVariables;
+
+ // The unbounded integer variables in this set.
+ std::vector<UnboundedIntegerVariable> unboundedIntegerVariables;
+
+ // A set of all variable names currently in use.
+ std::map<std::string, std::reference_wrapper<Variable>> variables;
+ };
+
+ }
+}
\ No newline at end of file
diff --git a/test/functional/builder/system_composition2.nm b/test/functional/builder/system_composition2.nm
new file mode 100644
index 000000000..3d8eff315
--- /dev/null
+++ b/test/functional/builder/system_composition2.nm
@@ -0,0 +1,30 @@
+mdp
+
+module one
+ x : [0 .. 2] init 0;
+
+ [a] x=0 -> (x'=1);
+ [] x>=0 -> (x'=2);
+ [done] x>=1 -> true;
+endmodule
+
+module two
+ y : [0 .. 2] init 0;
+
+ [b] y=0 -> (y'=1);
+ [] y>=0 -> (y'=2);
+ [done] y>=1 -> true;
+endmodule
+
+module three
+ z : [0 .. 2] init 0;
+
+ [a] z=0 -> (z'=1);
+ [] x=0&y=0&z=1 -> (z'=2);
+ [loop] z>=1 -> true;
+endmodule
+
+system
+ ((one || two {b <- a})) {done <- loop} || three
+endsystem
+