From d9345b19e97856be286bcf8bf76f244f740cbf8a Mon Sep 17 00:00:00 2001 From: dehnert Date: Tue, 15 Apr 2014 15:55:19 +0200 Subject: [PATCH] Further work on adapting explicit model generator to new PRISM classes. Former-commit-id: 01cefceb52e3bc80d7b025f77bed154f12e29069 --- src/adapters/ExplicitModelAdapter.h | 78 +++++++++++++++++++++-- src/parser/PrismParser.cpp | 12 ++-- src/storage/expressions/SimpleValuation.h | 1 + src/storage/prism/Program.cpp | 16 ++++- src/storage/prism/Program.h | 19 ++++++ src/utility/IRUtility.h | 2 +- 6 files changed, 114 insertions(+), 14 deletions(-) diff --git a/src/adapters/ExplicitModelAdapter.h b/src/adapters/ExplicitModelAdapter.h index b06c24b21..be293ebf6 100644 --- a/src/adapters/ExplicitModelAdapter.h +++ b/src/adapters/ExplicitModelAdapter.h @@ -15,6 +15,7 @@ #include #include #include +#include #include "src/storage/prism/Program.h" #include "src/storage/expressions/SimpleValuation.h" @@ -72,6 +73,62 @@ namespace storm { std::vector> choiceLabeling; }; + static std::map parseConstantDefinitionString(storm::prism::Program const& program, std::string const& constantDefinitionString) { + std::map constantDefinitions; + std::set definedConstants; + + if (!constantDefinitionString.empty()) { + // 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; + boost::split(definitions, constantDefinitionString, boost::is_any_of(",")); + for (auto& definition : definitions) { + boost::trim(definition); + + // Check whether the token could be a legal constant definition. + uint_fast64_t positionOfAssignmentOperator = definition.find('='); + 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); + std::string value = definition.substr(positionOfAssignmentOperator + 1); + boost::trim(value); + + // Check whether the constant is a legal undefined constant of the program and if so, of what type it is. + if (program.hasConstant(constantName)) { + // Get the actual constant and check whether it's in fact undefined. + auto const& constant = program.getConstant(constantName); + LOG_THROW(!constant.isDefined(), storm::exceptions::InvalidArgumentException, "Illegally trying to define already defined constant '" << constantName <<"'."); + LOG_THROW(definedConstants.find(constantName) == definedConstants.end(), storm::exceptions::InvalidArgumentException, "Illegally trying to define constant '" << constantName <<"' twice."); + definedConstants.insert(constantName); + + if (constant.getConstantType() == storm::expressions::ExpressionReturnType::Bool) { + if (value == "true") { + constantDefinitions[constantName] = storm::expressions::Expression::createTrue(); + } else if (value == "false") { + constantDefinitions[constantName] = storm::expressions::Expression::createFalse(); + } else { + throw storm::exceptions::InvalidArgumentException() << "Illegal value for boolean constant: " << value << "."; + } + } else if (constant.getConstantType() == storm::expressions::ExpressionReturnType::Int) { + int_fast64_t integerValue = std::stoi(value); + constantDefinitions[constantName] = storm::expressions::Expression::createIntegerLiteral(integerValue); + } else if (constant.getConstantType() == storm::expressions::ExpressionReturnType::Double) { + double doubleValue = std::stod(value); + constantDefinitions[constantName] = storm::expressions::Expression::createDoubleLiteral(doubleValue); + } + } else { + throw storm::exceptions::InvalidArgumentException() << "Illegal constant definition string: unknown undefined constant " << constantName << "."; + } + } + } + + return constantDefinitions; + } + /*! * Convert the program given at construction time to an abstract model. The type of the model is the one * specified in the program. The given reward model name selects the rewards that the model will contain. @@ -86,7 +143,11 @@ namespace storm { */ static std::unique_ptr> translateProgram(storm::prism::Program program, std::string const& constantDefinitionString = "", std::string const& rewardModelName = "") { // Start by defining the undefined constants in the model. + // First, we need to parse the constant definition string. + std::map constantDefinitions = parseConstantDefinitionString(program, constantDefinitionString); + storm::prism::Program definedProgram = program.defineUndefinedConstants(constantDefinitions); + LOG_THROW(!definedProgram.hasUndefinedConstants(), storm::exceptions::InvalidArgumentException, "Program still contains undefined constants."); ModelComponents modelComponents = buildModelComponents(definedProgram, rewardModelName); @@ -118,13 +179,12 @@ namespace storm { * Applies an update to the given state and returns the resulting new state object. This methods does not * modify the given state but returns a new one. * - * @param variableInformation A structure with information about the variables in the program. * @params state The state to which to apply the update. * @params update The update to apply. * @return The resulting state. */ - static StateType* applyUpdate(VariableInformation const& variableInformation, StateType const* state, storm::prism::Update const& update) { - return applyUpdate(variableInformation, state, state, update); + static StateType* applyUpdate(StateType const* state, storm::prism::Update const& update) { + return applyUpdate(state, state, update); } /*! @@ -132,14 +192,22 @@ namespace storm { * over the variable values of the given base state. This methods does not modify the given state but * returns a new one. * - * @param variableInformation A structure with information about the variables in the program. * @param state The state to which to apply the update. * @param baseState The state used for evaluating the update. * @param update The update to apply. * @return The resulting state. */ - static StateType* applyUpdate(VariableInformation const& variableInformation, StateType const* state, StateType const* baseState, storm::prism::Update const& update) { + static StateType* applyUpdate(StateType const* state, StateType const* baseState, storm::prism::Update const& update) { StateType* newState = new StateType(*state); + for (auto const& assignment : update.getAssignments()) { + switch (assignment.getExpression().getReturnType()) { + case storm::expressions::ExpressionReturnType::Bool: newState->setBooleanValue(assignment.getVariableName(), assignment.getExpression().evaluateAsBool(*baseState)); break; + case storm::expressions::ExpressionReturnType::Int: + int_fast64_t newValue = assignment.getExpression().evaluateAsInt(*baseState)); + newState->setIntegerValue(assignment.getVariableName(), assignment.getExpression().evaluateAsInt(*baseState)); break; + default: LOG_ASSERT(false, "Invalid type of assignment."); + } + } for (auto variableAssignmentPair : update.getBooleanAssignments()) { setValue(newState, variableInformation.booleanVariableToIndexMap.at(variableAssignmentPair.first), variableAssignmentPair.second.getExpression()->getValueAsBool(baseState)); } diff --git a/src/parser/PrismParser.cpp b/src/parser/PrismParser.cpp index 71843541b..c1a068d5c 100644 --- a/src/parser/PrismParser.cpp +++ b/src/parser/PrismParser.cpp @@ -464,32 +464,32 @@ namespace storm { storm::prism::Constant PrismParser::createUndefinedBooleanConstant(std::string const& newConstant) const { this->identifiers_.add(newConstant, storm::expressions::Expression::createBooleanConstant(newConstant)); - return storm::prism::Constant(storm::prism::Constant::ConstantType::Bool, newConstant, this->getFilename()); + return storm::prism::Constant(storm::expressions::ExpressionReturnType::Bool, newConstant, this->getFilename()); } storm::prism::Constant PrismParser::createUndefinedIntegerConstant(std::string const& newConstant) const { this->identifiers_.add(newConstant, storm::expressions::Expression::createIntegerConstant(newConstant)); - return storm::prism::Constant(storm::prism::Constant::ConstantType::Integer, newConstant, this->getFilename()); + return storm::prism::Constant(storm::expressions::ExpressionReturnType::Int, newConstant, this->getFilename()); } storm::prism::Constant PrismParser::createUndefinedDoubleConstant(std::string const& newConstant) const { this->identifiers_.add(newConstant, storm::expressions::Expression::createDoubleConstant(newConstant)); - return storm::prism::Constant(storm::prism::Constant::ConstantType::Double, newConstant, this->getFilename()); + return storm::prism::Constant(storm::expressions::ExpressionReturnType::Double, newConstant, this->getFilename()); } storm::prism::Constant PrismParser::createDefinedBooleanConstant(std::string const& newConstant, storm::expressions::Expression expression) const { this->identifiers_.add(newConstant, storm::expressions::Expression::createBooleanConstant(newConstant)); - return storm::prism::Constant(storm::prism::Constant::ConstantType::Bool, newConstant, expression, this->getFilename()); + return storm::prism::Constant(storm::expressions::ExpressionReturnType::Bool, newConstant, expression, this->getFilename()); } storm::prism::Constant PrismParser::createDefinedIntegerConstant(std::string const& newConstant, storm::expressions::Expression expression) const { this->identifiers_.add(newConstant, storm::expressions::Expression::createIntegerConstant(newConstant)); - return storm::prism::Constant(storm::prism::Constant::ConstantType::Integer, newConstant, expression, this->getFilename()); + return storm::prism::Constant(storm::expressions::ExpressionReturnType::Int, newConstant, expression, this->getFilename()); } storm::prism::Constant PrismParser::createDefinedDoubleConstant(std::string const& newConstant, storm::expressions::Expression expression) const { this->identifiers_.add(newConstant, storm::expressions::Expression::createDoubleConstant(newConstant)); - return storm::prism::Constant(storm::prism::Constant::ConstantType::Double, newConstant, expression, this->getFilename()); + return storm::prism::Constant(storm::expressions::ExpressionReturnType::Double, newConstant, expression, this->getFilename()); } storm::prism::Formula PrismParser::createFormula(std::string const& formulaName, storm::expressions::Expression expression) const { diff --git a/src/storage/expressions/SimpleValuation.h b/src/storage/expressions/SimpleValuation.h index 0cb3a00f6..0c2231a63 100644 --- a/src/storage/expressions/SimpleValuation.h +++ b/src/storage/expressions/SimpleValuation.h @@ -42,6 +42,7 @@ namespace storm { SimpleValuation(SimpleValuation&&) = default; SimpleValuation& operator=(SimpleValuation const&) = default; SimpleValuation& operator=(SimpleValuation&&) = default; + virtual ~SimpleValuation() = default; /*! * Compares two simple valuations wrt. equality. diff --git a/src/storage/prism/Program.cpp b/src/storage/prism/Program.cpp index 564665fc0..c635cbf63 100644 --- a/src/storage/prism/Program.cpp +++ b/src/storage/prism/Program.cpp @@ -5,7 +5,7 @@ namespace storm { namespace prism { - Program::Program(ModelType modelType, std::vector const& constants, std::vector const& globalBooleanVariables, std::vector const& globalIntegerVariables, std::vector const& formulas, std::vector const& modules, std::vector const& rewardModels, bool hasInitialStatesExpression, storm::expressions::Expression const& initialStatesExpression, std::vector