From d87c79d0f6d35162f91f7a24a5d168acbd054c9a Mon Sep 17 00:00:00 2001 From: dehnert Date: Mon, 7 Apr 2014 22:54:47 +0200 Subject: [PATCH] Added implies/iff to expression classes. Finished reworking PRISM classes. Former-commit-id: ca202042ed267b476c6cc900267b5cb031d79614 --- .../BinaryBooleanFunctionExpression.cpp | 21 +- .../BinaryBooleanFunctionExpression.h | 2 +- src/storage/expressions/Expression.cpp | 10 + src/storage/expressions/Expression.h | 3 + src/storage/prism/Module.cpp | 2 +- src/storage/prism/Module.h | 4 +- src/storage/prism/Program.cpp | 365 +++++++----------- src/storage/prism/Program.h | 35 +- src/storage/prism/Update.cpp | 2 +- 9 files changed, 206 insertions(+), 238 deletions(-) diff --git a/src/storage/expressions/BinaryBooleanFunctionExpression.cpp b/src/storage/expressions/BinaryBooleanFunctionExpression.cpp index 8f5abf57c..90ba44885 100644 --- a/src/storage/expressions/BinaryBooleanFunctionExpression.cpp +++ b/src/storage/expressions/BinaryBooleanFunctionExpression.cpp @@ -1,5 +1,5 @@ #include "src/storage/expressions/BinaryBooleanFunctionExpression.h" - +#include "src/storage/expressions/BooleanLiteralExpression.h" #include "src/exceptions/ExceptionMacros.h" #include "src/exceptions/InvalidTypeException.h" @@ -23,6 +23,8 @@ namespace storm { switch (this->getOperatorType()) { case OperatorType::And: result = firstOperandEvaluation && secondOperandEvaluation; break; case OperatorType::Or: result = firstOperandEvaluation || secondOperandEvaluation; break; + case OperatorType::Implies: result = !firstOperandEvaluation || secondOperandEvaluation; break; + case OperatorType::Iff: result = (firstOperandEvaluation && secondOperandEvaluation) || (!firstOperandEvaluation && !secondOperandEvaluation); break; } return result; @@ -52,6 +54,21 @@ namespace storm { } else if (secondOperandSimplified->isFalse()) { return firstOperandSimplified; } + break; + case OperatorType::Implies: if (firstOperandSimplified->isTrue()) { + return secondOperandSimplified; + } else if (firstOperandSimplified->isFalse()) { + return std::shared_ptr(new BooleanLiteralExpression(true)); + } else if (secondOperandSimplified->isTrue()) { + return std::shared_ptr(new BooleanLiteralExpression(true)); + } + break; + case OperatorType::Iff: if (firstOperandSimplified->isTrue() && secondOperandSimplified->isTrue()) { + return std::shared_ptr(new BooleanLiteralExpression(true)); + } else if (firstOperandSimplified->isFalse() && secondOperandSimplified->isFalse()) { + return std::shared_ptr(new BooleanLiteralExpression(true)); + } + break; } // If the two successors remain unchanged, we can return a shared_ptr to this very object. @@ -71,6 +88,8 @@ namespace storm { switch (this->getOperatorType()) { case OperatorType::And: stream << " && "; break; case OperatorType::Or: stream << " || "; break; + case OperatorType::Implies: stream << " => "; break; + case OperatorType::Iff: stream << " <=> "; break; } stream << *this->getSecondOperand() << ")"; } diff --git a/src/storage/expressions/BinaryBooleanFunctionExpression.h b/src/storage/expressions/BinaryBooleanFunctionExpression.h index 41ae92b7b..b4f8ad0a6 100644 --- a/src/storage/expressions/BinaryBooleanFunctionExpression.h +++ b/src/storage/expressions/BinaryBooleanFunctionExpression.h @@ -10,7 +10,7 @@ namespace storm { /*! * An enum type specifying the different operators applicable. */ - enum class OperatorType {And, Or}; + enum class OperatorType {And, Or, Implies, Iff}; /*! * Creates a binary boolean function expression with the given return type, operands and operator. diff --git a/src/storage/expressions/Expression.cpp b/src/storage/expressions/Expression.cpp index 0c641d3ec..b94d98db8 100644 --- a/src/storage/expressions/Expression.cpp +++ b/src/storage/expressions/Expression.cpp @@ -216,6 +216,16 @@ namespace storm { return Expression(std::shared_ptr(new BinaryNumericalFunctionExpression(lhs.getReturnType() == ExpressionReturnType::Int && rhs.getReturnType() == ExpressionReturnType::Int ? ExpressionReturnType::Int : ExpressionReturnType::Double, lhs.getBaseExpressionPointer(), rhs.getBaseExpressionPointer(), BinaryNumericalFunctionExpression::OperatorType::Max))); } + Expression Expression::implies(Expression const& other) const { + LOG_THROW(this->hasBooleanReturnType() && other.hasBooleanReturnType(), storm::exceptions::InvalidTypeException, "Operator '&&' requires boolean operands."); + return Expression(std::shared_ptr(new BinaryBooleanFunctionExpression(ExpressionReturnType::Bool, this->getBaseExpressionPointer(), other.getBaseExpressionPointer(), BinaryBooleanFunctionExpression::OperatorType::Implies))); + } + + Expression Expression::iff(Expression const& other) const { + LOG_THROW(this->hasBooleanReturnType() && other.hasBooleanReturnType(), storm::exceptions::InvalidTypeException, "Operator '&&' requires boolean operands."); + return Expression(std::shared_ptr(new BinaryBooleanFunctionExpression(ExpressionReturnType::Bool, this->getBaseExpressionPointer(), other.getBaseExpressionPointer(), BinaryBooleanFunctionExpression::OperatorType::Iff))); + } + Expression Expression::floor() const { LOG_THROW(this->hasNumericalReturnType(), storm::exceptions::InvalidTypeException, "Operator 'floor' requires numerical operand."); return Expression(std::shared_ptr(new UnaryNumericalFunctionExpression(ExpressionReturnType::Int, this->getBaseExpressionPointer(), UnaryNumericalFunctionExpression::OperatorType::Floor))); diff --git a/src/storage/expressions/Expression.h b/src/storage/expressions/Expression.h index 3002e4d35..875bcfbdc 100644 --- a/src/storage/expressions/Expression.h +++ b/src/storage/expressions/Expression.h @@ -53,6 +53,9 @@ namespace storm { Expression operator<(Expression const& other) const; Expression operator<=(Expression const& other) const; + Expression implies(Expression const& other) const; + Expression iff(Expression const& other) const; + Expression floor() const; Expression ceil() const; diff --git a/src/storage/prism/Module.cpp b/src/storage/prism/Module.cpp index 6da269889..5a90c4bda 100644 --- a/src/storage/prism/Module.cpp +++ b/src/storage/prism/Module.cpp @@ -122,7 +122,7 @@ namespace storm { } } - Module Module::restrictCommands(boost::container::flat_set const& indexSet) { + Module Module::restrictCommands(boost::container::flat_set const& indexSet) const { // First construct the new vector of commands. std::vector newCommands; for (auto const& command : commands) { diff --git a/src/storage/prism/Module.h b/src/storage/prism/Module.h index 595a48c5c..789cd0e09 100644 --- a/src/storage/prism/Module.h +++ b/src/storage/prism/Module.h @@ -147,7 +147,7 @@ namespace storm { * @param indexSet The set of indices for which to keep the commands. * @return The module resulting from erasing all commands whose indices are not in the given set. */ - Module restrictCommands(boost::container::flat_set const& indexSet); + Module restrictCommands(boost::container::flat_set const& indexSet) const; friend std::ostream& operator<<(std::ostream& stream, Module const& module); @@ -167,7 +167,7 @@ namespace storm { std::map integerVariables; // The commands associated with the module. - std::vector commands; + std::vector commands; // The set of actions present in this module. std::set actions; diff --git a/src/storage/prism/Program.cpp b/src/storage/prism/Program.cpp index 33c75c44f..a688a63dd 100644 --- a/src/storage/prism/Program.cpp +++ b/src/storage/prism/Program.cpp @@ -1,63 +1,18 @@ -/* - * Program.cpp - * - * Created on: 12.01.2013 - * Author: Christian Dehnert - */ - -#include -#include - -#include "Program.h" +#include "src/storage/prism/Program.h" +#include "src/exceptions/ExceptionMacros.h" #include "exceptions/InvalidArgumentException.h" #include "src/exceptions/OutOfRangeException.h" -#include "log4cplus/logger.h" -#include "log4cplus/loggingmacros.h" -extern log4cplus::Logger logger; - namespace storm { - namespace ir { - - Program::Program() : modelType(UNDEFINED), booleanUndefinedConstantExpressions(), integerUndefinedConstantExpressions(), doubleUndefinedConstantExpressions(), modules(), rewards(), actions(), actionsToModuleIndexMap(), variableToModuleIndexMap() { - // Nothing to do here. - } - - Program::Program(ModelType modelType, - std::map> const& booleanUndefinedConstantExpressions, - std::map> const& integerUndefinedConstantExpressions, - std::map> const& doubleUndefinedConstantExpressions, - std::vector const& globalBooleanVariables, - std::vector const& globalIntegerVariables, - std::map const& globalBooleanVariableToIndexMap, - std::map const& globalIntegerVariableToIndexMap, - std::vector const& modules, - std::map const& rewards, - std::map> const& labels) - : modelType(modelType), globalBooleanVariables(globalBooleanVariables), globalIntegerVariables(globalIntegerVariables), - globalBooleanVariableToIndexMap(globalBooleanVariableToIndexMap), globalIntegerVariableToIndexMap(globalIntegerVariableToIndexMap), - modules(modules), rewards(rewards), actionsToModuleIndexMap(), variableToModuleIndexMap() { - - // Perform a deep-copy of the maps. - for (auto const& booleanUndefinedConstant : booleanUndefinedConstantExpressions) { - this->booleanUndefinedConstantExpressions[booleanUndefinedConstant.first] = std::unique_ptr(new storm::ir::expressions::BooleanConstantExpression(*booleanUndefinedConstant.second)); - } - for (auto const& integerUndefinedConstant : integerUndefinedConstantExpressions) { - this->integerUndefinedConstantExpressions[integerUndefinedConstant.first] = std::unique_ptr(new storm::ir::expressions::IntegerConstantExpression(*integerUndefinedConstant.second)); - } - for (auto const& doubleUndefinedConstant : doubleUndefinedConstantExpressions) { - this->doubleUndefinedConstantExpressions[doubleUndefinedConstant.first] = std::unique_ptr(new storm::ir::expressions::DoubleConstantExpression(*doubleUndefinedConstant.second)); - } - for (auto const& label : labels) { - this->labels[label.first] = label.second->clone(); - } - + namespace prism { + Program::Program(ModelType modelType, std::set const& undefinedBooleanConstants, std::set const& undefinedIntegerConstants, std::set const& undefinedDoubleConstants, std::map const& globalBooleanVariables, std::map const& globalIntegerVariables, std::vector const& modules, std::map const& rewardModels, bool hasInitialStatesExpression, storm::expressions::Expression const& initialStatesExpression, std::map const& labels) : modelType(modelType), undefinedBooleanConstants(undefinedBooleanConstants), undefinedIntegerConstants(undefinedIntegerConstants), undefinedDoubleConstants(undefinedDoubleConstants), globalBooleanVariables(globalBooleanVariables), globalIntegerVariables(globalIntegerVariables), modules(modules), rewardModels(rewardModels), hasInitialStatesExpression(hasInitialStatesExpression), initialStatesExpression(initialStatesExpression), labels(labels), actions(), actionsToModuleIndexMap(), variableToModuleIndexMap() { // Now build the mapping from action names to module indices so that the lookup can later be performed quickly. - for (unsigned int moduleIndex = 0; moduleIndex < this->modules.size(); moduleIndex++) { - Module const& module = this->modules[moduleIndex]; + for (unsigned int moduleIndex = 0; moduleIndex < this->getNumberOfModules(); moduleIndex++) { + Module const& module = this->getModule(moduleIndex); for (auto const& action : module.getActions()) { - if (this->actionsToModuleIndexMap.count(action) == 0) { + auto const& actionModuleIndicesPair = this->actionsToModuleIndexMap.find(action); + if (actionModuleIndicesPair == this->actionsToModuleIndexMap.end()) { this->actionsToModuleIndexMap[action] = std::set(); } this->actionsToModuleIndexMap[action].insert(moduleIndex); @@ -65,235 +20,195 @@ namespace storm { } // 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; - } - } - } - - Program::Program(Program const& otherProgram) : modelType(otherProgram.modelType), globalBooleanVariables(otherProgram.globalBooleanVariables), - globalIntegerVariables(otherProgram.globalIntegerVariables), globalBooleanVariableToIndexMap(otherProgram.globalBooleanVariableToIndexMap), - globalIntegerVariableToIndexMap(otherProgram.globalIntegerVariableToIndexMap), modules(otherProgram.modules), rewards(otherProgram.rewards), - actions(otherProgram.actions), actionsToModuleIndexMap(), variableToModuleIndexMap() { - // Perform deep-copy of the maps. - for (auto const& booleanUndefinedConstant : otherProgram.booleanUndefinedConstantExpressions) { - this->booleanUndefinedConstantExpressions[booleanUndefinedConstant.first] = std::unique_ptr(new storm::ir::expressions::BooleanConstantExpression(*booleanUndefinedConstant.second)); - } - for (auto const& integerUndefinedConstant : otherProgram.integerUndefinedConstantExpressions) { - this->integerUndefinedConstantExpressions[integerUndefinedConstant.first] = std::unique_ptr(new storm::ir::expressions::IntegerConstantExpression(*integerUndefinedConstant.second)); - } - for (auto const& doubleUndefinedConstant : otherProgram.doubleUndefinedConstantExpressions) { - this->doubleUndefinedConstantExpressions[doubleUndefinedConstant.first] = std::unique_ptr(new storm::ir::expressions::DoubleConstantExpression(*doubleUndefinedConstant.second)); - } - for (auto const& label : otherProgram.labels) { - this->labels[label.first] = label.second->clone(); - } - } - - Program& Program::operator=(Program const& otherProgram) { - if (this != &otherProgram) { - this->modelType = otherProgram.modelType; - this->globalBooleanVariables = otherProgram.globalBooleanVariables; - this->globalIntegerVariables = otherProgram.globalIntegerVariables; - this->globalBooleanVariableToIndexMap = otherProgram.globalBooleanVariableToIndexMap; - this->globalIntegerVariableToIndexMap = otherProgram.globalIntegerVariableToIndexMap; - this->modules = otherProgram.modules; - this->rewards = otherProgram.rewards; - this->actions = otherProgram.actions; - this->actionsToModuleIndexMap = otherProgram.actionsToModuleIndexMap; - this->variableToModuleIndexMap = otherProgram.variableToModuleIndexMap; - - // Perform deep-copy of the maps. - for (auto const& booleanUndefinedConstant : otherProgram.booleanUndefinedConstantExpressions) { - this->booleanUndefinedConstantExpressions[booleanUndefinedConstant.first] = std::unique_ptr(new storm::ir::expressions::BooleanConstantExpression(*booleanUndefinedConstant.second)); - } - for (auto const& integerUndefinedConstant : otherProgram.integerUndefinedConstantExpressions) { - this->integerUndefinedConstantExpressions[integerUndefinedConstant.first] = std::unique_ptr(new storm::ir::expressions::IntegerConstantExpression(*integerUndefinedConstant.second)); + for (auto const& booleanVariable : module.getBooleanVariables()) { + this->variableToModuleIndexMap[booleanVariable.first] = moduleIndex; } - for (auto const& doubleUndefinedConstant : otherProgram.doubleUndefinedConstantExpressions) { - this->doubleUndefinedConstantExpressions[doubleUndefinedConstant.first] = std::unique_ptr(new storm::ir::expressions::DoubleConstantExpression(*doubleUndefinedConstant.second)); - } - for (auto const& label : otherProgram.labels) { - this->labels[label.first] = label.second->clone(); + for (auto const& integerVariable : module.getBooleanVariables()) { + this->variableToModuleIndexMap[integerVariable.first] = moduleIndex; } } - - return *this; } Program::ModelType Program::getModelType() const { return modelType; } - std::string Program::toString() const { - std::stringstream result; - switch (modelType) { - case UNDEFINED: result << "undefined"; break; - case DTMC: result << "dtmc"; break; - case CTMC: result << "ctmc"; break; - case MDP: result << "mdp"; break; - case CTMDP: result << "ctmdp"; break; - } - result << std::endl; - - for (auto const& element : booleanUndefinedConstantExpressions) { - result << "const bool " << element.second->toString() << ";" << std::endl; - } - for (auto const& element : integerUndefinedConstantExpressions) { - result << "const int " << element.second->toString() << ";" << std::endl; - } - for (auto const& element : doubleUndefinedConstantExpressions) { - result << "const double " << element.second->toString() << ";" << std::endl; - } - result << std::endl; - - for (auto const& element : globalBooleanVariables) { - result << "global " << element.toString() << std::endl; - } - for (auto const& element : globalIntegerVariables) { - result << "global " << element.toString() << std::endl; - } - result << std::endl; - - for (auto const& module : modules) { - result << module.toString() << std::endl; - } - - for (auto const& rewardModel : rewards) { - result << rewardModel.second.toString() << std::endl; - } - - for (auto const& label : labels) { - result << "label \"" << label.first << "\" = " << label.second->toString() <<";" << std::endl; - } - - return result.str(); + bool Program::hasUndefinedConstants() const { + return this->hasUndefinedBooleanConstants() || this->hasUndefinedIntegerConstants() || this->hasUndefinedDoubleConstants(); } - storm::ir::BooleanVariable const& Program::getGlobalBooleanVariable(uint_fast64_t index) const { - return this->globalBooleanVariables[index]; + bool Program::hasUndefinedBooleanConstants() const { + return !this->undefinedBooleanConstants.empty(); } - storm::ir::IntegerVariable const& Program::getGlobalIntegerVariable(uint_fast64_t index) const { - return this->globalIntegerVariables[index]; + bool Program::hasUndefinedIntegerConstants() const { + return !this->undefinedIntegerConstants.empty(); } - uint_fast64_t Program::getNumberOfModules() const { - return this->modules.size(); + bool Program::hasUndefinedDoubleConstants() const { + return !this->undefinedDoubleConstants.empty(); } - storm::ir::Module const& Program::getModule(uint_fast64_t index) const { - return this->modules[index]; + std::set const& Program::getUndefinedBooleanConstants() const { + return this->undefinedBooleanConstants; } - - std::set const& Program::getActions() const { - return this->actions; + + std::set const& Program::getUndefinedIntegerConstants() const { + return this->undefinedIntegerConstants; } - std::set const& Program::getModulesByAction(std::string const& action) const { - auto actionModuleSetPair = this->actionsToModuleIndexMap.find(action); - if (actionModuleSetPair == this->actionsToModuleIndexMap.end()) { - LOG4CPLUS_ERROR(logger, "Action name '" << action << "' does not exist."); - throw storm::exceptions::OutOfRangeException() << "Action name '" << action << "' does not exist."; - } - return actionModuleSetPair->second; + std::set const& Program::getUndefinedDoubleConstants() const { + return this->undefinedDoubleConstants; } - 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."; + std::map const& Program::getGlobalBooleanVariables() const { + return this->globalBooleanVariables; + } + + storm::prism::BooleanVariable const& Program::getGlobalBooleanVariable(std::string const& variableName) const { + auto const& nameVariablePair = this->getGlobalBooleanVariables().find(variableName); + LOG_THROW(nameVariablePair != this->getGlobalBooleanVariables().end(), storm::exceptions::OutOfRangeException, "Unknown boolean variable '" << variableName << "'."); + return nameVariablePair->second; } - uint_fast64_t Program::getNumberOfGlobalBooleanVariables() const { - return this->globalBooleanVariables.size(); + std::map const& Program::getGlobalIntegerVariables() const { + return this->globalIntegerVariables; + } + + storm::prism::IntegerVariable const& Program::getGlobalIntegerVariable(std::string const& variableName) const { + auto const& nameVariablePair = this->getGlobalIntegerVariables().find(variableName); + LOG_THROW(nameVariablePair != this->getGlobalIntegerVariables().end(), storm::exceptions::OutOfRangeException, "Unknown integer variable '" << variableName << "'."); + return nameVariablePair->second; } - uint_fast64_t Program::getNumberOfGlobalIntegerVariables() const { - return this->globalIntegerVariables.size(); + std::size_t Program::getNumberOfGlobalBooleanVariables() const { + return this->getGlobalBooleanVariables().size(); } - storm::ir::RewardModel const& Program::getRewardModel(std::string const& name) const { - auto nameRewardModelPair = this->rewards.find(name); - if (nameRewardModelPair == this->rewards.end()) { - LOG4CPLUS_ERROR(logger, "Reward model '" << name << "' does not exist."); - throw storm::exceptions::OutOfRangeException() << "Reward model '" << name << "' does not exist."; - } - return nameRewardModelPair->second; + std::size_t Program::getNumberOfGlobalIntegerVariables() const { + return this->getGlobalIntegerVariables().size(); } - std::map> const& Program::getLabels() const { - return this->labels; + std::size_t Program::getNumberOfModules() const { + return this->getModules().size(); } - bool Program::hasUndefinedBooleanConstant(std::string const& constantName) const { - return this->booleanUndefinedConstantExpressions.find(constantName) != this->booleanUndefinedConstantExpressions.end(); + storm::prism::Module const& Program::getModule(uint_fast64_t index) const { + return this->modules[index]; } - std::unique_ptr const& Program::getUndefinedBooleanConstantExpression(std::string const& constantName) const { - auto constantExpressionPair = this->booleanUndefinedConstantExpressions.find(constantName); - if (constantExpressionPair != this->booleanUndefinedConstantExpressions.end()) { - return constantExpressionPair->second; - } else { - throw storm::exceptions::InvalidArgumentException() << "Unknown undefined boolean constant " << constantName << "."; - } + std::vector const& Program::getModules() const { + return this->modules; } - bool Program::hasUndefinedIntegerConstant(std::string const& constantName) const { - return this->integerUndefinedConstantExpressions.find(constantName) != this->integerUndefinedConstantExpressions.end(); + bool Program::definesInitialStatesExpression() const { + return this->hasInitialStatesExpression; } - std::unique_ptr const& Program::getUndefinedIntegerConstantExpression(std::string const& constantName) const { - auto constantExpressionPair = this->integerUndefinedConstantExpressions.find(constantName); - if (constantExpressionPair != this->integerUndefinedConstantExpressions.end()) { - return constantExpressionPair->second; + storm::expressions::Expression Program::getInitialStatesExpression() const { + // If the program specifies the initial states explicitly, we simply return the expression. + if (this->definesInitialStatesExpression()) { + return this->initialStatesExpression; } else { - throw storm::exceptions::InvalidArgumentException() << "Unknown undefined integer constant " << constantName << "."; + // Otherwise, we need to assert that all variables are equal to their initial value. + storm::expressions::Expression result = storm::expressions::Expression::createTrue(); + + for (auto const& module : this->getModules()) { + for (auto const& booleanVariable : module.getBooleanVariables()) { + result = result && (storm::expressions::Expression::createBooleanVariable(booleanVariable.second.getName()).iff(booleanVariable.second.getInitialValueExpression())); + } + for (auto const& integerVariable : module.getIntegerVariables()) { + result = result && (storm::expressions::Expression::createIntegerVariable(integerVariable.second.getName()) == integerVariable.second.getInitialValueExpression()); + } + } + return result; } } - bool Program::hasUndefinedDoubleConstant(std::string const& constantName) const { - return this->doubleUndefinedConstantExpressions.find(constantName) != this->doubleUndefinedConstantExpressions.end(); + std::set const& Program::getActions() const { + return this->actions; } - std::unique_ptr const& Program::getUndefinedDoubleConstantExpression(std::string const& constantName) const { - auto constantExpressionPair = this->doubleUndefinedConstantExpressions.find(constantName); - if (constantExpressionPair != this->doubleUndefinedConstantExpressions.end()) { - return constantExpressionPair->second; - } else { - throw storm::exceptions::InvalidArgumentException() << "Unknown undefined double constant " << constantName << "."; - } + std::set const& Program::getModuleIndicesByAction(std::string const& action) const { + auto const& actionModuleSetPair = this->actionsToModuleIndexMap.find(action); + LOG_THROW(actionModuleSetPair != this->actionsToModuleIndexMap.end(), storm::exceptions::OutOfRangeException, "Action name '" << action << "' does not exist."); + return actionModuleSetPair->second; } - std::map> const& Program::getBooleanUndefinedConstantExpressionsMap() const { - return this->booleanUndefinedConstantExpressions; + uint_fast64_t Program::getModuleIndexByVariable(std::string const& variableName) const { + auto const& variableNameToModuleIndexPair = this->variableToModuleIndexMap.find(variableName); + LOG_THROW(variableNameToModuleIndexPair != this->variableToModuleIndexMap.end(), storm::exceptions::OutOfRangeException, "Variable '" << variableName << "' does not exist."); + return variableNameToModuleIndexPair->second; } - std::map> const& Program::getIntegerUndefinedConstantExpressionsMap() const { - return this->integerUndefinedConstantExpressions; + std::map const& Program::getRewardModels() const { + return this->rewardModels; } - std::map> const& Program::getDoubleUndefinedConstantExpressionsMap() const { - return this->doubleUndefinedConstantExpressions; + storm::prism::RewardModel const& Program::getRewardModel(std::string const& name) const { + auto const& nameRewardModelPair = this->getRewardModels().find(name); + LOG_THROW(nameRewardModelPair != this->getRewardModels().end(), storm::exceptions::OutOfRangeException, "Reward model '" << name << "' does not exist."); + return nameRewardModelPair->second; } - uint_fast64_t Program::getGlobalIndexOfBooleanVariable(std::string const& variableName) const { - return this->globalBooleanVariableToIndexMap.at(variableName); + std::map const& Program::getLabels() const { + return this->labels; } - uint_fast64_t Program::getGlobalIndexOfIntegerVariable(std::string const& variableName) const { - return this->globalIntegerVariableToIndexMap.at(variableName); + Program Program::restrictCommands(boost::container::flat_set const& indexSet) { + std::vector newModules; + newModules.reserve(this->getNumberOfModules()); + + for (auto const& module : this->getModules()) { + newModules.push_back(module.restrictCommands(indexSet)); + } + + return Program(this->getModelType(), this->getUndefinedBooleanConstants(), this->getUndefinedIntegerConstants(), this->getUndefinedDoubleConstants(), this->getGlobalBooleanVariables(), this->getGlobalIntegerVariables(), newModules, this->getRewardModels(), this->definesInitialStatesExpression(), this->getInitialStatesExpression(), this->getLabels()); } - void Program::restrictCommands(boost::container::flat_set const& indexSet) { - for (auto& module : modules) { - module.restrictCommands(indexSet); + std::ostream& operator<<(std::ostream& stream, Program const& program) { + switch (program.getModelType()) { + case Program::ModelType::UNDEFINED: stream << "undefined"; break; + case Program::ModelType::DTMC: stream << "dtmc"; break; + case Program::ModelType::CTMC: stream << "ctmc"; break; + case Program::ModelType::MDP: stream << "mdp"; break; + case Program::ModelType::CTMDP: stream << "ctmdp"; break; + case Program::ModelType::MA: stream << "ma"; break; + } + stream << std::endl; + + for (auto const& element : program.getUndefinedBooleanConstants()) { + stream << "const bool " << element << ";" << std::endl; + } + for (auto const& element : program.getUndefinedIntegerConstants()) { + stream << "const int " << element << ";" << std::endl; } + for (auto const& element : program.getUndefinedDoubleConstants()) { + stream << "const double " << element << ";" << std::endl; + } + stream << std::endl; + + for (auto const& element : program.getGlobalBooleanVariables()) { + stream << "global " << element.second << std::endl; + } + for (auto const& element : program.getGlobalIntegerVariables()) { + stream << "global " << element.second << std::endl; + } + stream << std::endl; + + for (auto const& module : program.getModules()) { + stream << module << std::endl; + } + + for (auto const& rewardModel : program.getRewardModels()) { + stream << rewardModel.second << std::endl; + } + + for (auto const& label : program.getLabels()) { + stream << "label \"" << label.first << "\" = " << label.second <<";" << std::endl; + } + + return stream; } } // namespace ir diff --git a/src/storage/prism/Program.h b/src/storage/prism/Program.h index 172d3f3b5..3f1b54e0d 100644 --- a/src/storage/prism/Program.h +++ b/src/storage/prism/Program.h @@ -17,7 +17,7 @@ namespace storm { /*! * An enum for the different model types. */ - enum ModelType {UNDEFINED, DTMC, CTMC, MDP, CTMDP, MA}; + enum class ModelType {UNDEFINED, DTMC, CTMC, MDP, CTMDP, MA}; /*! * Creates a program with the given model type, undefined constants, global variables, modules, reward @@ -32,9 +32,9 @@ namespace storm { * @param modules The modules of the program. * @param hasInitialStatesExpression A flag indicating whether the program specifies its initial states via * an explicit initial construct. - * @param initialStatesExpression If the model specifies an explicit initial construct, this expression - * defines its initial states. Otherwise it is irrelevant and may be set to an arbitrary (but valid) - * expression, e.g. false. + * @param initialStatesExpression If the model specifies an explicit initial construct, this + * expression defines its initial states. Otherwise it is irrelevant and may be set to an arbitrary (but + * valid) expression, e.g. false. * @param rewardModels The reward models of the program. * @param labels The labels defined for this program. */ @@ -116,7 +116,7 @@ namespace storm { * @param variableName The name of the global boolean variable to retrieve. * @return The global boolean variable with the given name. */ - storm::ir::BooleanVariable const& getGlobalBooleanVariable(std::string const& variableName) const; + storm::prism::BooleanVariable const& getGlobalBooleanVariable(std::string const& variableName) const; /*! * Retrieves the global integer variables of the program. @@ -131,7 +131,7 @@ namespace storm { * @param variableName The name of the global integer variable to retrieve. * @return The global integer variable with the given name. */ - storm::ir::IntegerVariable const& getGlobalIntegerVariable(std::string const& variableName) const; + storm::prism::IntegerVariable const& getGlobalIntegerVariable(std::string const& variableName) const; /*! * Retrieves the number of global boolean variables of the program. @@ -162,6 +162,27 @@ namespace storm { */ storm::prism::Module const& getModule(uint_fast64_t index) const; + /*! + * Retrieves all modules of the program. + * + * @return All modules of the program. + */ + std::vector const& getModules() const; + + /*! + * Retrieves whether the program explicitly specifies an expression characterizing the initial states. + * + * @return True iff the program specifies an expression defining the initial states. + */ + bool definesInitialStatesExpression() const; + + /*! + * Retrieves an expression characterizing the initial states of the program. + * + * @return An expression characterizing the initial states. + */ + storm::expressions::Expression getInitialStatesExpression() const; + /*! * Retrieves the set of actions present in the program. * @@ -206,7 +227,7 @@ namespace storm { * * @return A set of labels that are defined in the program. */ - std::map const& getLabels() const; + std::map const& getLabels() const; /*! * Creates a new program that drops all commands whose indices are not in the given set. diff --git a/src/storage/prism/Update.cpp b/src/storage/prism/Update.cpp index 7a4bb64ad..f08627479 100644 --- a/src/storage/prism/Update.cpp +++ b/src/storage/prism/Update.cpp @@ -81,7 +81,7 @@ namespace storm { } i = 0; for (auto const& assignment : update.getIntegerAssignments()) { - result << assignment.second; + stream << assignment.second; if (i < update.getIntegerAssignments().size() - 1) { stream << " & "; }