added some accessor functions and iteration capabilities. started on symbolic jani model builder

Former-commit-id: 4388aca60d

src/builder/DdJaniModelBuilder.cpp

@@ -0,0 +1,125 @@
+#include "src/builder/DdJaniModelBuilder.h"
+
+#include <sstream>
+
+#include <boost/algorithm/string/join.hpp>
+
+#include "src/logic/Formulas.h"
+
+#include "src/utility/macros.h"
+#include "src/utility/jani.h"
+#include "src/exceptions/InvalidArgumentException.h"
+
+namespace storm {
+    namespace builder {
+        
+        template <storm::dd::DdType Type, typename ValueType>
+        DdJaniModelBuilder<Type, ValueType>::Options::Options() : buildAllRewardModels(true), rewardModelsToBuild(), constantDefinitions(), terminalStates(), negatedTerminalStates() {
+            // Intentionally left empty.
+        }
+        
+        template <storm::dd::DdType Type, typename ValueType>
+        DdJaniModelBuilder<Type, ValueType>::Options::Options(storm::logic::Formula const& formula) : buildAllRewardModels(false), rewardModelsToBuild(), constantDefinitions(), terminalStates(), negatedTerminalStates() {
+            this->preserveFormula(formula);
+            this->setTerminalStatesFromFormula(formula);
+        }
+        
+        template <storm::dd::DdType Type, typename ValueType>
+        DdJaniModelBuilder<Type, ValueType>::Options::Options(std::vector<std::shared_ptr<storm::logic::Formula const>> const& formulas) : buildAllRewardModels(false), rewardModelsToBuild(), constantDefinitions(), terminalStates(), negatedTerminalStates() {
+            if (formulas.empty()) {
+                this->buildAllRewardModels = true;
+            } else {
+                for (auto const& formula : formulas) {
+                    this->preserveFormula(*formula);
+                }
+                if (formulas.size() == 1) {
+                    this->setTerminalStatesFromFormula(*formulas.front());
+                }
+            }
+        }
+        
+        template <storm::dd::DdType Type, typename ValueType>
+        void DdJaniModelBuilder<Type, ValueType>::Options::preserveFormula(storm::logic::Formula const& formula) {
+            // If we already had terminal states, we need to erase them.
+            if (terminalStates) {
+                terminalStates.reset();
+            }
+            if (negatedTerminalStates) {
+                negatedTerminalStates.reset();
+            }
+            
+            // If we are not required to build all reward models, we determine the reward models we need to build.
+            if (!buildAllRewardModels) {
+                std::set<std::string> referencedRewardModels = formula.getReferencedRewardModels();
+                rewardModelsToBuild.insert(referencedRewardModels.begin(), referencedRewardModels.end());
+            }
+        }
+        
+        template <storm::dd::DdType Type, typename ValueType>
+        void DdJaniModelBuilder<Type, ValueType>::Options::setTerminalStatesFromFormula(storm::logic::Formula const& formula) {
+            if (formula.isAtomicExpressionFormula()) {
+                terminalStates = formula.asAtomicExpressionFormula().getExpression();
+            } else if (formula.isEventuallyFormula()) {
+                storm::logic::Formula const& sub = formula.asEventuallyFormula().getSubformula();
+                if (sub.isAtomicExpressionFormula() || sub.isAtomicLabelFormula()) {
+                    this->setTerminalStatesFromFormula(sub);
+                }
+            } else if (formula.isUntilFormula()) {
+                storm::logic::Formula const& right = formula.asUntilFormula().getRightSubformula();
+                if (right.isAtomicExpressionFormula() || right.isAtomicLabelFormula()) {
+                    this->setTerminalStatesFromFormula(right);
+                }
+                storm::logic::Formula const& left = formula.asUntilFormula().getLeftSubformula();
+                if (left.isAtomicExpressionFormula()) {
+                    negatedTerminalStates = left.asAtomicExpressionFormula().getExpression();
+                }
+            } else if (formula.isProbabilityOperatorFormula()) {
+                storm::logic::Formula const& sub = formula.asProbabilityOperatorFormula().getSubformula();
+                if (sub.isEventuallyFormula() || sub.isUntilFormula()) {
+                    this->setTerminalStatesFromFormula(sub);
+                }
+            }
+        }
+        
+        template <storm::dd::DdType Type, typename ValueType>
+        void DdJaniModelBuilder<Type, ValueType>::Options::addConstantDefinitionsFromString(storm::jani::Model const& model, std::string const& constantDefinitionString) {
+            std::map<storm::expressions::Variable, storm::expressions::Expression> newConstantDefinitions = storm::utility::jani::parseConstantDefinitionString(model, constantDefinitionString);
+            
+            // If there is at least one constant that is defined, and the constant definition map does not yet exist,
+            // we need to create it.
+            if (!constantDefinitions && !newConstantDefinitions.empty()) {
+                constantDefinitions = std::map<storm::expressions::Variable, storm::expressions::Expression>();
+            }
+            
+            // Now insert all the entries that need to be defined.
+            for (auto const& entry : newConstantDefinitions) {
+                constantDefinitions.get().insert(entry);
+            }
+        }
+        
+        template <storm::dd::DdType Type, typename ValueType>
+        DdJaniModelBuilder<Type, ValueType>::DdJaniModelBuilder(storm::jani::Model const& model, Options const& options) : options(options) {
+            if (options.constantDefinitions) {
+                this->model = model.defineUndefinedConstants(options.constantDefinitions.get());
+            } else {
+                this->model = model;
+            }
+            
+            if (this->model->hasUndefinedConstants()) {
+                std::vector<std::reference_wrapper<storm::jani::Constant const>> undefinedConstants = this->model->getUndefinedConstants();
+                std::vector<std::string> strings;
+                for (auto const& constant : undefinedConstants) {
+                    std::stringstream stream;
+                    stream << constant.get().getName() << " (" << constant.get().getType() << ")";
+                    strings.push_back(stream.str());
+                }
+                STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "Program still contains these undefined constants: " << boost::join(strings, ", ") << ".");
+            }
+            
+            this->model = this->model->substituteConstants();
+        }
+        
+        template class DdJaniModelBuilder<storm::dd::DdType::CUDD, double>;
+        template class DdJaniModelBuilder<storm::dd::DdType::Sylvan, double>;
+    }
+}

src/builder/DdJaniModelBuilder.h

@@ -0,0 +1,121 @@
+#pragma once
+
+#include <boost/optional.hpp>
+
+#include "src/storage/dd/DdType.h"
+
+#include "src/logic/Formula.h"
+
+#include "src/storage/jani/Model.h"
+
+namespace storm {
+    namespace models {
+        namespace symbolic {
+            template <storm::dd::DdType Type, typename ValueType>
+            class Model;
+        }
+    }
+    
+    namespace builder {
+        
+        template <storm::dd::DdType Type, typename ValueType = double>
+        class DdJaniModelBuilder {
+        public:            
+            struct Options {
+                /*!
+                 * Creates an object representing the default building options.
+                 */
+                Options();
+                
+                /*! Creates an object representing the suggested building options assuming that the given formula is the
+                 * only one to check. Additional formulas may be preserved by calling <code>preserveFormula</code>.
+                 *
+                 * @param formula The formula based on which to choose the building options.
+                 */
+                Options(storm::logic::Formula const& formula);
+                
+                /*! Creates an object representing the suggested building options assuming that the given formulas are
+                 * the only ones to check. Additional formulas may be preserved by calling <code>preserveFormula</code>.
+                 *
+                 * @param formula Thes formula based on which to choose the building options.
+                 */
+                Options(std::vector<std::shared_ptr<storm::logic::Formula const>> const& formulas);
+                
+                /*!
+                 * Sets the constants definitions from the given string. The string must be of the form 'X=a,Y=b,Z=c',
+                 * etc. where X,Y,Z are the variable names and a,b,c are the values of the constants.
+                 *
+                 * @param program The program managing the constants that shall be defined. Note that the program itself
+                 * is not modified whatsoever.
+                 * @param constantDefinitionString The string from which to parse the constants' values.
+                 */
+                void addConstantDefinitionsFromString(storm::jani::Model const& model, std::string const& constantDefinitionString);
+                
+                /*!
+                 * Changes the options in a way that ensures that the given formula can be checked on the model once it
+                 * has been built.
+                 *
+                 * @param formula The formula that is to be ''preserved''.
+                 */
+                void preserveFormula(storm::logic::Formula const& formula);
+                
+                /*!
+                 * Analyzes the given formula and sets an expression for the states states of the model that can be
+                 * treated as terminal states. Note that this may interfere with checking properties different than the
+                 * one provided.
+                 *
+                 * @param formula The formula used to (possibly) derive an expression for the terminal states of the
+                 * model.
+                 */
+                void setTerminalStatesFromFormula(storm::logic::Formula const& formula);
+                
+                // A flag that indicates whether or not all reward models are to be build.
+                bool buildAllRewardModels;
+                
+                // A list of reward models to be build in case not all reward models are to be build.
+                std::set<std::string> rewardModelsToBuild;
+                
+                // An optional mapping that, if given, contains defining expressions for undefined constants.
+                boost::optional<std::map<storm::expressions::Variable, storm::expressions::Expression>> constantDefinitions;
+                
+                // An optional expression or label that (a subset of) characterizes the terminal states of the model.
+                // If this is set, the outgoing transitions of these states are replaced with a self-loop.
+                boost::optional<storm::expressions::Expression> terminalStates;
+                
+                // An optional expression or label whose negation characterizes (a subset of) the terminal states of the
+                // model. If this is set, the outgoing transitions of these states are replaced with a self-loop.
+                boost::optional<storm::expressions::Expression> negatedTerminalStates;
+            };
+            
+            /*!
+             * Creates a builder for the given model that uses the given options.
+             */
+            DdJaniModelBuilder(storm::jani::Model const& model, Options const& options = Options());
+            
+            /*!
+             * Translates the given program into a symbolic model (i.e. one that stores the transition relation as a
+             * decision diagram).
+             *
+             * @param model The model to translate.
+             * @return A pointer to the resulting model.
+             */
+            std::shared_ptr<storm::models::symbolic::Model<Type, ValueType>> translate();
+            
+            /*!
+             * Retrieves the model that was actually translated (i.e. including constant substitutions etc.). Note
+             * that this function may only be called after a succesful translation.
+             *
+             * @return The translated model.
+             */
+            storm::jani::Model const& getTranslatedModel() const;
+            
+        private:
+            /// The model to translate.
+            boost::optional<storm::jani::Model> model;
+            
+            /// The options to use for building the model.
+            Options options;
+        };
+        
+    }
+}

src/storage/jani/Assignment.cpp

@@ -15,6 +15,10 @@ namespace storm  {
             return expression;
         }
         
+        void Assignment::setAssignedExpression(storm::expressions::Expression const& expression) {
+            this->expression = expression;
+        }
+        
         std::ostream& operator<<(std::ostream& stream, Assignment const& assignment) {
             stream << assignment.getExpressionVariable().getName() << " := " << assignment.getAssignedExpression();
             return stream;

src/storage/jani/Assignment.h

@@ -22,6 +22,11 @@ namespace storm {
              * Retrieves the expression whose value is assigned to the target variable.
              */
             storm::expressions::Expression const& getAssignedExpression() const;
+            
+            /*!
+             * Sets a new expression that is assigned to the target variable.
+             */
+            void setAssignedExpression(storm::expressions::Expression const& expression);
 
             friend std::ostream& operator<<(std::ostream& stream, Assignment const& assignment);
             

src/storage/jani/Automaton.cpp

@@ -7,6 +7,132 @@
 namespace storm {
     namespace jani {
         
+        namespace detail {
+            EdgeIterator::EdgeIterator(Automaton& automaton, outer_iter out_it, outer_iter out_ite, inner_iter in_it) : automaton(automaton), out_it(out_it), out_ite(out_ite), in_it(in_it) {
+                // Intentionally left empty.
+            }
+            
+            EdgeIterator& EdgeIterator::operator++() {
+                incrementIterator();
+                return *this;
+            }
+            
+            EdgeIterator& EdgeIterator::operator++(int) {
+                incrementIterator();
+                return *this;
+            }
+            
+            Edge& EdgeIterator::operator*() {
+                return *in_it;
+            }
+            
+            bool EdgeIterator::operator==(EdgeIterator const& other) const {
+                return this->out_it == other.out_it && this->in_it == other.in_it;
+            }
+            
+            bool EdgeIterator::operator!=(EdgeIterator const& other) const {
+                return !(*this == other);
+            }
+            
+            void EdgeIterator::incrementIterator() {
+                ++in_it;
+                
+                // If the inner iterator has reached its end move it to the beginning of the next outer element.
+                if (in_it == out_it->end()) {
+                    ++out_it;
+                    while (out_it != out_ite && out_it->empty()) {
+                        ++out_it;
+                        in_it = out_it->end();
+                    }
+                    if (out_it != out_ite) {
+                        in_it = out_it->begin();
+                    }
+                }
+            }
+            
+            ConstEdgeIterator::ConstEdgeIterator(Automaton const& automaton, outer_iter out_it, outer_iter out_ite, inner_iter in_it) : automaton(automaton), out_it(out_it), out_ite(out_ite), in_it(in_it) {
+                // Intentionally left empty.
+            }
+            
+            ConstEdgeIterator& ConstEdgeIterator::operator++() {
+                incrementIterator();
+                return *this;
+            }
+            
+            ConstEdgeIterator& ConstEdgeIterator::operator++(int) {
+                incrementIterator();
+                return *this;
+            }
+            
+            Edge const& ConstEdgeIterator::operator*() const {
+                return *in_it;
+            }
+            
+            bool ConstEdgeIterator::operator==(ConstEdgeIterator const& other) const {
+                return this->out_it == other.out_it && this->in_it == other.in_it;
+            }
+            
+            bool ConstEdgeIterator::operator!=(ConstEdgeIterator const& other) const {
+                return !(*this == other);
+            }
+            
+            void ConstEdgeIterator::incrementIterator() {
+                ++in_it;
+                
+                // If the inner iterator has reached its end move it to the beginning of the next outer element.
+                if (in_it == out_it->end()) {
+                    ++out_it;
+                    while (out_it != out_ite && out_it->empty()) {
+                        ++out_it;
+                        in_it = out_it->end();
+                    }
+                    if (out_it != out_ite) {
+                        in_it = out_it->begin();
+                    }
+                }
+            }
+            
+            Edges::Edges(Automaton& automaton) : automaton(automaton) {
+                // Intentionally left empty.
+            }
+            
+            EdgeIterator Edges::begin() {
+                auto outer = automaton.edges.begin();
+                while (outer != automaton.edges.end() && outer->empty()) {
+                    ++outer;
+                }
+                if (outer == automaton.edges.end()) {
+                    return end();
+                } else {
+                    return EdgeIterator(automaton, outer, automaton.edges.end(), outer->begin());
+                }
+            }
+            
+            EdgeIterator Edges::end() {
+                return EdgeIterator(automaton, automaton.edges.end(), automaton.edges.end(), automaton.edges.back().end());
+            }
+            
+            ConstEdges::ConstEdges(Automaton const& automaton) : automaton(automaton) {
+                // Intentionally left empty.
+            }
+            
+            ConstEdgeIterator ConstEdges::begin() const {
+                auto outer = automaton.edges.begin();
+                while (outer != automaton.edges.end() && outer->empty()) {
+                    ++outer;
+                }
+                if (outer == automaton.edges.end()) {
+                    return end();
+                } else {
+                    return ConstEdgeIterator(automaton, outer, automaton.edges.end(), outer->begin());
+                }
+            }
+            
+            ConstEdgeIterator ConstEdges::end() const {
+                return ConstEdgeIterator(automaton, automaton.edges.end(), automaton.edges.end(), automaton.edges.back().end());
+            }
+        }
+        
         Automaton::Automaton(std::string const& name) : name(name) {
             // Intentionally left empty.
         }
@@ -26,7 +152,11 @@ namespace storm {
         void Automaton::addUnboundedIntegerVariable(UnboundedIntegerVariable const& variable) {
             variables.addUnboundedIntegerVariable(variable);
         }
-        
+
+        VariableSet& Automaton::getVariables() {
+            return variables;
+        }
+
         VariableSet const& Automaton::getVariables() const {
             return variables;
         }
@@ -90,6 +220,14 @@ namespace storm {
             edges[edge.getSourceLocationId()].addEdge(edge);
         }
         
+        Automaton::Edges Automaton::getEdges() {
+            return Edges(*this);
+        }
+        
+        Automaton::ConstEdges Automaton::getEdges() const {
+            return ConstEdges(*this);
+        }
+        
         uint64_t Automaton::getNumberOfLocations() const {
             return edges.size();
         }

src/storage/jani/Automaton.h

@@ -11,8 +11,122 @@
 namespace storm {
     namespace jani {
 
+        class Automaton;
+        
+        namespace detail {
+            class EdgeIterator {
+            private:
+                typedef std::vector<EdgeSet>::iterator outer_iter;
+                typedef EdgeSet::iterator inner_iter;
+                
+            public:
+                /*!
+                 * Creates an iterator over all edges.
+                 */
+                EdgeIterator(Automaton& automaton, outer_iter out_it, outer_iter out_ite, inner_iter in_it);
+                
+                // Methods to advance the iterator.
+                EdgeIterator& operator++();
+                EdgeIterator& operator++(int);
+                
+                Edge& operator*();
+                
+                bool operator==(EdgeIterator const& other) const;
+                bool operator!=(EdgeIterator const& other) const;
+                
+            private:
+                // Moves the iterator to the next position.
+                void incrementIterator();
+                
+                // The underlying automaton.
+                Automaton& automaton;
+                
+                // The current iterator positions.
+                outer_iter out_it;
+                outer_iter out_ite;
+                inner_iter in_it;
+            };
+            
+            class ConstEdgeIterator {
+            private:
+                typedef std::vector<EdgeSet>::const_iterator outer_iter;
+                typedef EdgeSet::const_iterator inner_iter;
+                
+            public:
+                /*!
+                 * Creates an iterator over all edges.
+                 */
+                ConstEdgeIterator(Automaton const& automaton, outer_iter out_it, outer_iter out_ite, inner_iter in_it);
+                
+                // Methods to advance the iterator.
+                ConstEdgeIterator& operator++();
+                ConstEdgeIterator& operator++(int);
+                
+                Edge const& operator*() const;
+                
+                bool operator==(ConstEdgeIterator const& other) const;
+                bool operator!=(ConstEdgeIterator const& other) const;
+                
+            private:
+                // Moves the iterator to the next position.
+                void incrementIterator();
+                
+                // The underlying automaton.
+                Automaton const& automaton;
+                
+                // The current iterator positions.
+                outer_iter out_it;
+                outer_iter out_ite;
+                inner_iter in_it;
+            };
+            
+            class Edges {
+            public:
+                Edges(Automaton& automaton);
+                
+                /*!
+                 * Retrieves an iterator to all edges of the automaton.
+                 */
+                EdgeIterator begin();
+                
+                /*!
+                 * Retrieves the end iterator to edges of the automaton.
+                 */
+                EdgeIterator end();
+                
+            private:
+                // The underlying automaton.
+                Automaton& automaton;
+            };
+            
+            class ConstEdges {
+            public:
+                ConstEdges(Automaton const& automaton);
+                
+                /*!
+                 * Retrieves an iterator to all edges of the automaton.
+                 */
+                ConstEdgeIterator begin() const;
+                
+                /*!
+                 * Retrieves the end iterator to edges of the automaton.
+                 */
+                ConstEdgeIterator end() const;
+                
+            private:
+                // The underlying automaton.
+                Automaton const& automaton;
+            };
+        }
+        
         class Automaton {
         public:
+            friend class detail::Edges;
+            friend class detail::ConstEdges;
+            
+            typedef detail::Edges Edges;
+            typedef detail::ConstEdges ConstEdges;
+            
             /*!
              * Creates an empty automaton.
              */
@@ -37,7 +151,12 @@ namespace storm {
              * Adds the given unbounded integer variable to this automaton.
              */
             void addUnboundedIntegerVariable(UnboundedIntegerVariable const& variable);
-            
+
+            /*!
+             * Retrieves the variables of this automaton.
+             */
+            VariableSet& getVariables();
+
             /*!
              * Retrieves the variables of this automaton.
              */
@@ -106,6 +225,16 @@ namespace storm {
              */
             void addEdge(Edge const& edge);
             
+            /*!
+             * Retrieves the edges of the automaton.
+             */
+            Edges getEdges();
+
+            /*!
+             * Retrieves the edges of the automaton.
+             */
+            ConstEdges getEdges() const;
+
             /*!
              * Retrieves the number of locations.
              */

src/storage/jani/BoundedIntegerVariable.cpp

@@ -11,9 +11,17 @@ namespace storm {
             return lowerBound;
         }
         
+        void BoundedIntegerVariable::setLowerBound(storm::expressions::Expression const& expression) {
+            this->lowerBound = expression;
+        }
+        
         storm::expressions::Expression const& BoundedIntegerVariable::getUpperBound() const {
             return upperBound;
         }
         
+        void BoundedIntegerVariable::setUpperBound(storm::expressions::Expression const& expression) {
+            this->upperBound = expression;
+        }
+        
     }
 }

src/storage/jani/BoundedIntegerVariable.h

@@ -18,11 +18,21 @@ namespace storm {
              */
             storm::expressions::Expression const& getLowerBound() const;
 
+            /*!
+             * Sets a new lower bound of the variable.
+             */
+            void setLowerBound(storm::expressions::Expression const& expression);
+            
             /*!
              * Retrieves the expression defining the upper bound of the variable.
              */
             storm::expressions::Expression const& getUpperBound() const;
 
+            /*!
+             * Sets a new upper bound of the variable.
+             */
+            void setUpperBound(storm::expressions::Expression const& expression);
+
         private:
             // The expression defining the lower bound of the variable.
             storm::expressions::Expression lowerBound;

src/storage/jani/Constant.cpp

@@ -35,5 +35,13 @@ namespace storm {
             return getType().isRationalType();
         }
         
+        storm::expressions::Variable const& Constant::getExpressionVariable() const {
+            return variable;
+        }
+        
+        storm::expressions::Expression const& Constant::getExpression() const {
+            return expression.get();
+        }
+        
     }
 }

src/storage/jani/Constant.h

@@ -52,6 +52,16 @@ namespace storm {
              */
             bool isRealConstant() const;
             
+            /*!
+             * Retrieves the expression variable associated with this constant.
+             */
+            storm::expressions::Variable const& getExpressionVariable() const;
+            
+            /*!
+             * Retrieves the expression that defines this constant (if any).
+             */
+            storm::expressions::Expression const& getExpression() const;
+            
         private:
             // The name of the constant.
             std::string name;

src/storage/jani/Edge.cpp

@@ -23,14 +23,26 @@ namespace storm {
             return rate.get();
         }
         
+        void Edge::setRate(storm::expressions::Expression const& rate) {
+            this->rate = rate;
+        }
+        
         storm::expressions::Expression const& Edge::getGuard() const {
             return guard;
         }
         
+        void Edge::setGuard(storm::expressions::Expression const& guard) {
+            this->guard = guard;
+        }
+        
         std::vector<EdgeDestination> const& Edge::getDestinations() const {
             return destinations;
         }
         
+        std::vector<EdgeDestination>& Edge::getDestinations() {
+            return destinations;
+        }
+        
         void Edge::addDestination(EdgeDestination const& destination) {
             destinations.push_back(destination);
         }

src/storage/jani/Edge.h

@@ -30,16 +30,31 @@ namespace storm {
              * 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;
+
+            /*!
+             * Sets a new rate for this edge.
+             */
+            void setRate(storm::expressions::Expression const& rate);
             
             /*!
              * Retrieves the guard of this edge.
              */
             storm::expressions::Expression const& getGuard() const;
             
+            /*!
+             * Sets a new guard for this edge.
+             */
+            void setGuard(storm::expressions::Expression const& guard);
+            
             /*!
              * Retrieves the destinations of this edge.
              */
             std::vector<EdgeDestination> const& getDestinations() const;
+
+            /*!
+             * Retrieves the destinations of this edge.
+             */
+            std::vector<EdgeDestination>& getDestinations();
             
             /*!
              * Adds the given destination to the destinations of this edge.

src/storage/jani/EdgeDestination.cpp

@@ -30,6 +30,14 @@ namespace storm {
             return probability;
         }
         
+        void EdgeDestination::setProbability(storm::expressions::Expression const& probability) {
+            this->probability = probability;
+        }
+        
+        std::vector<Assignment>& EdgeDestination::getAssignments() {
+            return assignments;
+        }
+        
         std::vector<Assignment> const& EdgeDestination::getAssignments() const {
             return assignments;
         }

src/storage/jani/EdgeDestination.h

@@ -37,6 +37,16 @@ namespace storm {
              */
             storm::expressions::Expression const& getProbability() const;
             
+            /*!
+             * Sets a new probability for this edge destination.
+             */
+            void setProbability(storm::expressions::Expression const& probability);
+
+            /*!
+             * Retrieves the assignments to make when choosing this destination.
+             */
+            std::vector<Assignment>& getAssignments();
+
             /*!
              * Retrieves the assignments to make when choosing this destination.
              */

src/storage/jani/EdgeSet.cpp

@@ -27,5 +27,9 @@ namespace storm {
             edges.push_back(edge);
         }
         
+        bool EdgeSet::empty() const {
+            return edges.empty();
+        }
+        
     }
 }

src/storage/jani/EdgeSet.h

@@ -21,6 +21,11 @@ namespace storm {
              */
             void addEdge(Edge const& edge);
             
+            /*!
+             * Retrieves whether the set of edges is empty.
+             */
+            bool empty() const;
+            
             // Methods to get an iterator to the edges.
             iterator begin();
             iterator end();

src/storage/jani/Exporter.cpp

@@ -227,7 +227,7 @@ namespace storm {
             
             appendIndent(out, indent + 1);
             appendField(out, "ref");
-            storm::jani::Variable const& variable = model.getVariables().hasVariable(assignment.getExpressionVariable()) ? model.getVariables().getVariable(assignment.getExpressionVariable()) : automaton.getVariables().getVariable(assignment.getExpressionVariable());
+            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);
@@ -399,7 +399,7 @@ namespace storm {
             clearLine(out);
             appendActions(out, model, 1);
             clearLine(out);
-            appendVariables(out, model.getVariables(), 1);
+            appendVariables(out, model.getGlobalVariables(), 1);
             clearLine(out);
             appendAutomata(out, model, 1);
             clearLine(out);

src/storage/jani/Model.cpp

@@ -8,6 +8,7 @@
 
 #include "src/utility/macros.h"
 #include "src/exceptions/WrongFormatException.h"
+#include "src/exceptions/InvalidOperationException.h"
 
 namespace storm {
     namespace jani {
@@ -72,6 +73,24 @@ namespace storm {
             return constants.size() - 1;
         }
         
+        bool Model::hasConstant(std::string const& name) const {
+            return constantToIndex.find(name) != constantToIndex.end();
+        }
+        
+        Constant const& Model::getConstant(std::string const& name) const {
+            auto it = constantToIndex.find(name);
+            STORM_LOG_THROW(it != constantToIndex.end(), storm::exceptions::WrongFormatException, "Unable to retrieve unknown constant '" << name << "'.");
+            return constants[it->second];
+        }
+        
+        std::vector<Constant> const& Model::getConstants() const {
+            return constants;
+        }
+
+        std::vector<Constant>& Model::getConstants() {
+            return constants;
+        }
+
         void Model::addBooleanVariable(BooleanVariable const& variable) {
             globalVariables.addBooleanVariable(variable);
         }
@@ -83,8 +102,12 @@ namespace storm {
         void Model::addUnboundedIntegerVariable(UnboundedIntegerVariable const& variable) {
             globalVariables.addUnboundedIntegerVariable(variable);
         }
-        
-        VariableSet const& Model::getVariables() const {
+
+        VariableSet& Model::getGlobalVariables() {
+            return globalVariables;
+        }
+
+        VariableSet const& Model::getGlobalVariables() const {
             return globalVariables;
         }
         
@@ -104,6 +127,14 @@ namespace storm {
             return automata.size() - 1;
         }
         
+        std::vector<Automaton>& Model::getAutomata() {
+            return automata;
+        }
+        
+        std::vector<Automaton> const& Model::getAutomata() const {
+            return automata;
+        }
+        
         std::shared_ptr<Composition> Model::getStandardSystemComposition() const {
             std::set<std::string> fullSynchronizationAlphabet = getActionNames(false);
             
@@ -129,6 +160,109 @@ namespace storm {
             return result;
         }
         
+        Model Model::defineUndefinedConstants(std::map<storm::expressions::Variable, storm::expressions::Expression> const& constantDefinitions) const {
+            Model result(*this);
+            
+            std::set<storm::expressions::Variable> definedUndefinedConstants;
+            for (auto& constant : result.constants) {
+                // If the constant is already defined, we need to replace the appearances of undefined constants in its
+                // defining expression
+                if (constant.isDefined()) {
+                    // Make sure we are not trying to define an already defined constant.
+                    STORM_LOG_THROW(constantDefinitions.find(constant.getExpressionVariable()) == constantDefinitions.end(), storm::exceptions::InvalidOperationException, "Illegally defining already defined constant '" << constant.getName() << "'.");
+                } else {
+                    auto const& variableExpressionPair = constantDefinitions.find(constant.getExpressionVariable());
+                    
+                    if (variableExpressionPair != constantDefinitions.end()) {
+                        // If we need to define it, we add it to the defined constants and assign it the appropriate expression.
+                        definedUndefinedConstants.insert(constant.getExpressionVariable());
+                        
+                        // Make sure the type of the constant is correct.
+                        STORM_LOG_THROW(variableExpressionPair->second.getType() == constant.getType(), storm::exceptions::InvalidOperationException, "Illegal type of expression defining constant '" << constant.getName() << "'.");
+                        
+                        // Now define the constant.
+                        constant.define(variableExpressionPair->second);
+                    }
+                }
+            }
+            
+            // As a sanity check, we make sure that the given mapping does not contain any definitions for identifiers
+            // that are not undefined constants.
+            for (auto const& constantExpressionPair : constantDefinitions) {
+                STORM_LOG_THROW(definedUndefinedConstants.find(constantExpressionPair.first) != definedUndefinedConstants.end(), storm::exceptions::InvalidOperationException, "Unable to define non-existant constant '" << constantExpressionPair.first.getName() << "'.");
+            }
+            return result;
+        }
+        
+        bool Model::hasUndefinedConstants() const {
+            for (auto const& constant : constants) {
+                if (!constant.isDefined()) {
+                    return true;
+                }
+            }
+            return false;
+        }
+        
+        std::vector<std::reference_wrapper<Constant const>> Model::getUndefinedConstants() const {
+            std::vector<std::reference_wrapper<Constant const>> result;
+            
+            for (auto const& constant : constants) {
+                if (!constant.isDefined()) {
+                    result.push_back(constant);
+                }
+            }
+            
+            return result;
+        }
+        
+        Model Model::substituteConstants() const {
+            Model result(*this);
+
+            // Gather all defining expressions of constants.
+            std::map<storm::expressions::Variable, storm::expressions::Expression> constantSubstitution;
+            for (auto& constant : result.getConstants()) {
+                if (constant.isDefined()) {
+                    constant.define(constant.getExpression().substitute(constantSubstitution));
+                    constantSubstitution[constant.getExpressionVariable()] = constant.getExpression();
+                }
+            }
+            
+            // Substitute constants in all global variables.
+            for (auto& variable : result.getGlobalVariables()) {
+                variable.setInitialValue(variable.getInitialValue().substitute(constantSubstitution));
+            }
+            for (auto& variable : result.getGlobalVariables().getBoundedIntegerVariables()) {
+                variable.setLowerBound(variable.getLowerBound().substitute(constantSubstitution));
+                variable.setUpperBound(variable.getUpperBound().substitute(constantSubstitution));
+            }
+            
+            // Substitute constants in variables of automata and their edges.
+            for (auto& automaton : result.getAutomata()) {
+                for (auto& variable : automaton.getVariables()) {
+                    variable.setInitialValue(variable.getInitialValue().substitute(constantSubstitution));
+                }
+                for (auto& variable : automaton.getVariables().getBoundedIntegerVariables()) {
+                    variable.setLowerBound(variable.getLowerBound().substitute(constantSubstitution));
+                    variable.setUpperBound(variable.getUpperBound().substitute(constantSubstitution));
+                }
+                
+                for (auto& edge : automaton.getEdges()) {
+                    edge.setGuard(edge.getGuard().substitute(constantSubstitution));
+                    if (edge.hasRate()) {
+                        edge.setRate(edge.getRate().substitute(constantSubstitution));
+                    }
+                    for (auto& destination : edge.getDestinations()) {
+                        destination.setProbability(destination.getProbability().substitute(constantSubstitution));
+                        for (auto& assignment : destination.getAssignments()) {
+                            assignment.setAssignedExpression(assignment.getAssignedExpression().substitute(constantSubstitution));
+                        }
+                    }
+                }
+            }
+            
+            return result;
+        }
+        
         bool Model::checkValidity(bool logdbg) const {
             // TODO switch to exception based return value.
             

src/storage/jani/Model.h

@@ -77,6 +77,26 @@ namespace storm {
              */
             uint64_t addConstant(Constant const& constant);
             
+            /*!
+             * Retrieves whether the model has a constant with the given name.
+             */
+            bool hasConstant(std::string const& name) const;
+            
+            /*!
+             * Retrieves the constants of the model.
+             */
+            std::vector<Constant> const& getConstants() const;
+
+            /*!
+             * Retrieves the constants of the model.
+             */
+            std::vector<Constant>& getConstants();
+
+            /*!
+             * Retrieves the constant with the given name (if any).
+             */
+            Constant const& getConstant(std::string const& name) const;
+            
             /*!
              * Adds the given boolean variable to this model.
              */
@@ -91,11 +111,16 @@ namespace storm {
              * Adds the given unbounded integer variable to this model.
              */
             void addUnboundedIntegerVariable(UnboundedIntegerVariable const& variable);
-            
+
+            /*!
+             * Retrieves the variables of this automaton.
+             */
+            VariableSet& getGlobalVariables();
+
             /*!
              * Retrieves the variables of this automaton.
              */
-            VariableSet const& getVariables() const;
+            VariableSet const& getGlobalVariables() const;
             
             /*!
              * Retrieves the manager responsible for the expressions in the JANI model.
@@ -112,6 +137,16 @@ namespace storm {
              */
             uint64_t addAutomaton(Automaton const& automaton);
             
+            /*!
+             * Retrieves the automata of the model.
+             */
+            std::vector<Automaton>& getAutomata();
+
+            /*!
+             * Retrieves the automata of the model.
+             */
+            std::vector<Automaton> const& getAutomata() const;
+
             /*!
              * Sets the system composition expression of the JANI model.
              */
@@ -137,6 +172,28 @@ namespace storm {
              */
             std::string const& getSilentActionName() const;
             
+            /*!
+             * Defines the undefined constants of the model by the given expressions. The original model is not modified,
+             * but instead a new model is created.
+             */
+            Model defineUndefinedConstants(std::map<storm::expressions::Variable, storm::expressions::Expression> const& constantDefinitions) const;
+            
+            /*!
+             * Retrieves whether the model still has undefined constants.
+             */
+            bool hasUndefinedConstants() const;
+            
+            /*!
+             * Retrieves all undefined constants of the model.
+             */
+            std::vector<std::reference_wrapper<Constant const>> getUndefinedConstants() const;
+            
+            /*!
+             * Substitutes all constants in all expressions of the model. The original model is not modified, but
+             * instead a new model is created.
+             */
+            Model substituteConstants() const;
+            
             /*!
              *  Checks if the model is valid JANI, which should be verified before any further operations are applied to a model.
              */

src/storage/jani/Variable.cpp

@@ -25,5 +25,9 @@ namespace storm {
             return initialValue;
         }
         
+        void Variable::setInitialValue(storm::expressions::Expression const& initialValue) {
+            this->initialValue = initialValue;
+        }
+        
     }
 }

src/storage/jani/Variable.h

@@ -31,6 +31,11 @@ namespace storm {
              */
             storm::expressions::Expression const& getInitialValue() const;
             
+            /*!
+             * Sets a new value as the initial value of the variable.
+             */
+            void setInitialValue(storm::expressions::Expression const& initialValue);
+            
             /*!
              * Retrieves whether the variable has an initial value.
              */

src/storage/jani/VariableSet.cpp

@@ -9,7 +9,7 @@ namespace storm {
         
         namespace detail {
             
-            VariableSetIterator::VariableSetIterator(VariableSet const& variableSet, boost::variant<bool_iter, bint_iter, int_iter> initialIterator) : variableSet(variableSet), it(initialIterator) {
+            VariableSetIterator::VariableSetIterator(VariableSet& variableSet, boost::variant<bool_iter, bint_iter, int_iter> initialIterator) : variableSet(variableSet), it(initialIterator) {
                 // Intentionally left empty.
             }
             
@@ -23,7 +23,7 @@ namespace storm {
                 return *this;
             }
             
-            Variable const& VariableSetIterator::operator*() {
+            Variable& VariableSetIterator::operator*() {
                 if (it.which() == 0) {
                     return *boost::get<bool_iter>(it);
                 } else if (it.which() == 1) {
@@ -61,37 +61,117 @@ namespace storm {
                 }
             }
             
-            IntegerVariables::IntegerVariables(VariableSet const& variableSet) : variableSet(variableSet) {
+            ConstVariableSetIterator::ConstVariableSetIterator(VariableSet const& variableSet, boost::variant<bool_iter, bint_iter, int_iter> initialIterator) : variableSet(variableSet), it(initialIterator) {
                 // Intentionally left empty.
             }
             
-            VariableSetIterator IntegerVariables::begin() const {
+            ConstVariableSetIterator& ConstVariableSetIterator::operator++() {
+                incrementIterator();
+                return *this;
+            }
+            
+            ConstVariableSetIterator& ConstVariableSetIterator::operator++(int) {
+                incrementIterator();
+                return *this;
+            }
+            
+            Variable const& ConstVariableSetIterator::operator*() {
+                if (it.which() == 0) {
+                    return *boost::get<bool_iter>(it);
+                } else if (it.which() == 1) {
+                    return *boost::get<bint_iter>(it);
+                } else {
+                    return *boost::get<int_iter>(it);
+                }
+            }
+            
+            bool ConstVariableSetIterator::operator==(ConstVariableSetIterator const& other) const {
+                return this->it == other.it;
+            }
+            
+            bool ConstVariableSetIterator::operator!=(ConstVariableSetIterator const& other) const {
+                return this->it != other.it;
+            }
+            
+            void ConstVariableSetIterator::incrementIterator() {
+                if (it.which() == 0) {
+                    bool_iter& tmp = boost::get<bool_iter>(it);
+                    if (tmp != variableSet.getBooleanVariables().end()) {
+                        ++tmp;
+                    } else {
+                        it = variableSet.getBoundedIntegerVariables().begin();
+                    }
+                } else if (it.which() == 1) {
+                    bint_iter& tmp = boost::get<bint_iter>(it);
+                    if (tmp != variableSet.getBoundedIntegerVariables().end()) {
+                        ++tmp;
+                    } else {
+                        it = variableSet.getUnboundedIntegerVariables().begin();
+                    }
+                } else {
+                    ++boost::get<int_iter>(it);
+                }
+            }
+            
+            IntegerVariables::IntegerVariables(VariableSet& variableSet) : variableSet(variableSet) {
+                // Intentionally left empty.
+            }
+            
+            VariableSetIterator IntegerVariables::begin() {
                 return VariableSetIterator(variableSet, variableSet.getBoundedIntegerVariables().begin());
             }
             
-            VariableSetIterator IntegerVariables::end() const {
+            VariableSetIterator IntegerVariables::end() {
                 return VariableSetIterator(variableSet, variableSet.getUnboundedIntegerVariables().end());
             }
+            
+            ConstIntegerVariables::ConstIntegerVariables(VariableSet const& variableSet) : variableSet(variableSet) {
+                // Intentionally left empty.
+            }
+            
+            ConstVariableSetIterator ConstIntegerVariables::begin() const {
+                return ConstVariableSetIterator(variableSet, variableSet.getBoundedIntegerVariables().begin());
+            }
+            
+            ConstVariableSetIterator ConstIntegerVariables::end() const {
+                return ConstVariableSetIterator(variableSet, variableSet.getUnboundedIntegerVariables().end());
+            }
         }
         
         VariableSet::VariableSet() {
             // Intentionally left empty.
         }
         
-        std::vector<BooleanVariable> const& VariableSet::getBooleanVariables() const {
+        std::vector<BooleanVariable>& VariableSet::getBooleanVariables() {
             return booleanVariables;
         }
         
+        std::vector<BooleanVariable> const& VariableSet::getBooleanVariables() const {
+            return booleanVariables;
+        }
+
+        std::vector<BoundedIntegerVariable>& VariableSet::getBoundedIntegerVariables() {
+            return boundedIntegerVariables;
+        }
+
         std::vector<BoundedIntegerVariable> const& VariableSet::getBoundedIntegerVariables() const {
             return boundedIntegerVariables;
         }
-        
+
+        std::vector<UnboundedIntegerVariable>& VariableSet::getUnboundedIntegerVariables() {
+            return unboundedIntegerVariables;
+        }
+
         std::vector<UnboundedIntegerVariable> const& VariableSet::getUnboundedIntegerVariables() const {
             return unboundedIntegerVariables;
         }
-        
-        detail::IntegerVariables VariableSet::getIntegerVariables() const {
-            return detail::IntegerVariables(*this);
+
+        VariableSet::IntegerVariables VariableSet::getIntegerVariables() {
+            return IntegerVariables(*this);
+        }
+
+        VariableSet::ConstIntegerVariables VariableSet::getIntegerVariables() const {
+            return ConstIntegerVariables(*this);
         }
         
         void VariableSet::addBooleanVariable(BooleanVariable const& variable) {
@@ -124,15 +204,23 @@ namespace storm {
             STORM_LOG_THROW(it != nameToVariable.end(), storm::exceptions::InvalidArgumentException, "Unable to retrieve unknown variable '" << name << "'.");
             return getVariable(it->second);
         }
-        
-        detail::VariableSetIterator VariableSet::begin() const {
-            return detail::VariableSetIterator(*this, booleanVariables.begin());
+
+        VariableSet::iterator VariableSet::begin() {
+            return iterator(*this, booleanVariables.begin());
         }
-        
-        detail::VariableSetIterator VariableSet::end() const {
-            return detail::VariableSetIterator(*this, unboundedIntegerVariables.end());
+
+        VariableSet::const_iterator VariableSet::begin() const {
+            return const_iterator(*this, booleanVariables.begin());
         }
         
+        VariableSet::iterator VariableSet::end() {
+            return iterator(*this, unboundedIntegerVariables.end());
+        }
+
+        VariableSet::const_iterator VariableSet::end() const {
+            return const_iterator(*this, unboundedIntegerVariables.end());
+        }
+
         Variable const& VariableSet::getVariable(storm::expressions::Variable const& variable) const {
             auto it = variableToVariable.find(variable);
             STORM_LOG_THROW(it != variableToVariable.end(), storm::exceptions::InvalidArgumentException, "Unable to retrieve unknown variable '" << variable.getName() << "'.");

src/storage/jani/VariableSet.h

@@ -18,21 +18,21 @@ namespace storm {
             
             class VariableSetIterator {
             private:
-                typedef std::vector<BooleanVariable>::const_iterator bool_iter;
-                typedef std::vector<BoundedIntegerVariable>::const_iterator bint_iter;
-                typedef std::vector<UnboundedIntegerVariable>::const_iterator int_iter;
+                typedef std::vector<BooleanVariable>::iterator bool_iter;
+                typedef std::vector<BoundedIntegerVariable>::iterator bint_iter;
+                typedef std::vector<UnboundedIntegerVariable>::iterator int_iter;
                 
             public:
                 /*!
                  * Creates an iterator over all variables.
                  */
-                VariableSetIterator(VariableSet const& variableSet, boost::variant<bool_iter, bint_iter, int_iter> initialIterator);
+                VariableSetIterator(VariableSet& variableSet, boost::variant<bool_iter, bint_iter, int_iter> initialIterator);
                 
                 // Methods to advance the iterator.
                 VariableSetIterator& operator++();
                 VariableSetIterator& operator++(int);
                 
-                Variable const& operator*();
+                Variable& operator*();
 
                 bool operator==(VariableSetIterator const& other) const;
                 bool operator!=(VariableSetIterator const& other) const;
@@ -42,25 +42,76 @@ namespace storm {
                 void incrementIterator();
                 
                 // The underlying variable set.
-                VariableSet const& variableSet;
+                VariableSet& variableSet;
 
                 // The current iterator position.
                 boost::variant<bool_iter, bint_iter, int_iter> it;
             };
             
+            class ConstVariableSetIterator {
+            private:
+                typedef std::vector<BooleanVariable>::const_iterator bool_iter;
+                typedef std::vector<BoundedIntegerVariable>::const_iterator bint_iter;
+                typedef std::vector<UnboundedIntegerVariable>::const_iterator int_iter;
+                
+            public:
+                /*!
+                 * Creates an iterator over all variables.
+                 */
+                ConstVariableSetIterator(VariableSet const& variableSet, boost::variant<bool_iter, bint_iter, int_iter> initialIterator);
+                
+                // Methods to advance the iterator.
+                ConstVariableSetIterator& operator++();
+                ConstVariableSetIterator& operator++(int);
+                
+                Variable const& operator*();
+                
+                bool operator==(ConstVariableSetIterator const& other) const;
+                bool operator!=(ConstVariableSetIterator const& other) const;
+                
+            private:
+                // Moves the iterator to the next position.
+                void incrementIterator();
+                
+                // The underlying variable set.
+                VariableSet const& variableSet;
+                
+                // The current iterator position.
+                boost::variant<bool_iter, bint_iter, int_iter> it;
+            };
+            
             class IntegerVariables {
             public:
-                IntegerVariables(VariableSet const& variableSet);
+                IntegerVariables(VariableSet& variableSet);
                 
                 /*!
                  * Retrieves an iterator to all integer variables (bounded and unbounded) in the variable set.
                  */
-                VariableSetIterator begin() const;
+                VariableSetIterator begin();
 
                 /*!
                  * Retrieves the end iterator to all integer variables (bounded and unbounded) in the variable set.
                  */
-                VariableSetIterator end() const;
+                VariableSetIterator end();
+                
+            private:
+                // The underlying variable set.
+                VariableSet& variableSet;
+            };
+            
+            class ConstIntegerVariables {
+            public:
+                ConstIntegerVariables(VariableSet const& variableSet);
+                
+                /*!
+                 * Retrieves an iterator to all integer variables (bounded and unbounded) in the variable set.
+                 */
+                ConstVariableSetIterator begin() const;
+                
+                /*!
+                 * Retrieves the end iterator to all integer variables (bounded and unbounded) in the variable set.
+                 */
+                ConstVariableSetIterator end() const;
                 
             private:
                 // The underlying variable set.
@@ -72,30 +123,55 @@ namespace storm {
         public:
             friend class detail::VariableSetIterator;
             
+            typedef detail::VariableSetIterator iterator;
+            typedef detail::ConstVariableSetIterator const_iterator;
+            typedef detail::IntegerVariables IntegerVariables;
+            typedef detail::ConstIntegerVariables ConstIntegerVariables;
+            
             /*!
              * Creates an empty variable set.
              */
             VariableSet();
             
+            /*!
+             * Retrieves the boolean variables in this set.
+             */
+            std::vector<BooleanVariable>& getBooleanVariables();
+
             /*!
              * Retrieves the boolean variables in this set.
              */
             std::vector<BooleanVariable> const& getBooleanVariables() const;
 
+            /*!
+             * Retrieves the bounded integer variables in this set.
+             */
+            std::vector<BoundedIntegerVariable>& getBoundedIntegerVariables();
+
             /*!
              * 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>& getUnboundedIntegerVariables();
+
             /*!
              * Retrieves the unbounded integer variables in this set.
              */
             std::vector<UnboundedIntegerVariable> const& getUnboundedIntegerVariables() const;
+
+            /*!
+             * Retrieves an iterable object to all integer (bounded and unbounded) variables in the variable set.
+             */
+            IntegerVariables getIntegerVariables();
             
             /*!
              * Retrieves an iterable object to all integer (bounded and unbounded) variables in the variable set.
              */
-            detail::IntegerVariables getIntegerVariables() const;
+            ConstIntegerVariables getIntegerVariables() const;
             
             /*!
              * Adds the given boolean variable to this set.
@@ -135,13 +211,23 @@ namespace storm {
             /*!
              * Retrieves an iterator to the variables in this set.
              */
-            detail::VariableSetIterator begin() const;
+            iterator begin();
+
+            /*!
+             * Retrieves an iterator to the variables in this set.
+             */
+            const_iterator begin() const;
 
             /*!
              * Retrieves the end iterator to the variables in this set.
              */
-            detail::VariableSetIterator end() const;
-            
+            iterator end();
+
+            /*!
+             * Retrieves the end iterator to the variables in this set.
+             */
+            const_iterator end() const;
+
         private:
             /// The boolean variables in this set.
             std::vector<BooleanVariable> booleanVariables;

src/utility/jani.cpp

@@ -0,0 +1,72 @@
+#include "src/utility/jani.h"
+
+#include <boost/algorithm/string.hpp>
+
+#include "src/storage/expressions/ExpressionManager.h"
+#include "src/storage/jani/Model.h"
+
+#include "src/utility/macros.h"
+#include "src/exceptions/InvalidArgumentException.h"
+
+namespace storm {
+    namespace utility {
+        namespace jani {
+            
+            std::map<storm::expressions::Variable, storm::expressions::Expression> parseConstantDefinitionString(storm::jani::Model const& model, std::string const& constantDefinitionString) {
+                std::map<storm::expressions::Variable, storm::expressions::Expression> constantDefinitions;
+                std::set<storm::expressions::Variable> definedConstants;
+                
+                if (!constantDefinitionString.empty()) {
+                    // Parse the string that defines the undefined constants of the model and make sure that it contains exactly
+                    // one value for each undefined constant of the model.
+                    std::vector<std::string> definitions;
+                    boost::split(definitions, constantDefinitionString, boost::is_any_of(","));
+                    for (auto& definition : definitions) {
+                        boost::trim(definition);
+                        
+                        // Check whether the token could be a legal constant definition.
+                        std::size_t positionOfAssignmentOperator = definition.find('=');
+                        STORM_LOG_THROW(positionOfAssignmentOperator != std::string::npos, storm::exceptions::InvalidArgumentException, "Illegal constant definition string: syntax error.");
+                        
+                        // Now extract the variable name and the value from the string.
+                        std::string constantName = definition.substr(0, positionOfAssignmentOperator);
+                        boost::trim(constantName);
+                        std::string value = definition.substr(positionOfAssignmentOperator + 1);
+                        boost::trim(value);
+                        
+                        // Check whether the constant is a legal undefined constant of the program and if so, of what type it is.
+                        if (model.hasConstant(constantName)) {
+                            // Get the actual constant and check whether it's in fact undefined.
+                            auto const& constant = model.getConstant(constantName);
+                            storm::expressions::Variable variable = constant.getExpressionVariable();
+                            STORM_LOG_THROW(!constant.isDefined(), storm::exceptions::InvalidArgumentException, "Illegally trying to define already defined constant '" << constantName <<"'.");
+                            STORM_LOG_THROW(definedConstants.find(variable) == definedConstants.end(), storm::exceptions::InvalidArgumentException, "Illegally trying to define constant '" << constantName <<"' twice.");
+                            definedConstants.insert(variable);
+                            
+                            if (constant.getType().isBooleanType()) {
+                                if (value == "true") {
+                                    constantDefinitions[variable] = model.getExpressionManager().boolean(true);
+                                } else if (value == "false") {
+                                    constantDefinitions[variable] = model.getExpressionManager().boolean(false);
+                                } else {
+                                    throw storm::exceptions::InvalidArgumentException() << "Illegal value for boolean constant: " << value << ".";
+                                }
+                            } else if (constant.getType().isIntegerType()) {
+                                int_fast64_t integerValue = std::stoi(value);
+                                constantDefinitions[variable] = model.getExpressionManager().integer(integerValue);
+                            } else if (constant.getType().isRationalType()) {
+                                double doubleValue = std::stod(value);
+                                constantDefinitions[variable] = model.getExpressionManager().rational(doubleValue);
+                            }
+                        } else {
+                            STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "Illegal constant definition string: unknown undefined constant '" << constantName << "'.");
+                        }
+                    }
+                }
+                
+                return constantDefinitions;
+            }
+            
+        }
+    }
+}

src/utility/jani.h

@@ -0,0 +1,23 @@
+#pragma once
+
+#include <map>
+
+namespace storm {
+    namespace expressions {
+        class Variable;
+        class Expression;
+    }
+    
+    namespace jani {
+        class Model;
+    }
+    
+    namespace utility {
+        namespace jani {
+            
+            std::map<storm::expressions::Variable, storm::expressions::Expression> parseConstantDefinitionString(storm::jani::Model const& model, std::string const& constantDefinitionString);
+            
+        }
+    }
+}
+