[Projects] XRM 60: Fix (almost completely) the PCTL/CSL grammar.

https://svn.lrde.epita.fr/svn/xrm/trunk


Index: ChangeLog
from  SIGOURE Benoit  <sigoure.benoit@lrde.epita.fr>

	Fix (almost completely) the PCTL/CSL grammar.
	Most of the PCTL files in the test suite are now parsed correctly (95
	out of 103). The remaining failing PCTL files fail because of a
	problem illustrated in the new test longuest-exp-match.pctl:
	  1 + 2 + 3<=4
	must be parsed as: (1 + 2 + 3)<=4
	However the current grammar yields the following extra possibilities:
	  (1) (+2 + 3)<=4
	  (1) (+2) (+3)<=4
	  (1 + 2) (+3)<=4
	  ...
	So basically we need a way to match the longuest Expression possible
	around binary operators. Besides that, our implementation of the PCTL
	grammar seems to be correct.

	* src/syn/pctl/PCTL-Property.sdf: Fix priorities.
	* src/syn/pctl/PCTL-Reward.sdf: Import PCTL-Formula.
	* THANKS: Bring up to date.
	* tests/pctl/longuest-exp-match.pctl: New.

 THANKS                             |   15 ++++++++++--
 src/syn/pctl/PCTL-Property.sdf     |   44 ++++++++++++++++++++++++++++---------
 src/syn/pctl/PCTL-Reward.sdf       |    1 
 tests/pctl/longuest-exp-match.pctl |   16 +++++++++++++
 4 files changed, 64 insertions(+), 12 deletions(-)

Index: src/syn/pctl/PCTL-Property.sdf
--- src/syn/pctl/PCTL-Property.sdf	(revision 59)
+++ src/syn/pctl/PCTL-Property.sdf	(working copy)
@@ -48,6 +48,8 @@
 
   %% EBNF Grammar: PCTL Properties as in PRISM's parser
   %%
+  %% PCTLImplies ::= PCTLOr ["=>" PCTLOr]
+  %%
   %% PCTLOr ::= PCTLAnd ["|" PCTLAnd]
   %%
   %% PCTLAnd ::= PCTLNot ["&" PCTLNot]
@@ -139,10 +141,15 @@
     %% The two following are inherited by Expression -> Property (see below)
     %%"true"			-> Property {cons("True")}
     %%"false"			-> Property {cons("False")}
-    Property "=>" Property	-> Property {cons("Implies")}
-    Property "|" Property	-> Property {cons("Or")}
-    Property "&" Property	-> Property {cons("And")}
-    "!" Property		-> Property {cons("Not")}
+    Property "=>" Property	-> Property {left,cons("Implies")}
+    %% FIXME: This is a dirty hack. See the FIXME about it in the priorities
+    %%        below...
+    Expression "=>" Expression	-> Property {left,cons("Implies")}
+    Expression "=>" Property	-> Property {left,cons("Implies")}
+    Property "=>" Expression	-> Property {left,cons("Implies")}
+    Property "|" Property	-> Property {left,cons("PropOr")}
+    Property "&" Property	-> Property {left,cons("PropAnd")}
+    "!" Property		-> Property {cons("PropNot")}
 
     "P" "<"   Expression "[" Path Filter? "]" -> Property {cons("ProbLt")}
     "P" "<="  Expression "[" Path Filter? "]" -> Property {cons("ProbLtEq")}
@@ -172,32 +179,49 @@
 
     "\"init\""			-> Property {cons("Init")}
     "\"" Identifier "\""	-> Property {cons("Label")}
-    Expression			-> Property
+    Expression			-> Property {cons("Exp2Prop")}
     "(" Property ")"		-> Property {bracket}
 
-  %% FIXME: Some priorities are probably missing here
   context-free priorities
-    {
+    {left:
       Property "=>" Property	-> Property
+      %% FIXME: This is a dirty hack. See the next FIXME.
+      Expression "=>" Expression -> Property
+      Expression "=>" Property	-> Property
+      Property "=>" Expression	-> Property
     }
-  > {
+  > {left:
       Property "|" Property	-> Property
     }
-  > {
+  > {left:
       Property "&" Property	-> Property
     }
   > {
       "!" Property		-> Property
     }
+  %% FIXME: The following priority will prevent things such as:
+  %%    Expression "=>" Expression -> Property
+  %%    Expression "=>" Property -> Property
+  %%    Property "=>" Expression -> Property
+  %% It seems we can't easily work around this problem because SDF priorities
+  %% are transitive. Instead these problematic cases have been hard coded in
+  %% the grammar :(
   > {
       Expression		-> Property
     }
 
-  %% FIXME: This looks a bit weird...
   context-free priorities
     {
       "(" Formula ")"		-> Formula
     }
   > {
+      Property			-> Formula
+    }
+
+  context-free priorities
+    {
       "(" Property ")"		-> Property
     }
+  > {
+      Expression		-> Property
+    }
Index: src/syn/pctl/PCTL-Reward.sdf
--- src/syn/pctl/PCTL-Reward.sdf	(revision 59)
+++ src/syn/pctl/PCTL-Reward.sdf	(working copy)
@@ -1,6 +1,7 @@
 module PCTL-Reward
 imports
   PRISM-Expression
+  PCTL-Formula
 exports
 
   %% EBNF Grammar: Rewards in PCTL
Index: THANKS
--- THANKS	(revision 59)
+++ THANKS	(working copy)
@@ -1,3 +1,14 @@
 Martin Bravenboer <martin@cs.uu.nl>
-  For his dedicated support on IRC and the time he took to understand and
-  solve the problems.
+  For his dedicated support on IRC and the huge amount of time he took to
+  understand and solve so many problems.
+
+Eelco Visser <visser@acm.org>
+  For his support on IRC.
+
+Akim Demaille <akim@lrde.epita.fr>
+  For his precious comments and continuous review of the work done on XRM. He
+  is also the one who had first suggested to have a dedicated tool to solve
+  the problems that PRISM has, using program transformation.
+
+Michael Cadilhac <micha@lrde.epita.fr>
+  For his beta-testing, his suggestions and many (good) ideas.
Index: tests/pctl/longuest-exp-match.pctl
--- tests/pctl/longuest-exp-match.pctl	(revision 0)
+++ tests/pctl/longuest-exp-match.pctl	(revision 0)
@@ -0,0 +1,16 @@
+1 + 2 + 3<=4
+
+//good:
+// (1 + 2 + 3)<=4
+
+//baddies:
+
+// (1)
+// (+2 + 3)<=4
+
+// (1)
+// (+2)
+// (+3)<=4
+
+// (1 + 2)
+// (+3)<=4