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<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());
@@ -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<storm::prism::Module> modules;
std::vector<storm::prism::RewardModel> rewardModels;
std::vector<storm::prism::Label> labels;
+ std::vector<storm::prism::ObservationLabel> observationLabels;
bool hasInitialConstruct;
storm::prism::InitialConstruct initialConstruct;
boost::optional<storm::prism::SystemCompositionConstruct> systemCompositionConstruct;
@@ -261,6 +263,7 @@ namespace storm {
// Rules for initial states expression.
qi::rule<Iterator, qi::unused_type(GlobalProgramInformation&), Skipper> initialStatesConstruct;
+ // Rules for POMDP observables (standard prism)
qi::rule<Iterator, qi::unused_type(), Skipper> observablesConstruct;
// Rules for invariant constructs
@@ -284,6 +287,10 @@ namespace storm {
qi::rule<Iterator, storm::prism::Label(), Skipper> labelDefinition;
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.
qi::rule<Iterator, std::string(), Skipper> formulaDefinitionRhs;
qi::rule<Iterator, storm::prism::Formula(), Skipper> 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<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::StateActionReward createStateActionReward(boost::optional<std::string> const& actionName, storm::expressions::Expression statePredicateExpression, storm::expressions::Expression rewardValueExpression, GlobalProgramInformation& globalProgramInformation) const;