From 484bbf3e83fabf886263d3dc1cebbd85aca482fe Mon Sep 17 00:00:00 2001
From: dehnert <dehnert@cs.rwth-aachen.de>
Date: Fri, 17 Oct 2014 11:26:14 +0200
Subject: [PATCH] Atomic propositions in formulas can now also be surrounded by
 quotation marks (to be compatible with the PRISM syntax).

Former-commit-id: e31a8c832ac1019fc2c2488473b8c89f36ed732f
---
 src/parser/CslParser.cpp   | 3 +--
 src/parser/LtlParser.cpp   | 3 +--
 src/parser/PrctlParser.cpp | 3 +--
 3 files changed, 3 insertions(+), 6 deletions(-)

diff --git a/src/parser/CslParser.cpp b/src/parser/CslParser.cpp
index 4aa8f7d91..b16e441e8 100644
--- a/src/parser/CslParser.cpp
+++ b/src/parser/CslParser.cpp
@@ -80,8 +80,7 @@ struct CslParser::CslGrammar : qi::grammar<Iterator, std::shared_ptr<csl::CslFil
 		//(Propositions, probabilistic/reward formulas, and state formulas in brackets)
 		atomicStateFormula %= probabilisticBoundOperator | steadyStateBoundOperator | atomicProposition | (qi::lit("(") >> stateFormula >> qi::lit(")")) | (qi::lit("[") >> stateFormula >> qi::lit("]"));
 		atomicStateFormula.name("atomic state formula");
-		atomicProposition = (freeIdentifierName)[qi::_val =
-				MAKE(csl::Ap<double>, qi::_1)];
+		atomicProposition = (freeIdentifierName)[qi::_val = MAKE(csl::Ap<double>, qi::_1)] | (qi::lit("\"") > (freeIdentifierName)[qi::_val = MAKE(csl::Ap<double>, qi::_1)] > qi::lit("\""));
 		atomicProposition.name("atomic proposition");
 		probabilisticBoundOperator = (
 				(qi::lit("P") >> comparisonType > qi::double_ > pathFormula )[qi::_val =
diff --git a/src/parser/LtlParser.cpp b/src/parser/LtlParser.cpp
index 86fff3b03..79059e994 100644
--- a/src/parser/LtlParser.cpp
+++ b/src/parser/LtlParser.cpp
@@ -88,8 +88,7 @@ struct LtlParser::LtlGrammar : qi::grammar<Iterator, std::shared_ptr<storm::prop
 		//(Propositions, probabilistic/reward formulas, and state formulas in brackets)
 		atomicLtlFormula %= pathFormula | atomicProposition | qi::lit("(") >> formula >> qi::lit(")")| qi::lit("[") >> formula >> qi::lit("]");
 		atomicLtlFormula.name("Atomic LTL formula");
-		atomicProposition = (freeIdentifierName)[qi::_val =
-				MAKE(ltl::Ap<double>, qi::_1)];
+		atomicProposition = (freeIdentifierName)[qi::_val = MAKE(ltl::Ap<double>, qi::_1)] | (qi::lit("\"") > (freeIdentifierName)[qi::_val = MAKE(ltl::Ap<double>, qi::_1)] > qi::lit("\""));
 		atomicProposition.name("Atomic Proposition");
 
 		//This block defines rules for parsing probabilistic path formulas
diff --git a/src/parser/PrctlParser.cpp b/src/parser/PrctlParser.cpp
index d2e6f06fa..d12fba12b 100644
--- a/src/parser/PrctlParser.cpp
+++ b/src/parser/PrctlParser.cpp
@@ -76,8 +76,7 @@ struct PrctlParser::PrctlGrammar : qi::grammar<Iterator, std::shared_ptr<storm::
 		// (Propositions, probabilistic/reward formulas, and state formulas in brackets)
 		atomicStateFormula %= probabilisticBoundOperator | rewardBoundOperator | atomicProposition | qi::lit("(") >> stateFormula >> qi::lit(")") | qi::lit("[") >> stateFormula >> qi::lit("]");
 		atomicStateFormula.name("atomic state formula");
-		atomicProposition = (freeIdentifierName)[qi::_val =
-				MAKE(prctl::Ap<double>, qi::_1)];
+		atomicProposition = (freeIdentifierName)[qi::_val = MAKE(prctl::Ap<double>, qi::_1)] | (qi::lit("\"") > (freeIdentifierName)[qi::_val = MAKE(prctl::Ap<double>, qi::_1)] > qi::lit("\""));
 		atomicProposition.name("atomic proposition");
 		probabilisticBoundOperator = ((qi::lit("P") >> comparisonType > qi::double_ > pathFormula)[qi::_val =
 				MAKE(prctl::ProbabilisticBoundOperator<double>, qi::_1, qi::_2, qi::_3)]);