From 0a3ff157f758c70508f3007ede640c2747653fa7 Mon Sep 17 00:00:00 2001 From: dehnert Date: Sun, 8 Jan 2017 12:08:02 +0100 Subject: [PATCH] constants defaulting to type int and allowing model type everywhere (on top level) of PRISM program --- src/storm/parser/FormulaParserGrammar.cpp | 6 +++--- src/storm/parser/PrismParser.cpp | 23 +++++++++++++++++------ src/storm/parser/PrismParser.h | 4 ++-- 3 files changed, 22 insertions(+), 11 deletions(-) diff --git a/src/storm/parser/FormulaParserGrammar.cpp b/src/storm/parser/FormulaParserGrammar.cpp index 825b36412..321878464 100644 --- a/src/storm/parser/FormulaParserGrammar.cpp +++ b/src/storm/parser/FormulaParserGrammar.cpp @@ -4,7 +4,7 @@ namespace storm { namespace parser { - FormulaParserGrammar::FormulaParserGrammar(std::shared_ptr const& manager) : FormulaParserGrammar::base_type(start), constManager(manager), expressionParser(*manager, keywords_, true, true) { + FormulaParserGrammar::FormulaParserGrammar(std::shared_ptr const& manager) : FormulaParserGrammar::base_type(start), constManager(manager), manager(nullptr), expressionParser(*manager, keywords_, true, true) { initialize(); } @@ -14,7 +14,7 @@ namespace storm { void FormulaParserGrammar::initialize() { // Register all variables so we can parse them in the expressions. - for (auto variableTypePair : *manager) { + for (auto variableTypePair : *constManager) { identifiers_.add(variableTypePair.first.getName(), variableTypePair.first); } // Set the identifier mapping to actually generate expressions. @@ -270,7 +270,7 @@ namespace storm { storm::logic::OperatorInformation FormulaParserGrammar::createOperatorInformation(boost::optional const& optimizationDirection, boost::optional const& comparisonType, boost::optional const& threshold) const { if (comparisonType && threshold) { - storm::expressions::ExpressionEvaluator evaluator(*manager); + storm::expressions::ExpressionEvaluator evaluator(*constManager); return storm::logic::OperatorInformation(optimizationDirection, storm::logic::Bound(comparisonType.get(), evaluator.asRational(threshold.get()))); } else { return storm::logic::OperatorInformation(optimizationDirection, boost::none); diff --git a/src/storm/parser/PrismParser.cpp b/src/storm/parser/PrismParser.cpp index 73b42fd45..b6241731a 100644 --- a/src/storm/parser/PrismParser.cpp +++ b/src/storm/parser/PrismParser.cpp @@ -87,13 +87,13 @@ namespace storm { undefinedBooleanConstantDefinition = ((qi::lit("const") >> qi::lit("bool")) > identifier > qi::lit(";"))[qi::_val = phoenix::bind(&PrismParser::createUndefinedBooleanConstant, phoenix::ref(*this), qi::_1)]; undefinedBooleanConstantDefinition.name("undefined boolean constant declaration"); - undefinedIntegerConstantDefinition = ((qi::lit("const") >> qi::lit("int")) > identifier > qi::lit(";"))[qi::_val = phoenix::bind(&PrismParser::createUndefinedIntegerConstant, phoenix::ref(*this), qi::_1)]; + undefinedIntegerConstantDefinition = ((qi::lit("const") >> -qi::lit("int")) >> identifier >> qi::lit(";"))[qi::_val = phoenix::bind(&PrismParser::createUndefinedIntegerConstant, phoenix::ref(*this), qi::_1)]; undefinedIntegerConstantDefinition.name("undefined integer constant declaration"); undefinedDoubleConstantDefinition = ((qi::lit("const") >> qi::lit("double")) > identifier > qi::lit(";"))[qi::_val = phoenix::bind(&PrismParser::createUndefinedDoubleConstant, phoenix::ref(*this), qi::_1)]; undefinedDoubleConstantDefinition.name("undefined double constant definition"); - undefinedConstantDefinition = (undefinedBooleanConstantDefinition | undefinedIntegerConstantDefinition | undefinedDoubleConstantDefinition); + undefinedConstantDefinition = (undefinedBooleanConstantDefinition | undefinedDoubleConstantDefinition | undefinedIntegerConstantDefinition); undefinedConstantDefinition.name("undefined constant definition"); definedBooleanConstantDefinition = ((qi::lit("const") >> qi::lit("bool") >> identifier >> qi::lit("=")) > expression_ > qi::lit(";"))[qi::_val = phoenix::bind(&PrismParser::createDefinedBooleanConstant, phoenix::ref(*this), qi::_1, qi::_2)]; @@ -105,7 +105,7 @@ namespace storm { definedDoubleConstantDefinition = ((qi::lit("const") >> qi::lit("double") >> identifier >> qi::lit("=")) > expression_ > qi::lit(";"))[qi::_val = phoenix::bind(&PrismParser::createDefinedDoubleConstant, phoenix::ref(*this), qi::_1, qi::_2)]; definedDoubleConstantDefinition.name("defined double constant declaration"); - definedConstantDefinition %= (definedBooleanConstantDefinition | definedIntegerConstantDefinition | definedDoubleConstantDefinition); + definedConstantDefinition %= (definedBooleanConstantDefinition | definedDoubleConstantDefinition | definedIntegerConstantDefinition); definedConstantDefinition.name("defined constant definition"); formulaDefinition = (qi::lit("formula") > identifier > qi::lit("=") > expression_ > qi::lit(";"))[qi::_val = phoenix::bind(&PrismParser::createFormula, phoenix::ref(*this), qi::_1, qi::_2)]; @@ -217,8 +217,8 @@ namespace storm { moduleDefinitionList.name("module list"); start = (qi::eps[phoenix::bind(&PrismParser::removeInitialConstruct, phoenix::ref(*this), qi::_a)] - > modelTypeDefinition[phoenix::bind(&GlobalProgramInformation::modelType, qi::_a) = qi::_1] - > *(definedConstantDefinition[phoenix::push_back(phoenix::bind(&GlobalProgramInformation::constants, qi::_a), qi::_1)] + > *(modelTypeDefinition[phoenix::bind(&PrismParser::setModelType, phoenix::ref(*this), qi::_a, qi::_1)] + | definedConstantDefinition[phoenix::push_back(phoenix::bind(&GlobalProgramInformation::constants, qi::_a), qi::_1)] | undefinedConstantDefinition[phoenix::push_back(phoenix::bind(&GlobalProgramInformation::constants, qi::_a), qi::_1)] | formulaDefinition[phoenix::push_back(phoenix::bind(&GlobalProgramInformation::formulas, qi::_a), qi::_1)] | globalVariableDefinition(qi::_a) @@ -299,6 +299,11 @@ namespace storm { return true; } + void PrismParser::setModelType(GlobalProgramInformation& globalProgramInformation, storm::prism::Program::ModelType const& modelType) { + STORM_LOG_THROW(globalProgramInformation.modelType == storm::prism::Program::ModelType::UNDEFINED, storm::exceptions::WrongFormatException, "Parsing error in " << this->getFilename() << ", line " << get_line(qi::_3) << ": Program must not set model type multiple times."); + globalProgramInformation.modelType = modelType; + } + std::shared_ptr PrismParser::createModuleComposition(std::string const& moduleName) const { return std::make_shared(moduleName); } @@ -648,7 +653,13 @@ namespace storm { } storm::prism::Program PrismParser::createProgram(GlobalProgramInformation const& globalProgramInformation) const { - return storm::prism::Program(manager, globalProgramInformation.modelType, globalProgramInformation.constants, globalProgramInformation.globalBooleanVariables, globalProgramInformation.globalIntegerVariables, globalProgramInformation.formulas, globalProgramInformation.modules, globalProgramInformation.actionIndices, globalProgramInformation.rewardModels, globalProgramInformation.labels, secondRun && !globalProgramInformation.hasInitialConstruct ? boost::none : boost::make_optional(globalProgramInformation.initialConstruct), globalProgramInformation.systemCompositionConstruct, this->getFilename(), 1, this->secondRun); + storm::prism::Program::ModelType finalModelType = globalProgramInformation.modelType; + if (globalProgramInformation.modelType == storm::prism::Program::ModelType::UNDEFINED) { + STORM_LOG_WARN("Program does not specify model type. Implicitly assuming 'mdp'."); + finalModelType = storm::prism::Program::ModelType::MDP; + } + + return storm::prism::Program(manager, finalModelType, globalProgramInformation.constants, globalProgramInformation.globalBooleanVariables, globalProgramInformation.globalIntegerVariables, globalProgramInformation.formulas, globalProgramInformation.modules, globalProgramInformation.actionIndices, globalProgramInformation.rewardModels, globalProgramInformation.labels, secondRun && !globalProgramInformation.hasInitialConstruct ? boost::none : boost::make_optional(globalProgramInformation.initialConstruct), globalProgramInformation.systemCompositionConstruct, this->getFilename(), 1, this->secondRun); } void PrismParser::removeInitialConstruct(GlobalProgramInformation& globalProgramInformation) const { diff --git a/src/storm/parser/PrismParser.h b/src/storm/parser/PrismParser.h index 64aaa7dba..f285c5cc9 100644 --- a/src/storm/parser/PrismParser.h +++ b/src/storm/parser/PrismParser.h @@ -25,7 +25,7 @@ namespace storm { class GlobalProgramInformation { public: // Default construct the header information. - GlobalProgramInformation() : modelType(), constants(), formulas(), globalBooleanVariables(), globalIntegerVariables(), moduleToIndexMap(), actionIndices(), modules(), rewardModels(), labels(), hasInitialConstruct(false), initialConstruct(), systemCompositionConstruct(boost::none), currentCommandIndex(0), currentUpdateIndex(0) { + GlobalProgramInformation() : modelType(storm::prism::Program::ModelType::UNDEFINED), constants(), formulas(), globalBooleanVariables(), globalIntegerVariables(), moduleToIndexMap(), actionIndices(), modules(), rewardModels(), labels(), hasInitialConstruct(false), initialConstruct(), systemCompositionConstruct(boost::none), currentCommandIndex(0), currentUpdateIndex(0) { // Map the empty action to index 0. actionIndices.emplace("", 0); } @@ -245,7 +245,7 @@ namespace storm { bool isValidIdentifier(std::string const& identifier); bool addInitialStatesConstruct(storm::expressions::Expression const& initialStatesExpression, GlobalProgramInformation& globalProgramInformation); bool addSystemCompositionConstruct(std::shared_ptr const& composition, GlobalProgramInformation& globalProgramInformation); - + void setModelType(GlobalProgramInformation& globalProgramInformation, storm::prism::Program::ModelType const& modelType); std::shared_ptr createModuleComposition(std::string const& moduleName) const; std::shared_ptr createRenamingComposition(std::shared_ptr const& subcomposition, std::map const& renaming) const;