From 290ede7404a670ebc35eb5bd0082f9f1fbbf7edc Mon Sep 17 00:00:00 2001 From: Sebastian Junges Date: Fri, 24 Jan 2020 18:27:49 +0100 Subject: [PATCH] extended the parser to handle observable expressions --- src/storm-parsers/parser/PrismParser.cpp | 30 +++++++++++++++++++++--- src/storm-parsers/parser/PrismParser.h | 9 +++++++ 2 files changed, 36 insertions(+), 3 deletions(-) diff --git a/src/storm-parsers/parser/PrismParser.cpp b/src/storm-parsers/parser/PrismParser.cpp index 70ac58af2..ea37addd4 100644 --- a/src/storm-parsers/parser/PrismParser.cpp +++ b/src/storm-parsers/parser/PrismParser.cpp @@ -238,9 +238,15 @@ namespace storm { freshLabelName = (identifier[qi::_val = qi::_1])[qi::_pass = phoenix::bind(&PrismParser::isFreshLabelName, phoenix::ref(*this), qi::_1)]; freshLabelName.name("fresh label name"); - + labelDefinition = (qi::lit("label") > -qi::lit("\"") > freshLabelName > -qi::lit("\"") > qi::lit("=") > boolExpression > qi::lit(";"))[qi::_val = phoenix::bind(&PrismParser::createLabel, phoenix::ref(*this), qi::_1, qi::_2)]; labelDefinition.name("label definition"); + + freshObservationLabelName = (identifier[qi::_val = qi::_1])[qi::_pass = phoenix::bind(&PrismParser::isFreshObservationLabelName, phoenix::ref(*this), qi::_1)]; + freshObservationLabelName.name("fresh observable name"); + + observableDefinition = (qi::lit("observable") > -qi::lit("\"") > freshObservationLabelName > -qi::lit("\"") > qi::lit("=") > (intExpression | boolExpression) > qi::lit(";"))[qi::_val = phoenix::bind(&PrismParser::createObservationLabel, phoenix::ref(*this), qi::_1, qi::_2)]; + observableDefinition.name("observable definition"); assignmentDefinition = ((qi::lit("(") >> identifier >> qi::lit("'")) > qi::lit("=") > expression_ > qi::lit(")"))[qi::_val = phoenix::bind(&PrismParser::createAssignment, phoenix::ref(*this), qi::_1, qi::_2)]; assignmentDefinition.name("assignment"); @@ -287,7 +293,8 @@ namespace storm { | initialStatesConstruct(phoenix::ref(globalProgramInformation)) | rewardModelDefinition(phoenix::ref(globalProgramInformation))[phoenix::push_back(phoenix::bind(&GlobalProgramInformation::rewardModels, phoenix::ref(globalProgramInformation)), qi::_1)] | labelDefinition[phoenix::push_back(phoenix::bind(&GlobalProgramInformation::labels, phoenix::ref(globalProgramInformation)), qi::_1)] - | formulaDefinition[phoenix::push_back(phoenix::bind(&GlobalProgramInformation::formulas, phoenix::ref(globalProgramInformation)), qi::_1)] + | observableDefinition[phoenix::push_back(phoenix::bind(&GlobalProgramInformation::observationLabels, phoenix::ref(globalProgramInformation)), qi::_1)] + | formulaDefinition[phoenix::push_back(phoenix::bind(&GlobalProgramInformation::formulas, phoenix::ref(globalProgramInformation)), qi::_1)] ) > -(systemCompositionConstruct(phoenix::ref(globalProgramInformation))) > qi::eoi)[qi::_val = phoenix::bind(&PrismParser::createProgram, phoenix::ref(*this), phoenix::ref(globalProgramInformation))]; start.name("probabilistic program"); @@ -309,6 +316,7 @@ namespace storm { qi::on_success(formulaDefinition, setLocationInfoFunction); qi::on_success(rewardModelDefinition, setLocationInfoFunction); qi::on_success(labelDefinition, setLocationInfoFunction); + qi::on_success(observableDefinition, setLocationInfoFunction); qi::on_success(commandDefinition, setLocationInfoFunction); qi::on_success(updateDefinition, setLocationInfoFunction); qi::on_success(assignmentDefinition, setLocationInfoFunction); @@ -440,6 +448,18 @@ namespace storm { } return true; } + + bool PrismParser::isFreshObservationLabelName(std::string const& labelName) { + if (!this->secondRun) { + for (auto const& existingLabel : this->globalProgramInformation.observationLabels) { + if (labelName == existingLabel.getName()) { + STORM_LOG_ERROR("Parsing error in " << this->getFilename() << ": Duplicate observable name '" << identifier << "'."); + return false; + } + } + } + return true; + } bool PrismParser::isFreshRewardModelName(std::string const& rewardModelName) { if (!this->secondRun) { @@ -599,6 +619,10 @@ namespace storm { storm::prism::Label PrismParser::createLabel(std::string const& labelName, storm::expressions::Expression expression) const { return storm::prism::Label(labelName, expression, this->getFilename()); } + + storm::prism::ObservationLabel PrismParser::createObservationLabel(std::string const& labelName, storm::expressions::Expression expression) const { + return storm::prism::ObservationLabel(labelName, expression, this->getFilename()); + } storm::prism::RewardModel PrismParser::createRewardModel(std::string const& rewardModelName, std::vector const& stateRewards, std::vector const& stateActionRewards, std::vector const& transitionRewards) const { return storm::prism::RewardModel(rewardModelName, stateRewards, stateActionRewards, transitionRewards, this->getFilename()); @@ -945,7 +969,7 @@ namespace storm { } } - return storm::prism::Program(manager, finalModelType, globalProgramInformation.constants, globalProgramInformation.globalBooleanVariables, globalProgramInformation.globalIntegerVariables, orderedFormulas, globalProgramInformation.modules, globalProgramInformation.actionIndices, globalProgramInformation.rewardModels, globalProgramInformation.labels, secondRun && !globalProgramInformation.hasInitialConstruct ? boost::none : boost::make_optional(globalProgramInformation.initialConstruct), globalProgramInformation.systemCompositionConstruct, prismCompatibility, this->getFilename(), 1, this->secondRun); + return storm::prism::Program(manager, finalModelType, globalProgramInformation.constants, globalProgramInformation.globalBooleanVariables, globalProgramInformation.globalIntegerVariables, orderedFormulas, globalProgramInformation.modules, globalProgramInformation.actionIndices, globalProgramInformation.rewardModels, globalProgramInformation.labels, globalProgramInformation.observationLabels, secondRun && !globalProgramInformation.hasInitialConstruct ? boost::none : boost::make_optional(globalProgramInformation.initialConstruct), globalProgramInformation.systemCompositionConstruct, prismCompatibility, this->getFilename(), 1, this->secondRun); } void PrismParser::removeInitialConstruct(GlobalProgramInformation& globalProgramInformation) const { diff --git a/src/storm-parsers/parser/PrismParser.h b/src/storm-parsers/parser/PrismParser.h index eecac5b2b..2668dcb68 100644 --- a/src/storm-parsers/parser/PrismParser.h +++ b/src/storm-parsers/parser/PrismParser.h @@ -41,6 +41,7 @@ namespace storm { modules.clear(); rewardModels.clear(); labels.clear(); + observationLabels.clear(); hasInitialConstruct = false; initialConstruct = storm::prism::InitialConstruct(); systemCompositionConstruct = boost::none; @@ -60,6 +61,7 @@ namespace storm { std::vector modules; std::vector rewardModels; std::vector labels; + std::vector observationLabels; bool hasInitialConstruct; storm::prism::InitialConstruct initialConstruct; boost::optional systemCompositionConstruct; @@ -261,6 +263,7 @@ namespace storm { // Rules for initial states expression. qi::rule initialStatesConstruct; + // Rules for POMDP observables (standard prism) qi::rule observablesConstruct; // Rules for invariant constructs @@ -284,6 +287,10 @@ namespace storm { qi::rule labelDefinition; qi::rule freshLabelName; + // Rules for observable (observation-label) definitions. + qi::rule observableDefinition; + qi::rule freshObservationLabelName; + // Rules for formula definitions. qi::rule formulaDefinitionRhs; qi::rule formulaDefinition; @@ -307,6 +314,7 @@ namespace storm { bool isKnownModuleName(std::string const& moduleName); bool isFreshModuleName(std::string const& moduleName); bool isFreshLabelName(std::string const& moduleName); + bool isFreshObservationLabelName(std::string const& labelName); bool isFreshRewardModelName(std::string const& moduleName); bool isOfBoolType(storm::expressions::Expression const& expression); bool isOfIntType(storm::expressions::Expression const& expression); @@ -332,6 +340,7 @@ namespace storm { storm::prism::Formula createFormulaFirstRun(std::string const& formulaName, std::string const& expression); storm::prism::Formula createFormulaSecondRun(std::string const& formulaName, storm::expressions::Expression const& expression); storm::prism::Label createLabel(std::string const& labelName, storm::expressions::Expression expression) const; + storm::prism::ObservationLabel createObservationLabel(std::string const& labelName, storm::expressions::Expression expression) const; storm::prism::RewardModel createRewardModel(std::string const& rewardModelName, std::vector const& stateRewards, std::vector const& stateActionRewards, std::vector const& transitionRewards) const; storm::prism::StateReward createStateReward(storm::expressions::Expression statePredicateExpression, storm::expressions::Expression rewardValueExpression) const; storm::prism::StateActionReward createStateActionReward(boost::optional const& actionName, storm::expressions::Expression statePredicateExpression, storm::expressions::Expression rewardValueExpression, GlobalProgramInformation& globalProgramInformation) const;