added conversion from PRISM to JANI. Added simplistic tests for that.

Former-commit-id: 5b31fa589c

src/parser/JaniParser.cpp

@@ -10,6 +10,8 @@
 #include <fstream>
 #include <boost/lexical_cast.hpp>
 
+#include "src/utility/macros.h"
+
 namespace storm {
     namespace parser {
 

src/storage/jani/Action.h

@@ -17,8 +17,8 @@ namespace storm {
             std::string const& getName() const;
 
         private:
+            /// The name of the action.
             std::string name;
-
         };
 
     }

src/storage/jani/Automaton.cpp

@@ -27,7 +27,7 @@ namespace storm {
             variables.addUnboundedIntegerVariable(variable);
         }
         
-        VariableSet const& Automaton::getVariableSet() const {
+        VariableSet const& Automaton::getVariables() const {
             return variables;
         }
         
@@ -39,10 +39,15 @@ namespace storm {
             return locations;
         }
         
+        Location const& Automaton::getLocation(uint64_t index) const {
+            return locations[index];
+        }
+        
         uint64_t 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);
+            edges.push_back(EdgeSet());
             return locations.size() - 1;
         }
 
@@ -80,5 +85,14 @@ namespace storm {
             return edges[index];
         }
         
+        void Automaton::addEdge(Edge const& edge) {
+            STORM_LOG_THROW(edge.getSourceLocationId() < locations.size(), storm::exceptions::InvalidArgumentException, "Cannot add edge with unknown source location index '" << edge.getSourceLocationId() << "'.");
+            edges[edge.getSourceLocationId()].addEdge(edge);
+        }
+        
+        uint64_t Automaton::getNumberOfLocations() const {
+            return edges.size();
+        }
+
     }
 }

src/storage/jani/Automaton.h

@@ -41,7 +41,7 @@ namespace storm {
             /*!
              * Retrieves the variables of this automaton.
              */
-            VariableSet const& getVariableSet() const;
+            VariableSet const& getVariables() const;
             
             /*!
              * Retrieves whether the automaton has a location with the given name.
@@ -61,6 +61,11 @@ namespace storm {
              */
             std::vector<Location> const& getLocations() const;
             
+            /*!
+             * Retrieves the location with the given index.
+             */
+            Location const& getLocation(uint64_t index) const;
+            
             /*!
              * Adds the given location to the automaton.
              */
@@ -96,6 +101,16 @@ namespace storm {
              */
             EdgeSet const& getEdgesFromLocation(uint64_t index) const;
             
+            /*!
+             * Adds an edge to the automaton.
+             */
+            void addEdge(Edge const& edge);
+            
+            /*!
+             * Retrieves the number of locations.
+             */
+            uint64_t getNumberOfLocations() const;
+            
         private:
             // The name of the automaton.
             std::string name;

src/storage/jani/BooleanVariable.h

@@ -10,7 +10,7 @@ namespace storm {
             /*!
              * Creates a boolean variable.
              */
-            BooleanVariable(std::string const& name, storm::expressions::Variable const& variable, storm::expressions::Expression const& initialValue);
+            BooleanVariable(std::string const& name, storm::expressions::Variable const& variable, storm::expressions::Expression const& initialValue = storm::expressions::Expression());
         };
         
     }

src/storage/jani/BoundedIntegerVariable.h

@@ -11,7 +11,7 @@ namespace storm {
             /*!
              * 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);
+            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 = storm::expressions::Expression());
             
             /*!
              * Retrieves the expression defining the lower bound of the variable.

src/storage/jani/Constant.cpp

@@ -3,10 +3,14 @@
 namespace storm {
     namespace jani {
         
-        Constant::Constant(std::string const& name, boost::optional<storm::expressions::Expression> const& expression) : name(name), expression(expression) {
+        Constant::Constant(std::string const& name, storm::expressions::Variable const& variable, boost::optional<storm::expressions::Expression> const& expression) : name(name), variable(variable), expression(expression) {
             // Intentionally left empty.
         }
         
+        std::string const& Constant::getName() const {
+            return name;
+        }
+        
         bool Constant::isDefined() const {
             return static_cast<bool>(expression);
         }

src/storage/jani/Constant.h

@@ -15,7 +15,12 @@ namespace storm {
             /*!
              * Creates a constant.
              */
-            Constant(std::string const& name, boost::optional<storm::expressions::Expression> const& expression = boost::none);
+            Constant(std::string const& name, storm::expressions::Variable const& variable, boost::optional<storm::expressions::Expression> const& expression = boost::none);
+            
+            /*!
+             * Retrieves the name of the constant.
+             */
+            std::string const& getName() const;
             
             /*!
              * Retrieves whether the constant is defined in the sense that it has a defining expression.

src/storage/jani/EdgeSet.cpp

@@ -23,5 +23,9 @@ namespace storm {
             return edges.cend();
         }
         
+        void EdgeSet::addEdge(Edge const& edge) {
+            edges.push_back(edge);
+        }
+        
     }
 }

src/storage/jani/EdgeSet.h

@@ -14,8 +14,13 @@ namespace storm {
             /*!
              * Creates a new set of edges.
              */
-            EdgeSet(std::vector<Edge> const& edges);
+            EdgeSet(std::vector<Edge> const& edges = std::vector<Edge>());
 
+            /*!
+             * Adds the edge to the edges.
+             */
+            void addEdge(Edge const& edge);
+            
             // Methods to get an iterator to the edges.
             iterator begin();
             iterator end();

src/storage/jani/Exporter.cpp

@@ -0,0 +1,412 @@
+#include "src/storage/jani/Exporter.h"
+
+#include <iostream>
+
+namespace storm {
+    namespace jani {
+        
+        void appendIndent(std::stringstream& out, uint64_t indent) {
+            for (uint64_t i = 0; i < indent; ++i) {
+                out << "\t";
+            }
+        }
+        
+        void appendField(std::stringstream& out, std::string const& name) {
+            out << "\"" << name << "\": ";
+        }
+        
+        void appendValue(std::stringstream& out, std::string const& value) {
+            out << "\"" << value << "\"";
+        }
+        
+        void clearLine(std::stringstream& out) {
+            out << std::endl;
+        }
+        
+        std::string expressionToString(storm::expressions::Expression const& expression) {
+            std::stringstream s;
+            s << expression;
+            return s.str();
+        }
+        
+        void Exporter::appendVersion(std::stringstream& out, uint64_t janiVersion, uint64_t indent) const {
+            appendIndent(out, indent);
+            appendField(out, "jani-version");
+        }
+        
+        void Exporter::appendModelName(std::stringstream& out, std::string const& name, uint64_t indent) const {
+            appendIndent(out, indent);
+            appendField(out, "name");
+            appendValue(out, name);
+        }
+        
+        void Exporter::appendModelType(std::stringstream& out, storm::jani::ModelType const& modelType, uint64_t indent) const {
+            appendIndent(out, indent);
+            appendField(out, "type");
+        }
+        
+        void Exporter::appendAction(std::stringstream& out, storm::jani::Action const& action, uint64_t indent) const {
+            appendIndent(out, indent);
+            out << "{" << std::endl;
+            appendIndent(out, indent + 1);
+            appendField(out, "name");
+            appendValue(out, action.getName());
+            clearLine(out);
+            appendIndent(out, indent);
+            out << "}";
+        }
+        
+        void Exporter::appendActions(std::stringstream& out, storm::jani::Model const& model, uint64_t indent) const {
+            appendIndent(out, indent);
+            appendField(out, "actions");
+            out << " [" << std::endl;
+            
+            for (uint64_t index = 0; index < model.actions.size(); ++index) {
+                appendAction(out, model.actions[index], indent + 1);
+                if (index < model.actions.size() - 1) {
+                    out << ",";
+                }
+                clearLine(out);
+            }
+            
+            appendIndent(out, indent);
+            out << "]";
+        }
+        
+        void Exporter::appendVariable(std::stringstream& out, storm::jani::BooleanVariable const& variable, uint64_t indent) const {
+            appendIndent(out, indent);
+            out << "{";
+            clearLine(out);
+            appendIndent(out, indent + 1);
+            appendField(out, "name");
+            appendValue(out, variable.getName());
+            out << ",";
+            clearLine(out);
+            appendIndent(out, indent + 1);
+            appendField(out, "type");
+            appendValue(out, "bool");
+            out << ",";
+            clearLine(out);
+            appendIndent(out, indent);
+            appendField(out, "initial-value");
+            appendValue(out, expressionToString(variable.getInitialValue()));
+            clearLine(out);
+            appendIndent(out, indent);
+            out << "}";
+        }
+
+        void Exporter::appendBoundedIntegerVariableType(std::stringstream& out, storm::jani::BoundedIntegerVariable const& variable, uint64_t indent) const {
+            out << " {";
+            clearLine(out);
+
+            appendIndent(out, indent);
+            appendField(out, "kind");
+            appendValue(out, "bounded");
+            clearLine(out);
+            
+            appendIndent(out, indent);
+            appendField(out, "base");
+            appendValue(out, "int");
+            clearLine(out);
+            
+            appendIndent(out, indent);
+            appendField(out, "lower-bound");
+            appendValue(out, expressionToString(variable.getLowerBound()));
+            clearLine(out);
+
+            appendIndent(out, indent);
+            appendField(out, "upper-bound");
+            appendValue(out, expressionToString(variable.getLowerBound()));
+            clearLine(out);
+            
+            appendIndent(out, indent - 1);
+            out << "}";
+        }
+        
+        void Exporter::appendVariable(std::stringstream& out, storm::jani::BoundedIntegerVariable const& variable, uint64_t indent) const {
+            appendIndent(out, indent);
+            out << "{";
+            clearLine(out);
+            appendIndent(out, indent + 1);
+            appendField(out, "name");
+            appendValue(out, variable.getName());
+            out << ",";
+            clearLine(out);
+            appendIndent(out, indent + 1);
+            appendField(out, "type");
+            appendBoundedIntegerVariableType(out, variable, indent + 2);
+            out << ",";
+            clearLine(out);
+            appendIndent(out, indent + 1);
+            appendField(out, "initial-value");
+            appendValue(out, expressionToString(variable.getInitialValue()));
+            clearLine(out);
+            appendIndent(out, indent);
+            out << "}";
+        }
+
+        void Exporter::appendVariable(std::stringstream& out, storm::jani::UnboundedIntegerVariable const& variable, uint64_t indent) const {
+            appendIndent(out, indent);
+            out << "{";
+            clearLine(out);
+            appendIndent(out, indent + 1);
+            appendField(out, "name");
+            appendValue(out, variable.getName());
+            out << ",";
+            clearLine(out);
+            appendIndent(out, indent + 1);
+            appendField(out, "type");
+            appendValue(out, "int");
+            out << ",";
+            clearLine(out);
+            appendIndent(out, indent + 1);
+            appendField(out, "initial-value");
+            appendValue(out, expressionToString(variable.getInitialValue()));
+            clearLine(out);
+            appendIndent(out, indent);
+            out << "}";
+        }
+        
+        void Exporter::appendVariables(std::stringstream& out, storm::jani::VariableSet const& variables, uint64_t indent) const {
+            appendIndent(out, indent);
+            appendField(out, "variables");
+            out << " [";
+            clearLine(out);
+            
+            for (auto const& variable : variables.getBooleanVariables()) {
+                appendVariable(out, variable, indent + 1);
+                clearLine(out);
+            }
+            for (auto const& variable : variables.getBoundedIntegerVariables()) {
+                appendVariable(out, variable, indent + 1);
+                clearLine(out);
+            }
+            for (auto const& variable : variables.getUnboundedIntegerVariables()) {
+                appendVariable(out, variable, indent + 1);
+                clearLine(out);
+            }
+            
+            appendIndent(out, indent);
+            out << "]";
+        }
+
+        void Exporter::appendLocation(std::stringstream& out, storm::jani::Location const& location, uint64_t indent) const {
+            appendIndent(out, indent);
+            out << "{";
+            clearLine(out);
+            
+            appendIndent(out, indent + 1);
+            appendField(out, "name");
+            appendValue(out, location.getName());
+            clearLine(out);
+
+            appendIndent(out, indent);
+            out << "}";
+        }
+        
+        void Exporter::appendLocations(std::stringstream& out, storm::jani::Automaton const& automaton, uint64_t indent) const {
+            appendIndent(out, indent);
+            appendField(out, "locations");
+            out << " [";
+            clearLine(out);
+            
+            for (auto const& location : automaton.getLocations()) {
+                appendLocation(out, location, indent + 1);
+                out << ",";
+                clearLine(out);
+            }
+            
+            appendIndent(out, indent);
+            out << "]";
+        }
+
+        void Exporter::appendAssignment(std::stringstream& out, storm::jani::Model const& model, storm::jani::Automaton const& automaton, storm::jani::Assignment const& assignment, uint64_t indent) const {
+            appendIndent(out, indent);
+            out << "{";
+            clearLine(out);
+            
+            appendIndent(out, indent + 1);
+            appendField(out, "ref");
+            storm::jani::Variable const& variable = model.getVariables().hasVariable(assignment.getExpressionVariable()) ? model.getVariables().getVariable(assignment.getExpressionVariable()) : automaton.getVariables().getVariable(assignment.getExpressionVariable());
+            appendValue(out, variable.getName());
+            out << ",";
+            clearLine(out);
+
+            appendIndent(out, indent + 1);
+            appendField(out, "value");
+            appendValue(out, expressionToString(assignment.getAssignedExpression()));
+            clearLine(out);
+
+            appendIndent(out, indent);
+            out << "}";
+        }
+        
+        void Exporter::appendEdgeDestination(std::stringstream& out, storm::jani::Model const& model, storm::jani::Automaton const& automaton, storm::jani::EdgeDestination const& destination, uint64_t indent) const {
+            appendIndent(out, indent);
+            out << "{";
+            clearLine(out);
+            
+            appendIndent(out, indent + 1);
+            appendField(out, "probability");
+            appendValue(out, expressionToString(destination.getProbability()));
+            out << ",";
+            clearLine(out);
+            
+            appendIndent(out, indent + 1);
+            appendField(out, "location");
+            appendValue(out, automaton.getLocation(destination.getLocationId()).getName());
+            out << ",";
+            clearLine(out);
+            
+            appendIndent(out, indent + 1);
+            appendField(out, "assignments");
+            out << " [";
+            clearLine(out);
+            
+            for (uint64_t index = 0; index < destination.getAssignments().size(); ++index) {
+                appendAssignment(out, model, automaton, destination.getAssignments()[index], indent + 2);
+                if (index < destination.getAssignments().size() - 1) {
+                    out << ",";
+                }
+                clearLine(out);
+            }
+            
+            appendIndent(out, indent + 1);
+            out << "]";
+            clearLine(out);
+            
+            appendIndent(out, indent);
+            out << "}";
+            clearLine(out);
+        }
+        
+        void Exporter::appendEdge(std::stringstream& out, storm::jani::Model const& model, storm::jani::Automaton const& automaton, storm::jani::Edge const& edge, uint64_t indent) const {
+            appendIndent(out, indent);
+            out << "{";
+            clearLine(out);
+            
+            appendIndent(out, indent + 1);
+            appendField(out, "location");
+            appendValue(out, automaton.getLocation(edge.getSourceLocationId()).getName());
+            out << ",";
+            clearLine(out);
+            
+            appendIndent(out, indent + 1);
+            appendField(out, "action");
+            appendValue(out, model.getAction(edge.getActionId()).getName());
+            out << ",";
+            clearLine(out);
+            
+            appendIndent(out, indent + 1);
+            appendField(out, "guard");
+            appendValue(out, expressionToString(edge.getGuard()));
+            out << ",";
+            clearLine(out);
+            
+            appendIndent(out, indent + 1);
+            appendField(out, "destinations");
+            out << " [";
+            clearLine(out);
+            
+            for (auto const& destination : edge.getDestinations()) {
+                appendEdgeDestination(out, model, automaton, destination, indent + 2);
+            }
+            
+            appendIndent(out, indent + 1);
+            out << "]";
+            clearLine(out);
+            
+            appendIndent(out, indent);
+            out << "}";
+        }
+        
+        void Exporter::appendEdges(std::stringstream& out, storm::jani::Model const& model, storm::jani::Automaton const& automaton, uint64_t indent) const {
+            appendIndent(out, indent);
+            appendField(out, "edges");
+            out << " [";
+            clearLine(out);
+            
+            for (uint64_t location = 0; location < automaton.getNumberOfLocations(); ++location) {
+                for (auto const& edge : automaton.getEdgesFromLocation(location)) {
+                    appendEdge(out, model, automaton, edge, indent + 1);
+                    out << ",";
+                    clearLine(out);
+                }
+            }
+            
+            appendIndent(out, indent);
+            out << "]";
+            clearLine(out);
+        }
+        
+        void Exporter::appendAutomaton(std::stringstream& out, storm::jani::Model const& model, storm::jani::Automaton const& automaton, uint64_t indent) const {
+            appendIndent(out, indent);
+            out << "{";
+            clearLine(out);
+
+            appendIndent(out, indent + 1);
+            appendField(out, "name");
+            appendValue(out, automaton.getName());
+            clearLine(out);
+            appendVariables(out, automaton.getVariables(), indent + 1);
+            out << ",";
+            clearLine(out);
+            
+            appendLocations(out, automaton, indent + 1);
+            out << ",";
+            clearLine(out);
+            appendIndent(out, indent + 1);
+            appendField(out, "initial-location");
+            appendValue(out, std::to_string(automaton.getInitialLocationIndex()));
+            clearLine(out);
+            
+            appendEdges(out, model, automaton, indent + 1);
+            
+            appendIndent(out, indent);
+            out << "}";
+        }
+        
+        void Exporter::appendAutomata(std::stringstream& out, storm::jani::Model const& model, uint64_t indent) const {
+            appendIndent(out, indent);
+            appendField(out, "automata");
+            out << " [";
+            clearLine(out);
+            
+            for (uint64_t index = 0; index < model.automata.size(); ++index) {
+                appendAutomaton(out, model, model.automata[index], indent + 1);
+                if (index < model.automata.size() - 1) {
+                    out << ",";
+                }
+                clearLine(out);
+            }
+            
+            appendIndent(out, indent);
+            out << "]";
+        }
+        
+        std::string Exporter::toJaniString(storm::jani::Model const& model) const {
+            std::stringstream out;
+            
+            out << "{" << std::endl;
+            appendVersion(out, model.getJaniVersion(), 1);
+            out << ",";
+            clearLine(out);
+            appendModelName(out, model.getName(), 1);
+            out << ",";
+            clearLine(out);
+            appendModelType(out, model.getModelType(), 1);
+            out << ",";
+            clearLine(out);
+            appendActions(out, model, 1);
+            clearLine(out);
+            appendVariables(out, model.getVariables(), 1);
+            clearLine(out);
+            appendAutomata(out, model, 1);
+            clearLine(out);
+            out << "}" << std::endl;
+            
+            return out.str();
+        }
+        
+    }
+}

src/storage/jani/Exporter.h

@@ -0,0 +1,48 @@
+#pragma once
+
+#include <sstream>
+#include <cstdint>
+
+#include "src/storage/jani/Model.h"
+
+namespace storm {
+    namespace jani {
+        
+        class Exporter {
+        public:
+            Exporter() = default;
+            
+            std::string toJaniString(storm::jani::Model const& model) const;
+            
+        private:
+            void appendVersion(std::stringstream& out, uint64_t janiVersion, uint64_t indent) const;
+            
+            void appendModelName(std::stringstream& out, std::string const& name, uint64_t indent) const;
+            
+            void appendModelType(std::stringstream& out, storm::jani::ModelType const& modelType, uint64_t indent) const;
+            
+            void appendAction(std::stringstream& out, storm::jani::Action const& action, uint64_t indent) const;
+            
+            void appendActions(std::stringstream& out, storm::jani::Model const& model, uint64_t indent) const;
+            
+            void appendVariables(std::stringstream& out, storm::jani::VariableSet const& variables, uint64_t indent) const;
+            
+            void appendVariable(std::stringstream& out, storm::jani::BooleanVariable const& variable, uint64_t indent) const;
+            void appendVariable(std::stringstream& out, storm::jani::BoundedIntegerVariable const& variable, uint64_t indent) const;
+            void appendBoundedIntegerVariableType(std::stringstream& out, storm::jani::BoundedIntegerVariable const& variable, uint64_t indent) const;
+            void appendVariable(std::stringstream& out, storm::jani::UnboundedIntegerVariable const& variable, uint64_t indent) const;
+
+            void appendAutomata(std::stringstream& out, storm::jani::Model const& model, uint64_t indent) const;
+            void appendAutomaton(std::stringstream& out, storm::jani::Model const& model, storm::jani::Automaton const& automaton, uint64_t indent) const;
+            
+            void appendLocation(std::stringstream& out, storm::jani::Location const& location, uint64_t indent) const;
+            void appendLocations(std::stringstream& out, storm::jani::Automaton const& automaton, uint64_t indent) const;
+            
+            void appendAssignment(std::stringstream& out, storm::jani::Model const& model, storm::jani::Automaton const& automaton, storm::jani::Assignment const& assignment, uint64_t indent) const;
+            void appendEdgeDestination(std::stringstream& out, storm::jani::Model const& model, storm::jani::Automaton const& automaton, storm::jani::EdgeDestination const& destination, uint64_t indent) const;
+            void appendEdge(std::stringstream& out, storm::jani::Model const& model, storm::jani::Automaton const& automaton, storm::jani::Edge const& edge, uint64_t indent) const;
+            void appendEdges(std::stringstream& out, storm::jani::Model const& model, storm::jani::Automaton const& automaton, uint64_t indent) const;
+        };
+        
+    }
+}

src/storage/jani/Model.cpp

@@ -1,54 +1,154 @@
-#include <src/exceptions/InvalidJaniException.h>
 #include "src/storage/jani/Model.h"
 
+#include "src/storage/expressions/ExpressionManager.h"
+
+#include "src/storage/jani/AutomatonComposition.h"
+#include "src/storage/jani/ParallelComposition.h"
+#include "src/storage/jani/RenameComposition.h"
+
+#include "src/utility/macros.h"
+#include "src/exceptions/WrongFormatException.h"
+
 namespace storm {
     namespace jani {
         
-        Model::Model(std::string const& name, ModelType const& modelType, uint64_t version) : name(name), modelType(modelType), version(version) {
+        static const std::string SILENT_ACTION_NAME = "";
+        
+        Model::Model() {
             // Intentionally left empty.
         }
-
-        uint64_t Model::addAction(Action const& act) {
-            STORM_LOG_THROW(actionToIndex.count(act.getName()) == 0, storm::exceptions::InvalidJaniException, "Action with name " + act.getName() + " already exists");
-            actionToIndex.emplace(act.getName(), actions.size());
-            actions.push_back(act);
+        
+        Model::Model(std::string const& name, ModelType const& modelType, uint64_t version, boost::optional<std::shared_ptr<storm::expressions::ExpressionManager>> const& expressionManager) : name(name), modelType(modelType), version(version), composition(nullptr) {
+            // Use the provided manager or create a new one.
+            if (expressionManager) {
+                this->expressionManager = expressionManager.get();
+            } else {
+                this->expressionManager = std::make_shared<storm::expressions::ExpressionManager>();
+            }
+            
+            // Add a prefined action that represents the silent action.
+            silentActionIndex = addAction(storm::jani::Action(SILENT_ACTION_NAME));
+        }
+        
+        uint64_t Model::getJaniVersion() const {
+            return version;
+        }
+        
+        ModelType const& Model::getModelType() const {
+            return modelType;
+        }
+        
+        std::string const& Model::getName() const {
+            return name;
+        }
+        
+        uint64_t Model::addAction(Action const& action) {
+            auto it = actionToIndex.find(action.getName());
+            STORM_LOG_THROW(it == actionToIndex.end(), storm::exceptions::WrongFormatException, "Action with name '" << action.getName() << "' already exists");
+            actionToIndex.emplace(action.getName(), actions.size());
+            actions.push_back(action);
             return actions.size() - 1;
         }
-
-        bool Model::hasAction(std::string const &name) const {
-            return actionToIndex.count(name) != 0;
+        
+        Action const& Model::getAction(uint64_t index) const {
+            return actions[index];
         }
-
+        
+        bool Model::hasAction(std::string const& name) const {
+            return actionToIndex.find(name) != actionToIndex.end();
+        }
+        
         uint64_t Model::getActionIndex(std::string const& name) const {
-            assert(this->hasAction(name));
-            return actionToIndex.at(name);
+            auto it = actionToIndex.find(name);
+            STORM_LOG_THROW(it != actionToIndex.end(), storm::exceptions::WrongFormatException, "Unable to retrieve index of unknown action '" << name << "'.");
+            return it->second;
         }
-
-
-        void Model::checkSupported() const {
-            //TODO
+        
+        uint64_t Model::addConstant(Constant const& constant) {
+            auto it = constantToIndex.find(constant.getName());
+            STORM_LOG_THROW(it == constantToIndex.end(), storm::exceptions::WrongFormatException, "Cannot add constant with name '" << constant.getName() << "', because a constant with that name already exists.");
+            constantToIndex.emplace(constant.getName(), constants.size());
+            constants.push_back(constant);
+            return constants.size() - 1;
         }
-
+        
+        void Model::addBooleanVariable(BooleanVariable const& variable) {
+            globalVariables.addBooleanVariable(variable);
+        }
+        
+        void Model::addBoundedIntegerVariable(BoundedIntegerVariable const& variable) {
+            globalVariables.addBoundedIntegerVariable(variable);
+        }
+        
+        void Model::addUnboundedIntegerVariable(UnboundedIntegerVariable const& variable) {
+            globalVariables.addUnboundedIntegerVariable(variable);
+        }
+        
+        VariableSet const& Model::getVariables() const {
+            return globalVariables;
+        }
+        
+        storm::expressions::ExpressionManager& Model::getExpressionManager() {
+            return *expressionManager;
+        }
+        
+        storm::expressions::ExpressionManager const& Model::getExpressionManager() const {
+            return *expressionManager;
+        }
+        
+        uint64_t Model::addAutomaton(Automaton const& automaton) {
+            auto it = automatonToIndex.find(automaton.getName());
+            STORM_LOG_THROW(it == automatonToIndex.end(), storm::exceptions::WrongFormatException, "Automaton with name '" << automaton.getName() << "' already exists.");
+            automatonToIndex.emplace(automaton.getName(), automata.size());
+            automata.push_back(automaton);
+            return automata.size() - 1;
+        }
+        
+        std::shared_ptr<Composition> Model::getStandardSystemComposition() const {
+            std::set<std::string> fullSynchronizationAlphabet = getActionNames(false);
+            
+            std::shared_ptr<Composition> current;
+            current = std::make_shared<AutomatonComposition>(this->automata.front().getName());
+            for (uint64_t index = 1; index < automata.size(); ++index) {
+                current = std::make_shared<ParallelComposition>(current, std::make_shared<AutomatonComposition>(automata[index].getName()), fullSynchronizationAlphabet);
+            }
+            return current;
+        }
+        
+        Composition const& Model::getSystemComposition() const {
+            return *composition;
+        }
+        
+        std::set<std::string> Model::getActionNames(bool includeSilent) const {
+            std::set<std::string> result;
+            for (auto const& entry : actionToIndex) {
+                if (includeSilent || entry.second != silentActionIndex) {
+                    result.insert(entry.first);
+                }
+            }
+            return result;
+        }
+        
         bool Model::checkValidity(bool logdbg) const {
             // TODO switch to exception based return value.
-
+            
             if (version == 0) {
                 if(logdbg) STORM_LOG_DEBUG("Jani version is unspecified");
                 return false;
             }
-
+            
             if(modelType == ModelType::UNDEFINED) {
                 if(logdbg) STORM_LOG_DEBUG("Model type is unspecified");
                 return false;
             }
-
+            
             if(automata.empty()) {
                 if(logdbg) STORM_LOG_DEBUG("No automata specified");
                 return false;
             }
             // All checks passed.
             return true;
-
+            
         }
         
     }

src/storage/jani/Model.h

@@ -1,25 +1,55 @@
 #pragma once
 
-#include "src/utility/macros.h"
+#include <memory>
 
 #include "src/storage/jani/Action.h"
 #include "src/storage/jani/ModelType.h"
 #include "src/storage/jani/Automaton.h"
+#include "src/storage/jani/Constant.h"
+#include "src/storage/jani/Composition.h"
 
 namespace storm {
+    namespace expressions {
+        class ExpressionManager;
+    }
+    
     namespace jani {
-
+        
+        class Exporter;
+        
         class Model {
         public:
+            friend class Exporter;
+            
+            /*!
+             * Creates an uninitialized model.
+             */
+            Model();
+            
             /*!
              * Creates an empty model with the given type.
              */
-            Model(std::string const& name, ModelType const& modelType, uint64_t version = 1);
-
+            Model(std::string const& name, ModelType const& modelType, uint64_t version = 1, boost::optional<std::shared_ptr<storm::expressions::ExpressionManager>> const& expressionManager = boost::none);
+            
+            /*!
+             * Retrieves the JANI-version of the model.
+             */
+            uint64_t getJaniVersion() const;
+            
+            /*!
+             * Retrieves the type of the model.
+             */
+            ModelType const& getModelType() const;
+            
+            /*!
+             * Retrievest the name of the model.
+             */
+            std::string const& getName() const;
+            
             /**
              * Checks whether the model has an action with the given name.
-             * 
-             * @param name The name to look for. 
+             *
+             * @param name The name to look for.
              */
             bool hasAction(std::string const& name) const;
             
@@ -35,39 +65,122 @@ namespace storm {
              *
              * @return the index for this action.
              */
-            uint64_t addAction(Action const& act);
-
+            uint64_t addAction(Action const& action);
+            
             /*!
-             *  Does some simple checks to determine whether the model is supported by Prism.
-             *  Mainly checks abscence of features the parser supports.
-             *
-             *  Throws UnsupportedModelException if something is wrong
+             * Retrieves the action with the given index.
              */
-            // TODO add engine as argument to check this for several engines.
-            void checkSupported() const;
+            Action const& getAction(uint64_t index) const;
+            
+            /*!
+             * Adds the given constant to the model.
+             */
+            uint64_t addConstant(Constant const& constant);
+            
+            /*!
+             * Adds the given boolean variable to this model.
+             */
+            void addBooleanVariable(BooleanVariable const& variable);
+            
+            /*!
+             * Adds the given bounded integer variable to this model.
+             */
+            void addBoundedIntegerVariable(BoundedIntegerVariable const& variable);
+            
+            /*!
+             * Adds the given unbounded integer variable to this model.
+             */
+            void addUnboundedIntegerVariable(UnboundedIntegerVariable const& variable);
+            
+            /*!
+             * Retrieves the variables of this automaton.
+             */
+            VariableSet const& getVariables() const;
+            
+            /*!
+             * Retrieves the manager responsible for the expressions in the JANI model.
+             */
+            storm::expressions::ExpressionManager& getExpressionManager();
 
-             /*!
+            /*!
+             * Retrieves the manager responsible for the expressions in the JANI model.
+             */
+            storm::expressions::ExpressionManager const& getExpressionManager() const;
+            
+            /*!
+             * Adds the given automaton to the automata of this model.
+             */
+            uint64_t addAutomaton(Automaton const& automaton);
+            
+            /*!
+             * Sets the system composition expression of the JANI model.
+             */
+            void setSystemComposition(std::shared_ptr<Composition> const& composition);
+            
+            /*!
+             * Gets the system composition as the standard, fully-synchronizing parallel composition.
+             */
+            std::shared_ptr<Composition> getStandardSystemComposition() const;
+            
+            /*!
+             * Retrieves the system composition expression.
+             */
+            Composition const& getSystemComposition() const;
+            
+            /*!
+             * Retrieves the set of action names.
+             */
+            std::set<std::string> getActionNames(bool includeSilent = true) const;
+            
+            /*!
+             * Retrieves the name of the silent action.
+             */
+            std::string const& getSilentActionName() const;
+            
+            /*!
              *  Checks if the model is valid JANI, which should be verified before any further operations are applied to a model.
              */
-             bool checkValidity(bool logdbg = true) const;
+            bool checkValidity(bool logdbg = true) const;
+            
         private:
-            /// The model name
+            /// The model name.
             std::string name;
-            /// The list of automata
-            std::vector<Automaton> automata;
-            /// A mapping from names to automata indices
-            std::unordered_map<std::string, size_t> automatonToIndex;
-            /// The list with actions
-            std::vector<Action> actions;
-            /// A mapping from names to action indices
-            std::unordered_map<std::string, uint64_t> actionToIndex;
-
+            
             /// The type of the model.
             ModelType modelType;
+            
             /// The JANI-version used to specify the model.
             uint64_t version;
-
-
+            
+            /// The manager responsible for the expressions in this model.
+            std::shared_ptr<storm::expressions::ExpressionManager> expressionManager;
+            
+            /// The list of actions.
+            std::vector<Action> actions;
+            
+            /// A mapping from names to action indices.
+            std::unordered_map<std::string, uint64_t> actionToIndex;
+            
+            /// The index of the silent action.
+            uint64_t silentActionIndex;
+            
+            /// The constants defined by the model.
+            std::vector<Constant> constants;
+            
+            /// A mapping from names to constants.
+            std::unordered_map<std::string, uint64_t> constantToIndex;
+            
+            /// The global variables of the model.
+            VariableSet globalVariables;
+            
+            /// The list of automata.
+            std::vector<Automaton> automata;
+            
+            /// A mapping from names to automata indices.
+            std::unordered_map<std::string, size_t> automatonToIndex;
+            
+            /// An expression describing how the system is composed of the automata.
+            std::shared_ptr<Composition> composition;
         };
     }
 }

src/storage/jani/ModelType.cpp

@@ -17,6 +17,9 @@ namespace storm {
                 case ModelType::MDP:
                     stream << "mdp";
                     break;
+                case ModelType::CTMDP:
+                    stream << "ctmdp";
+                    break;
                 case ModelType::MA:
                     stream << "ma";
                     break;
@@ -31,22 +34,25 @@ namespace storm {
         }
 
         ModelType getModelType(std::string const& input) {
-            if(input == "dtmc") {
+            if (input == "dtmc") {
                 return ModelType::DTMC;
             }
-            if(input == "ctmc") {
+            if (input == "ctmc") {
                 return ModelType::CTMC;
             }
-            if(input == "mdp") {
+            if (input == "mdp") {
                 return ModelType::MDP;
             }
-            if(input == "ma") {
+            if (input == "ctmdp") {
+                return ModelType::CTMDP;
+            }
+            if (input == "ma") {
                 return ModelType::MA;
             }
-            if(input == "pta") {
+            if (input == "pta") {
                 return ModelType::PTA;
             }
-            if(input == "sta") {
+            if (input == "sta") {
                 return ModelType::STA;
             }
             return ModelType::UNDEFINED;

src/storage/jani/ModelType.h

@@ -5,7 +5,7 @@
 namespace storm {
     namespace jani {
         
-        enum class ModelType {UNDEFINED = 0, DTMC = 1, CTMC = 2, MDP = 3, MA = 4, PTA = 5, STA = 6};
+        enum class ModelType {UNDEFINED = 0, DTMC = 1, CTMC = 2, MDP = 3, CTMDP = 4, MA = 5, PTA = 6, STA = 7};
 
         ModelType getModelType(std::string const& input);
         std::ostream& operator<<(std::ostream& stream, ModelType const& type);

src/storage/jani/UnboundedIntegerVariable.h

@@ -10,7 +10,7 @@ namespace storm {
             /*!
              * Creates an unbounded integer variable.
              */
-            UnboundedIntegerVariable(std::string const& name, storm::expressions::Variable const& variable, storm::expressions::Expression const& initialValue);
+            UnboundedIntegerVariable(std::string const& name, storm::expressions::Variable const& variable, storm::expressions::Expression const& initialValue = storm::expressions::Expression());
         };
         
     }

src/storage/jani/Variable.cpp

@@ -1,5 +1,7 @@
 #include "src/storage/jani/Variable.h"
 
+#include <iostream>
+
 namespace storm {
     namespace jani {
         
@@ -11,9 +13,17 @@ namespace storm {
             return variable;
         }
 
+        bool Variable::hasInitialValue() const {
+            return initialValue.isInitialized();
+        }
+        
         std::string const& Variable::getName() const {
             return name;
         }
         
+        storm::expressions::Expression const& Variable::getInitialValue() const {
+            return initialValue;
+        }
+        
     }
 }

src/storage/jani/Variable.h

@@ -31,6 +31,11 @@ namespace storm {
              */
             storm::expressions::Expression const& getInitialValue() const;
             
+            /*!
+             * Retrieves whether the variable has an initial value.
+             */
+            bool hasInitialValue() const;
+            
         private:
             // The name of the variable.
             std::string name;

src/storage/jani/VariableSet.cpp

@@ -97,29 +97,32 @@ namespace storm {
         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());
+            nameToVariable.emplace(variable.getName(), variable.getExpressionVariable());
+            variableToVariable.emplace(variable.getExpressionVariable(), std::make_pair(0, booleanVariables.size() - 1));
         }
         
         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());
+            nameToVariable.emplace(variable.getName(), variable.getExpressionVariable());
+            variableToVariable.emplace(variable.getExpressionVariable(), std::make_pair(1, boundedIntegerVariables.size() - 1));
         }
         
         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());
+            nameToVariable.emplace(variable.getName(), variable.getExpressionVariable());
+            variableToVariable.emplace(variable.getExpressionVariable(), std::make_pair(2, boundedIntegerVariables.size() - 1));
         }
         
         bool VariableSet::hasVariable(std::string const& name) const {
-            return variables.find(name) != variables.end();
+            return nameToVariable.find(name) != nameToVariable.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();
+            auto it = nameToVariable.find(name);
+            STORM_LOG_THROW(it != nameToVariable.end(), storm::exceptions::InvalidArgumentException, "Unable to retrieve unknown variable '" << name << "'.");
+            return getVariable(it->second);
         }
         
         detail::VariableSetIterator VariableSet::begin() const {
@@ -130,5 +133,21 @@ namespace storm {
             return detail::VariableSetIterator(*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() << "'.");
+            
+            if (it->second.first == 0) {
+                return booleanVariables[it->second.second];
+            } else if (it->second.first == 1) {
+                return boundedIntegerVariables[it->second.second];
+            } else {
+                return unboundedIntegerVariables[it->second.second];
+            }
+        }
+        
+        bool VariableSet::hasVariable(storm::expressions::Variable const& variable) const {
+            return variableToVariable.find(variable) != variableToVariable.end();
+        }
     }
 }

src/storage/jani/VariableSet.h

@@ -121,7 +121,17 @@ namespace storm {
              * Retrieves the variable with the given name.
              */
             Variable const& getVariable(std::string const& name) const;
+
+            /*!
+             * Retrieves whether this variable set contains a variable with the expression variable.
+             */
+            bool hasVariable(storm::expressions::Variable const& variable) const;
             
+            /*!
+             * Retrieves the variable object associated with the given expression variable (if any).
+             */
+            Variable const& getVariable(storm::expressions::Variable const& variable) const;
+
             /*!
              * Retrieves an iterator to the variables in this set.
              */
@@ -131,19 +141,22 @@ namespace storm {
              * Retrieves the end iterator to the variables in this set.
              */
             detail::VariableSetIterator end() const;
-
+            
         private:
-            // The boolean variables in this set.
+            /// The boolean variables in this set.
             std::vector<BooleanVariable> booleanVariables;
 
-            // The bounded integer variables in this set.
+            /// The bounded integer variables in this set.
             std::vector<BoundedIntegerVariable> boundedIntegerVariables;
 
-            // The unbounded integer variables in this set.
+            /// 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;
+            /// A set of all variable names currently in use.
+            std::map<std::string, storm::expressions::Variable> nameToVariable;
+            
+            /// A mapping from expression variables to their variable objects.
+            std::map<storm::expressions::Variable, std::pair<uint8_t, uint64_t>> variableToVariable;
         };
         
     }

src/storage/prism/Program.cpp

@@ -13,8 +13,11 @@
 #include "src/exceptions/OutOfRangeException.h"
 #include "src/exceptions/WrongFormatException.h"
 #include "src/exceptions/InvalidTypeException.h"
+#include "src/exceptions/InvalidOperationException.h"
 #include "src/solver/SmtSolver.h"
 
+#include "src/storage/jani/Model.h"
+
 #include "src/storage/prism/CompositionVisitor.h"
 #include "src/storage/prism/Compositions.h"
 
@@ -45,7 +48,7 @@ namespace storm {
             
             virtual boost::any visit(RenamingComposition const& composition, boost::any const& data) override {
                 std::set<uint_fast64_t> subSynchronizingActionIndices = boost::any_cast<std::set<uint_fast64_t>>(composition.getSubcomposition().accept(*this, data));
-
+                
                 std::set<uint_fast64_t> newSynchronizingActionIndices = subSynchronizingActionIndices;
                 for (auto const& namePair : composition.getActionRenaming()) {
                     if (!program.hasAction(namePair.first)) {
@@ -79,7 +82,7 @@ namespace storm {
                         subSynchronizingActionIndices.erase(it);
                     }
                 }
-
+                
                 return subSynchronizingActionIndices;
             }
             
@@ -96,7 +99,7 @@ namespace storm {
             virtual boost::any visit(InterleavingParallelComposition const& composition, boost::any const& data) override {
                 std::set<uint_fast64_t> leftSynchronizingActionIndices = boost::any_cast<std::set<uint_fast64_t>>(composition.getLeftSubcomposition().accept(*this, data));
                 std::set<uint_fast64_t> rightSynchronizingActionIndices = boost::any_cast<std::set<uint_fast64_t>>(composition.getRightSubcomposition().accept(*this, data));
-
+                
                 std::set<uint_fast64_t> synchronizingActionIndices;
                 std::set_union(leftSynchronizingActionIndices.begin(), leftSynchronizingActionIndices.end(), rightSynchronizingActionIndices.begin(), rightSynchronizingActionIndices.end(), std::inserter(synchronizingActionIndices, synchronizingActionIndices.begin()));
                 
@@ -132,18 +135,18 @@ namespace storm {
         
         Program::Program(std::shared_ptr<storm::expressions::ExpressionManager> manager, ModelType modelType, std::vector<Constant> const& constants, std::vector<BooleanVariable> const& globalBooleanVariables, std::vector<IntegerVariable> const& globalIntegerVariables, std::vector<Formula> const& formulas, std::vector<Module> const& modules, std::map<std::string, uint_fast64_t> const& actionToIndexMap, std::vector<RewardModel> const& rewardModels, std::vector<Label> const& labels, boost::optional<InitialConstruct> const& initialConstruct, boost::optional<SystemCompositionConstruct> const& compositionConstruct, std::string const& filename, uint_fast64_t lineNumber, bool finalModel)
         : LocatedInformation(filename, lineNumber), manager(manager),
-            modelType(modelType), constants(constants), constantToIndexMap(),
-            globalBooleanVariables(globalBooleanVariables), globalBooleanVariableToIndexMap(),
-            globalIntegerVariables(globalIntegerVariables), globalIntegerVariableToIndexMap(), 
-            formulas(formulas), formulaToIndexMap(), modules(modules), moduleToIndexMap(), 
-            rewardModels(rewardModels), rewardModelToIndexMap(), systemCompositionConstruct(compositionConstruct),
-            labels(labels), labelToIndexMap(), actionToIndexMap(actionToIndexMap), indexToActionMap(), actions(),
-            synchronizingActionIndices(), actionIndicesToModuleIndexMap(), variableToModuleIndexMap()
+        modelType(modelType), constants(constants), constantToIndexMap(),
+        globalBooleanVariables(globalBooleanVariables), globalBooleanVariableToIndexMap(),
+        globalIntegerVariables(globalIntegerVariables), globalIntegerVariableToIndexMap(),
+        formulas(formulas), formulaToIndexMap(), modules(modules), moduleToIndexMap(),
+        rewardModels(rewardModels), rewardModelToIndexMap(), systemCompositionConstruct(compositionConstruct),
+        labels(labels), labelToIndexMap(), actionToIndexMap(actionToIndexMap), indexToActionMap(), actions(),
+        synchronizingActionIndices(), actionIndicesToModuleIndexMap(), variableToModuleIndexMap()
         {
-
+            
             // Start by creating the necessary mappings from the given ones.
             this->createMappings();
-
+            
             // Set the initial construct.
             if (initialConstruct) {
                 this->initialConstruct = initialConstruct.get();
@@ -167,7 +170,7 @@ namespace storm {
                 }
                 this->initialConstruct = storm::prism::InitialConstruct(newInitialExpression, this->getInitialConstruct().getFilename(), this->getInitialConstruct().getLineNumber());
             }
-
+            
             if (finalModel) {
                 // If the model is supposed to be a CTMC, but contains probabilistic commands, we transform them to Markovian
                 // commands and issue a warning.
@@ -187,7 +190,7 @@ namespace storm {
                 this->checkValidity(Program::ValidityCheckLevel::VALIDINPUT);
             }
         }
-    
+        
         Program::ModelType Program::getModelType() const {
             return modelType;
         }
@@ -264,12 +267,12 @@ namespace storm {
             for (auto const& module : this->getModules()) {
                 module.containsVariablesOnlyInUpdateProbabilities(undefinedConstantVariables);
             }
-
+            
             // Check the reward models.
             for (auto const& rewardModel : this->getRewardModels()) {
                 rewardModel.containsVariablesOnlyInRewardValueExpressions(undefinedConstantVariables);
             }
-                     
+            
             // Initial construct.
             if (this->getInitialConstruct().getInitialStatesExpression().containsVariable(undefinedConstantVariables)) {
                 return false;
@@ -294,7 +297,7 @@ namespace storm {
             }
             return result;
         }
-
+        
         std::string Program::getUndefinedConstantsAsString() const {
             std::stringstream stream;
             bool printComma = false;
@@ -332,12 +335,12 @@ namespace storm {
             }
             return constantsSubstitution;
         }
-
-    
+        
+        
         std::size_t Program::getNumberOfConstants() const {
             return this->getConstants().size();
         }
-
+        
         std::vector<BooleanVariable> const& Program::getGlobalBooleanVariables() const {
             return this->globalBooleanVariables;
         }
@@ -359,7 +362,7 @@ namespace storm {
             STORM_LOG_THROW(nameIndexPair != this->globalBooleanVariableToIndexMap.end(), storm::exceptions::OutOfRangeException, "Unknown boolean variable '" << variableName << "'.");
             return this->getGlobalBooleanVariables()[nameIndexPair->second];
         }
-
+        
         IntegerVariable const& Program::getGlobalIntegerVariable(std::string const& variableName) const {
             auto const& nameIndexPair = this->globalIntegerVariableToIndexMap.find(variableName);
             STORM_LOG_THROW(nameIndexPair != this->globalIntegerVariableToIndexMap.end(), storm::exceptions::OutOfRangeException, "Unknown integer variable '" << variableName << "'.");
@@ -542,7 +545,7 @@ namespace storm {
             STORM_LOG_THROW(it == this->labels.end(), storm::exceptions::InvalidArgumentException, "Cannot add a label '" << name << "', because a label with that name already exists.");
             this->labels.emplace_back(name, statePredicateExpression);
         }
-
+        
         void Program::removeLabel(std::string const& name) {
             auto it = std::find_if(this->labels.begin(), this->labels.end(), [&name] (storm::prism::Label const& label) { return label.getName() == name; });
             STORM_LOG_THROW(it != this->labels.end(), storm::exceptions::InvalidArgumentException, "Canno remove unknown label '" << name << "'.");
@@ -630,7 +633,7 @@ namespace storm {
                     this->variableToModuleIndexMap[integerVariable.getName()] = moduleIndex;
                 }
             }
-
+            
         }
         
         Program Program::defineUndefinedConstants(std::map<storm::expressions::Variable, storm::expressions::Expression> const& constantDefinitions) const {
@@ -686,7 +689,7 @@ namespace storm {
                 // Put the corresponding expression in the substitution.
                 if(constant.isDefined()) {
                     constantSubstitution.emplace(constant.getExpressionVariable(), constant.getExpression().simplify());
-                
+                    
                     // If there is at least one more constant to come, we substitute the constants we have so far.
                     if (constantIndex + 1 < newConstants.size()) {
                         newConstants[constantIndex + 1] = newConstants[constantIndex + 1].substitute(constantSubstitution);
@@ -774,7 +777,7 @@ namespace storm {
                 std::set<storm::expressions::Variable> illegalVariables;
                 std::set_difference(containedVariables.begin(), containedVariables.end(), constants.begin(), constants.end(), std::inserter(illegalVariables, illegalVariables.begin()));
                 bool isValid = illegalVariables.empty();
-
+                
                 if (!isValid) {
                     std::vector<std::string> illegalVariableNames;
                     for (auto const& var : illegalVariables) {
@@ -782,7 +785,7 @@ namespace storm {
                     }
                     STORM_LOG_THROW(isValid, storm::exceptions::WrongFormatException, "Error in " << variable.getFilename() << ", line " << variable.getLineNumber() << ": initial value expression refers to unknown constants: " << boost::algorithm::join(illegalVariableNames, ",") << ".");
                 }
-
+                
                 // Record the new identifier for future checks.
                 variables.insert(variable.getExpressionVariable());
                 all.insert(variable.getExpressionVariable());
@@ -795,7 +798,7 @@ namespace storm {
                 std::set<storm::expressions::Variable> illegalVariables;
                 std::set_difference(containedVariables.begin(), containedVariables.end(), constants.begin(), constants.end(), std::inserter(illegalVariables, illegalVariables.begin()));
                 bool isValid = illegalVariables.empty();
-
+                
                 if (!isValid) {
                     std::vector<std::string> illegalVariableNames;
                     for (auto const& var : illegalVariables) {
@@ -803,7 +806,7 @@ namespace storm {
                     }
                     STORM_LOG_THROW(isValid, storm::exceptions::WrongFormatException, "Error in " << variable.getFilename() << ", line " << variable.getLineNumber() << ": lower bound expression refers to unknown constants: " << boost::algorithm::join(illegalVariableNames, ",") << ".");
                 }
-
+                
                 containedVariables = variable.getLowerBoundExpression().getVariables();
                 std::set_difference(containedVariables.begin(), containedVariables.end(), constants.begin(), constants.end(), std::inserter(illegalVariables, illegalVariables.begin()));
                 isValid = illegalVariables.empty();
@@ -833,7 +836,7 @@ namespace storm {
                 allGlobals.insert(variable.getExpressionVariable());
                 globalVariables.insert(variable.getExpressionVariable());
             }
-
+            
             // Now go through the variables of the modules.
             for (auto const& module : this->getModules()) {
                 for (auto const& variable : module.getBooleanVariables()) {
@@ -963,7 +966,7 @@ namespace storm {
                         std::set<storm::expressions::Variable> alreadyAssignedVariables;
                         for (auto const& assignment : update.getAssignments()) {
                             storm::expressions::Variable assignedVariable = manager->getVariable(assignment.getVariableName());
-
+                            
                             if (legalVariables.find(assignedVariable) == legalVariables.end()) {
                                 if (all.find(assignedVariable) != all.end()) {
                                     STORM_LOG_THROW(false, storm::exceptions::WrongFormatException, "Error in " << command.getFilename() << ", line " << command.getLineNumber() << ": assignment illegally refers to variable '" << assignment.getVariableName() << "'.");
@@ -1038,12 +1041,12 @@ namespace storm {
                     bool isValid = std::includes(variablesAndConstants.begin(), variablesAndConstants.end(), containedVariables.begin(), containedVariables.end());
                     STORM_LOG_THROW(isValid, storm::exceptions::WrongFormatException, "Error in " << transitionReward.getFilename() << ", line " << transitionReward.getLineNumber() << ": state reward expression refers to unknown identifiers.");
                     STORM_LOG_THROW(transitionReward.getSourceStatePredicateExpression().hasBooleanType(), storm::exceptions::WrongFormatException, "Error in " << transitionReward.getFilename() << ", line " << transitionReward.getLineNumber() << ": state predicate must evaluate to type 'bool'.");
-
+                    
                     containedVariables = transitionReward.getTargetStatePredicateExpression().getVariables();
                     isValid = std::includes(variablesAndConstants.begin(), variablesAndConstants.end(), containedVariables.begin(), containedVariables.end());
                     STORM_LOG_THROW(isValid, storm::exceptions::WrongFormatException, "Error in " << transitionReward.getFilename() << ", line " << transitionReward.getLineNumber() << ": state reward expression refers to unknown identifiers.");
                     STORM_LOG_THROW(transitionReward.getTargetStatePredicateExpression().hasBooleanType(), storm::exceptions::WrongFormatException, "Error in " << transitionReward.getFilename() << ", line " << transitionReward.getLineNumber() << ": state predicate must evaluate to type 'bool'.");
-
+                    
                     
                     containedVariables = transitionReward.getRewardValueExpression().getVariables();
                     isValid = std::includes(variablesAndConstants.begin(), variablesAndConstants.end(), containedVariables.begin(), containedVariables.end());
@@ -1088,14 +1091,14 @@ namespace storm {
                     for (auto const& command : module.getCommands()) {
                         if(!command.isLabeled()) continue;
                         for (auto const& update : command.getUpdates()) {
-                             for (auto const& assignment : update.getAssignments()) {
-                                 if(this->globalBooleanVariableExists(assignment.getVariable().getName())) {
-                                     globalBVarsWrittenToByCommandInThisModule.insert({assignment.getVariable().getName(), command.getActionName()});
-                                 }
-                                 else if(this->globalIntegerVariableExists(assignment.getVariable().getName())) {
-                                     globalIVarsWrittenToByCommandInThisModule.insert({assignment.getVariable().getName(), command.getActionName()});
-                                 }
-                             }
+                            for (auto const& assignment : update.getAssignments()) {
+                                if(this->globalBooleanVariableExists(assignment.getVariable().getName())) {
+                                    globalBVarsWrittenToByCommandInThisModule.insert({assignment.getVariable().getName(), command.getActionName()});
+                                }
+                                else if(this->globalIntegerVariableExists(assignment.getVariable().getName())) {
+                                    globalIVarsWrittenToByCommandInThisModule.insert({assignment.getVariable().getName(), command.getActionName()});
+                                }
+                            }
                         }
                     }
                     for(auto const& entry : globalIVarsWrittenToByCommandInThisModule) {
@@ -1150,7 +1153,7 @@ namespace storm {
                         }
                     }
                 }
-            
+                
                 std::vector<storm::prism::BooleanVariable> newBVars;
                 for(auto const& variable : module.getBooleanVariables()) {
                     if(booleanVars.count(variable.getExpressionVariable()) == 0) {
@@ -1316,7 +1319,7 @@ namespace storm {
                     solver->allSat(allCommandVariables, [&] (storm::solver::SmtSolver::ModelReference& modelReference) -> bool {
                         // Now we need to reconstruct the chosen commands from the valuation of the command variables.
                         std::vector<std::vector<std::reference_wrapper<Command const>>> chosenCommands(possibleCommands.size());
-
+                        
                         for (uint_fast64_t outerIndex = 0; outerIndex < commandVariables.size(); ++outerIndex) {
                             for (uint_fast64_t innerIndex = 0; innerIndex < commandVariables[outerIndex].size(); ++innerIndex) {
                                 if (modelReference.getBooleanValue(commandVariables[outerIndex][innerIndex])) {
@@ -1338,13 +1341,13 @@ namespace storm {
                             for (uint_fast64_t index = 0; index < iterators.size(); ++index) {
                                 commandCombination[index] = *iterators[index];
                             }
-
+                            
                             newCommands.push_back(synchronizeCommands(nextCommandIndex, actionIndex, nextUpdateIndex, indexToActionMap.find(actionIndex)->second, commandCombination));
                             
                             // Move the counters appropriately.
                             ++nextCommandIndex;
                             nextUpdateIndex += newCommands.back().getNumberOfUpdates();
-
+                            
                             movedAtLeastOneIterator = false;
                             for (uint_fast64_t index = 0; index < iterators.size(); ++index) {
                                 ++iterators[index];
@@ -1368,7 +1371,7 @@ namespace storm {
             storm::prism::Module singleModule(newModuleName.str(), allBooleanVariables, allIntegerVariables, newCommands, this->getFilename(), 0);
             return Program(manager, this->getModelType(), this->getConstants(), std::vector<storm::prism::BooleanVariable>(), std::vector<storm::prism::IntegerVariable>(), this->getFormulas(), {singleModule}, actionToIndexMap, this->getRewardModels(), this->getLabels(), this->getInitialConstruct(), this->getOptionalSystemCompositionConstruct(), this->getFilename(), 0, true);
         }
-
+        
         std::unordered_map<uint_fast64_t, std::string> Program::buildCommandIndexToActionNameMap() const {
             std::unordered_map<uint_fast64_t, std::string> res;
             for(auto const& m : this->modules) {
@@ -1378,7 +1381,7 @@ namespace storm {
             }
             return res;
         }
-
+        
         std::unordered_map<uint_fast64_t, std::string> Program::buildActionIndexToActionNameMap() const {
             std::unordered_map<uint_fast64_t, std::string> res;
             for(auto const& nameIndexPair : actionToIndexMap) {
@@ -1386,7 +1389,7 @@ namespace storm {
             }
             return res;
         }
-
+        
         std::unordered_map<uint_fast64_t, uint_fast64_t> Program::buildCommandIndexToActionIndex() const {
             std::unordered_map<uint_fast64_t, uint_fast64_t> res;
             for(auto const& m : this->modules) {
@@ -1395,7 +1398,7 @@ namespace storm {
                 }
             }
             return res;
-
+            
         }
         
         Command Program::synchronizeCommands(uint_fast64_t newCommandIndex, uint_fast64_t actionIndex, uint_fast64_t firstUpdateIndex, std::string const& actionName, std::vector<std::reference_wrapper<Command const>> const& commands) const {
@@ -1454,11 +1457,11 @@ namespace storm {
             
             return Command(newCommandIndex, false, actionIndex, actionName, newGuard, newUpdates, this->getFilename(), 0);
         }
-
+        
         uint_fast64_t Program::numberOfActions() const {
             return this->actions.size();
         }
-
+        
         uint_fast64_t Program::largestActionIndex() const {
             assert(numberOfActions() != 0);
             return this->indexToActionMap.rbegin()->first;
@@ -1467,11 +1470,149 @@ namespace storm {
         storm::expressions::ExpressionManager const& Program::getManager() const {
             return *this->manager;
         }
-
+        
         storm::expressions::ExpressionManager& Program::getManager() {
             return *this->manager;
         }
+        
+        storm::jani::Model Program::toJani() const {
+            STORM_LOG_THROW(!this->specifiesSystemComposition(), storm::exceptions::InvalidOperationException, "Cannot translate PRISM program with custom system composition to JANI.");
+            
+            // Start by creating an empty JANI model.
+            storm::jani::ModelType modelType;
+            switch (this->getModelType()) {
+                case Program::ModelType::DTMC: modelType = storm::jani::ModelType::DTMC;
+                    break;
+                case Program::ModelType::CTMC: modelType = storm::jani::ModelType::CTMC;
+                    break;
+                case Program::ModelType::MDP: modelType = storm::jani::ModelType::MDP;
+                    break;
+                case Program::ModelType::CTMDP: modelType = storm::jani::ModelType::CTMDP;
+                    break;
+                case Program::ModelType::MA: modelType = storm::jani::ModelType::MA;
+                    break;
+                default: modelType = storm::jani::ModelType::UNDEFINED;
+            }
+            storm::jani::Model janiModel("jani_from_prism", modelType, 1, manager);
+            
+            // Add all constants of the PRISM program to the JANI model.
+            for (auto const& constant : constants) {
+                janiModel.addConstant(storm::jani::Constant(constant.getName(), constant.getExpressionVariable(), constant.isDefined() ? boost::optional<storm::expressions::Expression>(constant.getExpression()) : boost::none));
+            }
+            
+            // Add all global variables of the PRISM program to the JANI model.
+            for (auto const& variable : globalBooleanVariables) {
+                janiModel.addBooleanVariable(storm::jani::BooleanVariable(variable.getName(), variable.getExpressionVariable(), variable.getInitialValueExpression()));
+            }
+            for (auto const& variable : globalIntegerVariables) {
+                janiModel.addBoundedIntegerVariable(storm::jani::BoundedIntegerVariable(variable.getName(), variable.getExpressionVariable(), variable.getLowerBoundExpression(), variable.getUpperBoundExpression(), variable.getInitialValueExpression()));
+            }
+            
+            // Add all actions of the PRISM program to the JANI model.
+            for (auto const& action : indexToActionMap) {
+                // Ignore the empty action as every JANI program has predefined tau action.
+                if (!action.second.empty()) {
+                    janiModel.addAction(storm::jani::Action(action.second));
+                }
+            }
+            
+            // Because of the rules of JANI, we have to make all variables of modules global that are read by other modules.
 
+            // Create a mapping from variables to the indices of module indices that read the variable.
+            std::map<storm::expressions::Variable, std::set<uint_fast64_t>> variablesToReadingModuleIndices;
+            for (auto const& module : modules) {
+                for (auto const& variable : module.getBooleanVariables()) {
+                    variablesToReadingModuleIndices.emplace(variable.getExpressionVariable(), std::set<uint_fast64_t>());
+                }
+                for (auto const& variable : module.getIntegerVariables()) {
+                    variablesToReadingModuleIndices.emplace(variable.getExpressionVariable(), std::set<uint_fast64_t>());
+                }
+            }
+            for (uint_fast64_t index = 0; index < modules.size(); ++index) {
+                storm::prism::Module const& module = modules[index];
+                
+                for (auto const& command : module.getCommands()) {
+                    std::set<storm::expressions::Variable> variables = command.getGuardExpression().getVariables();
+                    for (auto const& variable : variables) {
+                        variablesToReadingModuleIndices[variable].insert(index);
+                    }
+                    
+                    for (auto const& update : command.getUpdates()) {
+                        for (auto const& assignment : update.getAssignments()) {
+                            variables = assignment.getExpression().getVariables();
+                            for (auto const& variable : variables) {
+                                variablesToReadingModuleIndices[variable].insert(index);
+                            }
+                        }
+                    }
+                }
+            }
+            
+            // Now create the separate JANI automata from the modules of the PRISM program. While doing so, we use the
+            // previously built mapping to make variables global that are read by more than one module.
+            for (auto const& module : modules) {
+                storm::jani::Automaton automaton(module.getName());
+                for (auto const& variable : module.getBooleanVariables()) {
+                    storm::jani::BooleanVariable newBooleanVariable(variable.getName(), variable.getExpressionVariable(), variable.getInitialValueExpression());
+                    std::set<uint_fast64_t> const& readingModuleIndices = variablesToReadingModuleIndices[variable.getExpressionVariable()];
+                    if (readingModuleIndices.size() == 1) {
+                        // In this case, we can move the variable to the automaton.
+                        automaton.addBooleanVariable(newBooleanVariable);
+                    } else {
+                        // In this case, we need to make the variable global.
+                        janiModel.addBooleanVariable(newBooleanVariable);
+                    }
+                }
+                for (auto const& variable : module.getIntegerVariables()) {
+                    storm::jani::BoundedIntegerVariable newIntegerVariable(variable.getName(), variable.getExpressionVariable(), variable.getLowerBoundExpression(), variable.getUpperBoundExpression(), variable.getInitialValueExpression());
+                    std::set<uint_fast64_t> const& readingModuleIndices = variablesToReadingModuleIndices[variable.getExpressionVariable()];
+                    if (readingModuleIndices.size() == 1) {
+                        // In this case, we can move the variable to the automaton.
+                        automaton.addBoundedIntegerVariable(newIntegerVariable);
+                    } else {
+                        // In this case, we need to make the variable global.
+                        janiModel.addBoundedIntegerVariable(newIntegerVariable);
+                    }
+                }
+                
+                // Create a single location that will have all the edges.
+                uint64_t onlyLocation = automaton.addLocation(storm::jani::Location("l"));
+                automaton.setInitialLocation(onlyLocation);
+                
+                for (auto const& command : module.getCommands()) {
+                    boost::optional<storm::expressions::Expression> rateExpression;
+                    std::vector<storm::jani::EdgeDestination> destinations;
+                    if (this->getModelType() == Program::ModelType::CTMC || this->getModelType() == Program::ModelType::CTMDP) {
+                        for (auto const& update : command.getUpdates()) {
+                            if (rateExpression) {
+                                rateExpression = rateExpression.get() + update.getLikelihoodExpression();
+                            } else {
+                                rateExpression = update.getLikelihoodExpression();
+                            }
+                        }
+                    }
+                    
+                    for (auto const& update : command.getUpdates()) {
+                        std::vector<storm::jani::Assignment> assignments;
+                        for (auto const& assignment : update.getAssignments()) {
+                            assignments.push_back(storm::jani::Assignment(assignment.getVariable(), assignment.getExpression()));
+                        }
+                        
+                        if (rateExpression) {
+                            destinations.push_back(storm::jani::EdgeDestination(onlyLocation, manager->integer(1) / rateExpression.get(), assignments));
+                        } else {
+                            destinations.push_back(storm::jani::EdgeDestination(onlyLocation, update.getLikelihoodExpression(), assignments));
+                        }
+                    }
+                    automaton.addEdge(storm::jani::Edge(onlyLocation, janiModel.getActionIndex(command.getActionName()), rateExpression, command.getGuardExpression(), destinations));
+                }
+                
+                janiModel.addAutomaton(automaton);
+            }
+            
+            return janiModel;
+        }
+        
         std::ostream& operator<<(std::ostream& out, Program::ModelType const& type) {
             switch (type) {
                 case Program::ModelType::UNDEFINED: out << "undefined"; break;

src/storage/prism/Program.h

@@ -20,6 +20,10 @@
 #include "src/utility/OsDetection.h"
 
 namespace storm {
+    namespace jani {
+        class Model;
+    }
+    
     namespace prism {
         class Program : public LocatedInformation {
         public:
@@ -551,6 +555,11 @@ namespace storm {
 
             uint_fast64_t largestActionIndex() const;
             
+            /*!
+             * Converts the PRISM model into an equivalent JANI model.
+             */
+            storm::jani::Model toJani() const;
+            
         private:
             /*!
              * This function builds a command that corresponds to the synchronization of the given list of commands.

test/functional/storage/PrismProgramTest.cpp

@@ -4,6 +4,8 @@
 
 #include "src/utility/solver.h"
 
+#include "src/storage/jani/Model.h"
+
 #ifdef STORM_HAVE_MSAT
 TEST(PrismProgramTest, FlattenModules) {
     storm::prism::Program result;
@@ -22,3 +24,26 @@ TEST(PrismProgramTest, FlattenModules) {
     EXPECT_EQ(180, result.getModule(0).getNumberOfCommands());
 }
 #endif
+
+TEST(PrismProgramTest, ConvertToJani) {
+    storm::prism::Program prismProgram;
+    storm::jani::Model janiModel;
+
+    ASSERT_NO_THROW(prismProgram = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/parser/prism/leader3.nm"));
+    ASSERT_NO_THROW(janiModel = prismProgram.toJani());
+    
+    ASSERT_NO_THROW(prismProgram = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/parser/prism/wlan0_collide.nm"));
+    ASSERT_NO_THROW(janiModel = prismProgram.toJani());
+    
+    ASSERT_NO_THROW(prismProgram = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/brp-16-2.pm"));
+    ASSERT_NO_THROW(janiModel = prismProgram.toJani());
+
+    ASSERT_NO_THROW(prismProgram = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/crowds-5-5.pm"));
+    ASSERT_NO_THROW(janiModel = prismProgram.toJani());
+    
+    ASSERT_NO_THROW(prismProgram = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/leader-3-5.pm"));
+    ASSERT_NO_THROW(janiModel = prismProgram.toJani());
+
+    ASSERT_NO_THROW(prismProgram = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/nand-5-2.pm"));
+    ASSERT_NO_THROW(janiModel = prismProgram.toJani());
+}