diff --git a/src/adapters/SymbolicExpressionAdapter.h b/src/adapters/SymbolicExpressionAdapter.h index fd23864b7..efdd5e2d0 100644 --- a/src/adapters/SymbolicExpressionAdapter.h +++ b/src/adapters/SymbolicExpressionAdapter.h @@ -22,7 +22,7 @@ namespace adapters { class SymbolicExpressionAdapter : public storm::ir::expressions::ExpressionVisitor { public: - SymbolicExpressionAdapter(std::unordered_map>& variableToDecisionDiagramVariableMap) : stack(), variableToDecisionDiagramVariableMap(variableToDecisionDiagramVariableMap) { + SymbolicExpressionAdapter(storm::ir::Program const& program, std::unordered_map>& 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(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(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(i)); @@ -220,6 +222,7 @@ public: } private: + storm::ir::Program const& program; std::stack stack; std::unordered_map>& variableToDecisionDiagramVariableMap; }; diff --git a/src/adapters/SymbolicModelAdapter.h b/src/adapters/SymbolicModelAdapter.h index 0ab93ac4d..90067c5ee 100644 --- a/src/adapters/SymbolicModelAdapter.h +++ b/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 allDecisionDiagramVariables; diff --git a/src/ir/Module.cpp b/src/ir/Module.cpp index b28c9c9fe..321d022cb 100644 --- a/src/ir/Module.cpp +++ b/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(); } diff --git a/src/ir/Module.h b/src/ir/Module.h index 1b20991ea..3fd194b5c 100644 --- a/src/ir/Module.h +++ b/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. * diff --git a/src/ir/Program.cpp b/src/ir/Program.cpp index 0db9f7342..276b59134 100644 --- a/src/ir/Program.cpp +++ b/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> booleanUndefinedConstantExpressions, std::map> integerUndefinedConstantExpressions, std::map> doubleUndefinedConstantExpressions, std::vector modules, std::map rewards, std::map> 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(); } - 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()) { diff --git a/src/ir/Program.h b/src/ir/Program.h index 891b6abbf..23d154110 100644 --- a/src/ir/Program.h +++ b/src/ir/Program.h @@ -106,6 +106,14 @@ namespace storm { */ std::set 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> actionsToModuleIndexMap; + + // A mapping from variable names to the modules in which they were declared. + std::map variableToModuleIndexMap; }; } // namespace ir diff --git a/src/ir/expressions/ExpressionVisitor.h b/src/ir/expressions/ExpressionVisitor.h index 1ca3021e4..3891fa8f3 100644 --- a/src/ir/expressions/ExpressionVisitor.h +++ b/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; diff --git a/src/models/AbstractDeterministicModel.h b/src/models/AbstractDeterministicModel.h index a45b5df77..88ed50979 100644 --- a/src/models/AbstractDeterministicModel.h +++ b/src/models/AbstractDeterministicModel.h @@ -4,6 +4,7 @@ #include "AbstractModel.h" #include +#include namespace storm { @@ -64,6 +65,7 @@ class AbstractDeterministicModel: public AbstractModel { virtual typename storm::storage::SparseMatrix::ConstIndexIterator constStateSuccessorIteratorEnd(uint_fast64_t state) const { return this->transitionMatrix->constColumnIteratorEnd(state); } + }; } // namespace models diff --git a/src/models/AbstractModel.h b/src/models/AbstractModel.h index e632e7879..aaae20f71 100644 --- a/src/models/AbstractModel.h +++ b/src/models/AbstractModel.h @@ -266,10 +266,12 @@ class AbstractModel: public std::enable_shared_from_this> { } /*! - * 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 const getPropositionsForState(uint_fast64_t const& state) const { + std::set getLabelsForState(uint_fast64_t state) const { return stateLabeling->getPropositionsForState(state); } @@ -312,6 +314,70 @@ class AbstractModel: public std::enable_shared_from_this> { } 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 const* firstValue = nullptr, std::vector const* secondValue = nullptr, std::vector const* stateColoring = nullptr, std::vector 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. diff --git a/src/storm.cpp b/src/storm.cpp index 1fcd0c1ec..f98464ab4 100644 --- a/src/storm.cpp +++ b/src/storm.cpp @@ -48,6 +48,7 @@ #include #include +#include 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>()->writeDotToStream(std::cout); modelchecker = createPrctlModelChecker(*parser.getModel>()); 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: