adding real variables to JANI models. started to encapsulate PRISM to JANI converter

Former-commit-id: a7892b3d23 [formerly 411e830ca5]
Former-commit-id: 49ee703493

src/storage/jani/Assignment.cpp

@@ -8,7 +8,7 @@ namespace storm  {
         }
         
         bool Assignment::operator==(Assignment const& other) const {
-            return this->getExpressionVariable() == other.getExpressionVariable() && this->getAssignedExpression().isSyntacticallyEqual(other.getAssignedExpression());
+            return this->isTransientAssignment() == other.isTransientAssignment() && this->getExpressionVariable() == other.getExpressionVariable() && this->getAssignedExpression().isSyntacticallyEqual(other.getAssignedExpression());
         }
         
         storm::jani::Variable const& Assignment::getVariable() const {

src/storage/jani/Automaton.cpp

@@ -61,26 +61,32 @@ namespace storm {
 
         Variable const& Automaton::addVariable(Variable const &variable) {
             if (variable.isBooleanVariable()) {
-                return addBooleanVariable(variable.asBooleanVariable());
+                return addVariable(variable.asBooleanVariable());
             } else if (variable.isBoundedIntegerVariable()) {
-                return addBoundedIntegerVariable(variable.asBoundedIntegerVariable());
+                return addVariable(variable.asBoundedIntegerVariable());
             } else if (variable.isUnboundedIntegerVariable()) {
-                return addUnboundedIntegerVariable(variable.asUnboundedIntegerVariable());
+                return addVariable(variable.asUnboundedIntegerVariable());
+            } else if (variable.isRealVariable()) {
+                return addVariable(variable.asRealVariable());
             } else {
                 STORM_LOG_THROW(false, storm::exceptions::InvalidTypeException, "Variable has invalid type.");
             }
         }
         
-        BooleanVariable const& Automaton::addBooleanVariable(BooleanVariable const& variable) {
-            return variables.addBooleanVariable(variable);
+        BooleanVariable const& Automaton::addVariable(BooleanVariable const& variable) {
+            return variables.addVariable(variable);
         }
         
-        BoundedIntegerVariable const& Automaton::addBoundedIntegerVariable(BoundedIntegerVariable const& variable) {
-            return variables.addBoundedIntegerVariable(variable);
+        BoundedIntegerVariable const& Automaton::addVariable(BoundedIntegerVariable const& variable) {
+            return variables.addVariable(variable);
         }
 
-        UnboundedIntegerVariable const& Automaton::addUnboundedIntegerVariable(UnboundedIntegerVariable const& variable) {
-            return variables.addUnboundedIntegerVariable(variable);
+        UnboundedIntegerVariable const& Automaton::addVariable(UnboundedIntegerVariable const& variable) {
+            return variables.addVariable(variable);
+        }
+
+        RealVariable const& Automaton::addVariable(RealVariable const& variable) {
+            return variables.addVariable(variable);
         }
 
         VariableSet& Automaton::getVariables() {

src/storage/jani/Automaton.h

@@ -108,17 +108,22 @@ namespace storm {
             /*!
              * Adds the given Boolean variable to this automaton.
              */
-            BooleanVariable const& addBooleanVariable(BooleanVariable const& variable);
+            BooleanVariable const& addVariable(BooleanVariable const& variable);
             
             /*!
              * Adds the given bounded integer variable to this automaton.
              */
-            BoundedIntegerVariable const& addBoundedIntegerVariable(BoundedIntegerVariable const& variable);
+            BoundedIntegerVariable const& addVariable(BoundedIntegerVariable const& variable);
             
             /*!
              * Adds the given unbounded integer variable to this automaton.
              */
-            UnboundedIntegerVariable const& addUnboundedIntegerVariable(UnboundedIntegerVariable const& variable);
+            UnboundedIntegerVariable const& addVariable(UnboundedIntegerVariable const& variable);
+
+            /*!
+             * Adds the given real variable to this automaton.
+             */
+            RealVariable const& addVariable(RealVariable const& variable);
 
             /*!
              * Retrieves the variables of this automaton.

src/storage/jani/Edge.cpp

@@ -64,7 +64,28 @@ namespace storm {
         }
         
         void Edge::liftTransientDestinationAssignments() {
-            
+            if (!destinations.empty()) {
+                auto const& destination = *destinations.begin();
+                
+                for (auto const& assignment : destination.getTransientAssignments()) {
+                    // Check if we can lift the assignment to the edge.
+                    bool canBeLifted = true;
+                    for (auto const& destination : destinations) {
+                        if (!destination.hasAssignment(assignment)) {
+                            canBeLifted = false;
+                            break;
+                        }
+                    }
+                    
+                    // If so, remove the assignment from all destinations.
+                    if (canBeLifted) {
+                        this->addTransientAssignment(assignment);
+                        for (auto& destination : destinations) {
+                            destination.removeAssignment(assignment);
+                        }
+                    }
+                }
+            }
         }
         
         boost::container::flat_set<storm::expressions::Variable> const& Edge::getWrittenGlobalVariables() const {

src/storage/jani/EdgeDestination.cpp

@@ -72,6 +72,28 @@ namespace storm {
             return transientAssignments;
         }
         
+        bool EdgeDestination::hasAssignment(Assignment const& assignment) const {
+            for (auto const& containedAssignment : assignments) {
+                if (containedAssignment == assignment) {
+                    return true;
+                }
+            }
+            return false;
+        }
+        
+        bool EdgeDestination::removeAssignment(Assignment const& assignment) {
+            bool toRemove = removeAssignment(assignment, assignments);
+            if (toRemove) {
+                if (assignment.isTransientAssignment()) {
+                    removeAssignment(assignment, transientAssignments);
+                } else {
+                    removeAssignment(assignment, nonTransientAssignments);
+                }
+                return true;
+            }
+            return false;
+        }
+        
         void EdgeDestination::sortAssignments(std::vector<Assignment>& assignments) {
             std::sort(assignments.begin(), assignments.end(), [] (storm::jani::Assignment const& assignment1, storm::jani::Assignment const& assignment2) {
                 bool smaller = assignment1.getExpressionVariable().getType().isBooleanType() && !assignment2.getExpressionVariable().getType().isBooleanType();
@@ -82,5 +104,15 @@ namespace storm {
             });
         }
         
+        bool EdgeDestination::removeAssignment(Assignment const& assignment, std::vector<Assignment>& assignments) {
+            for (auto it = assignments.begin(), ite = assignments.end(); it != ite; ++it) {
+                if (assignment == *it) {
+                    assignments.erase(it);
+                    return true;
+                }
+            }
+            return false;
+        }
+
     }
 }

src/storage/jani/EdgeDestination.h

@@ -66,6 +66,20 @@ namespace storm {
              */
             std::vector<Assignment> const& getTransientAssignments() const;
 
+            /*!
+             * Retrieves whether this assignment is made when choosing this destination.
+             *
+             * @return True iff the assignment is made.
+             */
+            bool hasAssignment(Assignment const& assignment) const;
+            
+            /*!
+             * Removes the given assignment from this destination.
+             *
+             * @return True if the assignment was found and removed.
+             */
+            bool removeAssignment(Assignment const& assignment);
+            
         private:
             /*!
              * Sorts the assignments to make all assignments to boolean variables precede all others and order the
@@ -73,6 +87,13 @@ namespace storm {
              */
             static void sortAssignments(std::vector<Assignment>& assignments);
             
+            /*!
+             * Removes the given assignment from the provided list of assignments if found.
+             *
+             * @return True if the assignment was removed.
+             */
+            static bool removeAssignment(Assignment const& assignment, std::vector<Assignment>& assignments);
+            
             // The index of the destination location.
             uint64_t locationIndex;
 

src/storage/jani/Model.cpp

@@ -107,26 +107,32 @@ namespace storm {
 
         Variable const& Model::addVariable(Variable const& variable) {
             if (variable.isBooleanVariable()) {
-                return addBooleanVariable(variable.asBooleanVariable());
+                return addVariable(variable.asBooleanVariable());
             } else if (variable.isBoundedIntegerVariable()) {
-                return addBoundedIntegerVariable(variable.asBoundedIntegerVariable());
+                return addVariable(variable.asBoundedIntegerVariable());
             } else if (variable.isUnboundedIntegerVariable()) {
-                return addUnboundedIntegerVariable(variable.asUnboundedIntegerVariable());
+                return addVariable(variable.asUnboundedIntegerVariable());
+            } else if (variable.isRealVariable()) {
+                return addVariable(variable.asRealVariable());
             } else {
                 STORM_LOG_THROW(false, storm::exceptions::InvalidTypeException, "Variable has invalid type.");
             }
         }
 
-        BooleanVariable const& Model::addBooleanVariable(BooleanVariable const& variable) {
-            return globalVariables.addBooleanVariable(variable);
+        BooleanVariable const& Model::addVariable(BooleanVariable const& variable) {
+            return globalVariables.addVariable(variable);
         }
         
-        BoundedIntegerVariable const& Model::addBoundedIntegerVariable(BoundedIntegerVariable const& variable) {
-            return globalVariables.addBoundedIntegerVariable(variable);
+        BoundedIntegerVariable const& Model::addVariable(BoundedIntegerVariable const& variable) {
+            return globalVariables.addVariable(variable);
         }
         
-        UnboundedIntegerVariable const& Model::addUnboundedIntegerVariable(UnboundedIntegerVariable const& variable) {
-            return globalVariables.addUnboundedIntegerVariable(variable);
+        UnboundedIntegerVariable const& Model::addVariable(UnboundedIntegerVariable const& variable) {
+            return globalVariables.addVariable(variable);
+        }
+
+        RealVariable const& Model::addVariable(RealVariable const& variable) {
+            return globalVariables.addVariable(variable);
         }
 
         VariableSet& Model::getGlobalVariables() {

src/storage/jani/Model.h

@@ -115,17 +115,22 @@ namespace storm {
             /*!
              * Adds the given boolean variable to this model.
              */
-            BooleanVariable const& addBooleanVariable(BooleanVariable const& variable);
+            BooleanVariable const& addVariable(BooleanVariable const& variable);
             
             /*!
              * Adds the given bounded integer variable to this model.
              */
-            BoundedIntegerVariable const& addBoundedIntegerVariable(BoundedIntegerVariable const& variable);
+            BoundedIntegerVariable const& addVariable(BoundedIntegerVariable const& variable);
             
             /*!
              * Adds the given unbounded integer variable to this model.
              */
-            UnboundedIntegerVariable const& addUnboundedIntegerVariable(UnboundedIntegerVariable const& variable);
+            UnboundedIntegerVariable const& addVariable(UnboundedIntegerVariable const& variable);
+
+            /*!
+             * Adds the given real variable to this model.
+             */
+            RealVariable const& addVariable(RealVariable const& variable);
 
             /*!
              * Retrieves the variables of this automaton.

src/storage/jani/RealVariable.cpp

@@ -0,0 +1,19 @@
+#include "src/storage/jani/RealVariable.h"
+
+namespace storm {
+    namespace jani {
+        
+        RealVariable::RealVariable(std::string const& name, storm::expressions::Variable const& variable, bool transient) : storm::jani::Variable(name, variable, transient) {
+            // Intentionally left empty.
+        }
+        
+        RealVariable::RealVariable(std::string const& name, storm::expressions::Variable const& variable, storm::expressions::Expression const& initValue, bool transient) : storm::jani::Variable(name, variable, initValue, transient) {
+            // Intentionally left empty.
+        }
+        
+        bool RealVariable::isRealVariable() const {
+            return true;
+        }
+        
+    }
+}

src/storage/jani/RealVariable.h

@@ -0,0 +1,25 @@
+#pragma once
+
+#include "src/storage/jani/Variable.h"
+
+namespace storm {
+    namespace jani {
+        
+        class RealVariable : public Variable {
+        public:
+            /*!
+             * Creates a real variable without initial value.
+             */
+            RealVariable(std::string const& name, storm::expressions::Variable const& variable, bool transient=false);
+            
+            /*!
+             * Creates a real variable with initial value.
+             */
+            RealVariable(std::string const& name, storm::expressions::Variable const& variable, storm::expressions::Expression const& initValue, bool transient=false);
+            
+            virtual bool isRealVariable() const override;
+        };
+
+        
+    }
+}

src/storage/jani/Variable.cpp

@@ -3,6 +3,7 @@
 #include "src/storage/jani/BooleanVariable.h"
 #include "src/storage/jani/BoundedIntegerVariable.h"
 #include "src/storage/jani/UnboundedIntegerVariable.h"
+#include "src/storage/jani/RealVariable.h"
 
 namespace storm {
     namespace jani {
@@ -36,6 +37,10 @@ namespace storm {
             return false;
         }
 
+        bool Variable::isRealVariable() const {
+            return false;
+        }
+        
         bool Variable::isTransientVariable() const {
             return transient;
         }
@@ -53,27 +58,35 @@ namespace storm {
         }
         
         BooleanVariable& Variable::asBooleanVariable() {
-            return dynamic_cast<BooleanVariable&>(*this);
+            return static_cast<BooleanVariable&>(*this);
         }
         
         BooleanVariable const& Variable::asBooleanVariable() const {
-            return dynamic_cast<BooleanVariable const&>(*this);
+            return static_cast<BooleanVariable const&>(*this);
         }
         
         BoundedIntegerVariable& Variable::asBoundedIntegerVariable() {
-            return dynamic_cast<BoundedIntegerVariable&>(*this);
+            return static_cast<BoundedIntegerVariable&>(*this);
         }
         
         BoundedIntegerVariable const& Variable::asBoundedIntegerVariable() const {
-            return dynamic_cast<BoundedIntegerVariable const&>(*this);
+            return static_cast<BoundedIntegerVariable const&>(*this);
         }
         
         UnboundedIntegerVariable& Variable::asUnboundedIntegerVariable() {
-            return dynamic_cast<UnboundedIntegerVariable&>(*this);
+            return static_cast<UnboundedIntegerVariable&>(*this);
         }
         
         UnboundedIntegerVariable const& Variable::asUnboundedIntegerVariable() const {
-            return dynamic_cast<UnboundedIntegerVariable const&>(*this);
+            return static_cast<UnboundedIntegerVariable const&>(*this);
+        }
+        
+        RealVariable& Variable::asRealVariable() {
+            return static_cast<RealVariable&>(*this);
+        }
+        
+        RealVariable const& Variable::asRealVariable() const {
+            return static_cast<RealVariable const&>(*this);
         }
         
     }

src/storage/jani/Variable.h

@@ -13,6 +13,7 @@ namespace storm {
         class BooleanVariable;
         class BoundedIntegerVariable;
         class UnboundedIntegerVariable;
+        class RealVariable;
         
         class Variable {
         public:
@@ -58,6 +59,7 @@ namespace storm {
             virtual bool isBooleanVariable() const;
             virtual bool isBoundedIntegerVariable() const;
             virtual bool isUnboundedIntegerVariable() const;
+            virtual bool isRealVariable() const;
 
             virtual bool isTransientVariable() const;
             
@@ -68,6 +70,8 @@ namespace storm {
             BoundedIntegerVariable const& asBoundedIntegerVariable() const;
             UnboundedIntegerVariable& asUnboundedIntegerVariable();
             UnboundedIntegerVariable const& asUnboundedIntegerVariable() const;
+            RealVariable& asRealVariable();
+            RealVariable const& asRealVariable() const;
             
         private:
             // The name of the variable.

src/storage/jani/VariableSet.cpp

@@ -74,7 +74,15 @@ namespace storm {
             return detail::ConstVariables<UnboundedIntegerVariable>(unboundedIntegerVariables.begin(), unboundedIntegerVariables.end());
         }
 
-        BooleanVariable const& VariableSet::addBooleanVariable(BooleanVariable const& variable) {
+        detail::Variables<RealVariable> VariableSet::getRealVariables() {
+            return detail::Variables<RealVariable>(realVariables.begin(), realVariables.end());
+        }
+        
+        detail::ConstVariables<RealVariable> VariableSet::getRealVariables() const {
+            return detail::ConstVariables<RealVariable>(realVariables.begin(), realVariables.end());
+        }
+        
+        BooleanVariable const& VariableSet::addVariable(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.");
             std::shared_ptr<BooleanVariable> newVariable = std::make_shared<BooleanVariable>(variable);
             variables.push_back(newVariable);
@@ -84,7 +92,7 @@ namespace storm {
             return *newVariable;
         }
         
-        BoundedIntegerVariable const& VariableSet::addBoundedIntegerVariable(BoundedIntegerVariable const& variable) {
+        BoundedIntegerVariable const& VariableSet::addVariable(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.");
             std::shared_ptr<BoundedIntegerVariable> newVariable = std::make_shared<BoundedIntegerVariable>(variable);
             variables.push_back(newVariable);
@@ -94,7 +102,7 @@ namespace storm {
             return *newVariable;
         }
         
-        UnboundedIntegerVariable const& VariableSet::addUnboundedIntegerVariable(UnboundedIntegerVariable const& variable) {
+        UnboundedIntegerVariable const& VariableSet::addVariable(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.");
             std::shared_ptr<UnboundedIntegerVariable> newVariable = std::make_shared<UnboundedIntegerVariable>(variable);
             variables.push_back(newVariable);
@@ -104,6 +112,16 @@ namespace storm {
             return *newVariable;
         }
         
+        RealVariable const& VariableSet::addVariable(RealVariable 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.");
+            std::shared_ptr<RealVariable> newVariable = std::make_shared<RealVariable>(variable);
+            variables.push_back(newVariable);
+            realVariables.push_back(newVariable);
+            nameToVariable.emplace(variable.getName(), variable.getExpressionVariable());
+            variableToVariable.emplace(variable.getExpressionVariable(), newVariable);
+            return *newVariable;
+        }
+        
         bool VariableSet::hasVariable(std::string const& name) const {
             return nameToVariable.find(name) != nameToVariable.end();
         }
@@ -152,6 +170,10 @@ namespace storm {
             return !unboundedIntegerVariables.empty();
         }
         
+        bool VariableSet::containsRealVariables() const {
+            return !realVariables.empty();
+        }
+        
         bool VariableSet::empty() const {
             return !(containsBooleanVariable() || containsBoundedIntegerVariable() || containsUnboundedIntegerVariables());
         }

src/storage/jani/VariableSet.h

@@ -8,6 +8,7 @@
 #include "src/storage/jani/BooleanVariable.h"
 #include "src/storage/jani/UnboundedIntegerVariable.h"
 #include "src/storage/jani/BoundedIntegerVariable.h"
+#include "src/storage/jani/RealVariable.h"
 
 namespace storm {
     namespace jani {
@@ -97,20 +98,35 @@ namespace storm {
              */
             detail::ConstVariables<UnboundedIntegerVariable> getUnboundedIntegerVariables() const;
             
+            /*!
+             * Retrieves the real variables in this set.
+             */
+            detail::Variables<RealVariable> getRealVariables();
+            
+            /*!
+             * Retrieves the real variables in this set.
+             */
+            detail::ConstVariables<RealVariable> getRealVariables() const;
+            
             /*!
              * Adds the given boolean variable to this set.
              */
-            BooleanVariable const& addBooleanVariable(BooleanVariable const& variable);
+            BooleanVariable const& addVariable(BooleanVariable const& variable);
 
             /*!
              * Adds the given bounded integer variable to this set.
              */
-            BoundedIntegerVariable const& addBoundedIntegerVariable(BoundedIntegerVariable const& variable);
+            BoundedIntegerVariable const& addVariable(BoundedIntegerVariable const& variable);
 
             /*!
              * Adds the given unbounded integer variable to this set.
              */
-            UnboundedIntegerVariable const& addUnboundedIntegerVariable(UnboundedIntegerVariable const& variable);
+            UnboundedIntegerVariable const& addVariable(UnboundedIntegerVariable const& variable);
+            
+            /*!
+             * Adds the given real variable to this set.
+             */
+            RealVariable const& addVariable(RealVariable const& variable);
 
             /*!
              * Retrieves whether this variable set contains a variable with the given name.
@@ -167,6 +183,11 @@ namespace storm {
              */
             bool containsUnboundedIntegerVariables() const;
 
+            /*!
+             * Retrieves whether the set of variables contains an unbounded integer variable.
+             */
+            bool containsRealVariables() const;
+
             /*!
              * Retrieves whether this variable set is empty.
              */
@@ -185,6 +206,9 @@ namespace storm {
             /// The unbounded integer variables in this set.
             std::vector<std::shared_ptr<UnboundedIntegerVariable>> unboundedIntegerVariables;
             
+            /// The real variables in this set.
+            std::vector<std::shared_ptr<RealVariable>> realVariables;
+            
             /// A set of all variable names currently in use.
             std::map<std::string, storm::expressions::Variable> nameToVariable;
             

src/storage/prism/Program.cpp

@@ -20,7 +20,6 @@
 
 #include "src/storage/prism/CompositionVisitor.h"
 #include "src/storage/prism/Compositions.h"
-#include "src/storage/prism/CompositionToJaniVisitor.h"
 
 namespace storm {
     namespace prism {
@@ -1610,180 +1609,10 @@ namespace storm {
             return this->indexToActionMap.rbegin()->first;
         }
         
-        storm::expressions::ExpressionManager const& Program::getManager() const {
+        storm::expressions::ExpressionManager& Program::getManager() const {
             return *this->manager;
         }
         
-        storm::expressions::ExpressionManager& Program::getManager() {
-            return *this->manager;
-        }
-        
-        storm::jani::Model Program::toJani(bool allVariablesGlobal) const {
-            // 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));
-            }
-            
-            // Maintain a mapping from expression variables to JANI variables so we can fill in the correct objects when
-            // creating assignments.
-            std::map<storm::expressions::Variable, std::reference_wrapper<storm::jani::Variable const>> variableToVariableMap;
-            
-            // Add all global variables of the PRISM program to the JANI model.
-            for (auto const& variable : globalIntegerVariables) {
-                if (variable.hasInitialValue()) {
-                    storm::jani::BoundedIntegerVariable const& createdVariable = janiModel.addBoundedIntegerVariable(storm::jani::BoundedIntegerVariable(variable.getName(), variable.getExpressionVariable(), variable.getInitialValueExpression(), false, variable.getLowerBoundExpression(), variable.getUpperBoundExpression()));
-                    variableToVariableMap.emplace(variable.getExpressionVariable(), createdVariable);
-                } else {
-                    storm::jani::BoundedIntegerVariable const& createdVariable = janiModel.addBoundedIntegerVariable(storm::jani::BoundedIntegerVariable(variable.getName(), variable.getExpressionVariable(), false, variable.getLowerBoundExpression(), variable.getUpperBoundExpression()));
-                    variableToVariableMap.emplace(variable.getExpressionVariable(), createdVariable);
-                }
-            }
-            for (auto const& variable : globalBooleanVariables) {
-                if (variable.hasInitialValue()) {
-                    storm::jani::BooleanVariable const& createdVariable = janiModel.addBooleanVariable(storm::jani::BooleanVariable(variable.getName(), variable.getExpressionVariable(), variable.getInitialValueExpression(), false));
-                    variableToVariableMap.emplace(variable.getExpressionVariable(), createdVariable);
-                } else {
-                    storm::jani::BooleanVariable const& createdVariable = janiModel.addBooleanVariable(storm::jani::BooleanVariable(variable.getName(), variable.getExpressionVariable(), false));
-                    variableToVariableMap.emplace(variable.getExpressionVariable(), createdVariable);
-                }
-            }
-            
-            // 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 write/read the variable.
-            std::map<storm::expressions::Variable, std::set<uint_fast64_t>> variablesToAccessingModuleIndices;
-            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) {
-                        variablesToAccessingModuleIndices[variable].insert(index);
-                    }
-                    
-                    for (auto const& update : command.getUpdates()) {
-                        for (auto const& assignment : update.getAssignments()) {
-                            variables = assignment.getExpression().getVariables();
-                            for (auto const& variable : variables) {
-                                variablesToAccessingModuleIndices[variable].insert(index);
-                            }
-                            variablesToAccessingModuleIndices[assignment.getVariable()].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.getIntegerVariables()) {
-                    storm::jani::BoundedIntegerVariable newIntegerVariable = *storm::jani::makeBoundedIntegerVariable(variable.getName(), variable.getExpressionVariable(), variable.hasInitialValue() ? boost::make_optional(variable.getInitialValueExpression()) : boost::none, false, variable.getLowerBoundExpression(), variable.getUpperBoundExpression());
-                    std::set<uint_fast64_t> const& accessingModuleIndices = variablesToAccessingModuleIndices[variable.getExpressionVariable()];
-                    // If there is exactly one module reading and writing the variable, we can make the variable local to this module.
-                    if (!allVariablesGlobal && accessingModuleIndices.size() == 1) {
-                        storm::jani::BoundedIntegerVariable const& createdVariable = automaton.addBoundedIntegerVariable(newIntegerVariable);
-                        variableToVariableMap.emplace(variable.getExpressionVariable(), createdVariable);
-                    } else if (!accessingModuleIndices.empty()) {
-                        // Otherwise, we need to make it global.
-                        storm::jani::BoundedIntegerVariable const& createdVariable = janiModel.addBoundedIntegerVariable(newIntegerVariable);
-                        variableToVariableMap.emplace(variable.getExpressionVariable(), createdVariable);
-                    }
-                }
-                for (auto const& variable : module.getBooleanVariables()) {
-                    storm::jani::BooleanVariable newBooleanVariable = *storm::jani::makeBooleanVariable(variable.getName(), variable.getExpressionVariable(), variable.hasInitialValue() ? boost::make_optional(variable.getInitialValueExpression()) : boost::none, false);
-                    std::set<uint_fast64_t> const& accessingModuleIndices = variablesToAccessingModuleIndices[variable.getExpressionVariable()];
-                    // If there is exactly one module reading and writing the variable, we can make the variable local to this module.
-                    if (!allVariablesGlobal && accessingModuleIndices.size() == 1) {
-                        storm::jani::BooleanVariable const& createdVariable = automaton.addBooleanVariable(newBooleanVariable);
-                        variableToVariableMap.emplace(variable.getExpressionVariable(), createdVariable);
-                    } else if (!accessingModuleIndices.empty()) {
-                        // Otherwise, we need to make it global.
-                        storm::jani::BooleanVariable const& createdVariable = janiModel.addBooleanVariable(newBooleanVariable);
-                        variableToVariableMap.emplace(variable.getExpressionVariable(), createdVariable);
-                    }
-                }
-                automaton.setInitialStatesRestriction(manager->boolean(true));
-                
-                // Create a single location that will have all the edges.
-                uint64_t onlyLocation = automaton.addLocation(storm::jani::Location("l"));
-                automaton.addInitialLocation(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(variableToVariableMap.at(assignment.getVariable()).get(), 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);
-            }
-            
-            if (this->hasInitialConstruct()) {
-                janiModel.setInitialStatesRestriction(this->getInitialConstruct().getInitialStatesExpression());
-            } else {
-                janiModel.setInitialStatesRestriction(manager->boolean(true));
-            }
-            
-            // Set the standard system composition. This is possible, because we reject non-standard compositions anyway.
-            if (this->specifiesSystemComposition()) {
-                CompositionToJaniVisitor visitor;
-                janiModel.setSystemComposition(visitor.toJani(this->getSystemCompositionConstruct().getSystemComposition(), janiModel));
-            } else {
-                janiModel.setSystemComposition(janiModel.getStandardSystemComposition());
-            }
-            
-            janiModel.finalize();
-            
-            return janiModel;
-        }
-        
         void Program::createMissingInitialValues() {
             for (auto& variable : globalBooleanVariables) {
                 if (!variable.hasInitialValue()) {

src/storage/prism/Program.h

@@ -566,18 +566,8 @@ namespace storm {
              *
              * @return The manager responsible for the expressions of this program.
              */
-            storm::expressions::ExpressionManager const& getManager() const;
+            storm::expressions::ExpressionManager& getManager() const;
 
-            /*!
-             * Retrieves the manager responsible for the expressions of this program.
-             *
-             * @return The manager responsible for the expressions of this program.
-             */
-            storm::expressions::ExpressionManager& getManager();
-
-            /*!
-             *
-             */
             std::unordered_map<uint_fast64_t, std::string> buildCommandIndexToActionNameMap() const;
 
             std::unordered_map<uint_fast64_t, uint_fast64_t> buildCommandIndexToActionIndex() const;

src/storage/prism/ToJaniConverter.cpp

@@ -0,0 +1,187 @@
+#include "src/storage/prism/ToJaniConverter.h"
+
+#include "src/storage/expressions/ExpressionManager.h"
+
+#include "src/storage/prism/Program.h"
+#include "src/storage/prism/CompositionToJaniVisitor.h"
+#include "src/storage/jani/Model.h"
+
+namespace storm {
+    namespace prism {
+        
+        storm::jani::Model convert(storm::prism::Program const& program, bool allVariablesGlobal) {
+            std::shared_ptr<storm::expressions::ExpressionManager> manager = program.getManager().getSharedPointer();
+            
+            // Start by creating an empty JANI model.
+            storm::jani::ModelType modelType;
+            switch (program.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 : program.getConstants()) {
+                janiModel.addConstant(storm::jani::Constant(constant.getName(), constant.getExpressionVariable(), constant.isDefined() ? boost::optional<storm::expressions::Expression>(constant.getExpression()) : boost::none));
+            }
+            
+            // Maintain a mapping from expression variables to JANI variables so we can fill in the correct objects when
+            // creating assignments.
+            std::map<storm::expressions::Variable, std::reference_wrapper<storm::jani::Variable const>> variableToVariableMap;
+            
+            // Add all global variables of the PRISM program to the JANI model.
+            for (auto const& variable : program.getGlobalIntegerVariables()) {
+                if (variable.hasInitialValue()) {
+                    storm::jani::BoundedIntegerVariable const& createdVariable = janiModel.addVariable(storm::jani::BoundedIntegerVariable(variable.getName(), variable.getExpressionVariable(), variable.getInitialValueExpression(), false, variable.getLowerBoundExpression(), variable.getUpperBoundExpression()));
+                    variableToVariableMap.emplace(variable.getExpressionVariable(), createdVariable);
+                } else {
+                    storm::jani::BoundedIntegerVariable const& createdVariable = janiModel.addVariable(storm::jani::BoundedIntegerVariable(variable.getName(), variable.getExpressionVariable(), false, variable.getLowerBoundExpression(), variable.getUpperBoundExpression()));
+                    variableToVariableMap.emplace(variable.getExpressionVariable(), createdVariable);
+                }
+            }
+            for (auto const& variable : program.getGlobalBooleanVariables()) {
+                if (variable.hasInitialValue()) {
+                    storm::jani::BooleanVariable const& createdVariable = janiModel.addVariable(storm::jani::BooleanVariable(variable.getName(), variable.getExpressionVariable(), variable.getInitialValueExpression(), false));
+                    variableToVariableMap.emplace(variable.getExpressionVariable(), createdVariable);
+                } else {
+                    storm::jani::BooleanVariable const& createdVariable = janiModel.addVariable(storm::jani::BooleanVariable(variable.getName(), variable.getExpressionVariable(), false));
+                    variableToVariableMap.emplace(variable.getExpressionVariable(), createdVariable);
+                }
+            }
+            
+            // 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 write/read the variable.
+            std::map<storm::expressions::Variable, std::set<uint_fast64_t>> variablesToAccessingModuleIndices;
+            for (uint_fast64_t index = 0; index < program.getNumberOfModules(); ++index) {
+                storm::prism::Module const& module = program.getModule(index);
+                
+                for (auto const& command : module.getCommands()) {
+                    std::set<storm::expressions::Variable> variables = command.getGuardExpression().getVariables();
+                    for (auto const& variable : variables) {
+                        variablesToAccessingModuleIndices[variable].insert(index);
+                    }
+                    
+                    for (auto const& update : command.getUpdates()) {
+                        for (auto const& assignment : update.getAssignments()) {
+                            variables = assignment.getExpression().getVariables();
+                            for (auto const& variable : variables) {
+                                variablesToAccessingModuleIndices[variable].insert(index);
+                            }
+                            variablesToAccessingModuleIndices[assignment.getVariable()].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 : program.getModules()) {
+                storm::jani::Automaton automaton(module.getName());
+                for (auto const& variable : module.getIntegerVariables()) {
+                    storm::jani::BoundedIntegerVariable newIntegerVariable = *storm::jani::makeBoundedIntegerVariable(variable.getName(), variable.getExpressionVariable(), variable.hasInitialValue() ? boost::make_optional(variable.getInitialValueExpression()) : boost::none, false, variable.getLowerBoundExpression(), variable.getUpperBoundExpression());
+                    std::set<uint_fast64_t> const& accessingModuleIndices = variablesToAccessingModuleIndices[variable.getExpressionVariable()];
+                    // If there is exactly one module reading and writing the variable, we can make the variable local to this module.
+                    if (!allVariablesGlobal && accessingModuleIndices.size() == 1) {
+                        storm::jani::BoundedIntegerVariable const& createdVariable = automaton.addVariable(newIntegerVariable);
+                        variableToVariableMap.emplace(variable.getExpressionVariable(), createdVariable);
+                    } else if (!accessingModuleIndices.empty()) {
+                        // Otherwise, we need to make it global.
+                        storm::jani::BoundedIntegerVariable const& createdVariable = janiModel.addVariable(newIntegerVariable);
+                        variableToVariableMap.emplace(variable.getExpressionVariable(), createdVariable);
+                    }
+                }
+                for (auto const& variable : module.getBooleanVariables()) {
+                    storm::jani::BooleanVariable newBooleanVariable = *storm::jani::makeBooleanVariable(variable.getName(), variable.getExpressionVariable(), variable.hasInitialValue() ? boost::make_optional(variable.getInitialValueExpression()) : boost::none, false);
+                    std::set<uint_fast64_t> const& accessingModuleIndices = variablesToAccessingModuleIndices[variable.getExpressionVariable()];
+                    // If there is exactly one module reading and writing the variable, we can make the variable local to this module.
+                    if (!allVariablesGlobal && accessingModuleIndices.size() == 1) {
+                        storm::jani::BooleanVariable const& createdVariable = automaton.addVariable(newBooleanVariable);
+                        variableToVariableMap.emplace(variable.getExpressionVariable(), createdVariable);
+                    } else if (!accessingModuleIndices.empty()) {
+                        // Otherwise, we need to make it global.
+                        storm::jani::BooleanVariable const& createdVariable = janiModel.addVariable(newBooleanVariable);
+                        variableToVariableMap.emplace(variable.getExpressionVariable(), createdVariable);
+                    }
+                }
+                automaton.setInitialStatesRestriction(manager->boolean(true));
+                
+                // Create a single location that will have all the edges.
+                uint64_t onlyLocation = automaton.addLocation(storm::jani::Location("l"));
+                automaton.addInitialLocation(onlyLocation);
+                
+                for (auto const& command : module.getCommands()) {
+                    boost::optional<storm::expressions::Expression> rateExpression;
+                    std::vector<storm::jani::EdgeDestination> destinations;
+                    if (program.getModelType() == Program::ModelType::CTMC || program.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(variableToVariableMap.at(assignment.getVariable()).get(), 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);
+            }
+            
+            // Translate the reward models.
+            for (auto const& rewardModel : program.getRewardModels()) {
+                
+            }
+            
+            // Create an initial state restriction if there was an initial construct in the program.
+            if (program.hasInitialConstruct()) {
+                janiModel.setInitialStatesRestriction(program.getInitialConstruct().getInitialStatesExpression());
+            } else {
+                janiModel.setInitialStatesRestriction(manager->boolean(true));
+            }
+            
+            // Set the standard system composition. This is possible, because we reject non-standard compositions anyway.
+            if (program.specifiesSystemComposition()) {
+                CompositionToJaniVisitor visitor;
+                janiModel.setSystemComposition(visitor.toJani(program.getSystemCompositionConstruct().getSystemComposition(), janiModel));
+            } else {
+                janiModel.setSystemComposition(janiModel.getStandardSystemComposition());
+            }
+            
+            janiModel.finalize();
+            
+            return janiModel;
+        }
+        
+    }
+}

src/storage/prism/ToJaniConverter.h

@@ -0,0 +1,20 @@
+#pragma once
+
+namespace storm {
+    namespace jani {
+        class Model;
+    }
+    
+    namespace prism {
+        
+        class Program;
+        
+        class ToJaniConverter {
+        public:
+            ToJaniConverter();
+            
+            storm::jani::Model convert(storm::prism::Program const& program, bool allVariablesGlobal = false) const;
+        };
+        
+    }
+}