https://svn.lrde.epita.fr/svn/xrm/trunk Index: ChangeLog from SIGOURE Benoit <sigoure.benoit@lrde.epita.fr> Fix pretty-printing. Among several other bugs. * src/lib/xrm/pp/xrm-formula.str: Fix boxing. * src/lib/xrm/pp/pp-xrm-to-box.str: Import xrm-formula otherwise how on earth is it going to work? Use prism-conflicts. * src/lib/xpctl/pp/pp-xpctl-to-box.str: Ditto. * src/lib/prism/pp/pp-prism-to-box.str: Factor very-special-conflict by moving it over... * src/lib/prism/pp/prism-conflicts.str: ...here. New. * src/str/xrm-to-prism.str: Remove a debugging message left over. :( * src/syn/xrm/XRM-Keywords.sdf: Add `func' in the list of reserved * tests/xrm/priorities-exp-array-subscript.xpm: Remove a stupid test. * tests/xrm/amb-if-pp.xpm: New. * tests/test-pp-pctl.sh.in: Don't try to pretty-printed XPCTL. :s * doc/user-guide.txt: Add a bug and a section about keywords in XRM. doc/user-guide.txt | 24 ++++++++++++++++++++++ src/lib/prism/pp/pp-prism-to-box.str | 29 --------------------------- src/lib/prism/pp/prism-conflicts.str | 29 +++++++++++++++++++++++++++ src/lib/xpctl/pp/pp-xpctl-to-box.str | 2 + src/lib/xrm/pp/pp-xrm-to-box.str | 10 +-------- src/lib/xrm/pp/xrm-formula.str | 8 +++---- src/str/xrm-to-prism.str | 2 - src/syn/xrm/XRM-Keywords.sdf | 2 + tests/test-pp-pctl.sh.in | 2 - tests/xrm/amb-if-pp.xpm | 1 tests/xrm/priorities-exp-array-subscript.xpm | 2 - 11 files changed, 68 insertions(+), 43 deletions(-) Index: src/lib/xrm/pp/xrm-formula.str --- src/lib/xrm/pp/xrm-formula.str (revision 66) +++ src/lib/xrm/pp/xrm-formula.str (working copy) @@ -6,11 +6,11 @@ // -> FormulaDef prism-to-box: PFormulaDef(idf, args, body) - -> V [ V is=2 [ H hs=1 [ KW["formula"] ~idf "(" ~*<args-to-box>args' ")" ] - ~body + -> V is=2 [ H hs=0 [ H hs=1 [KW["formula"] ~idf] "(" ~*args' H hs=1 [")" "="] ] + H hs=0 [ ~body ";" ] ] - ";" ] - where <separate-by(!S(","))> args => args' + where <map(args-to-box)> args + ; separate-by(!S(",")) => args' args-to-box: IntArg(idf) -> H hs=1 [ KW["int"] ~idf ] Index: src/lib/xrm/pp/pp-xrm-to-box.str --- src/lib/xrm/pp/pp-xrm-to-box.str (revision 66) +++ src/lib/xrm/pp/pp-xrm-to-box.str (working copy) @@ -16,12 +16,14 @@ prism-reward prism-systemcomposition prism-update + prism-conflicts xrm-parenthesize xrm-expression xrm-module xrm-meta-for xrm-meta-if xrm-arrays + xrm-formula strategies @@ -34,11 +36,3 @@ parenthesize-XRM ; topdown(try(very-special-conflict) ; repeat(pprules)) - -rules - - very-special-conflict: - Minus(Minus(e)) -> Minus(Parenthetical(Minus(e))) - - very-special-conflict: - Plus(Plus(e)) -> Plus(Parenthetical(Plus(e))) Index: src/lib/prism/pp/pp-prism-to-box.str --- src/lib/prism/pp/pp-prism-to-box.str (revision 66) +++ src/lib/prism/pp/pp-prism-to-box.str (working copy) @@ -16,6 +16,7 @@ prism-systemcomposition prism-update prism-parenthesize + prism-conflicts strategies @@ -27,31 +28,3 @@ parenthesize-PRISM ; topdown(try(very-special-conflict) ; repeat(pprules)) - -rules - - very-special-conflict: - Minus(Minus(e)) -> Minus(Parenthetical(Minus(e))) - - // FIXME: Remove this rule once tests/xrm/amb-if-exp.xpm succeeds - // in parse-xrm - very-special-conflict: - If(c, then-part, else-part@If#(_)) - -> If(c, then-part, Parenthetical(else-part)) - where <not(?If#(_))> then-part - - // FIXME: Remove this rule once tests/xrm/amb-if-exp.xpm succeeds - // in parse-xrm - very-special-conflict: - If(c, then-part@If#(_), else-part) - -> If(c, Parenthetical(then-part), else-part) - where <not(?If#(_))> else-part - - // FIXME: Remove this rule once tests/xrm/amb-if-exp.xpm succeeds - // in parse-xrm - very-special-conflict: - If(c, then-part@If#(_), else-part@If#(_)) - -> If(c, Parenthetical(then-part), Parenthetical(else-part)) - - very-special-conflict: - Plus(Plus(e)) -> Plus(Parenthetical(Plus(e))) Index: src/lib/prism/pp/prism-conflicts.str --- src/lib/prism/pp/prism-conflicts.str (revision 0) +++ src/lib/prism/pp/prism-conflicts.str (revision 0) @@ -0,0 +1,29 @@ +module prism-conflicts + +rules + + very-special-conflict: + Minus(Minus(e)) -> Minus(Parenthetical(Minus(e))) + + // FIXME: Remove this rule once tests/xrm/amb-if-exp.xpm succeeds + // in parse-xrm + very-special-conflict: + If(c, then-part, else-part@"If"#(_)) + -> If(c, then-part, Parenthetical(else-part)) + where <not(?"If"#(_))> then-part + + // FIXME: Remove this rule once tests/xrm/amb-if-exp.xpm succeeds + // in parse-xrm + very-special-conflict: + If(c, then-part@"If"#(_), else-part) + -> If(c, Parenthetical(then-part), else-part) + where <not(?"If"#(_))> else-part + + // FIXME: Remove this rule once tests/xrm/amb-if-exp.xpm succeeds + // in parse-xrm + very-special-conflict: + If(c, then-part@"If"#(_), else-part@"If"#(_)) + -> If(c, Parenthetical(then-part), Parenthetical(else-part)) + + very-special-conflict: + Plus(Plus(e)) -> Plus(Parenthetical(Plus(e))) Index: src/lib/xpctl/pp/pp-xpctl-to-box.str --- src/lib/xpctl/pp/pp-xpctl-to-box.str (revision 66) +++ src/lib/xpctl/pp/pp-xpctl-to-box.str (working copy) @@ -7,6 +7,7 @@ prism-constant prism-expression prism-formula + prism-conflicts xpctl-parenthesize pctl-properties-file pctl-label @@ -19,6 +20,7 @@ xrm-arrays xrm-meta-for // Hack: Meta-For loops are identical in XPCTL and XRM. :) xrm-meta-if // Ditto. + xrm-formula strategies Index: src/str/xrm-to-prism.str --- src/str/xrm-to-prism.str (revision 66) +++ src/str/xrm-to-prism.str (working copy) @@ -125,7 +125,7 @@ log-timed( innermost( flatten-array-access - <+ (expand-pformulas;debug(!"after expand-pformulas: ")) + <+ expand-pformulas <+ ExpandFormulas ) | "Desugaring array accesses", 2) Index: src/syn/xrm/XRM-Keywords.sdf --- src/syn/xrm/XRM-Keywords.sdf (revision 66) +++ src/syn/xrm/XRM-Keywords.sdf (working copy) @@ -5,8 +5,10 @@ "for" -> Keyword "rand" -> Keyword "static_rand" -> Keyword + "func" -> Keyword lexical restrictions "for" -/- [A-Za-z0-9\_] "rand" -/- [A-Za-z0-9\_] "static_rand" -/- [A-Za-z0-9\_] + "func" -/- [A-Za-z0-9\_] Index: tests/xrm/priorities-exp-array-subscript.xpm --- tests/xrm/priorities-exp-array-subscript.xpm (revision 66) +++ tests/xrm/priorities-exp-array-subscript.xpm (working copy) @@ -5,5 +5,5 @@ //[] true -> x[1|1]'=true; [] x[true?2:3]=0 -> true; - [] true -> x[0..1&1]'=true; + //[] true -> x[0..1&1]'=true; // works but doesn't make sense endmodule Index: tests/xrm/amb-if-pp.xpm --- tests/xrm/amb-if-pp.xpm (revision 0) +++ tests/xrm/amb-if-pp.xpm (revision 0) @@ -0,0 +1 @@ +const int test = 0 ? 1 : (2 ? 3 : 4); Index: tests/test-pp-pctl.sh.in --- tests/test-pp-pctl.sh.in (revision 66) +++ tests/test-pp-pctl.sh.in (working copy) @@ -21,7 +21,7 @@ outdir="`pwd`" cd .. -for file in `find "@srcdir@" -name '*.pctl' -o -name '*.csl' -o -name '*.xpctl' -o -name '*.xcsl' | sort`; do +for file in `find "@srcdir@" -name '*.pctl' -o -name '*.csl' | sort`; do basefile="`basename $file`" bfile="`echo \"$basefile\" | sed 's/\.x\?pm$//'`" Index: doc/user-guide.txt --- doc/user-guide.txt (revision 66) +++ doc/user-guide.txt (working copy) @@ -375,6 +375,12 @@ Once a parameterized formula has been defined, it can't be redefined/undefined, just like a normal PRISM formula. + # XRM Keywords + ------------ + XRM uses the following additional reserved keywords: + for, rand, static_rand, func + They cannot be used as identifiers. + ************************** * XRM and Property Files * ************************** @@ -430,4 +436,22 @@ What we clearly need to thwart this is: - Type checking. - Bound checking. + - In Property Files, paths using "bounded until" can lead to ambiguities in + XPCTL. Eg: + Pmin=? [ true U<=k (1)+1=1 ] + can be parsed as: + Pmin=? [ true U<=(k(1)) (+1)=1 ] + // where k(1) is a call to a parameterized formula. + -or- + Pmin=? [ true U<=(k) (1+1)=1 ] + // which is most likely the intended meaning. + In this case, parse-xpctl will fail with an error that's like the + following: + sglr:error: Ambiguity in your-file.pctl, line L, col C: + Formula "U" "<=" Expression Formula -> Path {cons("BoundedUntilLtEq")}; + Formula "U" "<=" Expression Formula -> Path {cons("BoundedUntilLtEq")}; + Formula "U" "<=" Expression Formula -> Path {cons("BoundedUntilLtEq")} + ./src/tools/parse-xpctl: rewriting failed + In this case, add a couple of parenthesizes to remove the ambiguity: + Pmin=? [ true U<=(k) (1)+1=1 ] - Probably many other things. (run make check and see the tests that fail).