Added methods to retrieve module index by variable name from IR. This fixes an issue in the symbolic adapter.

src/adapters/SymbolicExpressionAdapter.h

@@ -22,7 +22,7 @@ namespace adapters {
 
 class SymbolicExpressionAdapter : public storm::ir::expressions::ExpressionVisitor {
 public:
-	SymbolicExpressionAdapter(std::unordered_map<std::string, std::vector<ADD*>>& variableToDecisionDiagramVariableMap) : stack(), variableToDecisionDiagramVariableMap(variableToDecisionDiagramVariableMap) {
+	SymbolicExpressionAdapter(storm::ir::Program const& program, std::unordered_map<std::string, std::vector<ADD*>>& variableToDecisionDiagramVariableMap) : program(program), stack(), variableToDecisionDiagramVariableMap(variableToDecisionDiagramVariableMap) {
 
 	}
 
@@ -131,7 +131,7 @@ public:
 		stack.push(new ADD(*cuddUtility->getConstant(expression->getValue() ? 1 : 0)));
 	}
 
-	virtual void visit(storm::ir::expressions::BooleanLiteral* expression) {
+	virtual void visit(storm::ir::expressions::BooleanLiteralExpression* expression) {
 		storm::utility::CuddUtility* cuddUtility = storm::utility::cuddUtilityInstance();
 		stack.push(new ADD(*cuddUtility->getConstant(expression->getValueAsBool(nullptr) ? 1 : 0)));
 	}
@@ -146,7 +146,7 @@ public:
 		stack.push(new ADD(*cuddUtility->getConstant(expression->getValue())));
 	}
 
-	virtual void visit(storm::ir::expressions::DoubleLiteral* expression) {
+	virtual void visit(storm::ir::expressions::DoubleLiteralExpression* expression) {
 		storm::utility::CuddUtility* cuddUtility = storm::utility::cuddUtilityInstance();
 		stack.push(new ADD(*cuddUtility->getConstant(expression->getValueAsDouble(nullptr))));
 	}
@@ -161,7 +161,7 @@ public:
 		stack.push(new ADD(*cuddUtility->getConstant(static_cast<double>(expression->getValue()))));
 	}
 
-	virtual void visit(storm::ir::expressions::IntegerLiteral* expression) {
+	virtual void visit(storm::ir::expressions::IntegerLiteralExpression* expression) {
 		storm::utility::CuddUtility* cuddUtility = storm::utility::cuddUtilityInstance();
 		stack.push(new ADD(*cuddUtility->getConstant(static_cast<double>(expression->getValueAsInt(nullptr)))));
 	}
@@ -208,8 +208,10 @@ public:
 		if (expression->getType() == storm::ir::expressions::BaseExpression::bool_) {
 			cuddUtility->setValueAtIndex(result, 1, variables, 1);
 		} else {
-			int64_t low = expression->getLowerBound()->getValueAsInt(nullptr);
-			int64_t high = expression->getUpperBound()->getValueAsInt(nullptr);
+            storm::ir::Module const& module = program.getModule(program.getModuleIndexForVariable(expression->getVariableName()));
+            storm::ir::IntegerVariable const& integerVariable = module.getIntegerVariable(expression->getVariableName());
+			int64_t low = integerVariable.getLowerBound()->getValueAsInt(nullptr);
+			int64_t high = integerVariable.getUpperBound()->getValueAsInt(nullptr);
 
 			for (int_fast64_t i = low; i <= high; ++i) {
 				cuddUtility->setValueAtIndex(result, i - low, variables, static_cast<double>(i));
@@ -220,6 +222,7 @@ public:
 	}
 
 private:
+    storm::ir::Program const& program;
 	std::stack<ADD*> stack;
 	std::unordered_map<std::string, std::vector<ADD*>>& variableToDecisionDiagramVariableMap;
 };

src/adapters/SymbolicModelAdapter.h

@@ -25,16 +25,16 @@ namespace adapters {
 class SymbolicModelAdapter {
 public:
 
-	SymbolicModelAdapter() : cuddUtility(storm::utility::cuddUtilityInstance()), allDecisionDiagramVariables(),
+	SymbolicModelAdapter(storm::ir::Program const& program) : program(program), cuddUtility(storm::utility::cuddUtilityInstance()), allDecisionDiagramVariables(),
 		allRowDecisionDiagramVariables(), allColumnDecisionDiagramVariables(), booleanRowDecisionDiagramVariables(),
 		integerRowDecisionDiagramVariables(), booleanColumnDecisionDiagramVariables(), integerColumnDecisionDiagramVariables(),
 		variableToRowDecisionDiagramVariableMap(), variableToColumnDecisionDiagramVariableMap(),
 		variableToIdentityDecisionDiagramMap(),
-		rowExpressionAdapter(variableToRowDecisionDiagramVariableMap), columnExpressionAdapter(variableToColumnDecisionDiagramVariableMap) {
+		rowExpressionAdapter(program, variableToRowDecisionDiagramVariableMap), columnExpressionAdapter(program, variableToColumnDecisionDiagramVariableMap) {
 
 	}
 
-	void toMTBDD(storm::ir::Program const& program) {
+	void toMTBDD() {
 		LOG4CPLUS_INFO(logger, "Creating MTBDD representation for probabilistic program.");
 		createDecisionDiagramVariables(program);
 		createIdentityDecisionDiagrams(program);
@@ -122,6 +122,7 @@ public:
 	}
 
 private:
+    storm::ir::Program const& program;
 	storm::utility::CuddUtility* cuddUtility;
 
 	std::vector<ADD*> allDecisionDiagramVariables;

src/ir/Module.cpp

@@ -86,6 +86,11 @@ namespace storm {
             return this->booleanVariables[index];
         }
         
+        storm::ir::BooleanVariable const& Module::getBooleanVariable(std::string const& variableName) const {
+            uint_fast64_t index = this->getBooleanVariableIndex(variableName);
+            return this->booleanVariables[index];
+        }
+        
         uint_fast64_t Module::getNumberOfIntegerVariables() const {
             return this->integerVariables.size();
         }
@@ -94,6 +99,11 @@ namespace storm {
             return this->integerVariables[index];
         }
         
+        storm::ir::IntegerVariable const& Module::getIntegerVariable(std::string const& variableName) const {
+            uint_fast64_t index = this->getIntegerVariableIndex(variableName);
+            return this->integerVariables[index];
+        }
+        
         uint_fast64_t Module::getNumberOfCommands() const {
             return this->commands.size();
         }

src/ir/Module.h

@@ -83,6 +83,13 @@ namespace storm {
              */
             storm::ir::BooleanVariable const& getBooleanVariable(uint_fast64_t index) const;
             
+            /*!
+             * Retrieves a reference to the boolean variable with the given name.
+             *
+             * @return A reference to the boolean variable with the given name.
+             */
+            storm::ir::BooleanVariable const& getBooleanVariable(std::string const& variableName) const;
+            
             /*!
              * Retrieves the number of integer variables in the module.
              *
@@ -97,6 +104,13 @@ namespace storm {
              */
             storm::ir::IntegerVariable const& getIntegerVariable(uint_fast64_t index) const;
             
+            /*!
+             * Retrieves a reference to the boolean variable with the given name.
+             *
+             * @return A reference to the boolean variable with the given name.
+             */
+            storm::ir::IntegerVariable const& getIntegerVariable(std::string const& variableName) const;
+            
             /*!
              * Retrieves the number of commands of this module.
              *

src/ir/Program.cpp

@@ -19,21 +19,31 @@ extern log4cplus::Logger logger;
 namespace storm {
     namespace ir {
         
-        Program::Program() : modelType(UNDEFINED), booleanUndefinedConstantExpressions(), integerUndefinedConstantExpressions(), doubleUndefinedConstantExpressions(), modules(), rewards(), actions(), actionsToModuleIndexMap() {
+        Program::Program() : modelType(UNDEFINED), booleanUndefinedConstantExpressions(), integerUndefinedConstantExpressions(), doubleUndefinedConstantExpressions(), modules(), rewards(), actions(), actionsToModuleIndexMap(), variableToModuleIndexMap() {
             // Nothing to do here.
         }
         
         Program::Program(ModelType modelType, std::map<std::string, std::shared_ptr<storm::ir::expressions::BooleanConstantExpression>> booleanUndefinedConstantExpressions, std::map<std::string, std::shared_ptr<storm::ir::expressions::IntegerConstantExpression>> integerUndefinedConstantExpressions, std::map<std::string, std::shared_ptr<storm::ir::expressions::DoubleConstantExpression>> doubleUndefinedConstantExpressions, std::vector<storm::ir::Module> modules, std::map<std::string, storm::ir::RewardModel> rewards, std::map<std::string, std::shared_ptr<storm::ir::expressions::BaseExpression>> labels)
-        : modelType(modelType), booleanUndefinedConstantExpressions(booleanUndefinedConstantExpressions), integerUndefinedConstantExpressions(integerUndefinedConstantExpressions), doubleUndefinedConstantExpressions(doubleUndefinedConstantExpressions), modules(modules), rewards(rewards), labels(labels), actionsToModuleIndexMap() {
+        : modelType(modelType), booleanUndefinedConstantExpressions(booleanUndefinedConstantExpressions), integerUndefinedConstantExpressions(integerUndefinedConstantExpressions), doubleUndefinedConstantExpressions(doubleUndefinedConstantExpressions), modules(modules), rewards(rewards), labels(labels), actionsToModuleIndexMap(), variableToModuleIndexMap() {
             // Now build the mapping from action names to module indices so that the lookup can later be performed quickly.
-            for (unsigned int moduleId = 0; moduleId < this->modules.size(); moduleId++) {
-                for (auto const& action : this->modules[moduleId].getActions()) {
+            for (unsigned int moduleIndex = 0; moduleIndex < this->modules.size(); moduleIndex++) {
+                Module const& module = this->modules[moduleIndex];
+                
+                for (auto const& action : module.getActions()) {
                     if (this->actionsToModuleIndexMap.count(action) == 0) {
                         this->actionsToModuleIndexMap[action] = std::set<uint_fast64_t>();
                     }
-                    this->actionsToModuleIndexMap[action].insert(moduleId);
+                    this->actionsToModuleIndexMap[action].insert(moduleIndex);
                     this->actions.insert(action);
                 }
+                
+                // Put in the appropriate entries for the mapping from variable names to module index.
+                for (uint_fast64_t booleanVariableIndex = 0; booleanVariableIndex < module.getNumberOfBooleanVariables(); ++booleanVariableIndex) {
+                    this->variableToModuleIndexMap[module.getBooleanVariable(booleanVariableIndex).getName()] = moduleIndex;
+                }
+                for (uint_fast64_t integerVariableIndex = 0; integerVariableIndex < module.getNumberOfIntegerVariables(); ++integerVariableIndex) {
+                    this->variableToModuleIndexMap[module.getIntegerVariable(integerVariableIndex).getName()] = moduleIndex;
+                }
             }
         }
         
@@ -99,6 +109,14 @@ namespace storm {
             return actionModuleSetPair->second;
         }
         
+        uint_fast64_t Program::getModuleIndexForVariable(std::string const& variableName) const {
+            auto variableNameToModuleIndexPair = this->variableToModuleIndexMap.find(variableName);
+            if (variableNameToModuleIndexPair != this->variableToModuleIndexMap.end()) {
+                return variableNameToModuleIndexPair->second;
+            }
+            throw storm::exceptions::OutOfRangeException() << "Variable '" << variableName << "' does not exist.";
+        }
+        
         storm::ir::RewardModel const& Program::getRewardModel(std::string const& name) const {
             auto nameRewardModelPair = this->rewards.find(name);
             if (nameRewardModelPair == this->rewards.end()) {

src/ir/Program.h

@@ -106,6 +106,14 @@ namespace storm {
              */
             std::set<uint_fast64_t> const& getModulesByAction(std::string const& action) const;
             
+            /*!
+             * Retrieves the index of the module in which the given variable name was declared.
+             *
+             * @param variableName The name of the variable to search.
+             * @return The index of the module in which the given variable name was declared.
+             */
+            uint_fast64_t getModuleIndexForVariable(std::string const& variableName) const;
+            
             /*!
              * Retrieves the reward model with the given name.
              *
@@ -148,6 +156,9 @@ namespace storm {
             
             // A map of actions to the set of modules containing commands labelled with this action.
             std::map<std::string, std::set<uint_fast64_t>> actionsToModuleIndexMap;
+            
+            // A mapping from variable names to the modules in which they were declared.
+            std::map<std::string, uint_fast64_t> variableToModuleIndexMap;
         };
         
     } // namespace ir

src/ir/expressions/ExpressionVisitor.h

@@ -17,11 +17,11 @@ namespace storm {
             class BinaryNumericalFunctionExpression;
             class BinaryRelationExpression;
             class BooleanConstantExpression;
-            class BooleanLiteral;
+            class BooleanLiteralExpression;
             class DoubleConstantExpression;
-            class DoubleLiteral;
+            class DoubleLiteralExpression;
             class IntegerConstantExpression;
-            class IntegerLiteral;
+            class IntegerLiteralExpression;
             class UnaryBooleanFunctionExpression;
             class UnaryNumericalFunctionExpression;
             class VariableExpression;
@@ -33,11 +33,11 @@ namespace storm {
                 virtual void visit(BinaryNumericalFunctionExpression* expression) = 0;
                 virtual void visit(BinaryRelationExpression* expression) = 0;
                 virtual void visit(BooleanConstantExpression* expression) = 0;
-                virtual void visit(BooleanLiteral* expression) = 0;
+                virtual void visit(BooleanLiteralExpression* expression) = 0;
                 virtual void visit(DoubleConstantExpression* expression) = 0;
-                virtual void visit(DoubleLiteral* expression) = 0;
+                virtual void visit(DoubleLiteralExpression* expression) = 0;
                 virtual void visit(IntegerConstantExpression* expression) = 0;
-                virtual void visit(IntegerLiteral* expression) = 0;
+                virtual void visit(IntegerLiteralExpression* expression) = 0;
                 virtual void visit(UnaryBooleanFunctionExpression* expression) = 0;
                 virtual void visit(UnaryNumericalFunctionExpression* expression) = 0;
                 virtual void visit(VariableExpression* expression) = 0;

src/models/AbstractDeterministicModel.h

@@ -4,6 +4,7 @@
 #include "AbstractModel.h"
 
 #include <memory>
+#include <sstream>
 
 namespace storm {
 
@@ -64,6 +65,7 @@ class AbstractDeterministicModel: public AbstractModel<T> {
         virtual typename storm::storage::SparseMatrix<T>::ConstIndexIterator constStateSuccessorIteratorEnd(uint_fast64_t state) const {
             return this->transitionMatrix->constColumnIteratorEnd(state);
         }
+    
 };
 
 } // namespace models

src/models/AbstractModel.h

@@ -266,10 +266,12 @@ class AbstractModel: public std::enable_shared_from_this<AbstractModel<T>> {
 		}
 
 		/*!
-		 * Returns the set of states with which the given state is labeled.
-		 * @return The set of states with which the given state is labeled.
+		 * Returns the set of labels with which the given state is labeled.
+         *
+         * @param state The state for which to return the set of labels.
+		 * @return The set of labels with which the given state is labeled.
 		 */
-		std::set<std::string> const getPropositionsForState(uint_fast64_t const& state) const {
+		std::set<std::string> getLabelsForState(uint_fast64_t state) const {
 			return stateLabeling->getPropositionsForState(state);
 		}
 
@@ -313,6 +315,70 @@ class AbstractModel: public std::enable_shared_from_this<AbstractModel<T>> {
 			return result;
 		}
     
+        /*!
+         * Exports the model to the dot-format and prints the result to the given stream.
+         *
+         * @param outStream The stream to which the model is to be written. 
+         * @param includeLabling If set to true, the states will be exported with their labels.
+         * @param subsystem If not null, this represents the subsystem that is to be exported.
+         * @param firstValue If not null, the values in this vector are attached to the states.
+         * @param secondValue If not null, the values in this vector are attached to the states.
+         * @param stateColoring If not null, this is a mapping from states to color codes.
+         * @param colors A mapping of color codes to color names.
+         * @return A string containing the exported model in dot-format.
+         */
+        virtual void writeDotToStream(std::ostream& outStream, bool includeLabeling = true, storm::storage::BitVector const* subsystem = nullptr, std::vector<T> const* firstValue = nullptr, std::vector<T> const* secondValue = nullptr, std::vector<uint_fast64_t> const* stateColoring = nullptr, std::vector<std::string> const* colors = nullptr) const {
+            outStream << "digraph deterministicModel {" << std::endl;
+        
+            for (uint_fast64_t stateIndex = 0, highestStateIndex = this->getNumberOfStates() - 1; stateIndex <= highestStateIndex; ++stateIndex) {
+                outStream << "\t" << stateIndex;
+                if (includeLabeling || firstValue != nullptr || secondValue != nullptr || stateColoring != nullptr) {
+                    outStream << " [ ";
+                    if (includeLabeling || firstValue != nullptr || secondValue != nullptr) {
+                        outStream << "label = \"";
+                    
+                        // Now print the state labeling to the stream if requested.
+                        if (includeLabeling) {
+                            bool insertComma = true;
+                            for (std::string const& label : this->getLabelsForState(stateIndex)) {
+                                if (insertComma) {
+                                    outStream << ", ";
+                                    insertComma = false;
+                                }
+                                outStream << label;
+                            }
+                        }
+                    
+                        // If we are to include some values for the state as well, we do so now.
+                        if (firstValue != nullptr || secondValue != nullptr) {
+                            outStream << "[";
+                            if (firstValue != nullptr) {
+                                outStream << (*firstValue)[stateIndex];
+                                if (secondValue != nullptr) {
+                                    outStream << ", ";
+                                }
+                            }
+                            if (secondValue != nullptr) {
+                                outStream << (*secondValue)[stateIndex];
+                            }
+                            outStream << "]";
+                        }
+                        outStream << "\"";
+                    
+                        // Now, we color the states if there were colors given.
+                        if (stateColoring != nullptr && colors != nullptr) {
+                            outStream << ", ";
+                            outStream << " fillcolor = \"" << (*colors)[(*stateColoring)[stateIndex]] << "\"";
+                        }
+                    }
+                    outStream << " ]";
+                }
+                outStream << ";";
+            }
+            
+            outStream << "}" << std::endl;
+        }
+
 		/*!
 		 * Prints information about the model to the specified stream.
 		 * @param out The stream the information is to be printed to.

src/storm.cpp

@@ -48,6 +48,7 @@
 
 #include <iostream>
 #include <iomanip>
+#include <fstream>
 
 void printUsage() {
 #ifndef WINDOWS	
@@ -288,6 +289,7 @@ int main(const int argc, const char* argv[]) {
 			switch (parser.getType()) {
 			case storm::models::DTMC:
 				LOG4CPLUS_INFO(logger, "Model is a DTMC.");
+                parser.getModel<storm::models::Dtmc<double>>()->writeDotToStream(std::cout);
                 modelchecker = createPrctlModelChecker(*parser.getModel<storm::models::Dtmc<double>>());
 				checkPrctlFormulae(*modelchecker);
 				break;
@@ -301,7 +303,7 @@ int main(const int argc, const char* argv[]) {
                 LOG4CPLUS_ERROR(logger, "The selected model type is not supported.");
                 break;
 			case storm::models::CTMDP:
-                LOG4CPLUS_INFO(logger, "Model is a CTMC.");
+                LOG4CPLUS_INFO(logger, "Model is a CTMDP.");
                 LOG4CPLUS_ERROR(logger, "The selected model type is not supported.");
 				break;
 			case storm::models::Unknown: