diff --git a/src/adapters/ExplicitModelAdapter.cpp b/src/adapters/ExplicitModelAdapter.cpp index 0d9eb7cf7..eedf77160 100644 --- a/src/adapters/ExplicitModelAdapter.cpp +++ b/src/adapters/ExplicitModelAdapter.cpp @@ -39,7 +39,7 @@ namespace storm { this->clearInternalState(); } - std::shared_ptr> ExplicitModelAdapter::getModel(std::string const& constantDefinitionString, std::string const& rewardModelName) { + void ExplicitModelAdapter::defineUndefinedConstants(std::string const& constantDefinitionString) { // Parse the string that defines the undefined constants of the model and make sure that it contains exactly // one value for each undefined constant of the model. std::vector definitions; @@ -52,7 +52,7 @@ namespace storm { if (positionOfAssignmentOperator == std::string::npos) { throw storm::exceptions::InvalidArgumentException() << "Illegal constant definition string: syntax error."; } - + // Now extract the variable name and the value from the string. std::string constantName = definition.substr(0, positionOfAssignmentOperator); boost::trim(constantName); @@ -86,12 +86,28 @@ namespace storm { } catch (std::out_of_range const& e) { throw storm::exceptions::InvalidArgumentException() << "Illegal value of double constant: " << value << " (value too big)."; } - + } else { throw storm::exceptions::InvalidArgumentException() << "Illegal constant definition string: unknown undefined constant " << constantName << "."; } - } + } + + void ExplicitModelAdapter::undefineUndefinedConstants() { + for (auto nameExpressionPair : program.getBooleanUndefinedConstantExpressionsMap()) { + nameExpressionPair.second->undefine(); + } + for (auto nameExpressionPair : program.getIntegerUndefinedConstantExpressionsMap()) { + nameExpressionPair.second->undefine(); + } + for (auto nameExpressionPair : program.getDoubleUndefinedConstantExpressionsMap()) { + nameExpressionPair.second->undefine(); + } + } + + std::shared_ptr> ExplicitModelAdapter::getModel(std::string const& constantDefinitionString, std::string const& rewardModelName) { + // Start by defining the remaining constants in the model. + this->defineUndefinedConstants(constantDefinitionString); // Initialize reward model. this->rewardModel = nullptr; @@ -111,31 +127,32 @@ namespace storm { stateRewards.reset(this->getStateRewards(this->rewardModel->getStateRewards())); } + std::shared_ptr> result; // Build and return actual model. switch (this->program.getModelType()) { case storm::ir::Program::DTMC: { storm::storage::SparseMatrix matrix = this->buildDeterministicMatrix(); - return std::shared_ptr>(new storm::models::Dtmc(matrix, stateLabeling, stateRewards, this->transitionRewards, this->choiceLabeling)); + result = std::shared_ptr>(new storm::models::Dtmc(matrix, stateLabeling, stateRewards, this->transitionRewards, this->choiceLabeling)); break; } case storm::ir::Program::CTMC: { storm::storage::SparseMatrix matrix = this->buildDeterministicMatrix(); - return std::shared_ptr>(new storm::models::Ctmc(matrix, stateLabeling, stateRewards, this->transitionRewards, this->choiceLabeling)); + result = std::shared_ptr>(new storm::models::Ctmc(matrix, stateLabeling, stateRewards, this->transitionRewards, this->choiceLabeling)); break; } case storm::ir::Program::MDP: { storm::storage::SparseMatrix matrix = this->buildNondeterministicMatrix(); - return std::shared_ptr>(new storm::models::Mdp(matrix, stateLabeling, this->choiceIndices, stateRewards, this->transitionRewards, this->choiceLabeling)); + result = std::shared_ptr>(new storm::models::Mdp(matrix, stateLabeling, this->choiceIndices, stateRewards, this->transitionRewards, this->choiceLabeling)); break; } case storm::ir::Program::CTMDP: { storm::storage::SparseMatrix matrix = this->buildNondeterministicMatrix(); - return std::shared_ptr>(new storm::models::Ctmdp(matrix, stateLabeling, this->choiceIndices, stateRewards, this->transitionRewards, this->choiceLabeling)); + result = std::shared_ptr>(new storm::models::Ctmdp(matrix, stateLabeling, this->choiceIndices, stateRewards, this->transitionRewards, this->choiceLabeling)); break; } default: @@ -143,6 +160,11 @@ namespace storm { throw storm::exceptions::WrongFormatException() << "Error while creating model from probabilistic program: cannot handle this model type."; break; } + + // Undefine the constants so that the program can be used again somewhere else. + undefineUndefinedConstants(); + + return result; } void ExplicitModelAdapter::setValue(StateType* state, uint_fast64_t index, bool value) { @@ -418,6 +440,8 @@ namespace storm { std::unordered_map* newTargetStates = new std::unordered_map(); (*currentTargetStates)[new StateType(*currentState)] = 1.0; + // FIXME: This does not check whether a global variable is written multiple times. While the + // behaviour for this is undefined anyway, a warning should be issued in that case. double probabilitySum = 0; for (uint_fast64_t i = 0; i < iteratorList.size(); ++i) { storm::ir::Command const& command = *iteratorList[i]; diff --git a/src/adapters/ExplicitModelAdapter.h b/src/adapters/ExplicitModelAdapter.h index a691bb05a..028b93b8a 100644 --- a/src/adapters/ExplicitModelAdapter.h +++ b/src/adapters/ExplicitModelAdapter.h @@ -239,6 +239,18 @@ namespace storm { */ void clearInternalState(); + /*! + * Defines the undefined constants of the program using the given string. + * + * @param constantDefinitionString A comma-separated list of constant definitions. + */ + void defineUndefinedConstants(std::string const& constantDefinitionString); + + /*! + * Sets all values of program constants to undefined again. + */ + void undefineUndefinedConstants(); + // Program that is to be converted. storm::ir::Program program; diff --git a/src/ir/Program.cpp b/src/ir/Program.cpp index 14a6af59a..d997e8cbd 100644 --- a/src/ir/Program.cpp +++ b/src/ir/Program.cpp @@ -203,5 +203,17 @@ namespace storm { } } + std::map> const& Program::getBooleanUndefinedConstantExpressionsMap() const { + return this->booleanUndefinedConstantExpressions; + } + + std::map> const& Program::getIntegerUndefinedConstantExpressionsMap() const { + return this->integerUndefinedConstantExpressions; + } + + std::map> const& Program::getDoubleUndefinedConstantExpressionsMap() const { + return this->doubleUndefinedConstantExpressions; + } + } // namespace ir } // namepsace storm diff --git a/src/ir/Program.h b/src/ir/Program.h index ae92db0de..6e31feaa6 100644 --- a/src/ir/Program.h +++ b/src/ir/Program.h @@ -212,6 +212,27 @@ namespace storm { */ std::shared_ptr getUndefinedDoubleConstantExpression(std::string const& constantName) const; + /*! + * Retrieves the mapping of undefined boolean constant names to their expression objects. + * + * @return The mapping of undefined boolean constant names to their expression objects. + */ + std::map> const& getBooleanUndefinedConstantExpressionsMap() const; + + /*! + * Retrieves the mapping of undefined integer constant names to their expression objects. + * + * @return The mapping of undefined integer constant names to their expression objects. + */ + std::map> const& getIntegerUndefinedConstantExpressionsMap() const; + + /*! + * Retrieves the mapping of undefined double constant names to their expression objects. + * + * @return The mapping of undefined double constant names to their expression objects. + */ + std::map> const& getDoubleUndefinedConstantExpressionsMap() const; + private: // The type of the model. ModelType modelType; diff --git a/src/ir/expressions/ConstantExpression.h b/src/ir/expressions/ConstantExpression.h index e23cc454e..dd0db446c 100644 --- a/src/ir/expressions/ConstantExpression.h +++ b/src/ir/expressions/ConstantExpression.h @@ -108,6 +108,14 @@ namespace storm { this->valueStructPointer->value = value; } + /*! + * Undefines the value that was previously set for this constant (if any). + */ + void undefine() { + this->valueStructPointer->defined = false; + this->valueStructPointer->value = T(); + } + private: // The name of the constant. std::string constantName;