From ff572c7f6f68de71ba75fee081f0fbeeb15f619e Mon Sep 17 00:00:00 2001
From: dehnert <dehnert@cs.rwth-aachen.de>
Date: Fri, 8 Aug 2014 10:12:38 +0200
Subject: [PATCH] Sped up PRISM parser by letting it skip the actual command
definitions in the first run (because only gathering constants, variables and
formulas is important in this particular run).
Former-commit-id: 0b25c73fa4333237b99d4ac2e948c00e96f9059d
---
src/parser/PrismParser.cpp | 6 +++++-
1 file changed, 5 insertions(+), 1 deletion(-)
diff --git a/src/parser/PrismParser.cpp b/src/parser/PrismParser.cpp
index cb4ccbe69..ba87a2baa 100644
--- a/src/parser/PrismParser.cpp
+++ b/src/parser/PrismParser.cpp
@@ -139,7 +139,7 @@ namespace storm {
updateListDefinition %= +updateDefinition(qi::_r1) % "+";
updateListDefinition.name("update list");
- commandDefinition = (qi::lit("[") > -(identifier[qi::_a = qi::_1]) > qi::lit("]") > expressionParser > qi::lit("->") > updateListDefinition(qi::_r1) > qi::lit(";"))[qi::_val = phoenix::bind(&PrismParser::createCommand, phoenix::ref(*this), qi::_a, qi::_2, qi::_3, qi::_r1)];
+ commandDefinition = qi::lit("[") > +(qi::char_ - qi::lit(";")) > qi::lit(";")[qi::_val = phoenix::construct<storm::prism::Command>()];
commandDefinition.name("command definition");
moduleDefinition = ((qi::lit("module") >> identifier >> *(variableDefinition(qi::_a, qi::_b))) > +commandDefinition(qi::_r1) > qi::lit("endmodule"))[qi::_val = phoenix::bind(&PrismParser::createModule, phoenix::ref(*this), qi::_1, qi::_a, qi::_b, qi::_2, qi::_r1)];
@@ -189,6 +189,10 @@ namespace storm {
}
void PrismParser::moveToSecondRun() {
+ // In the second run, we actually need to parse the commands instead of just skipping them,
+ // so we adapt the rule for parsing commands.
+ commandDefinition = (qi::lit("[") > -(identifier[qi::_a = qi::_1]) > qi::lit("]") > expressionParser > qi::lit("->") > updateListDefinition(qi::_r1) > qi::lit(";"))[qi::_val = phoenix::bind(&PrismParser::createCommand, phoenix::ref(*this), qi::_a, qi::_2, qi::_3, qi::_r1)];
+
this->secondRun = true;
this->expressionParser.setIdentifierMapping(&this->identifiers_);
}