sp
/
tempest
1
0
Fork 0
Code Issues Pull Requests Projects Releases Wiki Activity
Browse Source

extended the parser to handle observable expressions

main
Sebastian Junges 6 years ago
parent
e177a5420a
commit
290ede7404
2 changed files with 36 additions and 3 deletions
Whitespace
Show all changes Ignore whitespace when comparing lines Ignore changes in amount of whitespace Ignore changes in whitespace at EOL
Unified View
Diff Options
Show Stats Download Patch File Download Diff File
  1. 28
      src/storm-parsers/parser/PrismParser.cpp
  2. 9
      src/storm-parsers/parser/PrismParser.h

28
src/storm-parsers/parser/PrismParser.cpp
View File

@ -242,6 +242,12 @@ namespace storm {
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 = (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"); 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 = ((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"); assignmentDefinition.name("assignment");
@ -287,7 +293,8 @@ namespace storm {
| initialStatesConstruct(phoenix::ref(globalProgramInformation)) | initialStatesConstruct(phoenix::ref(globalProgramInformation))
| rewardModelDefinition(phoenix::ref(globalProgramInformation))[phoenix::push_back(phoenix::bind(&GlobalProgramInformation::rewardModels, phoenix::ref(globalProgramInformation)), qi::_1)] | 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)] | 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))]; > -(systemCompositionConstruct(phoenix::ref(globalProgramInformation))) > qi::eoi)[qi::_val = phoenix::bind(&PrismParser::createProgram, phoenix::ref(*this), phoenix::ref(globalProgramInformation))];
start.name("probabilistic program"); start.name("probabilistic program");
@ -309,6 +316,7 @@ namespace storm {
qi::on_success(formulaDefinition, setLocationInfoFunction); qi::on_success(formulaDefinition, setLocationInfoFunction);
qi::on_success(rewardModelDefinition, setLocationInfoFunction); qi::on_success(rewardModelDefinition, setLocationInfoFunction);
qi::on_success(labelDefinition, setLocationInfoFunction); qi::on_success(labelDefinition, setLocationInfoFunction);
qi::on_success(observableDefinition, setLocationInfoFunction);
qi::on_success(commandDefinition, setLocationInfoFunction); qi::on_success(commandDefinition, setLocationInfoFunction);
qi::on_success(updateDefinition, setLocationInfoFunction); qi::on_success(updateDefinition, setLocationInfoFunction);
qi::on_success(assignmentDefinition, setLocationInfoFunction); qi::on_success(assignmentDefinition, setLocationInfoFunction);
@ -441,6 +449,18 @@ namespace storm {
return true; 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) { bool PrismParser::isFreshRewardModelName(std::string const& rewardModelName) {
if (!this->secondRun) { if (!this->secondRun) {
for (auto const& existingRewardModel : this->globalProgramInformation.rewardModels) { for (auto const& existingRewardModel : this->globalProgramInformation.rewardModels) {
@ -600,6 +620,10 @@ namespace storm {
return storm::prism::Label(labelName, expression, this->getFilename()); 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<storm::prism::StateReward> const& stateRewards, std::vector<storm::prism::StateActionReward> const& stateActionRewards, std::vector<storm::prism::TransitionReward> const& transitionRewards) const { storm::prism::RewardModel PrismParser::createRewardModel(std::string const& rewardModelName, std::vector<storm::prism::StateReward> const& stateRewards, std::vector<storm::prism::StateActionReward> const& stateActionRewards, std::vector<storm::prism::TransitionReward> const& transitionRewards) const {
return storm::prism::RewardModel(rewardModelName, stateRewards, stateActionRewards, transitionRewards, this->getFilename()); 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 { void PrismParser::removeInitialConstruct(GlobalProgramInformation& globalProgramInformation) const {

9
src/storm-parsers/parser/PrismParser.h
View File

@ -41,6 +41,7 @@ namespace storm {
modules.clear(); modules.clear();
rewardModels.clear(); rewardModels.clear();
labels.clear(); labels.clear();
observationLabels.clear();
hasInitialConstruct = false; hasInitialConstruct = false;
initialConstruct = storm::prism::InitialConstruct(); initialConstruct = storm::prism::InitialConstruct();
systemCompositionConstruct = boost::none; systemCompositionConstruct = boost::none;
@ -60,6 +61,7 @@ namespace storm {
std::vector<storm::prism::Module> modules; std::vector<storm::prism::Module> modules;
std::vector<storm::prism::RewardModel> rewardModels; std::vector<storm::prism::RewardModel> rewardModels;
std::vector<storm::prism::Label> labels; std::vector<storm::prism::Label> labels;
std::vector<storm::prism::ObservationLabel> observationLabels;
bool hasInitialConstruct; bool hasInitialConstruct;
storm::prism::InitialConstruct initialConstruct; storm::prism::InitialConstruct initialConstruct;
boost::optional<storm::prism::SystemCompositionConstruct> systemCompositionConstruct; boost::optional<storm::prism::SystemCompositionConstruct> systemCompositionConstruct;
@ -261,6 +263,7 @@ namespace storm {
// Rules for initial states expression. // Rules for initial states expression.
qi::rule<Iterator, qi::unused_type(GlobalProgramInformation&), Skipper> initialStatesConstruct; qi::rule<Iterator, qi::unused_type(GlobalProgramInformation&), Skipper> initialStatesConstruct;
// Rules for POMDP observables (standard prism)
qi::rule<Iterator, qi::unused_type(), Skipper> observablesConstruct; qi::rule<Iterator, qi::unused_type(), Skipper> observablesConstruct;
// Rules for invariant constructs // Rules for invariant constructs
@ -284,6 +287,10 @@ namespace storm {
qi::rule<Iterator, storm::prism::Label(), Skipper> labelDefinition; qi::rule<Iterator, storm::prism::Label(), Skipper> labelDefinition;
qi::rule<Iterator, std::string(), Skipper> freshLabelName; qi::rule<Iterator, std::string(), Skipper> freshLabelName;
// Rules for observable (observation-label) definitions.
qi::rule<Iterator, storm::prism::ObservationLabel(), Skipper> observableDefinition;
qi::rule<Iterator, std::string(), Skipper> freshObservationLabelName;
// Rules for formula definitions. // Rules for formula definitions.
qi::rule<Iterator, std::string(), Skipper> formulaDefinitionRhs; qi::rule<Iterator, std::string(), Skipper> formulaDefinitionRhs;
qi::rule<Iterator, storm::prism::Formula(), Skipper> formulaDefinition; qi::rule<Iterator, storm::prism::Formula(), Skipper> formulaDefinition;
@ -307,6 +314,7 @@ namespace storm {
bool isKnownModuleName(std::string const& moduleName); bool isKnownModuleName(std::string const& moduleName);
bool isFreshModuleName(std::string const& moduleName); bool isFreshModuleName(std::string const& moduleName);
bool isFreshLabelName(std::string const& moduleName); bool isFreshLabelName(std::string const& moduleName);
bool isFreshObservationLabelName(std::string const& labelName);
bool isFreshRewardModelName(std::string const& moduleName); bool isFreshRewardModelName(std::string const& moduleName);
bool isOfBoolType(storm::expressions::Expression const& expression); bool isOfBoolType(storm::expressions::Expression const& expression);
bool isOfIntType(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 createFormulaFirstRun(std::string const& formulaName, std::string const& expression);
storm::prism::Formula createFormulaSecondRun(std::string const& formulaName, storm::expressions::Expression 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::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<storm::prism::StateReward> const& stateRewards, std::vector<storm::prism::StateActionReward> const& stateActionRewards, std::vector<storm::prism::TransitionReward> const& transitionRewards) const; storm::prism::RewardModel createRewardModel(std::string const& rewardModelName, std::vector<storm::prism::StateReward> const& stateRewards, std::vector<storm::prism::StateActionReward> const& stateActionRewards, std::vector<storm::prism::TransitionReward> const& transitionRewards) const;
storm::prism::StateReward createStateReward(storm::expressions::Expression statePredicateExpression, storm::expressions::Expression rewardValueExpression) const; storm::prism::StateReward createStateReward(storm::expressions::Expression statePredicateExpression, storm::expressions::Expression rewardValueExpression) const;
storm::prism::StateActionReward createStateActionReward(boost::optional<std::string> const& actionName, storm::expressions::Expression statePredicateExpression, storm::expressions::Expression rewardValueExpression, GlobalProgramInformation& globalProgramInformation) const; storm::prism::StateActionReward createStateActionReward(boost::optional<std::string> const& actionName, storm::expressions::Expression statePredicateExpression, storm::expressions::Expression rewardValueExpression, GlobalProgramInformation& globalProgramInformation) const;

Write Preview
Loading…
Cancel
Save