more work and fixes for symbolic JANI builder

Former-commit-id: 5ca11938c1

src/builder/DdJaniModelBuilder.cpp

@@ -154,10 +154,10 @@ namespace storm {
             std::vector<std::pair<storm::expressions::Variable, storm::expressions::Variable>> rowColumnMetaVariablePairs;
 
             // A mapping from automata to the meta variable encoding their location.
-            std::map<std::string, storm::expressions::Variable> automatonToLocationVariableMap;
+            std::map<std::string, std::pair<storm::expressions::Variable, storm::expressions::Variable>> automatonToLocationVariableMap;
             
-            // The meta variables used to encode the actions.
-            std::vector<storm::expressions::Variable> actionVariables;
+            // A mapping from action indices to the meta variables used to encode these actions.
+            std::map<uint64_t, storm::expressions::Variable> actionVariablesMap;
             
             // The meta variables used to encode the remaining nondeterminism.
             std::vector<storm::expressions::Variable> nondeterminismVariables;
@@ -224,7 +224,7 @@ namespace storm {
                 for (auto const& action : this->model.getActions()) {
                     if (this->model.getActionIndex(action.getName()) != this->model.getSilentActionIndex()) {
                         std::pair<storm::expressions::Variable, storm::expressions::Variable> variablePair = result.manager->addMetaVariable(action.getName());
-                        result.actionVariables.push_back(variablePair.first);
+                        result.actionVariablesMap[this->model.getActionIndex(action.getName())] = variablePair.first;
                     }
                 }
                 
@@ -252,8 +252,8 @@ namespace storm {
                     storm::dd::Bdd<Type> range = result.manager->getBddOne();
                     
                     // Start by creating a meta variable for the location of the automaton.
-                    std::pair<storm::expressions::Variable, storm::expressions::Variable> variablePair = result.manager->addMetaVariable("l_" + automaton.getName(), 0, automaton.getNumberOfLocations());
-                    result.automatonToLocationVariableMap[automaton.getName()] = variablePair.first;
+                    std::pair<storm::expressions::Variable, storm::expressions::Variable> variablePair = result.manager->addMetaVariable("l_" + automaton.getName(), 0, automaton.getNumberOfLocations() - 1);
+                    result.automatonToLocationVariableMap[automaton.getName()] = variablePair;
                     storm::dd::Add<Type, ValueType> variableIdentity = result.manager->template getIdentity<ValueType>(variablePair.first).equals(result.manager->template getIdentity<ValueType>(variablePair.second)).template toAdd<ValueType>() * result.manager->getRange(variablePair.first).template toAdd<ValueType>() * result.manager->getRange(variablePair.second).template toAdd<ValueType>();
                     identity &= variableIdentity.toBdd();
                     range &= result.manager->getRange(variablePair.first);
@@ -278,6 +278,7 @@ namespace storm {
             }
             
             void createVariable(storm::jani::BoundedIntegerVariable const& variable, CompositionVariables<Type, ValueType>& result) {
+                std::cout << "creating int variable " << variable.getName() << std::endl;
                 int_fast64_t low = variable.getLowerBound().evaluateAsInt();
                 int_fast64_t high = variable.getUpperBound().evaluateAsInt();
                 std::pair<storm::expressions::Variable, storm::expressions::Variable> variablePair = result.manager->addMetaVariable(variable.getName(), low, high);
@@ -298,6 +299,7 @@ namespace storm {
             }
             
             void createVariable(storm::jani::BooleanVariable const& variable, CompositionVariables<Type, ValueType>& result) {
+                std::cout << "creating bool variable " << variable.getName() << std::endl;
                 std::pair<storm::expressions::Variable, storm::expressions::Variable> variablePair = result.manager->addMetaVariable(variable.getName());
                 
                 STORM_LOG_TRACE("Created meta variables for global boolean variable: " << variablePair.first.getName() << " and " << variablePair.second.getName() << ".");
@@ -405,6 +407,8 @@ namespace storm {
             return result;
         }
         
+        static int c = 0;
+        
         // A class that is responsible for performing the actual composition.
         template <storm::dd::DdType Type, typename ValueType>
         class AutomatonComposer : public storm::jani::CompositionVisitor {
@@ -523,7 +527,7 @@ namespace storm {
                     storm::dd::Add<Type, ValueType> writtenVariable = variables.manager->template getIdentity<ValueType>(primedMetaVariable);
                     
                     // Translate the expression that is being assigned.
-                    storm::dd::Add<Type, ValueType> updateExpression = variables.rowExpressionAdapter->translateExpression(assignment.getExpressionVariable());
+                    storm::dd::Add<Type, ValueType> updateExpression = variables.rowExpressionAdapter->translateExpression(assignment.getAssignedExpression());
                     
                     // Combine the update expression with the guard.
                     storm::dd::Add<Type, ValueType> result = updateExpression * guard;
@@ -535,6 +539,7 @@ namespace storm {
                     // Restrict the transitions to the range of the written variable.
                     result = result * variables.manager->getRange(primedMetaVariable).template toAdd<ValueType>();
                     
+                    // Combine the assignment DDs.
                     transitionsDd *= result;
                 }
                 
@@ -558,7 +563,7 @@ namespace storm {
                     }
                 }
                 
-                return EdgeDestinationDd<Type, ValueType>(transitionsDd * variables.rowExpressionAdapter->translateExpression(destination.getProbability()), assignedGlobalVariables);
+                return EdgeDestinationDd<Type, ValueType>(variables.manager->getEncoding(variables.automatonToLocationVariableMap.at(automaton.getName()).second, destination.getLocationId()).template toAdd<ValueType>() * transitionsDd * variables.rowExpressionAdapter->translateExpression(destination.getProbability()), assignedGlobalVariables);
             }
             
             /*!
@@ -607,7 +612,10 @@ namespace storm {
                         transitionsDd += destinationDd.transitionsDd;
                     }
                     
-                    return EdgeDd<Type, ValueType>(guard, guard * transitionsDd, globalVariablesInSomeUpdate);
+                    transitionsDd.exportToDot("trans_edge" + std::to_string(c) + ".dot");
+                    ++c;
+                    
+                    return EdgeDd<Type, ValueType>(guard, variables.manager->getEncoding(variables.automatonToLocationVariableMap.at(automaton.getName()).first, edge.getSourceLocationId()).template toAdd<ValueType>() * guard * transitionsDd, globalVariablesInSomeUpdate);
                 } else {
                     return EdgeDd<Type, ValueType>(variables.manager->template getAddZero<ValueType>(), variables.manager->template getAddZero<ValueType>());
                 }
@@ -638,6 +646,111 @@ namespace storm {
             CompositionVariables<Type, ValueType> const& variables;
         };
         
+        template <storm::dd::DdType Type, typename ValueType>
+        storm::dd::Add<Type, ValueType> encodeAction(uint64_t trueIndex, std::vector<storm::expressions::Variable> const& actionVariables, CompositionVariables<Type, ValueType> const& variables) {
+            storm::dd::Add<Type, ValueType> encoding = variables.manager->template getAddZero<ValueType>();
+            
+            trueIndex = actionVariables.size() - (trueIndex + 1);
+            uint64_t index = 0;
+            for (auto it = actionVariables.rbegin(), ite = actionVariables.rend(); it != ite; ++it, ++index) {
+                if (index == trueIndex) {
+                    encoding *= variables.manager->getEncoding(*it, 1).template toAdd<ValueType>();
+                } else {
+                    encoding *= variables.manager->getEncoding(*it, 0).template toAdd<ValueType>();
+                }
+            }
+            
+            return encoding;
+        }
+        
+        template <storm::dd::DdType Type, typename ValueType>
+        storm::dd::Add<Type, ValueType> computeMissingGlobalVariableIdentities(EdgeDd<Type, ValueType> const& edge, CompositionVariables<Type, ValueType> const& variables) {
+            std::set<storm::expressions::Variable> missingIdentities;
+            std::set_difference(variables.allGlobalVariables.begin(), variables.allGlobalVariables.end(), edge.writtenGlobalVariables.begin(), edge.writtenGlobalVariables.end(), std::inserter(missingIdentities, missingIdentities.begin()));
+            storm::dd::Add<Type, ValueType> identityEncoding = variables.manager->template getAddOne<ValueType>();
+            for (auto const& variable : missingIdentities) {
+                identityEncoding *= variables.variableToIdentityMap.at(variable);
+            }
+            return identityEncoding;
+        }
+        
+        template <storm::dd::DdType Type, typename ValueType>
+        storm::dd::Add<Type, ValueType> encodeIndex(uint64_t index, std::vector<storm::expressions::Variable> const& nondeterminismVariables, CompositionVariables<Type, ValueType> const& variables) {
+            storm::dd::Add<Type, ValueType> result = variables.manager->template getAddZero<ValueType>();
+            
+            STORM_LOG_TRACE("Encoding " << index << " with " << nondeterminismVariables.size() << " binary variable(s).");
+            
+            std::map<storm::expressions::Variable, int_fast64_t> metaVariableNameToValueMap;
+            for (uint_fast64_t i = 0; i < nondeterminismVariables.size(); ++i) {
+                if (index & (1ull << (nondeterminismVariables.size() - i - 1))) {
+                    metaVariableNameToValueMap.emplace(nondeterminismVariables[i], 1);
+                } else {
+                    metaVariableNameToValueMap.emplace(nondeterminismVariables[i], 0);
+                }
+            }
+            
+            result.setValue(metaVariableNameToValueMap, 1);
+            return result;
+        }
+        
+        template <storm::dd::DdType Type, typename ValueType>
+        storm::dd::Add<Type, ValueType> createGlobalTransitionRelation(storm::jani::Model const& model, AutomatonDd<Type, ValueType> const& automatonDd, CompositionVariables<Type, ValueType> const& variables) {
+            // If the model is an MDP, we need to encode the nondeterminism using additional variables.
+            if (model.getModelType() == storm::jani::ModelType::MDP) {
+                // Determine how many nondeterminism variables we need.
+                std::vector<storm::expressions::Variable> actionVariables;
+                std::map<uint64_t, uint64_t> actionIndexToVariableIndex;
+                uint64_t maximalNumberOfEdgesPerAction = 0;
+                for (auto const& action : automatonDd.actionIndexToEdges) {
+                    actionVariables.push_back(variables.actionVariablesMap.at(action.first));
+                    actionIndexToVariableIndex[action.first] = actionVariables.size() - 1;
+                    maximalNumberOfEdgesPerAction = std::max(maximalNumberOfEdgesPerAction, static_cast<uint64_t>(action.second.size()));
+                }
+                uint64_t numberOfNondeterminismVariables = static_cast<uint64_t>(std::ceil(std::log2(maximalNumberOfEdgesPerAction)));
+                std::vector<storm::expressions::Variable> nondeterminismVariables(numberOfNondeterminismVariables);
+                std::copy(variables.nondeterminismVariables.begin(), variables.nondeterminismVariables.begin() + numberOfNondeterminismVariables, nondeterminismVariables.begin());
+                
+                // Prepare result.
+                storm::dd::Add<Type, ValueType> result = variables.manager->template getAddZero<ValueType>();
+                
+                // Add edges to the result.
+                for (auto const& action : automatonDd.actionIndexToEdges) {
+                    storm::dd::Add<Type, ValueType> edgesForAction = variables.manager->template getAddZero<ValueType>();
+                    
+                    uint64_t edgeIndex = 0;
+                    for (auto const& edge : action.second) {
+                        edgesForAction += edge.transitionsDd * computeMissingGlobalVariableIdentities(edge, variables) * encodeIndex(edgeIndex, nondeterminismVariables, variables);
+                        ++edgeIndex;
+                    }
+                    
+                    result += edgesForAction * encodeAction<Type, ValueType>(actionIndexToVariableIndex.at(action.first), actionVariables, variables);
+                }
+            } else if (model.getModelType() == storm::jani::ModelType::DTMC || model.getModelType() == storm::jani::ModelType::CTMC) {
+                // Simply add all actions, but make sure to include the missing global variable identities.
+                storm::dd::Add<Type, ValueType> result = variables.manager->template getAddZero<ValueType>();
+                for (auto const& action : automatonDd.actionIndexToEdges) {
+                    uint64_t edgeIndex = 0;
+                    for (auto const& edge : action.second) {
+                        result += edge.transitionsDd * computeMissingGlobalVariableIdentities(edge, variables);
+                        edge.transitionsDd.exportToDot("edge_" + std::to_string(edgeIndex) + ".dot");
+                        ++edgeIndex;
+                    }
+                }
+                result.exportToDot("result.dot");
+                std::cout << "nnz: " << result.getNonZeroCount() << std::endl;
+                std::cout << "nodecnt: " << result.getNodeCount() << std::endl;
+                std::cout << "meta var: " << std::endl;
+                for (auto const& var : result.getContainedMetaVariables()) {
+                    std::cout << var.getName() << std::endl;
+                }
+                std::cout << std::endl;
+                return result;
+            } else {
+                STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "Illegal model type.");
+            }
+            return storm::dd::Add<Type, ValueType>();
+        }
+        
         template <storm::dd::DdType Type, typename ValueType>
         std::shared_ptr<storm::models::symbolic::Model<Type, ValueType>> DdJaniModelBuilder<Type, ValueType>::translate() {
             CompositionVariableCreator<Type, ValueType> variableCreator(*this->model);
@@ -646,6 +759,9 @@ namespace storm {
             AutomatonComposer<Type, ValueType> composer(*this->model, variables);
             AutomatonDd<Type, ValueType> system = composer.compose();
             
+            storm::dd::Add<Type, ValueType> transitions = createGlobalTransitionRelation(*this->model, system, variables);
+            transitions.exportToDot("trans.dot");
+            
             // FIXME
             return nullptr;
         }

src/builder/DdPrismModelBuilder.cpp

@@ -1067,10 +1067,30 @@ namespace storm {
                 
                 return result;
             } else if (generationInfo.program.getModelType() == storm::prism::Program::ModelType::DTMC || generationInfo.program.getModelType() == storm::prism::Program::ModelType::CTMC) {
-                // Simply add all actions.
-                storm::dd::Add<Type, ValueType> result = module.independentAction.transitionsDd;
+                // Simply add all actions, but make sure to include the missing global variable identities.
+                
+                // Compute missing global variable identities in independent action.
+                std::set<storm::expressions::Variable> missingIdentities;
+                std::set_difference(generationInfo.allGlobalVariables.begin(), generationInfo.allGlobalVariables.end(), module.independentAction.assignedGlobalVariables.begin(), module.independentAction.assignedGlobalVariables.end(), std::inserter(missingIdentities, missingIdentities.begin()));
+                storm::dd::Add<Type, ValueType> identityEncoding = generationInfo.manager->template getAddOne<ValueType>();
+                for (auto const& variable : missingIdentities) {
+                    STORM_LOG_TRACE("Multiplying identity of global variable " << variable.getName() << " to independent action.");
+                    identityEncoding *= generationInfo.variableToIdentityMap.at(variable);
+                }
+
+                storm::dd::Add<Type, ValueType> result = identityEncoding * module.independentAction.transitionsDd;
+                
                 for (auto const& synchronizingAction : module.synchronizingActionToDecisionDiagramMap) {
-                    result += synchronizingAction.second.transitionsDd;
+                    // Compute missing global variable identities in synchronizing actions.
+                    missingIdentities = std::set<storm::expressions::Variable>();
+                    std::set_difference(generationInfo.allGlobalVariables.begin(), generationInfo.allGlobalVariables.end(), synchronizingAction.second.assignedGlobalVariables.begin(), synchronizingAction.second.assignedGlobalVariables.end(), std::inserter(missingIdentities, missingIdentities.begin()));
+                    identityEncoding = generationInfo.manager->template getAddOne<ValueType>();
+                    for (auto const& variable : missingIdentities) {
+                        STORM_LOG_TRACE("Multiplying identity of global variable " << variable.getName() << " to synchronizing action '" << synchronizingAction.first << "'.");
+                        identityEncoding *= generationInfo.variableToIdentityMap.at(variable);
+                    }
+                    
+                    result += identityEncoding * synchronizingAction.second.transitionsDd;
                 }
                 return result;
             } else {
@@ -1084,6 +1104,14 @@ namespace storm {
             ModuleDecisionDiagram system = composer.compose(generationInfo.program.specifiesSystemComposition() ? generationInfo.program.getSystemCompositionConstruct().getSystemComposition() : *generationInfo.program.getDefaultSystemComposition());
             
             storm::dd::Add<Type, ValueType> result = createSystemFromModule(generationInfo, system);
+            result.exportToDot("result_prism.dot");
+            std::cout << "nnz: " << result.getNonZeroCount() << std::endl;
+            std::cout << "nodecnt: " << result.getNodeCount() << std::endl;
+            std::cout << "meta var: " << std::endl;
+            for (auto const& var : result.getContainedMetaVariables()) {
+                std::cout << var.getName() << std::endl;
+            }
+            std::cout << std::endl;
             
             // Create an auxiliary DD that is used later during the construction of reward models.
             storm::dd::Add<Type, ValueType> stateActionDd = result.sumAbstract(generationInfo.columnMetaVariables);

src/storage/dd/DdManager.cpp

@@ -103,10 +103,15 @@ namespace storm {
             STORM_LOG_THROW(!this->hasMetaVariable(name), storm::exceptions::InvalidArgumentException, "A meta variable '" << name << "' already exists.");
             
             // Check that the range is legal.
-            STORM_LOG_THROW(high != low, storm::exceptions::InvalidArgumentException, "Range of meta variable must be at least 2 elements.");
+            STORM_LOG_THROW(high >= low, storm::exceptions::InvalidArgumentException, "Illegal empty range for meta variable.");
             
             std::size_t numberOfBits = static_cast<std::size_t>(std::ceil(std::log2(high - low + 1)));
             
+            // For the case where low and high coincide, we need to have a single bit.
+            if (numberOfBits == 0) {
+                ++numberOfBits;
+            }
+            
             storm::expressions::Variable unprimed = manager->declareBitVectorVariable(name, numberOfBits);
             storm::expressions::Variable primed = manager->declareBitVectorVariable(name + "'", numberOfBits);
             

src/storage/jani/Automaton.cpp

@@ -164,6 +164,14 @@ namespace storm {
             return edges;
         }
         
+        std::set<uint64_t> Automaton::getActionIndices() const {
+            std::set<uint64_t> result;
+            for (auto const& edge : edges) {
+                result.insert(edge.getActionId());
+            }
+            return result;
+        }
+        
         uint64_t Automaton::getNumberOfLocations() const {
             return locations.size();
         }

src/storage/jani/Automaton.h

@@ -195,6 +195,11 @@ namespace storm {
              */
             std::vector<Edge> const& getEdges() const;
 
+            /*!
+             * Retrieves the set of action indices that are labels of edges of this automaton.
+             */
+            std::set<uint64_t> getActionIndices() const;
+            
             /*!
              * Retrieves the number of locations.
              */

src/storage/jani/BooleanVariable.cpp

@@ -7,5 +7,9 @@ namespace storm {
             // Intentionally left empty.
         }
         
+        bool BooleanVariable::isBooleanVariable() const {
+            return true;
+        }
+        
     }
 }

src/storage/jani/BooleanVariable.h

@@ -11,6 +11,8 @@ namespace storm {
              * Creates a boolean variable.
              */
             BooleanVariable(std::string const& name, storm::expressions::Variable const& variable, storm::expressions::Expression const& initialValue = storm::expressions::Expression());
+            
+            virtual bool isBooleanVariable() const;
         };
         
     }

src/storage/jani/BoundedIntegerVariable.cpp

@@ -23,5 +23,9 @@ namespace storm {
             this->upperBound = expression;
         }
         
+        bool BoundedIntegerVariable::isBoundedIntegerVariable() const {
+            return true;
+        }
+        
     }
 }

src/storage/jani/BoundedIntegerVariable.h

@@ -33,6 +33,8 @@ namespace storm {
              */
             void setUpperBound(storm::expressions::Expression const& expression);
 
+            virtual bool isBoundedIntegerVariable() const;
+
         private:
             // The expression defining the lower bound of the variable.
             storm::expressions::Expression lowerBound;

src/storage/jani/Model.cpp

@@ -156,12 +156,33 @@ namespace storm {
         }
         
         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());
+            std::set<uint64_t> leftHandActionIndices = this->automata.front().getActionIndices();
+            
             for (uint64_t index = 1; index < automata.size(); ++index) {
-                current = std::make_shared<ParallelComposition>(current, std::make_shared<AutomatonComposition>(automata[index].getName()), fullSynchronizationAlphabet);
+                std::set<uint64_t> newActionIndices = automata[index].getActionIndices();
+                
+                // Compute the intersection of actions of the left- and right-hand side.
+                std::set<uint64_t> intersectionActions;
+                std::set_intersection(leftHandActionIndices.begin(), leftHandActionIndices.end(), newActionIndices.begin(), newActionIndices.end(), std::inserter(intersectionActions, intersectionActions.begin()));
+                
+                // If the silent action is in the intersection, we remove it since we cannot synchronize over it.
+                auto it = intersectionActions.find(this->getSilentActionIndex());
+                if (it != intersectionActions.end()) {
+                    intersectionActions.erase(it);
+                }
+                
+                // Then join the actions to reflect the actions of the new left-hand side.
+                leftHandActionIndices.insert(newActionIndices.begin(), newActionIndices.end());
+                
+                // Create the set of strings that represents the actions over which to synchronize.
+                std::set<std::string> intersectionActionNames;
+                for (auto const& actionIndex : intersectionActions) {
+                    intersectionActionNames.insert(this->getAction(actionIndex).getName());
+                }
+
+                current = std::make_shared<ParallelComposition>(current, std::make_shared<AutomatonComposition>(automata[index].getName()), intersectionActionNames);
             }
             return current;
         }

src/storage/jani/ParallelComposition.cpp

@@ -5,7 +5,7 @@
 namespace storm {
     namespace jani {
         
-        ParallelComposition::ParallelComposition(std::shared_ptr<Composition> const& leftSubcomposition, std::shared_ptr<Composition> const& rightSubcomposition, std::set<std::string> const& alphabet) : leftSubcomposition(leftSubcomposition), rightSubcomposition(rightSubcomposition) {
+        ParallelComposition::ParallelComposition(std::shared_ptr<Composition> const& leftSubcomposition, std::shared_ptr<Composition> const& rightSubcomposition, std::set<std::string> const& alphabet) : leftSubcomposition(leftSubcomposition), rightSubcomposition(rightSubcomposition), alphabet(alphabet) {
             // Intentionally left empty.
         }
         

src/storage/jani/UnboundedIntegerVariable.cpp

@@ -7,5 +7,9 @@ namespace storm {
             // Intentionally left empty.
         }
         
+        bool UnboundedIntegerVariable::isUnboundedIntegerVariable() const {
+            return true;
+        }
+        
     }
 }

src/storage/jani/UnboundedIntegerVariable.h

@@ -11,6 +11,8 @@ namespace storm {
              * Creates an unbounded integer variable.
              */
             UnboundedIntegerVariable(std::string const& name, storm::expressions::Variable const& variable, storm::expressions::Expression const& initialValue = storm::expressions::Expression());
+            
+            virtual bool isUnboundedIntegerVariable() const override;
         };
         
     }

src/storage/jani/Variable.cpp

@@ -1,6 +1,8 @@
 #include "src/storage/jani/Variable.h"
 
-#include <iostream>
+#include "src/storage/jani/BooleanVariable.h"
+#include "src/storage/jani/BoundedIntegerVariable.h"
+#include "src/storage/jani/UnboundedIntegerVariable.h"
 
 namespace storm {
     namespace jani {
@@ -29,5 +31,41 @@ namespace storm {
             this->initialValue = initialValue;
         }
         
+        bool Variable::isBooleanVariable() const {
+            return false;
+        }
+        
+        bool Variable::isBoundedIntegerVariable() const {
+            return false;
+        }
+        
+        bool Variable::isUnboundedIntegerVariable() const {
+            return false;
+        }
+        
+        BooleanVariable& Variable::asBooleanVariable() {
+            return dynamic_cast<BooleanVariable&>(*this);
+        }
+        
+        BooleanVariable const& Variable::asBooleanVariable() const {
+            return dynamic_cast<BooleanVariable const&>(*this);
+        }
+        
+        BoundedIntegerVariable& Variable::asBoundedIntegerVariable() {
+            return dynamic_cast<BoundedIntegerVariable&>(*this);
+        }
+        
+        BoundedIntegerVariable const& Variable::asBoundedIntegerVariable() const {
+            return dynamic_cast<BoundedIntegerVariable const&>(*this);
+        }
+        
+        UnboundedIntegerVariable& Variable::asUnboundedIntegerVariable() {
+            return dynamic_cast<UnboundedIntegerVariable&>(*this);
+        }
+        
+        UnboundedIntegerVariable const& Variable::asUnboundedIntegerVariable() const {
+            return dynamic_cast<UnboundedIntegerVariable const&>(*this);
+        }
+        
     }
 }

src/storage/jani/Variable.h

@@ -9,6 +9,10 @@
 namespace storm {
     namespace jani {
         
+        class BooleanVariable;
+        class BoundedIntegerVariable;
+        class UnboundedIntegerVariable;
+        
         class Variable {
         public:
             /*!
@@ -41,6 +45,19 @@ namespace storm {
              */
             bool hasInitialValue() const;
             
+            // Methods to determine the type of the variable.
+            virtual bool isBooleanVariable() const;
+            virtual bool isBoundedIntegerVariable() const;
+            virtual bool isUnboundedIntegerVariable() const;
+            
+            // Methods to get the variable as a different type.
+            BooleanVariable& asBooleanVariable();
+            BooleanVariable const& asBooleanVariable() const;
+            BoundedIntegerVariable& asBoundedIntegerVariable();
+            BoundedIntegerVariable const& asBoundedIntegerVariable() const;
+            UnboundedIntegerVariable& asUnboundedIntegerVariable();
+            UnboundedIntegerVariable const& asUnboundedIntegerVariable() const;
+            
         private:
             // The name of the variable.
             std::string name;

src/storage/prism/Program.cpp

@@ -1518,31 +1518,24 @@ namespace storm {
             
             // 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>());
-                }
-            }
+            // 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) {
-                        variablesToReadingModuleIndices[variable].insert(index);
+                        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) {
-                                variablesToReadingModuleIndices[variable].insert(index);
+                                variablesToAccessingModuleIndices[variable].insert(index);
                             }
+                            variablesToAccessingModuleIndices[assignment.getVariable()].insert(index);
                         }
                     }
                 }
@@ -1554,23 +1547,23 @@ namespace storm {
                 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.
+                    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 (accessingModuleIndices.size() == 1) {
                         automaton.addBooleanVariable(newBooleanVariable);
-                    } else {
-                        // In this case, we need to make the variable global.
+                    } else { // if (accessingModuleIndices.size() > 1) {
+                        // Otherwise, we need to make it 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.
+                    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 (accessingModuleIndices.size() == 1) {
                         automaton.addBoundedIntegerVariable(newIntegerVariable);
-                    } else {
-                        // In this case, we need to make the variable global.
+                    } else { //if (accessingModuleIndices.size() > 1) {
+                        // Otherwise, we need to make it global.
                         janiModel.addBoundedIntegerVariable(newIntegerVariable);
                     }
                 }

test/functional/builder/DdJaniModelBuilderTest.cpp

@@ -79,6 +79,15 @@ TEST(DdJaniModelBuilderTest_Cudd, Dtmc) {
     //    EXPECT_EQ(13ul, model->getNumberOfStates());
     //    EXPECT_EQ(20ul, model->getNumberOfTransitions());
 
+//    program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/brp-2-2.pm");
+//    janiModel = program.toJani();
+//    
+//    builder = storm::builder::DdJaniModelBuilder<storm::dd::DdType::CUDD, double>(janiModel);
+//    t1 = std::chrono::high_resolution_clock::now();
+//    builder.translate();
+//    t2 = std::chrono::high_resolution_clock::now();
+//    std::cout << "brp2: " << std::chrono::duration_cast<std::chrono::milliseconds>(t2 - t1).count() << std::endl;
+    
     program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/brp-16-2.pm");
     janiModel = program.toJani();
     builder = storm::builder::DdJaniModelBuilder<storm::dd::DdType::CUDD, double>(janiModel);
@@ -86,38 +95,38 @@ TEST(DdJaniModelBuilderTest_Cudd, Dtmc) {
     model = builder.translate();
     t2 = std::chrono::high_resolution_clock::now();
     std::cout << "brp: " << std::chrono::duration_cast<std::chrono::milliseconds>(t2 - t1).count() << std::endl;
-    //    EXPECT_EQ(677ul, model->getNumberOfStates());
-    //    EXPECT_EQ(867ul, model->getNumberOfTransitions());
-    
-    program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/crowds-5-5.pm");
-    janiModel = program.toJani();
-    builder = storm::builder::DdJaniModelBuilder<storm::dd::DdType::CUDD, double>(janiModel);
-    t1 = std::chrono::high_resolution_clock::now();
-    model = builder.translate();
-    t2 = std::chrono::high_resolution_clock::now();
-    std::cout << "crowds: " << std::chrono::duration_cast<std::chrono::milliseconds>(t2 - t1).count() << std::endl;
-    //    EXPECT_EQ(8607ul, model->getNumberOfStates());
-    //    EXPECT_EQ(15113ul, model->getNumberOfTransitions());
-    
-    program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/leader-3-5.pm");
-    janiModel = program.toJani();
-    builder = storm::builder::DdJaniModelBuilder<storm::dd::DdType::CUDD, double>(janiModel);
-    t1 = std::chrono::high_resolution_clock::now();
-    model = builder.translate();
-    t2 = std::chrono::high_resolution_clock::now();
-    std::cout << "lead: " << std::chrono::duration_cast<std::chrono::milliseconds>(t2 - t1).count() << std::endl;
-    //    EXPECT_EQ(273ul, model->getNumberOfStates());
-    //    EXPECT_EQ(397ul, model->getNumberOfTransitions());
-    
-    program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/nand-5-2.pm");
-    janiModel = program.toJani();
-    builder = storm::builder::DdJaniModelBuilder<storm::dd::DdType::CUDD, double>(janiModel);
-    t1 = std::chrono::high_resolution_clock::now();
-    model = builder.translate();
-    t2 = std::chrono::high_resolution_clock::now();
-    std::cout << "nand: " << std::chrono::duration_cast<std::chrono::milliseconds>(t2 - t1).count() << std::endl;
-    //    EXPECT_EQ(1728ul, model->getNumberOfStates());
-    //    EXPECT_EQ(2505ul, model->getNumberOfTransitions());
+//    //    EXPECT_EQ(677ul, model->getNumberOfStates());
+//    //    EXPECT_EQ(867ul, model->getNumberOfTransitions());
+//    
+//    program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/crowds-5-5.pm");
+//    janiModel = program.toJani();
+//    builder = storm::builder::DdJaniModelBuilder<storm::dd::DdType::CUDD, double>(janiModel);
+//    t1 = std::chrono::high_resolution_clock::now();
+//    model = builder.translate();
+//    t2 = std::chrono::high_resolution_clock::now();
+//    std::cout << "crowds: " << std::chrono::duration_cast<std::chrono::milliseconds>(t2 - t1).count() << std::endl;
+//    //    EXPECT_EQ(8607ul, model->getNumberOfStates());
+//    //    EXPECT_EQ(15113ul, model->getNumberOfTransitions());
+//    
+//    program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/leader-3-5.pm");
+//    janiModel = program.toJani();
+//    builder = storm::builder::DdJaniModelBuilder<storm::dd::DdType::CUDD, double>(janiModel);
+//    t1 = std::chrono::high_resolution_clock::now();
+//    model = builder.translate();
+//    t2 = std::chrono::high_resolution_clock::now();
+//    std::cout << "lead: " << std::chrono::duration_cast<std::chrono::milliseconds>(t2 - t1).count() << std::endl;
+//    //    EXPECT_EQ(273ul, model->getNumberOfStates());
+//    //    EXPECT_EQ(397ul, model->getNumberOfTransitions());
+//    
+//    program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/nand-5-2.pm");
+//    janiModel = program.toJani();
+//    builder = storm::builder::DdJaniModelBuilder<storm::dd::DdType::CUDD, double>(janiModel);
+//    t1 = std::chrono::high_resolution_clock::now();
+//    model = builder.translate();
+//    t2 = std::chrono::high_resolution_clock::now();
+//    std::cout << "nand: " << std::chrono::duration_cast<std::chrono::milliseconds>(t2 - t1).count() << std::endl;
+//    //    EXPECT_EQ(1728ul, model->getNumberOfStates());
+//    //    EXPECT_EQ(2505ul, model->getNumberOfTransitions());
 }
 
 //TEST(DdPrismModelBuilderTest_Cudd, Dtmc) {

test/functional/builder/DdPrismModelBuilderTest.cpp

@@ -60,6 +60,11 @@ TEST(DdPrismModelBuilderTest_Cudd, Dtmc) {
     EXPECT_EQ(13ul, model->getNumberOfStates());
     EXPECT_EQ(20ul, model->getNumberOfTransitions());
 
+//    program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/brp-2-2.pm");
+//    model = storm::builder::DdPrismModelBuilder<storm::dd::DdType::CUDD>().translateProgram(program);
+//
+//    exit(-1);
+    
     program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/brp-16-2.pm");
     model = storm::builder::DdPrismModelBuilder<storm::dd::DdType::CUDD>().translateProgram(program);
     EXPECT_EQ(677ul, model->getNumberOfStates());