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

https://svn.lrde.epita.fr/svn/xrm/trunk Index: ChangeLog from SIGOURE Benoit &lt;sigoure.benoit(a)lrde.epita.fr&gt; 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 &lt;martin(a)cs.uu.nl&gt; - 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 &lt;visser(a)acm.org&gt; + For his support on IRC. + +Akim Demaille &lt;akim(a)lrde.epita.fr&gt; + 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 &lt;micha(a)lrde.epita.fr&gt; + 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