started working on jani data structures

Former-commit-id: 30deb6d38d

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;
+        }
+        
+    }
+}

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;
+        };
+        
+    }
+}

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];
+        }
+        
+    }
+}

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;
+        };
+        
     }
 }

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.
+        }
+        
+    }
+}

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);
+        };
+        
+    }
+}

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;
+        }
+        
+    }
+}

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;
+        };
+        
+    }
+}

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);
+        }
+        
+    }
+}

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;
+        };
+        
+    }
+}

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;
+        }
+        
+    }
+}

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;
+        };
+        
+    }
+}

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();
+        }
+        
+    }
+}

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;
+        };
+        
+    }
+}

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;
+        }
+        
+    }
+}

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;
+        };
+        
+    }
+}

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.
+        }
+        
+    }
+}

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;
+        };
+        
+    }
+}

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.
+        }
+        
+    }
+}

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);
+        };
+        
+    }
+}

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;
+        }
+        
+    }
+}

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;
+        };
+        
+    }
+}

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();
+        }
+        
+    }
+}

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;
+        };
+        
+    }
+}

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
+