June 2006 - Projects

Re: XRM 53: Add meta-if at Expression level.
by Akim Demaille 12 Jun '06

12 Jun '06

>>> "SIGOURE" == SIGOURE Benoit <sigoure.benoit(a)lrde.epita.fr> writes: > https://svn.lrde.epita.fr/svn/xrm/trunk > Index: ChangeLog > from SIGOURE Benoit <sigoure.benoit(a)lrde.epita.fr> > Add meta-if at Expression level. > So basically, it is now possible to have a meta-if statement everywhere > we can find an Expression. /!\ NOTE: meta-if statements at Expression > level are restricted to one single expressions in the then-part and > else-part. eg: > if some-condition then > exp1 > exp2 > end > is *invalid* at Expression level because neither the base language > nor the extended language provide real statements/sequences of > expressions. > Other improvements: PRISM-If statements (cond ? then-part : else-part) > are now evaluated by prism-desugar when possible. It is also possible > to reduce the condition of a meta-if statement down to a simple > Int(_) or Double(_). If that Int(_) or Double(_) is zero, the > condition will evaluate as False() otherwise True() [like in C]. > NOTE: for Double(_) all tests are performed with a precision of 10^-7 > in other words if 0.000000001 then ... else /*executed*/ end will be > false. This is nice!

1 0

Vcs cassé sur brasilia
by Roland Levillain 12 Jun '06

12 Jun '06

Vcs est malade chez moi [1]: brasilia ~/src/oln % svn status /usr/lib/ruby/gems/1.8/gems/core_ex-0.5.6.2/lib/core_ex/lazy_loading.rb:120:in `result': uninitialized constant Commands::Runners::Runner::Datas (NameError) from /usr/lib/ruby/gems/1.8/gems/core_ex-0.5.6.2/lib/core_ex/lazy_loading.rb:71:in `load' from /usr/lib/ruby/gems/1.8/gems/core_ex-0.5.6.2/lib/core_ex/lazy_loading.rb:133:in `load' from /usr/lib/ruby/gems/1.8/gems/core_ex-0.5.6.2/lib/core_ex/lazy_loading.rb:149:in `const_missing' from /usr/lib/ruby/gems/1.8/gems/activesupport-1.2.5/lib/active_support/binding_of_caller.rb:80:in `of_caller' from /usr/lib/ruby/gems/1.8/gems/core_ex-0.5.6.2/lib/core_ex/lazy_loading.rb:147:in `const_missing' from /usr/lib/ruby/gems/1.8/gems/ruby_ex-0.4.6.2/lib/commands/runners/runner.rb:42:in `initialize' from /usr/lib/ruby/gems/1.8/gems/ruby_ex-0.4.6.2/lib/concrete.rb:18:in `new' from /usr/lib/ruby/gems/1.8/gems/ruby_ex-0.4.6.2/lib/uri/generic_ex.rb:37 ... 29 levels... from /usr/lib/ruby/gems/1.8/gems/vcs-0.5.2.4/bin/../lib/vcs/app.rb:17 from /usr/local/lib/site_ruby/1.8/rubygems/custom_require.rb:21:in `require' from /usr/lib/ruby/gems/1.8/gems/vcs-0.5.2.4/bin/vcs-svn:7 from /usr/bin/vcs-svn:18 brasilia ~/src/oln % which svn svn: aliased to vcs-svn brasilia ~/src/oln % gem list *** LOCAL GEMS *** activesupport (1.3.1, 1.2.5, 1.1.1, 1.0.4) Support and utility classes used by the Rails framework. core_ex (0.5.6.2, 0.5.5.0, 0.4.0, 0.3.1, 0.1.3) CoreEx is a proposal for a standard library extension. highline (1.2.0, 1.0.1) HighLine is a high-level command-line IO library. ruby_ex (0.4.6.2, 0.4.5.0, 0.3.0, 0.2.0, 0.1.2) RubyEx contains general purpose Ruby extensions. rubygems-update (0.8.11) RubyGems Update GEM sources (0.0.1) This package provides download sources for remote gem installation ttk (0.2.1) TTK is an extensible framework for dynamic testing. vcs (0.5.2.4, 0.4.1, 0.4.0, 0.3.0, 0.2.148, 0.1) A wrapper over Version Control Systems C'est peut-être une mise à jour de Ruby (dans Debian unstable) qui a cassé Vcs. C'est grave docteur ? Notes: [1] Encore une satanée allergie printanière, sans doute ! :)

2 2

XRM 67: Fix pretty-printing.
by SIGOURE Benoit 12 Jun '06

12 Jun '06

https://svn.lrde.epita.fr/svn/xrm/trunk Index: ChangeLog from SIGOURE Benoit <sigoure.benoit(a)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).

1 0

XRM 66: Add parameterized formulas.
by SIGOURE Benoit 12 Jun '06

12 Jun '06

https://svn.lrde.epita.fr/svn/xrm/trunk Index: ChangeLog from SIGOURE Benoit <sigoure.benoit(a)lrde.epita.fr> Add parameterized formulas. * src/lib/xrm/pp/xrm-formula.str: New. * src/lib/xrm/pp/xrm-formula.meta: New. * src/lib/xrm/pp/xrm-expression.str: Add boxing for parameterized formulas. * src/lib/prism/pp/pp-prism-to-box.str (very-special-conflict): Handle problematic cases with nested If's (revealed by rivf.xpm). * src/str/flatten-array-access.str: Remove useless call to concat-strings. * src/str/eval-meta-code.str: Ditto. * src/str/builtin-rand.str: Ditto. * src/str/check-meta-vars.str: Handle parameterized formulas. * src/str/xrm-to-prism.str: Ditto. * src/str/inline.str: New. * src/str/prism-desugar.str: Ditto + fix desugaring of conditional expression involving literals (int and double) which was flawed! * src/str/ice.str: Handle lists of strings. * src/str/collect-static-const-decl.str: Put some code in common. Collect parameterized formula definitions. * src/str/desugar-array-access.str: Remove deprecated and useless use of UnscopedMetaVarList. * src/str/reals.str: Add an ICE'ing condition. * src/syn/xrm/XRM-Formula.sdf: Add syntax definitions for parameterized formulas. * src/syn/xrm/XRM-Keywords.sdf: Add `rand' and `static_rand' in the list of reserved keywords... * tests/xrm/rand.xpm: ... and take that change into account here. * src/syn/xrm/XRM-Expression.sdf: Add calls to parameterized formulas. * tests/pctl/xrm-formula.xpctl: New. * tests/xrm/if-desugar.xpm: New. * tests/xrm/parametrized-formula.xpm: New. * tests/test-parse-xrm.sh.in: Fix the counting of failing tests. * tests/test-parse-xpctl.sh.in: Ditto. * TODO: Bring up to date. * doc/user-guide.txt: Ditto. TODO | 4 - doc/user-guide.txt | 29 +++++++++++- src/lib/prism/pp/pp-prism-to-box.str | 20 ++++++++ src/lib/xrm/pp/xrm-expression.str | 9 ++- src/lib/xrm/pp/xrm-formula.meta | 1 src/lib/xrm/pp/xrm-formula.str | 25 ++++++++++ src/str/builtin-rand.str | 8 +-- src/str/check-meta-vars.str | 36 ++++++++++++-- src/str/collect-static-const-decl.str | 82 ++++++++++++++++++++++------------ src/str/desugar-array-access.str | 4 - src/str/eval-meta-code.str | 16 ++---- src/str/flatten-array-access.str | 4 - src/str/ice.str | 35 +++++++++----- src/str/inline.str | 42 +++++++++++++++++ src/str/prism-desugar.str | 42 +++++++++++++---- src/str/reals.str | 4 + src/str/xrm-to-prism.str | 43 ++++++++++++----- src/syn/xrm/XRM-Expression.sdf | 4 + src/syn/xrm/XRM-Formula.sdf | 20 +++++++- src/syn/xrm/XRM-Keywords.sdf | 4 + tests/pctl/xrm-formula.xpctl | 5 ++ tests/test-parse-xpctl.sh.in | 2 tests/test-parse-xrm.sh.in | 2 tests/xrm/if-desugar.xpm | 4 + tests/xrm/parametrized-formula.xpm | 3 + tests/xrm/rand.xpm | 2 26 files changed, 350 insertions(+), 100 deletions(-) Index: src/lib/xrm/pp/xrm-formula.str --- src/lib/xrm/pp/xrm-formula.str (revision 0) +++ src/lib/xrm/pp/xrm-formula.str (revision 0) @@ -0,0 +1,25 @@ +module xrm-formula + +rules + + // "formula" Identifier "(" {Argument ","}* ")" "=" Expression ";" + // -> FormulaDef + prism-to-box: + PFormulaDef(idf, args, body) + -> V [ V is=2 [ H hs=1 [ KW["formula"] ~idf "(" ~*<args-to-box>args' ")" ] + ~body + ] + ";" ] + where <separate-by(!S(","))> args => args' + + args-to-box: + IntArg(idf) -> H hs=1 [ KW["int"] ~idf ] + + args-to-box: + DoubleArg(idf) -> H hs=1 [ KW["double"] ~idf ] + + args-to-box: + BoolArg(idf) -> H hs=1 [ KW["bool"] ~idf ] + + args-to-box: + ExpArg(idf) -> H hs=1 [ KW["exp"] ~idf ] Index: src/lib/xrm/pp/xrm-formula.meta --- src/lib/xrm/pp/xrm-formula.meta (revision 0) +++ src/lib/xrm/pp/xrm-formula.meta (revision 0) @@ -0,0 +1 @@ +Meta([Syntax("Stratego-Box")]) Index: src/lib/xrm/pp/xrm-expression.str --- src/lib/xrm/pp/xrm-expression.str (revision 65) +++ src/lib/xrm/pp/xrm-expression.str (working copy) @@ -19,10 +19,15 @@ prism-to-box: // NOTE: we use the old builtin-call style Rand(args) // because func(rand, ...) is just uggly. - -> box |[ H hs=0 [ KW["rand"] "(" H hs=1 [~args-imploded] ")" ] ]| + -> H hs=0 [ KW["rand"] "(" H hs=1 [~args-imploded] ")" ] where <implode-list(|",")> args => args-imploded prism-to-box: StaticRand(args) - -> box |[ H hs=0 [ KW["static_rand"] "(" H hs=1 [~args-imploded] ")" ] ]| + -> H hs=0 [ KW["static_rand"] "(" H hs=1 [~args-imploded] ")" ] + where <implode-list(|",")> args => args-imploded + + prism-to-box: + PFormulaCall(name, args) + -> H hs=0 [ ~name "(" H hs=1 [~args-imploded] ")" ] where <implode-list(|",")> args => args-imploded Index: src/lib/prism/pp/pp-prism-to-box.str --- src/lib/prism/pp/pp-prism-to-box.str (revision 65) +++ src/lib/prism/pp/pp-prism-to-box.str (working copy) @@ -33,5 +33,25 @@ 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/str/flatten-array-access.str --- src/str/flatten-array-access.str (revision 65) +++ src/str/flatten-array-access.str (working copy) @@ -47,7 +47,7 @@ */ invalid-array-access = if ?Identifier(i) then - err-msg(|<concat-strings>["undeclared meta-variable: ", i]) + err-msg(|["undeclared meta-variable: ", i]) else if (is-int; neg) then err-msg(|"negative array subscript detected:") @@ -55,7 +55,7 @@ else err-msg(|"invalid array access:") ; debug - ; err-msg(|<concat-strings>["array subscripts must be evaluable ", + ; err-msg(|["array subscripts must be evaluable ", "down to constant positive integers."]) end end Index: src/str/check-meta-vars.str --- src/str/check-meta-vars.str (revision 65) +++ src/str/check-meta-vars.str (working copy) @@ -15,6 +15,7 @@ check-meta-for <+ check-meta-forin <+ check-meta-if + <+ check-pformula-def <+ ArrayAccess(id, check-all-identifers-are-meta-vars) <+ ArrayAccessPrime(id, check-all-identifers-are-meta-vars) <+ all(check-meta-vars) @@ -45,6 +46,21 @@ ; <check-meta-vars> else-part ) + check-pformula-def = + ?PFormulaDef(fname, args, body) + ; where({| MetaVars: + <add-args-as-meta-vars> args // Cheat: fake meta-vars. + ; <check-meta-vars> body + |}) + + add-args-as-meta-vars = + map({a: + (?_#([a]) <+ ice(|"add-args-as-meta-vars", "invalid argument", <id>)) + ; <add-meta-var> a + }) + +strategies + check-all-identifers-are-meta-vars = (?Identifier(_); check-meta-var-declared) <+ all(check-all-identifers-are-meta-vars) @@ -53,7 +69,6 @@ check-meta-var-unicity ; ?meta-var ; rules(MetaVars: meta-var) - ; rules(UnscopedMetaVarList: meta-var) check-meta-var-declared = ?Identifier(idf) @@ -61,25 +76,32 @@ /* static consts can be seen as a meta-vars here. */ + <ExpandStaticConsts> Identifier(idf) /* formulas too, as long as they are statically evaluable. */ - + (<ExpandFormulas> Identifier(idf) - ; check-all-identifers-are-meta-vars)) then - err-msg(|<concat-strings>["undeclared meta-var: ", idf]) + + ( + ( <ExpandFormulas> Identifier(idf) + + <ExpandPFormulas> Identifier(idf) + ) + /* if we successfully expanded a formula we need to check + * it's made only of meta-vars. */ + ; check-all-identifers-are-meta-vars + ) + ) then + err-msg(|["undeclared meta-var: ", idf]) ; <xtc-exit> 2 end check-meta-var-unicity = ?Identifier(idf) ; if <MetaVars> Identifier(idf) then - err-msg(|<concat-strings>["meta-var already defined: ", idf]) + err-msg(|["meta-var already defined: ", idf]) ; <xtc-exit> 2 end ; if <ExpandStaticConsts> Identifier(idf) then - err-msg(|<concat-strings>["cannot redefine `", idf, "': already ", + err-msg(|["cannot redefine `", idf, "': already ", "defined as a constant value"]) ; <xtc-exit> 2 end ; if <ExpandFormulas> Identifier(idf) then - err-msg(|<concat-strings>["cannot redefine `", idf, "': already ", + err-msg(|["cannot redefine `", idf, "': already ", "defined as a formula"]) ; <xtc-exit> 2 end Index: src/str/inline.str --- src/str/inline.str (revision 0) +++ src/str/inline.str (revision 0) @@ -0,0 +1,42 @@ +module inline + +strategies + + /** + ** Inline a call to a parameterized formula. + ** @param fname Name of the formula called (only used for + ** error messages) [string] + ** @param formal-args List of formal arguments. + ** @param effective-args List of effective arguments. + */ + inline-call(|fname, formal-args, effective-args) = + (<replace-formal-args>(fname, formal-args, effective-args, <id>) + <+ ice(|"inline-call", "replace-formal-args failed", <id>)) + +rules + + // terminate the recursion + replace-formal-args: (_, [], [], b) -> b + + replace-formal-args: + (fname, [x|xs], [], b) -> b + where err-msg(|["invalid call to the parameterized formula `", fname + ,"': not enough arguments"]) + ; <xtc-exit> 6 + + replace-formal-args: + (fname, [], [y|ys], b) -> b + where err-msg(|["invalid call to the parameterized formula `", fname + ,"': too many arguments"]) + ; <xtc-exit> 6 + + replace-formal-args: + (fname, [x|xs], [y|ys], b) -> b' + where (<?_#([x'])>x <+ ice(|"replace-formal-args", "invalid argument", x)) + //<topdown(\ x -> y \)> b // => SIGSEGV! + // FIXME: Type checking: does y (effective arg) have a compatible + // type with x (formal arg)? + ; <topdown(try(?x'; !y))> b + ; <replace-formal-args>(fname, xs, ys, <id>) => b' + + Index: src/str/xrm-to-prism.str --- src/str/xrm-to-prism.str (revision 65) +++ src/str/xrm-to-prism.str (working copy) @@ -17,13 +17,13 @@ ** - ExpandFormulas: created by the strategy collect-formulas and used by ** prism-desugar for constant propagation. Maps an identifier with an ** expression. +** - ExpandPFormulas: Same as ExpandFormulas but for parameterized +** formulas. ** - RandGenModules: each call to the XRM builtin rand generates a module ** which is stored in this DR. Just before xrm-to-prism finishes, we ** paste these modules at the end of the source code. ** - MetaVars: (scoped) temporary used by check-meta-vars to store the list ** of meta-vars declared in the current scope. -** - UnscopedMetaVarList: Same as MetaVars but unscoped. Used as a *dirty* -** workaround to allow declarations using meta-vars. */ module xrm-to-prism imports @@ -50,11 +50,13 @@ * Two goals: expand them if needed, look for variable name conflicts. */ ; log-timed( if <is-module-file> start-symbol then - ModulesFile(id, map(try(collect-static-const-decl) - ; try(collect-formulas))) + ModulesFile(id, map(try(collect-static-const-decl + + collect-formulas + + collect-pformulas))) else - PropertiesFile(map(try(collect-static-const-decl) - ; try(collect-and-remove-formulas))) + PropertiesFile(map(try(collect-static-const-decl + + collect-and-remove-formulas + + collect-pformulas))) end | "Collecting static const and formulas", 2) @@ -66,10 +68,14 @@ /* unroll meta loops, eval meta if */ ; log-timed(eval-meta-code | "Evaluating meta-code", 2) - /*; notice-msg(|"debug: pretty printing current AST in ATerms to debug.aterm") - ; where(write-to => FILE(tmp-file) + /* Useful for debugging: + ; log-timed( + where( + write-to => FILE(tmp-file) ; <xtc-command(!"pp-aterm")> ["-i", tmp-file, "-o", "debug.aterm"] - )*/ + ) + | "debug: pretty printing current AST in ATerms to debug.aterm", 2) + */ /* Desugar array declarations * eg: x[4][5] is transformed into two nested meta for loops @@ -102,15 +108,26 @@ | "Adding modules for random numbers", 2) end - /* remove array accesses: x[i] -> x_i */ - // FIXME: can we make this more efficient than a complete bottomup? + /* Remove array accesses: x[i] -> x_i + * Remove calls to parameterized formulas. + */ + // FIXME: can we make this more efficient than a complete innermost? ; if <is-module-file> start-symbol then - log-timed(bottomup(try(flatten-array-access)) + log-timed( + innermost( + flatten-array-access + <+ expand-pformulas + ) | "Desugaring array accesses", 2) else /* NOTE: for XPCTL files we also need to expand use of XRM-Formulas * because the original definition has been removed. */ - log-timed(innermost(flatten-array-access <+ ExpandFormulas) + log-timed( + innermost( + flatten-array-access + <+ (expand-pformulas;debug(!"after expand-pformulas: ")) + <+ ExpandFormulas + ) | "Desugaring array accesses", 2) end Index: src/str/prism-desugar.str --- src/str/prism-desugar.str (revision 65) +++ src/str/prism-desugar.str (working copy) @@ -41,16 +41,18 @@ ** If we are on the node where N is declared (that is: ** |[ const int N = 10; ]|) we should NOT expand `N' here. Otherwise ** we'll end up with |[ const int 10 = 10; ]|. The same thing applies for - ** formulas and ExpandFormulas. + ** formulas and ExpandFormulas and ExpandPFormulas. */ prism-desugar-first-pass = ?Int(_); IntToDouble - <+ ExpandStaticConsts; prism-desugar-first-pass // we must desugar the + <+ ExpandStaticConsts; prism-desugar-first-pass // We must desugar the <+ ExpandFormulas; prism-desugar-first-pass // expansed code. + <+ ExpandPFormulas; prism-desugar-first-pass // Ditto. <+ ConstInt(id, prism-desugar) <+ ConstDouble(id, prism-desugar) <+ ConstBool(id, prism-desugar) <+ FormulaDef(id, prism-desugar) + <+ PFormulaDef(id, id, prism-desugar) // parameterized formula defs. <+ all(prism-desugar-first-pass) rules @@ -283,6 +285,18 @@ rules EvalAnd: + |[ d & e ]| -> |[ e ]| + where <not(real-eq)>(d, "0") + EvalAnd: + |[ d & e ]| -> |[ false ]| + where <real-eq>(d, "0") + EvalAnd: + |[ e & d ]| -> |[ e ]| + where <not(real-eq)>(d, "0") + EvalAnd: + |[ e & d ]| -> |[ false ]| + where <real-eq>(d, "0") + EvalAnd: |[ true & true ]| -> |[ true ]| EvalAnd: |[ e & false ]| -> |[ false ]| @@ -294,6 +308,18 @@ |[ true & e ]| -> |[ e ]| EvalOr: + |[ d | e ]| -> |[ true ]| + where <not(real-eq)>(d, "0") + EvalOr: + |[ d | e ]| -> |[ e ]| + where <real-eq>(d, "0") + EvalOr: + |[ e | d ]| -> |[ true ]| + where <not(real-eq)>(d, "0") + EvalOr: + |[ e | d ]| -> |[ e ]| + where <real-eq>(d, "0") + EvalOr: |[ true | e ]| -> |[ true ]| EvalOr: |[ e | true ]| -> |[ true ]| @@ -320,11 +346,11 @@ EvalIf: |[ d ? e1 : e2 ]| -> |[ e1 ]| - where <not(compare(real-eq))>(d, 0) + where <not(real-eq)>(d, "0") EvalIf: |[ d ? e1 : e2 ]| -> |[ e2 ]| - where <compare(real-eq)>(d, 0) + where <real-eq>(d, "0") /* ** ## ============= ## @@ -388,9 +414,5 @@ where <not(eq)>(i, "0") LitToBool: - |[ d ]| -> |[ false ]| - where <compare(real-eq)>(d, 0) - - LitToBool: - |[ d ]| -> |[ true ]| - where <not(compare(real-eq))>(d, 0) + |[ d ]| -> res + where <compare(real-eq)>(d, "0") => res Index: src/str/eval-meta-code.str --- src/str/eval-meta-code.str (revision 65) +++ src/str/eval-meta-code.str (working copy) @@ -48,8 +48,7 @@ if !condition-value => False() then <eval-meta-code> else-part else - ice(|"eval-meta-code", <concat-strings> [ - "the conditional test of a meta if could ", + ice(|"eval-meta-code", ["the conditional test of a meta if could ", "not be reduced to a single value (True or", " False), this should have been detected ", "earlier"], @@ -90,20 +89,17 @@ check-loop-validity(|meta-var, from, to, step) = !meta-var => Identifier(idf) ; if not(!from => Int(_); !to => Int(_); !step => Int(_)) then - err-msg(|<concat-strings>["invalid meta-for loop on the meta-var `", - idf, "': the value of the ", - "fields `from', `to' and `step' must be ", - "statically evaluable down to a ", - "simple integer"]) + err-msg(|["invalid meta-for loop on the meta-var `", idf, + "': the value of the fields `from', `to' and `step' must", + "be statically evaluable down to a simple integer"]) ; <debug> from ; <debug> to ; <debug> step ; <xtc-exit> 2 end ; if <gtS>(from, to) then - err-msg(|<concat-strings>["bad `for' loop on the meta-var ", - idf, " starts at ", from, - " which is less than ", to]) + err-msg(|["bad `for' loop on the meta-var ", idf, " starts at ", + from, " which is less than ", to]) ; <xtc-exit> 2 end Index: src/str/builtin-rand.str --- src/str/builtin-rand.str (revision 65) +++ src/str/builtin-rand.str (working copy) @@ -88,7 +88,7 @@ ?current-term // save the current term for error messages /* check that rand is called with exactly two arguments */ ; if not( !args => [from, to] ) then - err-msg(|<concat-strings>["invalid call to XRM builtin: ", + err-msg(|["invalid call to XRM builtin: ", builtin-name, " takes either one or two arguments"]) ; !current-term; debug; <xtc-exit> 4 end @@ -100,8 +100,8 @@ <invalid-call-to-rand-non-int> current-term end ; if <gtS>(ifrom, ito) then - err-msg(|<concat-strings>["invalid call to XRM builtin: ", - builtin-name, "(x,y) where x > y"]) + err-msg(|["invalid call to XRM builtin: ", builtin-name + , "(x,y) where x > y"]) ; !current-term; debug; <xtc-exit> 4 end ; !(ifrom, ito) @@ -113,7 +113,7 @@ ; rules(RandUpdateList:+ _ -> rand-update) invalid-call-to-rand-non-int = - err-msg(|<concat-strings>["invalid call to XRM builtin: rand's", + err-msg(|["invalid call to XRM builtin: rand's", " arguments must be statically evaluable."]) ; debug ; <xtc-exit> 4 Index: src/str/ice.str --- src/str/ice.str (revision 65) +++ src/str/ice.str (working copy) @@ -2,35 +2,44 @@ ** Handle internal errors (things that should not happen) */ module ice +imports tool-doc // for package-bugreport strategies ice(|calling-strategy-name) = ice(|calling-strategy-name, "unknown reason") - /** Reports an ICE and exit 42 */ + /** Reports an ICE and exit 42. + ** @param reason string or list of strings. + */ ice(|calling-strategy-name, reason) = - log(|Critical(), <concat-strings>["internal compiler error in strategy ", - calling-strategy-name, ": ", reason]) + <is-list <+ ![<id>]> reason => reason' + ; log(|Critical(), ["internal compiler error in strategy ", + calling-strategy-name, ":\n", <?[<id>]>reason', + "\nPlease report this bug to ", <package-bugreport>]) ; <xtc-exit> 42 + /** Reports an ICE and exit 42. + ** @param reason string or list of strings. + ** @param term print this term before exiting. + */ ice(|calling-strategy-name, reason, term) = - // FIXME: if has-annotation ... - log(|Critical(), <concat-strings>["internal compiler error in strategy ", - calling-strategy-name, ": ", reason]) - ; !term - ; debug + // FIXME: if has-annotation ... (locations) + <is-list <+ ![<id>]> reason => reason' + ; log(|Critical(), ["internal compiler error in strategy ", + calling-strategy-name, ":\n", <?[<id>]>reason', + "\nPlease report this bug to ", <package-bugreport>] + , term) ; <xtc-exit> 42 /** Things that should work but are not yet supported. */ not-implemented(|calling-strategy-name, what) = - err-msg(|<concat-strings>["not yet implemented: ", what, " (in strategy ", + err-msg(|["not yet implemented: ", what, " (in strategy ", calling-strategy-name, ")"]) ; <xtc-exit> 51 not-implemented(|calling-strategy-name, what, term) = - // FIXME: if has-annotation ... - err-msg(|<concat-strings>["not yet implemented: ", what, " (in strategy ", + // FIXME: if has-annotation ... (locations) + err-msg(|["not yet implemented: ", what, " (in strategy ", calling-strategy-name, ")"]) - ; !term - ; debug + ; <debug> term ; <xtc-exit> 51 Index: src/str/collect-static-const-decl.str --- src/str/collect-static-const-decl.str (revision 65) +++ src/str/collect-static-const-decl.str (working copy) @@ -4,42 +4,29 @@ ** (see prism-desugar) */ module collect-static-const-decl -imports signatures +imports + signatures + inline strategies collect-static-const-decl = ?ConstInt(idf, value) - ; if <ExpandStaticConsts> idf then - cannot-redefine-static-const(|idf) - end - ; if <ExpandFormulas> idf then - cannot-redefine-formula(|idf) - end + ; check-identifier-unicity(|idf) ; where(<innermost(ExpandStaticConsts + ExpandFormulas)> value => v' ; !v'{Type("int")} => v) ; rules(ExpandStaticConsts: idf -> v) collect-static-const-decl = ?ConstDouble(idf, value) - ; if <ExpandStaticConsts> idf then - cannot-redefine-static-const(|idf) - end - ; if <ExpandFormulas> idf then - cannot-redefine-formula(|idf) - end + ; check-identifier-unicity(|idf) ; where(<innermost(ExpandStaticConsts + ExpandFormulas)> value => v' ; !v'{Type("double")} => v) ; rules(ExpandStaticConsts: idf -> v) collect-static-const-decl = ?ConstBool(idf, value) - ; if <ExpandStaticConsts> idf then - cannot-redefine-static-const(|idf) - end - ; if <ExpandFormulas> idf then - cannot-redefine-formula(|idf) - end + ; check-identifier-unicity(|idf) ; where(<innermost(ExpandStaticConsts + ExpandFormulas)> value => v' ; !v'{Type("bool")} => v) ; rules(ExpandStaticConsts: idf -> v) @@ -49,14 +36,37 @@ collect-formulas = //?|[ formula x = e; ]| ?FormulaDef(x, e) - ; if <ExpandStaticConsts> x then - cannot-redefine-static-const(|x) - end - ; if <ExpandFormulas> x then - cannot-redefine-formula(|x) - end + ; check-identifier-unicity(|x) ; rules(ExpandFormulas: x -> e) +strategies + + collect-pformulas = + //?|[ formula x(a*) = e; ]| + ?PFormulaDef(name@Identifier(fname), args, body) + ; check-identifier-unicity(|name) + ; <innermost(ExpandStaticConsts + ExpandFormulas)> body => body' + // FIXME: Catch recursive call (error) + ; rules(ExpandPFormulas: + PFormulaCall(name, a*) -> e + where <inline-call(|fname, args, a*)> body' => e + ) + ; ![] // we remove the parameterized formula definition + +strategies + + /** Ensure that a call to a parameterized formula is expanded. Use this + ** to catch calls to undefined formulas. */ + expand-pformulas = + ?PFormulaCall(Identifier(fname), _) + ; (ExpandPFormulas <+ call-to-undefined-pformula(|fname)) + + call-to-undefined-pformula(|fname) = + err-msg(|["invalid call to the undefined parameterized formula `" + , fname, "'"]) + ; debug + ; <xtc-exit> 6 + rules collect-and-remove-formulas: @@ -68,20 +78,38 @@ ; if <ExpandFormulas> x then cannot-redefine-formula(|x) end + ; if <ExpandPFormulas> x then + cannot-redefine-parameterized-formula(|x) + end ; rules(ExpandFormulas: x -> e) strategies + check-identifier-unicity(|idf) = + if <ExpandStaticConsts> idf then + cannot-redefine-static-const(|idf) + end + ; if <ExpandFormulas> idf then + cannot-redefine-formula(|idf) + end + cannot-redefine-static-const(|idf) = !idf => Identifier(idf') - ; err-msg(|<concat-strings>["Cannot redefine `", idf', "': already defined", + ; err-msg(|["Cannot redefine `", idf', "': already defined", " as a static const variable."]) ; <debug> (<ExpandStaticConsts> idf) ; <xtc-exit> 2 cannot-redefine-formula(|idf) = !idf => Identifier(idf') - ; err-msg(|<concat-strings>["Cannot redefine `", idf', "': already defined", + ; err-msg(|["Cannot redefine `", idf', "': already defined", " as a formula."]) ; <debug> (<ExpandFormulas> idf) ; <xtc-exit> 2 + + cannot-redefine-parameterized-formula(|idf) = + !idf => Identifier(idf') + ; err-msg(|["Cannot redefine `", idf', "': already defined", + " as a parameterized formula."]) + ; <debug> (<ExpandPFormulas> idf) + ; <xtc-exit> 2 Index: src/str/desugar-array-access.str --- src/str/desugar-array-access.str (revision 65) +++ src/str/desugar-array-access.str (working copy) @@ -40,7 +40,6 @@ collect-all(?ArrayAccess(_, <id>), conc) // collect gives us the list... ; reverse // ... with deepest array accesses first (we want the opposite) ; prism-desugar - ; if has-meta-vars then ice(|"desugar-subscripts", "shouldn't be here") end ; map( // traverse the list of dimensions map( // traverse the subscripts for a given dimension if ?Int(_) then @@ -58,9 +57,6 @@ ; flatten-list // because Ranges create nested lists ) // end outer map - has-meta-vars = - oncetd(?Identifier(_); UnscopedMetaVarList) - strategies /** Create the Cartesian product of all possible array subscripts. Index: src/str/reals.str --- src/str/reals.str (revision 65) +++ src/str/reals.str (working copy) @@ -66,9 +66,11 @@ ** => tests if there difference is less than the precision given in parameter ** operates on the input term (a, b) ** eg: <real-eq(|0.00001)> ("0.42", "0.43") -> fail + ** NOTE: The current term must be a tuple of strings containing reals! */ real-eq(|precision) = - (string-to-real, string-to-real) + ((is-string, is-string) <+ ice(|"real-eq", "bad call.")) + ; (string-to-real, string-to-real) ; subtr ; abs => difference ; <not(gtr)>(difference, precision) Index: src/syn/xrm/XRM-Formula.sdf --- src/syn/xrm/XRM-Formula.sdf (revision 65) +++ src/syn/xrm/XRM-Formula.sdf (working copy) @@ -7,8 +7,26 @@ exports %% the whole PRISM stuff.. dirty hack inside! %% EBNF Grammar: Extended Formulas - %% FormulaDef ::= "formula" ArrayAccess "=" Expression ";" + %% FormulaDef ::= + %% "formula" ArrayAccess "=" Expression ";" + %% | "formula" Identifier "(" {Argument ","} ")" "=" Expression ";" + %% + %% Argument ::= + %% "int" Identifier + %% | "double" Identifier + %% | "bool" Identifier context-free syntax "formula" ArrayAccess "=" Expression ";" -> FormulaDef {cons("FormulaDef")} + + context-free syntax + "formula" Identifier "(" {Argument ","}* ")" "=" Expression ";" + -> FormulaDef {cons("PFormulaDef")} + + sorts Argument + context-free syntax + "int" Identifier -> Argument {cons("IntArg")} + "double" Identifier -> Argument {cons("DoubleArg")} + "bool" Identifier -> Argument {cons("BoolArg")} + "exp" Identifier -> Argument {cons("ExpArg")} Index: src/syn/xrm/XRM-Keywords.sdf --- src/syn/xrm/XRM-Keywords.sdf (revision 65) +++ src/syn/xrm/XRM-Keywords.sdf (working copy) @@ -3,6 +3,10 @@ exports lexical syntax "for" -> Keyword + "rand" -> Keyword + "static_rand" -> Keyword lexical restrictions "for" -/- [A-Za-z0-9\_] + "rand" -/- [A-Za-z0-9\_] + "static_rand" -/- [A-Za-z0-9\_] Index: src/syn/xrm/XRM-Expression.sdf --- src/syn/xrm/XRM-Expression.sdf (revision 65) +++ src/syn/xrm/XRM-Expression.sdf (working copy) @@ -42,6 +42,10 @@ "func" "(" "static_rand" "," {Expression ","}+ ")" -> Expression {cons("StaticRand")} + %% "Function" calls (parametrized formulas) + Identifier "(" {Expression ","}+ ")" + -> Expression {cons("PFormulaCall")} + %% Ranges in XRM with different priority (for array accesses) sorts XRMRange context-free syntax Index: tests/pctl/xrm-formula.xpctl --- tests/pctl/xrm-formula.xpctl (revision 0) +++ tests/pctl/xrm-formula.xpctl (revision 0) @@ -0,0 +1,5 @@ +formula lfree = p2=0..4,6,10; +formula isfree(int i) = p[i]=0..4,6,10; + +P=? [ true U lfree ] +Pmin=? [ true U isfree(2) ] Index: tests/xrm/if-desugar.xpm --- tests/xrm/if-desugar.xpm (revision 0) +++ tests/xrm/if-desugar.xpm (revision 0) @@ -0,0 +1,4 @@ +const int success = 1; +const int fail = 0; + +const int test = 42 ? success : fail; Index: tests/xrm/rand.xpm --- tests/xrm/rand.xpm (revision 65) +++ tests/xrm/rand.xpm (working copy) @@ -1,5 +1,5 @@ -module rand // NOTE: no conflict here (rand isn't a reserved name) +module randtest // NOTE: rand is now a reserved keyword x : [0..42]; y : [0..1]; [] x=0 -> (x'=rand(5)); Index: tests/xrm/parametrized-formula.xpm --- tests/xrm/parametrized-formula.xpm (revision 0) +++ tests/xrm/parametrized-formula.xpm (revision 0) @@ -0,0 +1,3 @@ +formula add(int lhs, int rhs) = lhs + rhs; + +const int test = add(1, 2); Index: tests/test-parse-xrm.sh.in --- tests/test-parse-xrm.sh.in (revision 65) +++ tests/test-parse-xrm.sh.in (working copy) @@ -18,7 +18,7 @@ "@top_builddir@/src/tools/parse-xrm" -i "$file" -o /dev/null rv=$? test_cnt=$((test_cnt + 1)) - if [ $? -eq 0 ]; then + if [ $rv -eq 0 ]; then echo 'OK, no ambiguities found' test_pass=$((test_pass + 1)) else Index: tests/test-parse-xpctl.sh.in --- tests/test-parse-xpctl.sh.in (revision 65) +++ tests/test-parse-xpctl.sh.in (working copy) @@ -18,7 +18,7 @@ "@top_builddir@/src/tools/parse-xpctl" -i "$file" -o /dev/null rv=$? test_cnt=$((test_cnt + 1)) - if [ $? -eq 0 ]; then + if [ $rv -eq 0 ]; then echo 'OK, no ambiguities found' test_pass=$((test_pass + 1)) else Index: TODO --- TODO (revision 65) +++ TODO (working copy) @@ -94,8 +94,6 @@ * Add a possibility to import another module, eg: import common.pm A module can be imported only once. - * Add parameterized formulas. (Pretty much like macro-functions in C) - * Add scopes for meta variables eg: for i ... do for i ... // `i' shadows its previous definition @@ -268,3 +266,5 @@ * Write some sort of formal descriptions of the extensions offered. => see under /doc + + * Add parameterized formulas. (Pretty much like macro-functions in C) Index: doc/user-guide.txt --- doc/user-guide.txt (revision 65) +++ doc/user-guide.txt (working copy) @@ -101,8 +101,9 @@ - 1: rewriting failed (eg: it might be a bug in xrm-front) - 2: error with meta-vars (eg: undefined meta-var, redefined meta-var) - 3: arithmetic error when evaluating code (eg: division/modulo by 0) - - 4: invalid call to a builtin (eg rand(1,2,3)) + - 4: invalid call to a builtin (eg: rand(1,2,3)) - 5: invalid array access (eg: subscript is not a positive integer) + - 6: invalid call to a parameterized formula (eg: not enough arguments) - 42: internal compiler error (please send a bug report) - 51: not yet implemented @@ -308,6 +309,8 @@ XRM introduces two new builtins for generating random numbers: rand and static_rand. + o In XRM, "rand" and "static_rand" are reserved keywords and cannot be + used for identifiers. o Both rand and static_rand take either one or two arguments which must be evaluable down to simple integers at compile-time. If rand or static_rand is called with a single argument, a second @@ -350,6 +353,28 @@ in the module which called rand. The variable will be updated each time it's accessed to ensure real random numbers. + # XRM Parameterized formulas + -------------------------- + XRM formulas have been eXtended and can now be parameterized, eg: + formula isfree(int i) = p[i]=0..4,6,10; + Parameterized formulas can have 4 kinds of arguments: + o int (as in the example above) + o double + o bool + o exp + With the `exp' type, the formula behaves a bit like C's macro-functions. + We can also see that as a void type since no type-checking will be + performed on this kind of arguments. + Parameterized formulas definitions will be removed in the output PRISM + code. Invoking parameterized formulas is somewhat like calling a + function, eg: + isfree(2) will be inlined as p[2]=0..4,6,10; + However note that using the PRISM-3 calling style for builtins cannot be + used for formulas, eg: func(isfree, 2) is not supported at the moment. We + _might_ add support for this. + Once a parameterized formula has been defined, it can't be + redefined/undefined, just like a normal PRISM formula. + ************************** * XRM and Property Files * ************************** @@ -357,6 +382,8 @@ Almost all the features of the XRM language are available in eXtended Property Files. There is an exception: o The rand builtin cannot be used in property files. + It is also possible to define formulas and parameterized formulas in + XPCTL files. ********************* * Incoming features *

1 0

XRM 65: Add XRM-like formulas in eXtended PCTL.
by SIGOURE Benoit 11 Jun '06

11 Jun '06

https://svn.lrde.epita.fr/svn/xrm/trunk Index: ChangeLog from SIGOURE Benoit <sigoure.benoit(a)lrde.epita.fr> Add XRM-like formulas in eXtended PCTL. * src/lib/xpctl/pp/pp-xpctl-to-box.str: Import prism-formula. * src/str/xrm-to-prism.str: Add XRM-like formulas in eXtended PCTL. * src/str/collect-static-const-decl.str: Remove XRM-like formula definitions when gathering them. * src/syn/xrm/XRM-Formula.sdf: Hack imports so that this file can be imported from the XPCTL SDFs. * src/syn/xpctl/XPCTL-PropertiesFile.sdf: New. * src/syn/xpctl/XPCTL-Main.sdf: Import XPCTL-PropertiesFile. * doc/user-guide.txt: Add a NOTE about SdfChecker's warnings/errors. doc/user-guide.txt | 3 +++ src/lib/xpctl/pp/pp-xpctl-to-box.str | 1 + src/str/collect-static-const-decl.str | 15 ++++++++++++++- src/str/xrm-to-prism.str | 11 +++++++++-- src/syn/xpctl/XPCTL-Main.sdf | 1 + src/syn/xpctl/XPCTL-PropertiesFile.sdf | 12 ++++++++++++ src/syn/xrm/XRM-Formula.sdf | 8 ++++++-- 7 files changed, 46 insertions(+), 5 deletions(-) Index: src/lib/xpctl/pp/pp-xpctl-to-box.str --- src/lib/xpctl/pp/pp-xpctl-to-box.str (revision 64) +++ src/lib/xpctl/pp/pp-xpctl-to-box.str (working copy) @@ -6,6 +6,7 @@ XRM // signature (required since we use parts of the language) prism-constant prism-expression + prism-formula xpctl-parenthesize pctl-properties-file pctl-label Index: src/str/xrm-to-prism.str --- src/str/xrm-to-prism.str (revision 64) +++ src/str/xrm-to-prism.str (working copy) @@ -54,7 +54,7 @@ ; try(collect-formulas))) else PropertiesFile(map(try(collect-static-const-decl) - ; try(collect-formulas))) + ; try(collect-and-remove-formulas))) end | "Collecting static const and formulas", 2) @@ -104,8 +104,15 @@ /* remove array accesses: x[i] -> x_i */ // FIXME: can we make this more efficient than a complete bottomup? - ; log-timed(bottomup(try(flatten-array-access)) + ; if <is-module-file> start-symbol then + log-timed(bottomup(try(flatten-array-access)) | "Desugaring array accesses", 2) + else + /* NOTE: for XPCTL files we also need to expand use of XRM-Formulas + * because the original definition has been removed. */ + log-timed(innermost(flatten-array-access <+ ExpandFormulas) + | "Desugaring array accesses", 2) + end ; if <is-module-file> start-symbol then /* re-order modules so that all declarations appear before commands */ Index: src/str/collect-static-const-decl.str --- src/str/collect-static-const-decl.str (revision 64) +++ src/str/collect-static-const-decl.str (working copy) @@ -44,7 +44,7 @@ ; !v'{Type("bool")} => v) ; rules(ExpandStaticConsts: idf -> v) -rules +strategies collect-formulas = //?|[ formula x = e; ]| @@ -57,6 +57,19 @@ end ; rules(ExpandFormulas: x -> e) +rules + + collect-and-remove-formulas: + //?|[ formula x = e; ]| + FormulaDef(x, e) -> [] + where if <ExpandStaticConsts> x then + cannot-redefine-static-const(|x) + end + ; if <ExpandFormulas> x then + cannot-redefine-formula(|x) + end + ; rules(ExpandFormulas: x -> e) + strategies cannot-redefine-static-const(|idf) = Index: src/syn/xrm/XRM-Formula.sdf --- src/syn/xrm/XRM-Formula.sdf (revision 64) +++ src/syn/xrm/XRM-Formula.sdf (working copy) @@ -1,6 +1,10 @@ module XRM-Formula -imports PRISM-to-XRM -exports +imports + XRM-Expression + XRM-Arrays +%%imports %% import commented out so that we can import +%% PRISM-to-XRM %% XRM-MetaIfExp from XPCTL without importing +exports %% the whole PRISM stuff.. dirty hack inside! %% EBNF Grammar: Extended Formulas %% FormulaDef ::= "formula" ArrayAccess "=" Expression ";" Index: src/syn/xpctl/XPCTL-PropertiesFile.sdf --- src/syn/xpctl/XPCTL-PropertiesFile.sdf (revision 0) +++ src/syn/xpctl/XPCTL-PropertiesFile.sdf (revision 0) @@ -0,0 +1,12 @@ +module XPCTL-PropertiesFile +imports + PRISM-Formula + XRM-Formula +exports + + %% EBNF Grammar: eXtended PCTL top level stuff + %% + %% PropertiesFileSection ::= FormulaDef + + context-free syntax + FormulaDef -> PropertiesFileSection Index: src/syn/xpctl/XPCTL-Main.sdf --- src/syn/xpctl/XPCTL-Main.sdf (revision 64) +++ src/syn/xpctl/XPCTL-Main.sdf (working copy) @@ -1,6 +1,7 @@ module XPCTL-Main imports PCTL-Main + XPCTL-PropertiesFile XPCTL-MetaFor XPCTL-MetaIf XRM-Expression Index: doc/user-guide.txt --- doc/user-guide.txt (revision 64) +++ doc/user-guide.txt (working copy) @@ -61,6 +61,9 @@ /usr/lib/pkgconfig/sdf2-bundle.pc /usr/lib/pkgconfig/stratego*.pc o Then simply type `make all check' then `make install' + o NOTE: If you see many warnings/errors from SdfChecker during + compilation, don't worry, it's normal (unless it actually stops the + build) *************************** * Tools provided with XRM *

1 0

XRM 64: Use --verbose instead of --statistics.
by SIGOURE Benoit 11 Jun '06

11 Jun '06

https://svn.lrde.epita.fr/svn/xrm/trunk Index: ChangeLog from SIGOURE Benoit <sigoure.benoit(a)lrde.epita.fr> Use --verbose instead of --statistics. This cancels the note of the previous commit. * src/str/log-timed.str: Use --verbose instead of --statistics. * src/str/xrm-front.str: Change verbosity levels. log-timed.str | 6 +++--- xrm-front.str | 10 +++++----- 2 files changed, 8 insertions(+), 8 deletions(-) Index: src/str/log-timed.str --- src/str/log-timed.str (revision 63) +++ src/str/log-timed.str (working copy) @@ -14,7 +14,7 @@ ** printed. (default level=1) */ log-timed(s | msg, level) = - if <geq>(<get-config> "--statistics", level) then + if <geq>(<verbosity>(), level) then where( times => start ; print-log-msg(|msg) @@ -42,7 +42,7 @@ ** Same thing as log-timed but nothing will be printed until s finished. */ log-timed-reentrant(s | msg, level) = - if <geq>(<get-config> "--statistics", level) then + if <geq>(<verbosity>(), level) then where(times => start) ; s ; where( @@ -68,6 +68,6 @@ <concat-strings>["[ " , <log-src> , " | info ] " - , <align-left>(' ', msg, 40) // 40 = max strlen(msg) + , <align-left>(' ', msg, 36) // 36 = max strlen(msg) ] ; log-puts Index: src/str/xrm-front.str --- src/str/xrm-front.str (revision 63) +++ src/str/xrm-front.str (working copy) @@ -31,14 +31,14 @@ ; if not(<get-config> "-b") then if must-pp-aterm then // output pp-ATerms log-timed(xtc-transform(!"pp-aterm", pass-verbose) - | "pretty printed ATerms", 1) + | "pretty printed ATerms", 2) else if must-parse-pctl then // output PCTL source log-timed(xtc-transform(!"pp-pctl", pass-verbose) - | "pretty printed PCTL code", 1) + | "pretty printed PCTL code", 2) else // output PRISM source log-timed(xtc-transform(!"pp-prism", pass-verbose) - | "pretty printed PRISM code", 1) + | "pretty printed PRISM code", 2) end end end @@ -48,9 +48,9 @@ /** pipeline of transformations performed by xrm-front */ xrm-front-pipeline = where(<set-random-seed> (<time>)) - ; log-timed-reentrant(xrm-to-prism | "XRM to PRISM succeeded", 0) + ; log-timed-reentrant(xrm-to-prism | "XRM to PRISM succeeded", 2) ; if must-desugar then - log-timed(prism-desugar | "Additionnal desugarisation (-D)", 0) + log-timed(prism-desugar | "Additionnal desugarisation (-D)", 2) end /** list of available options for xrm-front */

1 0

XRM 63: Finish eXtended PCTL integration in xrm-front.
by SIGOURE Benoit 11 Jun '06

11 Jun '06

https://svn.lrde.epita.fr/svn/xrm/trunk Index: ChangeLog from SIGOURE Benoit <sigoure.benoit(a)lrde.epita.fr> Finish eXtended PCTL integration in xrm-front. NOTE: instead of using --verbose notice you should now use --statistics 1 or 2. * src/tools/parse-pctl.str: Fix a typo. * src/tools/parse-xpctl.str: Ditto. * src/lib/xrm/pp/Makefile.am: Fix dependencies. * src/lib/xpctl/pp/Makefile.am: Ditto. * src/lib/xpctl/pp/pp-xpctl-to-box.str: Fix imports. * src/str/xrm-to-prism.str: Re-organize. Use log-timed. * src/str/log-timed.str: New. * src/str/xrm-front.str: Use log-timed. * src/syn/xrm/XRM-Arrays.sdf: Dirty hack with imports. * src/syn/xrm/XRM-Expression.sdf: Ditto. * src/syn/xrm/XRM-Keywords.sdf: New. * src/syn/xrm/XRM-Main.sdf: Import XRM-Keywords. * src/syn/xrm/XRM-MetaFor.sdf: Ditto. * src/syn/xpctl/XPCTL-MetaFor.sdf: Extend ForIn with Property. * src/syn/xpctl/XPCTL-Main.sdf: Import XRM-Expression and XRM-Arrays. * tests/pctl/rivf.xpctl: New. * doc/user-guide.txt: Bring up to date. doc/user-guide.txt | 11 +++++ src/lib/xpctl/pp/Makefile.am | 8 --- src/lib/xpctl/pp/pp-xpctl-to-box.str | 3 + src/lib/xrm/pp/Makefile.am | 8 --- src/str/log-timed.str | 73 +++++++++++++++++++++++++++++++++++ src/str/xrm-front.str | 39 +++++++++--------- src/str/xrm-to-prism.str | 65 +++++++++++++++++-------------- src/syn/xpctl/XPCTL-Main.sdf | 2 src/syn/xpctl/XPCTL-MetaFor.sdf | 3 - src/syn/xrm/XRM-Arrays.sdf | 6 +- src/syn/xrm/XRM-Expression.sdf | 6 +- src/syn/xrm/XRM-Keywords.sdf | 8 +++ src/syn/xrm/XRM-Main.sdf | 1 src/syn/xrm/XRM-MetaFor.sdf | 1 src/tools/parse-pctl.str | 2 src/tools/parse-xpctl.str | 2 tests/pctl/rivf.xpctl | 12 +++++ 17 files changed, 182 insertions(+), 68 deletions(-) Index: src/tools/parse-pctl.str --- src/tools/parse-pctl.str (revision 62) +++ src/tools/parse-pctl.str (working copy) @@ -59,7 +59,7 @@ strategies /* ** We use two parse tables for performances. One of them (PCTL.tbl) has a - ** single start symbol (ModulesFile) and the other (PCTL-StartSymbols) has + ** single start symbol (PropertiesFile) and the other (PCTL-StartSymbols) has ** several other start symbols. We're doing this because start symbol ** selection happens *after* parsing in sglr. So first all the alternatives ** are parsed, and then the selected start symbol is chosen. Index: src/tools/parse-xpctl.str --- src/tools/parse-xpctl.str (revision 62) +++ src/tools/parse-xpctl.str (working copy) @@ -59,7 +59,7 @@ strategies /* ** We use two parse tables for performances. One of them (XPCTL.tbl) has a - ** single start symbol (ModulesFile) and the other (XPCTL-StartSymbols) has + ** single start symbol (PropertiesFile) and the other (XPCTL-StartSymbols) has ** several other start symbols. We're doing this because start symbol ** selection happens *after* parsing in sglr. So first all the alternatives ** are parsed, and then the selected start symbol is chosen. Index: src/lib/xrm/pp/Makefile.am --- src/lib/xrm/pp/Makefile.am (revision 62) +++ src/lib/xrm/pp/Makefile.am (working copy) @@ -5,7 +5,7 @@ ## Mail <sigoure.benoit(a)lrde.epita.fr> ## ## Started on Wed May 10 19:27:12 2006 SIGOURE Benoit -## Last update Sun Jun 11 03:26:50 2006 SIGOURE Benoit +## Last update Sun Jun 11 04:08:22 2006 SIGOURE Benoit ## include $(top_srcdir)/config/toplevel.mk @@ -29,11 +29,7 @@ EXTRA_DIST = $(wildcard *.str) $(wildcard *.meta) -SDEFS = \ - $(top_builddir)/src/syn/prism/PRISM.def \ - $(top_builddir)/src/syn/xrm/XRM.def - -xrm-parenthesize.str: $(SDEFS) +xrm-parenthesize.str: $(top_builddir)/src/syn/xrm/XRM.def $(SDF_TOOLS)/bin/sdf2parenthesize -i $< -o $@ \ -m XRM \ --omod xrm-parenthesize \ Index: src/lib/xpctl/pp/pp-xpctl-to-box.str --- src/lib/xpctl/pp/pp-xpctl-to-box.str (revision 62) +++ src/lib/xpctl/pp/pp-xpctl-to-box.str (working copy) @@ -3,6 +3,7 @@ Box XPCTL // signature PCTL // signature of the base language + XRM // signature (required since we use parts of the language) prism-constant prism-expression xpctl-parenthesize @@ -13,6 +14,8 @@ pctl-path pctl-reward pctl-filter + xrm-expression + xrm-arrays xrm-meta-for // Hack: Meta-For loops are identical in XPCTL and XRM. :) xrm-meta-if // Ditto. Index: src/lib/xpctl/pp/Makefile.am --- src/lib/xpctl/pp/Makefile.am (revision 62) +++ src/lib/xpctl/pp/Makefile.am (working copy) @@ -5,7 +5,7 @@ ## Mail <sigoure.benoit(a)lrde.epita.fr> ## ## Started on Sat Jun 10 03:59:11 2006 SIGOURE Benoit -## Last update Sun Jun 11 03:26:36 2006 SIGOURE Benoit +## Last update Sun Jun 11 04:08:59 2006 SIGOURE Benoit ## include $(top_srcdir)/config/toplevel.mk @@ -31,11 +31,7 @@ EXTRA_DIST = $(wildcard *.str) $(wildcard *.meta) -SDEFS = \ - $(top_builddir)/src/syn/pctl/PCTL.def \ - $(top_builddir)/src/syn/xpctl/XPCTL.def - -xpctl-parenthesize.str: $(SDEFS) +xpctl-parenthesize.str: $(top_builddir)/src/syn/xpctl/XPCTL.def $(SDF_TOOLS)/bin/sdf2parenthesize -i $< -o $@ \ -m XPCTL \ --omod xpctl-parenthesize \ Index: src/str/xrm-to-prism.str --- src/str/xrm-to-prism.str (revision 62) +++ src/str/xrm-to-prism.str (working copy) @@ -36,46 +36,36 @@ eval-meta-code array-decl-desugar builtin-rand + log-timed strategies xrm-to-prism = /* bind the start-symbol (ModulesFile or PropertiesFile) */ ?start-symbol#(_) - ; if <is-module-file> start-symbol then - /* remove XRM sugar, normalize some nodes */ - innermost(xrm-generic-desugar <+ DesugarRand <+ EvalRand) - else - if <is-properties-file> start-symbol then - /* rand isn't allowed in PropertiesFile hence the catch-rand */ - innermost(xrm-generic-desugar <+ catch-rand) - else - ice(|"xrm-to-prism", "Unexpected start-symbol", start-symbol) - end - end - ; notice-msg(|"xrm-to-prism: XRM sugar removed") + + ; log-timed(remove-xrm-sugar(|start-symbol) | "Removing XRM sugar", 2) /* Collect static const variables * Two goals: expand them if needed, look for variable name conflicts. */ - ; if <is-module-file> start-symbol then + ; log-timed( + if <is-module-file> start-symbol then ModulesFile(id, map(try(collect-static-const-decl) ; try(collect-formulas))) else PropertiesFile(map(try(collect-static-const-decl) ; try(collect-formulas))) end - ; notice-msg(|"xrm-to-prism: static const and formulas collected") + | "Collecting static const and formulas", 2) /* Check that meta vars are always defined in the current scope when used * and that they are not redefined twice in the same scope. This must come * AFTER collect-static-const-decl/collect-formulas since it needs some of * the information gathered by them (in DR's). */ - ; check-meta-vars - ; notice-msg(|"xrm-to-prism: meta-vars checked") + ; log-timed(check-meta-vars | "Checking meta-vars", 2) /* unroll meta loops, eval meta if */ - ; eval-meta-code - ; notice-msg(|"xrm-to-prism: eval-meta-code done") + ; log-timed(eval-meta-code | "Evaluating meta-code", 2) /*; notice-msg(|"debug: pretty printing current AST in ATerms to debug.aterm") ; where(write-to => FILE(tmp-file) ; <xtc-command(!"pp-aterm")> ["-i", tmp-file, "-o", "debug.aterm"] @@ -89,32 +79,38 @@ * This must come AFTER collect-static-const-decl since we might need * to expand an arrays which rely on static const variables. */ - ; topdown(try(array-decl-desugar); try(EvalStaticRand)) - ; notice-msg(|"xrm-to-prism: array declarations desugared") + ; log-timed(topdown(try(array-decl-desugar); try(EvalStaticRand)) + | "Desugaring array declarations", 2) /* flatten nested lists */ - ; if <is-module-file> start-symbol then + ; log-timed( + if <is-module-file> start-symbol then ModulesFile(id, flatten-list) ; ModulesFile(id, map(try(Module(id, flatten-list)))) - ; notice-msg(|"xrm-to-prism: flatten-list done") + else + PropertiesFile(flatten-list) + end + | "AST normalization (flatten-list)", 2) + ; if <is-module-file> start-symbol then + log-timed( /* get the modules that generates random numbers (XRM rand builtin) */ - ; where(bagof-RandGenModules; reverse => rand-gen-modules) + where(bagof-RandGenModules; reverse => rand-gen-modules) /* paste them at the end of the file */ ; ModulesFile(id, <conc>(<id>, rand-gen-modules)) - ; notice-msg(|"xrm-to-prism: added modules for random numbers") + | "Adding modules for random numbers", 2) end /* remove array accesses: x[i] -> x_i */ // FIXME: can we make this more efficient than a complete bottomup? - ; bottomup(try(flatten-array-access)) - ; notice-msg(|"xrm-to-prism: flatten-array-access done") + ; log-timed(bottomup(try(flatten-array-access)) + | "Desugaring array accesses", 2) ; if <is-module-file> start-symbol then /* re-order modules so that all declarations appear before commands */ - ModulesFile(id, map(try(reorder-module-contents))) - ; notice-msg(|"xrm-to-prism: reorder-module-contents done") + log-timed(ModulesFile(id, map(try(reorder-module-contents))) + | "Reordering module contents", 2) end is-module-file = ?"ModulesFile" @@ -122,6 +118,19 @@ strategies + /** remove XRM sugar, normalize some nodes */ + remove-xrm-sugar(|start-symbol) = + if <is-module-file> start-symbol then + innermost(xrm-generic-desugar <+ DesugarRand <+ EvalRand) + else + if <is-properties-file> start-symbol then + /* rand isn't allowed in PropertiesFile hence the catch-rand */ + innermost(xrm-generic-desugar <+ catch-rand) + else + ice(|"xrm-to-prism", "Unexpected start-symbol", start-symbol) + end + end + /** ** Perform generic transformations which can apply to either a ModulesFile ** or a PropertiesFile. Index: src/str/log-timed.str --- src/str/log-timed.str (revision 0) +++ src/str/log-timed.str (revision 0) @@ -0,0 +1,73 @@ +/** +** Original code from strc (The Stratego Compiler) +** by Eelco Visser <visser(a)acm.org> +*/ +module log-timed + +strategies + + /** + ** Execute and time a strategy. + ** @param s strategy to execute. + ** @param msg message to print. + ** @param level --statistics level from which the timing+msg will be + ** printed. (default level=1) + */ + log-timed(s | msg, level) = + if <geq>(<get-config> "--statistics", level) then + where( + times => start + ; print-log-msg(|msg) + ) + ; s + ; where( + <diff-times>(<times>, start) + ; <concat-strings>[" : [user=" + , <self-children-user-time + ; ticks-to-seconds + ; real-to-string(|2)> + , "s/system=" + , <self-children-sys-time + ; ticks-to-seconds + ; real-to-string(|2)> + , "s]\n" + ] + ; log-puts + ) + else + s + end + + /** + ** Same thing as log-timed but nothing will be printed until s finished. + */ + log-timed-reentrant(s | msg, level) = + if <geq>(<get-config> "--statistics", level) then + where(times => start) + ; s + ; where( + print-log-msg(|msg) + ; <diff-times>(<times>, start) + ; <concat-strings>[" : [user=" + , <self-children-user-time + ; ticks-to-seconds + ; real-to-string(|2)> + , "s/system=" + , <self-children-sys-time + ; ticks-to-seconds + ; real-to-string(|2)> + , "s]\n" + ] + ; log-puts + ) + else + s + end + + print-log-msg(|msg) = + <concat-strings>["[ " + , <log-src> + , " | info ] " + , <align-left>(' ', msg, 40) // 40 = max strlen(msg) + ] + ; log-puts Index: src/str/xrm-front.str --- src/str/xrm-front.str (revision 62) +++ src/str/xrm-front.str (working copy) @@ -5,6 +5,7 @@ tool-doc xrm-to-prism prism-desugar + log-timed strategies @@ -14,7 +15,7 @@ xrm-front-options , xrm-front-usage , xrm-front-about - , !["parse-xrm", "pp-prism", "pp-aterm"] + , !["parse-xrm", "parse-xpctl", "pp-prism", "pp-pctl", "pp-aterm"] , main-wrapped ) @@ -29,15 +30,15 @@ ; write-to ; if not(<get-config> "-b") then if must-pp-aterm then // output pp-ATerms - notice-msg(|"pretty printing ATerms") - ; xtc-transform(!"pp-aterm", pass-verbose) + log-timed(xtc-transform(!"pp-aterm", pass-verbose) + | "pretty printed ATerms", 1) else if must-parse-pctl then // output PCTL source - notice-msg(|"pretty printing PCTL code") - ; xtc-transform(!"pp-pctl", pass-verbose) + log-timed(xtc-transform(!"pp-pctl", pass-verbose) + | "pretty printed PCTL code", 1) else // output PRISM source - notice-msg(|"pretty printing PRISM code") - ; xtc-transform(!"pp-prism", pass-verbose) + log-timed(xtc-transform(!"pp-prism", pass-verbose) + | "pretty printed PRISM code", 1) end end end @@ -46,12 +47,10 @@ /** pipeline of transformations performed by xrm-front */ xrm-front-pipeline = - notice-msg(|"transformation pipeline starting") - ; where(<set-random-seed> (<time>)) - ; xrm-to-prism + where(<set-random-seed> (<time>)) + ; log-timed-reentrant(xrm-to-prism | "XRM to PRISM succeeded", 0) ; if must-desugar then - prism-desugar - ; notice-msg(|"prism-desugar finished") + log-timed(prism-desugar | "Additionnal desugarisation (-D)", 0) end /** list of available options for xrm-front */ @@ -78,7 +77,7 @@ Option("-K" + "--keep-attributes" , <set-keep-attributes> "yes" , !HelpString("-K | --keep-attributes", "Don't remove attributes when - printing ATerms (this includes positions)") + printing ATerms (this includes positions).") ) set-keep-attributes = @@ -92,7 +91,7 @@ pp-aterm-option = Option("-A" + "--pp-aterm" , <set-pp-aterm> "yes" - , !HelpString("-A | --pp-aterm", "Pretty print output with pp-aterm") + , !HelpString("-A | --pp-aterm", "Pretty print output with pp-aterm.") ) set-pp-aterm = @@ -106,7 +105,7 @@ desugar-option = Option("-D" + "--desugar" , <set-desugar> "yes" - , !HelpString("-D | --desugar", "Desugar the generated PRISM code") + , !HelpString("-D | --desugar", "Desugar the generated PRISM code.") ) set-desugar = @@ -136,18 +135,18 @@ strategies parse-pctl-option = - Option("-p" + "--pctl" + Option("-p" + "--pctl" + "--xpctl" , <set-parse-pctl> "yes" - , !HelpString("-p | --pctl", "The input file is an eXtended PCTL file") + , !HelpString("-p | --pctl", "The input file is an eXtended PCTL file.") ) set-parse-pctl = - <set-config> ("parse-pctl", <id>) + <set-config> ("parse-xpctl", <id>) must-parse-pctl = - <get-config> "parse-pctl" => "yes" + <get-config> "parse-xpctl" => "yes" - get-parser = must-parse-pctl < !"parse-pctl" + !"parse-xrm" + get-parser = must-parse-pctl < !"parse-xpctl" + !"parse-xrm" /** * Documentation Index: src/syn/xrm/XRM-Arrays.sdf --- src/syn/xrm/XRM-Arrays.sdf (revision 62) +++ src/syn/xrm/XRM-Arrays.sdf (working copy) @@ -1,7 +1,9 @@ module XRM-Arrays imports - PRISM-to-XRM -exports + XRM-Expression +%%imports %% import commented out so that we can import +%% PRISM-to-XRM %% XRM-MetaIfExp from XPCTL without importing +exports %% the whole PRISM stuff.. dirty hack inside! %% FIXME: we can probably make this look nicer. %% EBNF Grammar: Arrays Index: src/syn/xrm/XRM-Keywords.sdf --- src/syn/xrm/XRM-Keywords.sdf (revision 0) +++ src/syn/xrm/XRM-Keywords.sdf (revision 0) @@ -0,0 +1,8 @@ +module XRM-Keywords +imports PRISM-Keywords +exports + lexical syntax + "for" -> Keyword + + lexical restrictions + "for" -/- [A-Za-z0-9\_] Index: src/syn/xrm/XRM-Main.sdf --- src/syn/xrm/XRM-Main.sdf (revision 62) +++ src/syn/xrm/XRM-Main.sdf (working copy) @@ -11,3 +11,4 @@ XRM-Command XRM-Formula XRM-Constant + XRM-Keywords Index: src/syn/xrm/XRM-MetaFor.sdf --- src/syn/xrm/XRM-MetaFor.sdf (revision 62) +++ src/syn/xrm/XRM-MetaFor.sdf (working copy) @@ -2,6 +2,7 @@ imports PRISM-to-XRM XRM-Module + XRM-Keywords exports %% EBNF Grammar: Meta For Loops Index: src/syn/xrm/XRM-Expression.sdf --- src/syn/xrm/XRM-Expression.sdf (revision 62) +++ src/syn/xrm/XRM-Expression.sdf (working copy) @@ -1,7 +1,7 @@ module XRM-Expression -imports - PRISM-to-XRM -exports +%%imports %% import commented out so that we can import +%% PRISM-to-XRM %% XRM-MetaIfExp from XPCTL without importing +exports %% the whole PRISM stuff.. dirty hack inside! %% EBNF Grammar: Extended Expressions %% Expression ::= Index: src/syn/xpctl/XPCTL-MetaFor.sdf --- src/syn/xpctl/XPCTL-MetaFor.sdf (revision 62) +++ src/syn/xpctl/XPCTL-MetaFor.sdf (working copy) @@ -1,6 +1,7 @@ module XPCTL-MetaFor imports PCTL-PropertiesFile + XRM-Keywords exports %% EBNF Grammar: Meta For Loops @@ -20,5 +21,5 @@ "for" Identifier "from" Expression "to" Expression "step" Expression "do" PropertiesFileSection* "end" -> PropertiesFileSection {cons("MetaFor")} - "for" Identifier "in" {Expression ","}+ "do" + "for" Identifier "in" {Property ","}+ "do" PropertiesFileSection* "end" -> PropertiesFileSection {cons("MetaForIn")} Index: src/syn/xpctl/XPCTL-Main.sdf --- src/syn/xpctl/XPCTL-Main.sdf (revision 62) +++ src/syn/xpctl/XPCTL-Main.sdf (working copy) @@ -3,3 +3,5 @@ PCTL-Main XPCTL-MetaFor XPCTL-MetaIf + XRM-Expression + XRM-Arrays Index: tests/pctl/rivf.xpctl --- tests/pctl/rivf.xpctl (revision 0) +++ tests/pctl/rivf.xpctl (revision 0) @@ -0,0 +1,12 @@ +for i from 0 to 1200 step 100 do + P=? [ true U (t <= i & (sensor[0][0]= 4 | sensor[0][1]= 4 | sensor[0][2]= 4 + | sensor[0][3]= 4 | sensor[0][4]= 4 | sensor[0][5]= 4 | sensor[0][6]= 4 | + sensor[0][7]= 4 | sensor[0][8]= 4 | sensor[0][9]= 4 | sensor[9][0] = 4 | + sensor[9][1] = 4 | sensor[9][2] = 4 | sensor[9][3] = 4 | sensor[9][4] = 4 | + sensor[9][5] = 4 | sensor[9][6] = 4 | sensor[9][7] = 4 | sensor[9][8] = 4 | + sensor[9][9] = 4 | sensor[1][0] = 4 | sensor[2][0] = 4 | sensor[3][0] = 4 | + sensor[4][0] = 4 | sensor[5][0] = 4 | sensor[6][0] = 4 | sensor[7][0] = 4 | + sensor[8][0] = 4 | sensor[1][9] = 4 | sensor[2][9] = 4 | sensor[3][9] = 4 | + sensor[4][9] = 4 | sensor[5][9] = 4 | sensor[6][9] = 4 | sensor[7][9] = 4 | + sensor[8][9] = 4)) ] +end Index: doc/user-guide.txt --- doc/user-guide.txt (revision 62) +++ doc/user-guide.txt (working copy) @@ -89,6 +89,7 @@ -D | --desugar Desugar the generated PRISM code. --verbose notice Keep you informed about stages of the pipeline. -A | --pp-aterm Pretty print output with pp-aterm. + -p | --pctl The input file is an eXtended PCTL file. # Return value ------------ @@ -214,6 +215,8 @@ In each of these 3 cases, the variable `i' will be considered as a meta-variable, meaning it will only exists at the meta-level and won't appear in the final source code. + o The word "for" is a reserved keyword in XRM and cannot be used for an + identifier. o For Pascal-like for-loops, the fields `from', `to' and `step' must be evaluable down to simple integers at compile time. The value of the field `from' must be less than or equal to that of the field `to'. @@ -344,6 +347,14 @@ in the module which called rand. The variable will be updated each time it's accessed to ensure real random numbers. + ************************** + * XRM and Property Files * + ************************** + + Almost all the features of the XRM language are available in eXtended + Property Files. There is an exception: + o The rand builtin cannot be used in property files. + ********************* * Incoming features * *********************

1 0

XRM 62: Add the base for eXtended PCTL.
by SIGOURE Benoit 11 Jun '06

11 Jun '06

https://svn.lrde.epita.fr/svn/xrm/trunk Index: ChangeLog from SIGOURE Benoit <sigoure.benoit(a)lrde.epita.fr> Add the base for eXtended PCTL. * src/tools/Makefile.am: Add parse-xpctl and pp-xpctl. * src/tools/parse-xpctl.str: New. * src/tools/pp-xpctl.str: New. * src/sig/Makefile.am: Add signature for XPCTL. * src/lib/xrm/pp/Makefile.am: Fix dependencies. * src/lib/Makefile.am (SUBDIRS): Add xpctl. * src/syn/Makefile.am: Ditto. * src/lib/prism/pp/Makefile.am: Fix a comment. * src/lib/xpctl: New. * src/lib/xpctl/pp: New. * src/lib/xpctl/pp/pp-xpctl-to-box.str: New. * src/lib/xpctl/pp/xpctl-to-abox.str: New. * src/lib/xpctl/pp/Makefile.am: New. * src/lib/xpctl/Makefile.am: New. * src/str/xrm-to-prism.str: Make the pipe-line aware of PropertiesFile. * src/str/builtin-rand.str: Add catch-rand. * src/str/xrm-front.str: Add the -p|--pctl option for using PCTL files in xrm-front. Adapt the main-wrapped strategy. * src/syn/pctl/PCTL-Formula.sdf: Remove old comment. * src/syn/xrm/XRM-MetaIf.sdf: Move meta-if statements at the Expression level... * src/syn/xrm/XRM-MetaIfExp.sdf: ... here. * src/syn/xrm/StrategoXRM.sdf: Use StrategoPRISM. * src/syn/xrm/Makefile.am: Add XRM-MetaIfExp.sdf. * src/syn/xpctl: New. * src/syn/xpctl/XPCTL-MetaFor.sdf: New. * src/syn/xpctl/XPCTL.sdf: New. * src/syn/xpctl/XPCTL-MetaVars.sdf: New. * src/syn/xpctl/XPCTL-MetaCongruences.sdf: New. * src/syn/xpctl/XPCTL-Main.sdf: New. * src/syn/xpctl/XPCTL-MetaIf.sdf: New. * src/syn/xpctl/Makefile.am: New. * src/syn/xpctl/XPCTL-StartSymbols.sdf: New. * src/syn/xpctl/StrategoXPCTL.sdf: New. * tests/test-pp-xpctl.sh.in: New. * tests/Makefile.am: Add new tests for parse-xpctl and pp-xpctl. * tests/test-parse-xpctl.sh.in: New. * configure.ac: Add new Makefiles and test scripts. * TODO: New thing to do. TODO | 3 + configure.ac | 13 ++++- src/lib/Makefile.am | 4 - src/lib/prism/pp/Makefile.am | 4 - src/lib/xpctl/Makefile.am | 6 +- src/lib/xpctl/pp/Makefile.am | 34 ++++++++------ src/lib/xpctl/pp/pp-xpctl-to-box.str | 43 +++++++----------- src/lib/xpctl/pp/xpctl-to-abox.str | 22 ++++----- src/lib/xrm/pp/Makefile.am | 10 ++-- src/sig/Makefile.am | 15 ++++-- src/str/builtin-rand.str | 8 ++- src/str/xrm-front.str | 40 +++++++++++++---- src/str/xrm-to-prism.str | 56 ++++++++++++++++++----- src/syn/Makefile.am | 4 - src/syn/pctl/PCTL-Formula.sdf | 2 src/syn/xpctl/Makefile.am | 61 ++++++++++++-------------- src/syn/xpctl/StrategoXPCTL.sdf | 12 +++++ src/syn/xpctl/XPCTL-Main.sdf | 7 +- src/syn/xpctl/XPCTL-MetaCongruences.sdf | 1 src/syn/xpctl/XPCTL-MetaFor.sdf | 33 +++----------- src/syn/xpctl/XPCTL-MetaIf.sdf | 75 +++++--------------------------- src/syn/xpctl/XPCTL-MetaVars.sdf | 1 src/syn/xpctl/XPCTL-StartSymbols.sdf | 4 - src/syn/xpctl/XPCTL.sdf | 4 - src/syn/xrm/Makefile.am | 3 - src/syn/xrm/StrategoXRM.sdf | 20 -------- src/syn/xrm/XRM-MetaIf.sdf | 31 ------------- src/syn/xrm/XRM-MetaIfExp.sdf | 36 +++++++++++++++ src/tools/Makefile.am | 12 ++++- src/tools/parse-xpctl.str | 38 ++++++++-------- src/tools/pp-xpctl.str | 24 +++++----- tests/Makefile.am | 6 ++ tests/test-parse-xpctl.sh.in | 6 +- tests/test-pp-xpctl.sh.in | 28 +++++------ 34 files changed, 345 insertions(+), 321 deletions(-) Index: src/tools/Makefile.am --- src/tools/Makefile.am (revision 61) +++ src/tools/Makefile.am (working copy) @@ -5,7 +5,7 @@ ## Mail <sigoure.benoit(a)lrde.epita.fr> ## ## Started on Mon May 8 21:16:56 2006 SIGOURE Benoit -## Last update Sat Jun 10 04:48:43 2006 SIGOURE Benoit +## Last update Sun Jun 11 03:30:17 2006 SIGOURE Benoit ## include $(top_srcdir)/config/Transformers.mk @@ -15,9 +15,11 @@ parse-prism \ parse-pctl \ parse-xrm \ + parse-xpctl \ pp-prism \ pp-pctl \ - pp-xrm + pp-xrm \ + pp-xpctl EXTRA_DIST = $(wildcard *.str) $(wildcard *.meta) CLEANFILES = $(wildcard *.c) $(wildcard *.dep) @@ -29,9 +31,11 @@ -I $(top_srcdir)/src/lib/prism/pp \ -I $(top_srcdir)/src/lib/pctl/pp \ -I $(top_srcdir)/src/lib/xrm/pp \ + -I $(top_srcdir)/src/lib/xpctl/pp \ -I $(top_builddir)/src/lib/prism/pp \ -I $(top_builddir)/src/lib/pctl/pp \ -I $(top_builddir)/src/lib/xrm/pp \ + -I $(top_builddir)/src/lib/xpctl/pp \ -I $(top_builddir)/src/sig LDADD += $(SSL_LIBS) @@ -46,3 +50,7 @@ parse_xrm_SOURCES = parse-xrm.c pp_xrm_SOURCES = pp-xrm.c pp_xrm_LDADD = $(STRATEGO_GPP_LIBS) + +parse_xpctl_SOURCES = parse-xpctl.c +pp_xpctl_SOURCES = pp-xpctl.c +pp_xpctl_LDADD = $(STRATEGO_GPP_LIBS) Index: src/tools/parse-xpctl.str --- src/tools/parse-xpctl.str (revision 61) +++ src/tools/parse-xpctl.str (working copy) @@ -1,23 +1,23 @@ // Code mostly from parse-java by Martin Bravenboer <martin(a)cs.uu.nl> -module parse-xrm +module parse-xpctl imports libxtclib // FIXME: import libstratego-xtc for strc 0.17 tool-doc parser-common strategies - main-parse-xrm = + main-parse-xpctl = // xtc-io-wrap(extra-opts, usage, about, deps, s) xtc-io-wrap( - parse-xrm-options - , parse-xrm-usage + parse-xpctl-options + , parse-xpctl-usage , parser-about - , !["sglr", "implode-asfix", "XRM.tbl", "pp-aterm"] - , parse-xrm + , !["sglr", "implode-asfix", "XPCTL.tbl", "pp-aterm"] + , parse-xpctl ) - parse-xrm-options = + parse-xpctl-options = symbol-option + preserve-comments-option + preserve-positions-option @@ -26,7 +26,7 @@ strategies - parse-xrm = + parse-xpctl = where(?FILE(input-file-name) + !"stdin" => input-file-name) ; xtc-sglr-no-heuristics(get-parse-table, get-start-symbol) ; if must-preserve-comments then @@ -47,29 +47,29 @@ ArgOption("-s" + "--start-symbol" , set-start-symbol , !HelpString("-s | --start-symbol s", - "Start parsing with symbol s [ModulesFile]") + "Start parsing with symbol s [PropertiesFile]") ) set-start-symbol = <set-config> ("start-symbol", <id>) get-start-symbol = - <get-config> "start-symbol" <+ !"ModulesFile" + <get-config> "start-symbol" <+ !"PropertiesFile" strategies /* - ** We use two parse tables for performances. One of them (XRM.tbl) has a - ** single start symbol (ModulesFile) and the other (XRM-StartSymbols) has + ** We use two parse tables for performances. One of them (XPCTL.tbl) has a + ** single start symbol (ModulesFile) and the other (XPCTL-StartSymbols) has ** several other start symbols. We're doing this because start symbol ** selection happens *after* parsing in sglr. So first all the alternatives ** are parsed, and then the selected start symbol is chosen. */ get-parse-table = - <get-config> "parsetable"; not(?"XRM.tbl") - <+ if get-start-symbol => "ModulesFile" then - !"XRM.tbl" + <get-config> "parsetable"; not(?"XPCTL.tbl") + <+ if get-start-symbol => "PropertiesFile" then + !"XPCTL.tbl" else - !"XRM-StartSymbols.tbl" + !"XPCTL-StartSymbols.tbl" end /** @@ -77,11 +77,11 @@ */ strategies - parse-xrm-usage = + parse-xpctl-usage = <tool-doc> - [ Usage("parse-xrm [OPTIONS]") + [ Usage("parse-xpctl [OPTIONS]") , Summary( - "Parses an eXtended Reactive Module source file to an abstract syntax + "Parses an eXtended Properties source file to an abstract syntax tree in the ATerm format.") , OptionUsage() , AutoReportBugs() Index: src/tools/pp-xpctl.str --- src/tools/pp-xpctl.str (revision 61) +++ src/tools/pp-xpctl.str (working copy) @@ -1,26 +1,26 @@ // Code mostly from pp-java by Martin Bravenboer <martin(a)cs.uu.nl> -module pp-xrm +module pp-xpctl imports libstratego-lib tool-doc libstratego-gpp - pp-xrm-to-box + pp-xpctl-to-box strategies - main-pp-xrm = + main-pp-xpctl = // io-stream-wrap(extra-opts, usage, about, s) io-stream-wrap( fail - , pp-xrm-usage - , pp-xrm-about - , pp-xrm + , pp-xpctl-usage + , pp-xpctl-about + , pp-xpctl ) - pp-xrm = + pp-xpctl = ?(<read-from-stream>, out-file) - ; pp-xrm-to-abox + ; pp-xpctl-to-abox ; box2text-stream(|80, out-file) ; <fputs> ("\n", out-file) @@ -29,17 +29,17 @@ */ strategies - pp-xrm-usage = + pp-xpctl-usage = <tool-doc> - [ Usage("pp-xrm [OPTIONS]") - , Summary("Pretty-prints an eXtended Reactive Module abstract syntax + [ Usage("pp-xpctl [OPTIONS]") + , Summary("Pretty-prints an eXtended Properties abstract syntax tree in ATerm format to an eXtended Reactive Module source file.") , OptionUsage() , AutoReportBugs() ] - pp-xrm-about = + pp-xpctl-about = <tool-doc> [ AutoProgram() , Author(Person("SIGOURE Benoit", "sigoure.benoit(a)lrde.epita.fr")) Index: src/sig/Makefile.am --- src/sig/Makefile.am (revision 61) +++ src/sig/Makefile.am (working copy) @@ -5,28 +5,33 @@ ## Mail <sigoure.benoit(a)lrde.epita.fr> ## ## Started on Mon May 8 18:38:32 2006 SIGOURE Benoit -## Last update Sat Jun 10 04:43:36 2006 SIGOURE Benoit +## Last update Sun Jun 11 02:54:51 2006 SIGOURE Benoit ## include $(top_srcdir)/config/Transformers.mk pkgdata_DATA = PRISM.rtg PRISM.str \ PCTL.rtg PCTL.str \ + XPCTL.rtg XPCTL.str \ XRM.rtg XRM.str EXTRA_DIST = $(pkgdata_DATA) -CLEANFILES = $(pkgdata_DATA) PRISM.def PCTL.def XRM.def +CLEANFILES = $(pkgdata_DATA) PRISM.def PCTL.def XPCTL.def XRM.def SDF2RTG_FLAGS = --main $* PRISM.def: $(top_builddir)/src/syn/prism/PRISM.def rm -f $@ - $(LN_S) $(top_builddir)/src/syn/prism/$@ $@ + $(LN_S) $^ $@ PCTL.def: $(top_builddir)/src/syn/pctl/PCTL.def rm -f $@ - $(LN_S) $(top_builddir)/src/syn/pctl/$@ $@ + $(LN_S) $^ $@ + +XPCTL.def: $(top_builddir)/src/syn/xpctl/XPCTL.def + rm -f $@ + $(LN_S) $^ $@ XRM.def: $(top_builddir)/src/syn/xrm/XRM.def rm -f $@ - $(LN_S) $(top_builddir)/src/syn/xrm/$@ $@ + $(LN_S) $^ $@ Index: src/lib/xrm/pp/Makefile.am --- src/lib/xrm/pp/Makefile.am (revision 61) +++ src/lib/xrm/pp/Makefile.am (working copy) @@ -5,7 +5,7 @@ ## Mail <sigoure.benoit(a)lrde.epita.fr> ## ## Started on Wed May 10 19:27:12 2006 SIGOURE Benoit -## Last update Thu May 25 17:27:04 2006 SIGOURE Benoit +## Last update Sun Jun 11 03:26:50 2006 SIGOURE Benoit ## include $(top_srcdir)/config/toplevel.mk @@ -23,13 +23,17 @@ SCFLAGS = --main main-$* LDADD += $(SSL_LIBS) -# We put it in BUILT_SOURCES so that it's symlinked before we compile +# We put it in BUILT_SOURCES so that it's built before we compile # xrm-to-abox BUILT_SOURCES = xrm-parenthesize.str EXTRA_DIST = $(wildcard *.str) $(wildcard *.meta) -xrm-parenthesize.str: $(top_builddir)/src/syn/xrm/XRM.def +SDEFS = \ + $(top_builddir)/src/syn/prism/PRISM.def \ + $(top_builddir)/src/syn/xrm/XRM.def + +xrm-parenthesize.str: $(SDEFS) $(SDF_TOOLS)/bin/sdf2parenthesize -i $< -o $@ \ -m XRM \ --omod xrm-parenthesize \ Index: src/lib/Makefile.am --- src/lib/Makefile.am (revision 61) +++ src/lib/Makefile.am (working copy) @@ -5,7 +5,7 @@ ## Mail <sigoure.benoit(a)lrde.epita.fr> ## ## Started on Wed May 10 19:27:12 2006 SIGOURE Benoit -## Last update Sat Jun 10 03:57:26 2006 SIGOURE Benoit +## Last update Sun Jun 11 02:56:24 2006 SIGOURE Benoit ## -SUBDIRS = prism pctl xrm native +SUBDIRS = prism pctl xrm xpctl native Index: src/lib/prism/pp/Makefile.am --- src/lib/prism/pp/Makefile.am (revision 61) +++ src/lib/prism/pp/Makefile.am (working copy) @@ -5,7 +5,7 @@ ## Mail <sigoure.benoit(a)lrde.epita.fr> ## ## Started on Wed May 10 19:27:12 2006 SIGOURE Benoit -## Last update Thu May 25 17:26:51 2006 SIGOURE Benoit +## Last update Sun Jun 11 02:59:46 2006 SIGOURE Benoit ## include $(top_srcdir)/config/toplevel.mk @@ -22,7 +22,7 @@ SCFLAGS = --main main-$* LDADD += $(SSL_LIBS) -# We put it in BUILT_SOURCES so that it's symlinked before we compile +# We put it in BUILT_SOURCES so that it's built before we compile # prism-to-abox BUILT_SOURCES = prism-parenthesize.str Index: src/lib/xpctl/pp/pp-xpctl-to-box.str --- src/lib/xpctl/pp/pp-xpctl-to-box.str (revision 0) +++ src/lib/xpctl/pp/pp-xpctl-to-box.str (working copy) @@ -1,37 +1,30 @@ -module pp-xrm-to-box +module pp-xpctl-to-box imports Box - XRM // signature - PRISM // signature of the base language (see README) - prism-command + XPCTL // signature + PCTL // signature of the base language prism-constant - prism-declaration prism-expression - prism-formula - prism-global - prism-init - prism-module - prism-modulesfile - prism-modulesfiletype - prism-reward - prism-systemcomposition - prism-update - xrm-parenthesize - xrm-expression - xrm-module - xrm-meta-for - xrm-meta-if - xrm-arrays + xpctl-parenthesize + pctl-properties-file + pctl-label + pctl-formula + pctl-property + pctl-path + pctl-reward + pctl-filter + xrm-meta-for // Hack: Meta-For loops are identical in XPCTL and XRM. :) + xrm-meta-if // Ditto. strategies - pp-xrm-to-abox = - pp-xrm-to-abox(prism-to-box) // we keep prism-to-box as rule name + pp-xpctl-to-abox = + pp-xpctl-to-abox(prism-to-box) // we keep prism-to-box as rule name // because we simply extend it - pp-xrm-to-abox(pprules) = - // strategy from xrm-parenthesize.str generated by sdf2parenthesize - parenthesize-XRM + pp-xpctl-to-abox(pprules) = + // strategy from xpctl-parenthesize.str generated by sdf2parenthesize + parenthesize-XPCTL ; topdown(try(very-special-conflict) ; repeat(pprules)) Index: src/lib/xpctl/pp/xpctl-to-abox.str --- src/lib/xpctl/pp/xpctl-to-abox.str (revision 0) +++ src/lib/xpctl/pp/xpctl-to-abox.str (working copy) @@ -1,26 +1,26 @@ -module xrm-to-abox +module xpctl-to-abox imports libxtclib // FIXME: import libstratego-xtc for strc 0.17 tool-doc - pp-xrm-to-box + pp-xpctl-to-box strategies - main-xrm-to-abox = + main-xpctl-to-abox = // xtc-io-wrap(extra-opts, usage, about, deps, s) xtc-io-wrap( fail - , xrm-to-abox-usage - , xrm-to-abox-about + , xpctl-to-abox-usage + , xpctl-to-abox-about , ![] , main-wrapped ) - // main wrapped in main-xrm-to-abox + // main wrapped in main-xpctl-to-abox main-wrapped = // read data from input read-from - ; pp-xrm-to-abox + ; pp-xpctl-to-abox ; if <get-config> "-b" then write-to // write binary output else @@ -32,16 +32,16 @@ */ strategies - xrm-to-abox-usage = + xpctl-to-abox-usage = <tool-doc> - [ Usage("xrm-to-abox [OPTIONS]") - , Summary("Transforms an XRM abstract syntax tree in ATerm format + [ Usage("xpctl-to-abox [OPTIONS]") + , Summary("Transforms an XPCTL abstract syntax tree in ATerm format to a box representation of the AST for pretty-printing") , OptionUsage() , AutoReportBugs() ] - xrm-to-abox-about = + xpctl-to-abox-about = <tool-doc> [ AutoProgram() , Author(Person("SIGOURE Benoit", "sigoure.benoit(a)lrde.epita.fr")) Index: src/lib/xpctl/pp/Makefile.am --- src/lib/xpctl/pp/Makefile.am (revision 0) +++ src/lib/xpctl/pp/Makefile.am (working copy) @@ -1,38 +1,44 @@ ## -## Makefile.am for xrm in /home/tsuna/work/xrm/trunk/src/lib/pctl/pp +## Makefile.am for xrm in /home/tsuna/work/xrm/trunk/src/lib/xpctl/pp ## ## Made by SIGOURE Benoit ## Mail <sigoure.benoit(a)lrde.epita.fr> ## ## Started on Sat Jun 10 03:59:11 2006 SIGOURE Benoit -## Last update Sat Jun 10 04:00:21 2006 SIGOURE Benoit +## Last update Sun Jun 11 03:26:36 2006 SIGOURE Benoit ## include $(top_srcdir)/config/toplevel.mk -include $(wildcard *.dep) -pkgdata_DATA = pctl-parenthesize.str -libexec_PROGRAMS = pctl-to-abox +pkgdata_DATA = xpctl-parenthesize.str +libexec_PROGRAMS = xpctl-to-abox -pctl_to_abox_SOURCES = pctl-to-abox.c +xpctl_to_abox_SOURCES = xpctl-to-abox.c STRINCLUDES = -I $(GPP)/share/sdf/gpp -I $(GPP)/share/gpp \ -I $(top_srcdir)/src/lib/prism/pp \ + -I $(top_srcdir)/src/lib/pctl/pp \ -I $(top_builddir)/src/lib/pctl/pp -I $(srcdir) \ + -I $(top_srcdir)/src/lib/xrm/pp \ + -I $(top_builddir)/src/lib/xrm/pp -I $(srcdir) \ + -I $(top_builddir)/src/lib/xpctl/pp -I $(srcdir) \ -I $(top_builddir)/src/sig SCFLAGS = --main main-$* LDADD += $(SSL_LIBS) -# We put it in BUILT_SOURCES so that it's symlinked before we compile -# pctl-to-abox -BUILT_SOURCES = pctl-parenthesize.str +BUILT_SOURCES = xpctl-parenthesize.str EXTRA_DIST = $(wildcard *.str) $(wildcard *.meta) -pctl-parenthesize.str: $(top_builddir)/src/syn/pctl/PCTL.def +SDEFS = \ + $(top_builddir)/src/syn/pctl/PCTL.def \ + $(top_builddir)/src/syn/xpctl/XPCTL.def + +xpctl-parenthesize.str: $(SDEFS) $(SDF_TOOLS)/bin/sdf2parenthesize -i $< -o $@ \ - -m PCTL \ - --omod pctl-parenthesize \ - --sig-module $(top_builddir)/src/sig/PCTL \ - --main-strategy io-pctl-parenthesize \ - --lang PCTL + -m XPCTL \ + --omod xpctl-parenthesize \ + --sig-module $(top_builddir)/src/sig/XPCTL \ + --main-strategy io-xpctl-parenthesize \ + --lang XPCTL Index: src/lib/xpctl/Makefile.am --- src/lib/xpctl/Makefile.am (revision 0) +++ src/lib/xpctl/Makefile.am (working copy) @@ -1,11 +1,11 @@ ## -## Makefile.am for xrm in /home/tsuna/work/xrm/trunk/src/lib/pctl +## Makefile.am for xrm in /home/tsuna/work/xrm/trunk/src/lib/xpctl ## ## Made by SIGOURE Benoit ## Mail <sigoure.benoit(a)lrde.epita.fr> ## -## Started on Sat Jun 10 03:57:49 2006 SIGOURE Benoit -## Last update Sat Jun 10 03:58:01 2006 SIGOURE Benoit +## Started on Sun Jun 11 02:56:41 2006 SIGOURE Benoit +## Last update Sun Jun 11 02:56:52 2006 SIGOURE Benoit ## SUBDIRS = pp Index: src/str/xrm-to-prism.str --- src/str/xrm-to-prism.str (revision 61) +++ src/str/xrm-to-prism.str (working copy) @@ -27,7 +27,8 @@ */ module xrm-to-prism imports - XRM + XRM // signature + PCTL // signature collect-static-const-decl prism-desugar flatten-array-access @@ -39,20 +40,30 @@ strategies xrm-to-prism = + /* bind the start-symbol (ModulesFile or PropertiesFile) */ + ?start-symbol#(_) + ; if <is-module-file> start-symbol then /* remove XRM sugar, normalize some nodes */ - innermost( - DesugarRightShift <+ DesugarLeftShift - <+ DesugarImplicitForStep <+ DesugarImplicitElse - <+ DesugarRand <+ EvalRand - /*FIXME: to be implemented. - <+ DesugarArrayEq <+ DesugarArrayNotEq - <+ DesugarArrayExistsEq <+ DesugarArrayExistsNotEq*/ - ) + innermost(xrm-generic-desugar <+ DesugarRand <+ EvalRand) + else + if <is-properties-file> start-symbol then + /* rand isn't allowed in PropertiesFile hence the catch-rand */ + innermost(xrm-generic-desugar <+ catch-rand) + else + ice(|"xrm-to-prism", "Unexpected start-symbol", start-symbol) + end + end ; notice-msg(|"xrm-to-prism: XRM sugar removed") /* Collect static const variables * Two goals: expand them if needed, look for variable name conflicts. */ - ; ModulesFile(id, map(try(collect-static-const-decl); try(collect-formulas))) + ; if <is-module-file> start-symbol then + ModulesFile(id, map(try(collect-static-const-decl) + ; try(collect-formulas))) + else + PropertiesFile(map(try(collect-static-const-decl) + ; try(collect-formulas))) + end ; notice-msg(|"xrm-to-prism: static const and formulas collected") /* Check that meta vars are always defined in the current scope when used @@ -82,7 +93,8 @@ ; notice-msg(|"xrm-to-prism: array declarations desugared") /* flatten nested lists */ - ; ModulesFile(id, flatten-list) + ; if <is-module-file> start-symbol then + ModulesFile(id, flatten-list) ; ModulesFile(id, map(try(Module(id, flatten-list)))) ; notice-msg(|"xrm-to-prism: flatten-list done") @@ -92,15 +104,35 @@ /* paste them at the end of the file */ ; ModulesFile(id, <conc>(<id>, rand-gen-modules)) ; notice-msg(|"xrm-to-prism: added modules for random numbers") + end /* remove array accesses: x[i] -> x_i */ // FIXME: can we make this more efficient than a complete bottomup? ; bottomup(try(flatten-array-access)) ; notice-msg(|"xrm-to-prism: flatten-array-access done") + ; if <is-module-file> start-symbol then /* re-order modules so that all declarations appear before commands */ - ; ModulesFile(id, map(try(reorder-module-contents))) + ModulesFile(id, map(try(reorder-module-contents))) ; notice-msg(|"xrm-to-prism: reorder-module-contents done") + end + + is-module-file = ?"ModulesFile" + is-properties-file = ?"PropertiesFile" + +strategies + + /** + ** Perform generic transformations which can apply to either a ModulesFile + ** or a PropertiesFile. + */ + xrm-generic-desugar = + DesugarRightShift <+ DesugarLeftShift + <+ DesugarImplicitForStep <+ DesugarImplicitElse + /*FIXME: to be implemented. + <+ DesugarArrayEq <+ DesugarArrayNotEq + <+ DesugarArrayExistsEq <+ DesugarArrayExistsNotEq + */ rules Index: src/str/builtin-rand.str --- src/str/builtin-rand.str (revision 61) +++ src/str/builtin-rand.str (working copy) @@ -114,10 +114,16 @@ invalid-call-to-rand-non-int = err-msg(|<concat-strings>["invalid call to XRM builtin: rand's", - " arguments must be statically evaluable"]) + " arguments must be statically evaluable."]) ; debug ; <xtc-exit> 4 + /** Issue an error if rand is called in a property file */ + catch-rand = + ?Rand(_) + ; err-msg(|"you cannot use the XRM builtin rand in a property file.") + ; <xtc-exit> 4 + strategies /** Index: src/str/xrm-front.str --- src/str/xrm-front.str (revision 61) +++ src/str/xrm-front.str (working copy) @@ -20,22 +20,29 @@ main-wrapped = check-options - ; xtc-transform(!"parse-xrm", // parse input (returns a FILE) + ; xtc-transform(get-parser, // parse input (returns a FILE) <concat>[ ["-b"], <pass-verbose>(), <pass-add-pos>() ]) ; read-from // read parsed input ; xrm-front-pipeline // transformations ; if not(must-keep-attributes) then strip-annos end - ; if <get-config> "-b" then - write-to // output binary ATerms - else + /* save the current term in a /tmp file with binary ATerms */ + ; write-to + ; if not(<get-config> "-b") then if must-pp-aterm then // output pp-ATerms notice-msg(|"pretty printing ATerms") - ; write-to; xtc-transform(!"pp-aterm", pass-verbose) + ; xtc-transform(!"pp-aterm", pass-verbose) + else + if must-parse-pctl then // output PCTL source + notice-msg(|"pretty printing PCTL code") + ; xtc-transform(!"pp-pctl", pass-verbose) else // output PRISM source notice-msg(|"pretty printing PRISM code") - ; write-to; xtc-transform(!"pp-prism", pass-verbose) + ; xtc-transform(!"pp-prism", pass-verbose) + end end end + /* default: if we don't get inside the previous if, we will output + * binary ATerms. */ /** pipeline of transformations performed by xrm-front */ xrm-front-pipeline = @@ -53,6 +60,7 @@ + add-pos-option + keep-attributes-option + desugar-option + + parse-pctl-option /** checks the options are consistent */ check-options = @@ -125,6 +133,22 @@ pass-add-pos = must-add-pos < !["--preserve-positions"] + ![] +strategies + + parse-pctl-option = + Option("-p" + "--pctl" + , <set-parse-pctl> "yes" + , !HelpString("-p | --pctl", "The input file is an eXtended PCTL file") + ) + + set-parse-pctl = + <set-config> ("parse-pctl", <id>) + + must-parse-pctl = + <get-config> "parse-pctl" => "yes" + + get-parser = must-parse-pctl < !"parse-pctl" + !"parse-xrm" + /** * Documentation */ @@ -133,8 +157,8 @@ xrm-front-usage = <tool-doc> [ Usage("xrm-front [OPTIONS]") - , Summary("Transforms an eXtended Reactive Module source file in a - PRISM-equivalent source code (default) or abstract syntax + , Summary("Transforms an eXtended Reactive Module or Property source file + in a PRISM-equivalent source code (default) or abstract syntax tree. (see option -A)") , OptionUsage() , AutoReportBugs() Index: src/syn/pctl/PCTL-Formula.sdf --- src/syn/pctl/PCTL-Formula.sdf (revision 61) +++ src/syn/pctl/PCTL-Formula.sdf (working copy) @@ -15,8 +15,6 @@ %% %% PCTLFormula ::= PCTLImplies %% - %% PCTLImplies ::= PCTLOr ["=>" PCTLOr] - %% sorts Formula context-free syntax Index: src/syn/xrm/XRM-MetaIf.sdf --- src/syn/xrm/XRM-MetaIf.sdf (revision 61) +++ src/syn/xrm/XRM-MetaIf.sdf (working copy) @@ -2,6 +2,7 @@ imports PRISM-to-XRM XRM-Module + XRM-MetaIfExp exports %% EBNF Grammar: Meta if-then-else @@ -22,19 +23,6 @@ %% "else" %% {DeclarationOrCommand} %% "end" - %% - %% (* if-then-else inside expressions *) - %% (* NOTE: it's not possible to have more than 1 exp in the then-part - %% * and else-part of the meta-if statements for expression. This is - %% * because the current base and extended language don't have real - %% * statements nor sequences of expressions. *) - %% Expression ::= - %% "if" Expression "then" Expression "end" - %% | "if" Expression "then" - %% Expression - %% "else" - %% Expression - %% "end" context-free syntax @@ -61,20 +49,3 @@ "else" DeclarationOrCommand* "end" -> DeclarationOrCommand {cons("MetaIf")} - - %% NOTE: it's not possible to have more than 1 exp in the then-part - %% and else-part of the meta-if statements for expression. This is - %% because the current base and extended language don't have real - %% statements nor sequences of expressions. - context-free syntax - - %% if-then within expressions - "if" Expression "then" Expression "end" - -> Expression {cons("MetaIf")} - - %% if-then-else within expressions - "if" Expression "then" - Expression - "else" - Expression - "end" -> Expression {cons("MetaIf")} Index: src/syn/xrm/StrategoXRM.sdf --- src/syn/xrm/StrategoXRM.sdf (revision 61) +++ src/syn/xrm/StrategoXRM.sdf (working copy) @@ -1,32 +1,14 @@ module StrategoXRM imports - StrategoRenamed + StrategoPRISM XRM PRISM-MetaVars PRISM-MetaCongruences XRM-MetaVars XRM-MetaCongruences - XRM-MetaFor - XRM-MetaIf exports - context-free start-symbols StrategoModule context-free syntax - - "|[" Module "]|" -> StrategoTerm {prefer,cons("ToTerm")} - "|[" RenamedModule "]|" -> StrategoTerm {prefer,cons("ToTerm")} - "|[" Expression "]|" -> StrategoTerm {prefer,cons("ToTerm")} - "|[" Declaration "]|" -> StrategoTerm {prefer,cons("ToTerm")} - "|[" Command "]|" -> StrategoTerm {prefer,cons("ToTerm")} "|[" MetaFor "]|" -> StrategoTerm {prefer,cons("ToTerm")} "|[" MetaIf "]|" -> StrategoTerm {prefer,cons("ToTerm")} - - context-free syntax - - "~" StrategoTerm -> Expression {prefer,cons("FromTerm")} - "~id:" StrategoTerm -> ID {prefer,cons("FromTerm")} - %% FIXME: the following rule is b0rken - "~id':" StrategoTerm -> IdentifierPrime {prefer,cons("FromTerm")} - "~int:" StrategoTerm -> LInt {prefer,cons("FromTerm")} - "~double:" StrategoTerm -> LDouble {prefer,cons("FromTerm")} Index: src/syn/xrm/XRM-MetaIfExp.sdf --- src/syn/xrm/XRM-MetaIfExp.sdf (revision 0) +++ src/syn/xrm/XRM-MetaIfExp.sdf (revision 0) @@ -0,0 +1,36 @@ +module XRM-MetaIfExp +%%imports %% import commented out so that we can import +%% PRISM-to-XRM %% XRM-MetaIfExp from XPCTL without importing +exports %% the whole PRISM stuff.. dirty hack inside! + + %% EBNF Grammar: Meta if-then-else + %% + %% (* if-then-else inside expressions *) + %% (* NOTE: it's not possible to have more than 1 exp in the then-part + %% * and else-part of the meta-if statements for expression. This is + %% * because the current base and extended language don't have real + %% * statements nor sequences of expressions. *) + %% Expression ::= + %% "if" Expression "then" Expression "end" + %% | "if" Expression "then" + %% Expression + %% "else" + %% Expression + %% "end" + + %% NOTE: it's not possible to have more than 1 exp in the then-part + %% and else-part of the meta-if statements for expression. This is + %% because the current base and extended language don't have real + %% statements nor sequences of expressions. + context-free syntax + + %% if-then within expressions + "if" Expression "then" Expression "end" + -> Expression {cons("MetaIf")} + + %% if-then-else within expressions + "if" Expression "then" + Expression + "else" + Expression + "end" -> Expression {cons("MetaIf")} Index: src/syn/xrm/Makefile.am --- src/syn/xrm/Makefile.am (revision 61) +++ src/syn/xrm/Makefile.am (working copy) @@ -5,7 +5,7 @@ ## Mail <sigoure.benoit(a)lrde.epita.fr> ## ## Started on Thu Apr 27 17:40:41 2006 SIGOURE Benoit -## Last update Sat Jun 10 00:20:27 2006 SIGOURE Benoit +## Last update Sun Jun 11 02:39:02 2006 SIGOURE Benoit ## include $(top_srcdir)/config/Transformers.mk @@ -53,6 +53,7 @@ XRM-MetaCongruences.sdf \ XRM-MetaFor.sdf \ XRM-MetaIf.sdf \ + XRM-MetaIfExp.sdf \ XRM-MetaVars.sdf \ XRM-Module.sdf \ XRM-StartSymbols.sdf \ Index: src/syn/Makefile.am --- src/syn/Makefile.am (revision 61) +++ src/syn/Makefile.am (working copy) @@ -5,7 +5,7 @@ ## Mail <sigoure.benoit(a)lrde.epita.fr> ## ## Started on Thu Apr 27 17:40:41 2006 SIGOURE Benoit -## Last update Fri Jun 9 19:16:48 2006 SIGOURE Benoit +## Last update Sun Jun 11 02:30:13 2006 SIGOURE Benoit ## -SUBDIRS = prism pctl xrm +SUBDIRS = prism pctl xrm xpctl Index: src/syn/xpctl/XPCTL-MetaFor.sdf --- src/syn/xpctl/XPCTL-MetaFor.sdf (revision 0) +++ src/syn/xpctl/XPCTL-MetaFor.sdf (working copy) @@ -1,41 +1,24 @@ -module XRM-MetaFor +module XPCTL-MetaFor imports - PRISM-to-XRM - XRM-Module + PCTL-PropertiesFile exports %% EBNF Grammar: Meta For Loops %% (* Meta For loops at the top level *) - %% ModulesFileSection ::= + %% PropertiesFileSection ::= %% "for" Identifier "from" Expression "to" Expression %% ["step" Expression] "do" - %% {ModulesFileSection} "end" + %% {PropertiesFileSection} "end" %% - %% (* Meta For loops inside modules *) - %% DeclarationOrCommand ::= - %% "for" Identifier "from" Expression "to" Expression - %% ["step" Expression] "do" - %% {DeclarationOrCommand} "end" context-free syntax %% This MetaFor can be found only at top-level - %% So we can see it as a ModulesFileSection - "for" Identifier "from" Expression "to" Expression "do" - ModulesFileSection* "end" -> ModulesFileSection {cons("MetaFor")} - - "for" Identifier "from" Expression "to" Expression "step" Expression "do" - ModulesFileSection* "end" -> ModulesFileSection {cons("MetaFor")} - - "for" Identifier "in" {Expression ","}+ "do" - ModulesFileSection* "end" -> ModulesFileSection {cons("MetaForIn")} - - %% This MetaFor can be found only inside Modules - %% So we can see it as a DeclarationOrCommand + %% So we can see it as a PropertiesFileSection "for" Identifier "from" Expression "to" Expression "do" - DeclarationOrCommand* "end" -> DeclarationOrCommand {cons("MetaFor")} + PropertiesFileSection* "end" -> PropertiesFileSection {cons("MetaFor")} "for" Identifier "from" Expression "to" Expression "step" Expression "do" - DeclarationOrCommand* "end" -> DeclarationOrCommand {cons("MetaFor")} + PropertiesFileSection* "end" -> PropertiesFileSection {cons("MetaFor")} "for" Identifier "in" {Expression ","}+ "do" - ModulesFileSection* "end" -> DeclarationOrCommand {cons("MetaForIn")} + PropertiesFileSection* "end" -> PropertiesFileSection {cons("MetaForIn")} Index: src/syn/xpctl/XPCTL.sdf --- src/syn/xpctl/XPCTL.sdf (revision 0) +++ src/syn/xpctl/XPCTL.sdf (working copy) @@ -2,9 +2,9 @@ %% This is because, unfortunately, start symbol selection happens *after* %% parsing in sglr. So first all the alternatives are parsed, and then %% the selected start symbol is chosen. -module PCTL +module XPCTL imports - PCTL-Main + XPCTL-Main exports context-free start-symbols Index: src/syn/xpctl/XPCTL-MetaVars.sdf --- src/syn/xpctl/XPCTL-MetaVars.sdf (revision 0) +++ src/syn/xpctl/XPCTL-MetaVars.sdf (revision 0) @@ -0,0 +1 @@ +module XPCTL-MetaVars Index: src/syn/xpctl/XPCTL-MetaCongruences.sdf --- src/syn/xpctl/XPCTL-MetaCongruences.sdf (revision 0) +++ src/syn/xpctl/XPCTL-MetaCongruences.sdf (revision 0) @@ -0,0 +1 @@ +module XPCTL-MetaCongruences Index: src/syn/xpctl/XPCTL-Main.sdf --- src/syn/xpctl/XPCTL-Main.sdf (revision 0) +++ src/syn/xpctl/XPCTL-Main.sdf (working copy) @@ -1,4 +1,5 @@ -module PCTL-Main +module XPCTL-Main imports - PRISM-Layout - PCTL-PropertiesFile + PCTL-Main + XPCTL-MetaFor + XPCTL-MetaIf Index: src/syn/xpctl/XPCTL-MetaIf.sdf --- src/syn/xpctl/XPCTL-MetaIf.sdf (revision 0) +++ src/syn/xpctl/XPCTL-MetaIf.sdf (working copy) @@ -1,80 +1,29 @@ -module XRM-MetaIf +module XPCTL-MetaIf imports - PRISM-to-XRM - XRM-Module + PCTL-PropertiesFile + XRM-MetaIfExp exports %% EBNF Grammar: Meta if-then-else %% (* if-then-else at top-level *) - %% ModulesFileSection ::= - %% "if" Expression "then" {ModulesFileSection} "end" + %% PropertiesFile ::= + %% "if" Expression "then" {PropertiesFile} "end" %% | "if" Expression "then" - %% {ModulesFileSection} + %% {PropertiesFile} %% "else" - %% {ModulesFileSection} + %% {PropertiesFile} %% "end" %% - %% (* if-then-else inside modules *) - %% DeclarationOrCommand ::= - %% "if" Expression "then" {DeclarationOrCommand} "end" - %% | "if" Expression "then" - %% {DeclarationOrCommand} - %% "else" - %% {DeclarationOrCommand} - %% "end" - %% - %% (* if-then-else inside expressions *) - %% (* NOTE: it's not possible to have more than 1 exp in the then-part - %% * and else-part of the meta-if statements for expression. This is - %% * because the current base and extended language don't have real - %% * statements nor sequences of expressions. *) - %% Expression ::= - %% "if" Expression "then" Expression "end" - %% | "if" Expression "then" - %% Expression - %% "else" - %% Expression - %% "end" context-free syntax %% if-then at top-level - "if" Expression "then" ModulesFileSection* "end" - -> ModulesFileSection {cons("MetaIf")} + "if" Expression "then" PropertiesFile* "end" + -> PropertiesFile {cons("MetaIf")} %% if-then-else at top-level "if" Expression "then" - ModulesFileSection* - "else" - ModulesFileSection* - "end" -> ModulesFileSection {cons("MetaIf")} - - context-free syntax - - %% if-then within modules - "if" Expression "then" DeclarationOrCommand* "end" - -> DeclarationOrCommand {cons("MetaIf")} - - %% if-then-else within modules - "if" Expression "then" - DeclarationOrCommand* - "else" - DeclarationOrCommand* - "end" -> DeclarationOrCommand {cons("MetaIf")} - - %% NOTE: it's not possible to have more than 1 exp in the then-part - %% and else-part of the meta-if statements for expression. This is - %% because the current base and extended language don't have real - %% statements nor sequences of expressions. - context-free syntax - - %% if-then within expressions - "if" Expression "then" Expression "end" - -> Expression {cons("MetaIf")} - - %% if-then-else within expressions - "if" Expression "then" - Expression + PropertiesFile* "else" - Expression - "end" -> Expression {cons("MetaIf")} + PropertiesFile* + "end" -> PropertiesFile {cons("MetaIf")} Index: src/syn/xpctl/Makefile.am --- src/syn/xpctl/Makefile.am (revision 0) +++ src/syn/xpctl/Makefile.am (working copy) @@ -1,11 +1,11 @@ ## -## Makefile.am for xrm in /home/tsuna/work/xrm/trunk/src/syn/pctl +## Makefile.am for xrm in /home/tsuna/work/xrm/trunk/src/syn/xpctl ## ## Made by SIGOURE Benoit ## Mail <sigoure.benoit(a)lrde.epita.fr> ## ## Started on Sat Jun 10 00:17:31 2006 SIGOURE Benoit -## Last update Sat Jun 10 00:36:56 2006 SIGOURE Benoit +## Last update Sun Jun 11 02:42:19 2006 SIGOURE Benoit ## include $(top_srcdir)/config/Transformers.mk @@ -17,49 +17,46 @@ STRINCLUDES = -I $(srcdir) SDFINCLUDES = -I $(srcdir) \ -I $(STRATEGO_FRONT)/share/sdf/stratego-front \ - -I $(top_srcdir)/src/syn/prism + -I $(top_srcdir)/src/syn/prism \ + -I $(top_srcdir)/src/syn/xrm \ + -I $(top_srcdir)/src/syn/pctl pkgdata_DATA_built = \ - PCTL.def \ - PCTL.tbl \ - PCTL.rtg \ - PCTL.str \ - PCTL-StartSymbols.tbl \ - PCTL-Prefixed.def \ - StrategoPCTL.def \ - StrategoPCTL.tbl + XPCTL.def \ + XPCTL.tbl \ + XPCTL.rtg \ + XPCTL.str \ + XPCTL-StartSymbols.tbl \ + XPCTL-Prefixed.def \ + StrategoXPCTL.def \ + StrategoXPCTL.tbl pkgdata_DATA = $(pkgdata_DATA_built) sdfdata_DATA = $(pkgdata_DATA_built) -nobase_sdfdata_DATA = PCTL-Prefixed.sdf $(SDFS) +nobase_sdfdata_DATA = XPCTL-Prefixed.sdf $(SDFS) CLEANFILES = $(pkgdata_DATA_built) \ $(wildcard *.dep) \ - PCTL.{c,str,c.dep} \ - PCTL-StartSymbols.def \ - PCTL-Prefixed.def + XPCTL.{c,str,c.dep} \ + XPCTL-StartSymbols.def \ + XPCTL-Prefixed.def SDFS = \ - PCTL-Filter.sdf \ - PCTL-Formula.sdf \ - PCTL-Label.sdf \ - PCTL-Main.sdf \ - PCTL-Path.sdf \ - PCTL-PropertiesFile.sdf \ - PCTL-Property.sdf \ - PCTL-Reward.sdf \ - PCTL-StartSymbols.sdf \ - PCTL.sdf + XPCTL-Main.sdf \ + XPCTL-MetaFor.sdf \ + XPCTL-MetaIf.sdf \ + XPCTL-StartSymbols.sdf \ + XPCTL.sdf EXTRA_DIST = $(SDFS) -PCTL.def: $(SDFS) -PCTL-StartSymbols.def: $(SDFS) +XPCTL.def: $(SDFS) +XPCTL-StartSymbols.def: $(SDFS) -StrategoPCTL.def: StrategoPCTL.sdf \ - PCTL-MetaVars.sdf \ - PCTL-MetaCongruences.sdf +StrategoXPCTL.def: StrategoXPCTL.sdf \ + XPCTL-MetaVars.sdf \ + XPCTL-MetaCongruences.sdf -PCTL-Prefixed.sdf: PCTL.def +XPCTL-Prefixed.sdf: XPCTL.def $(SDF_TOOLS)/bin/gen-renamed-sdf-module -i $< -o $@ \ - --main PCTL --name PCTL-Prefixed --prefix PCTL + --main XPCTL --name XPCTL-Prefixed --prefix XPCTL Index: src/syn/xpctl/XPCTL-StartSymbols.sdf --- src/syn/xpctl/XPCTL-StartSymbols.sdf (revision 0) +++ src/syn/xpctl/XPCTL-StartSymbols.sdf (working copy) @@ -2,9 +2,9 @@ %% This is because, unfortunately, start symbol selection happens *after* %% parsing in sglr. So first all the alternatives are parsed, and then %% the selected start symbol is chosen. -module PCTL-StartSymbols +module XPCTL-StartSymbols imports - PCTL-Main + XPCTL-Main exports context-free start-symbols Index: src/syn/xpctl/StrategoXPCTL.sdf --- src/syn/xpctl/StrategoXPCTL.sdf (revision 0) +++ src/syn/xpctl/StrategoXPCTL.sdf (revision 0) @@ -0,0 +1,12 @@ +module StrategoXPCTL +imports + StrategoPCTL + XPCTL + XPCTL-MetaVars + XPCTL-MetaCongruences + +exports + + context-free syntax + "|[" MetaFor "]|" -> StrategoTerm {prefer,cons("ToTerm")} + "|[" MetaIf "]|" -> StrategoTerm {prefer,cons("ToTerm")} Index: tests/test-pp-xpctl.sh.in --- tests/test-pp-xpctl.sh.in (revision 61) +++ tests/test-pp-xpctl.sh.in (working copy) @@ -1,6 +1,6 @@ #!/bin/sh ## -## test-pp-xrm.sh for xrm in /home/tsuna/work/xrm/trunk/tests +## test-pp-xpctl.sh for xrm in /home/tsuna/work/xrm/trunk/tests ## ## Made by SIGOURE Benoit ## Mail <sigoure.benoit(a)lrde.epita.fr> @@ -11,7 +11,7 @@ test_cnt=0 test_pass=0 -target_dir='output-pp-xrm' +target_dir='output-pp-xpctl' rm -f failed_tests.$$ test ! -d $target_dir && { mkdir $target_dir \ @@ -21,15 +21,15 @@ outdir="`pwd`" cd .. -for file in `find "@srcdir@" -name '*.pm' -o -name '*.nm' -o -name '*.sm' -o -name '*.xpm' | sort`; do +for file in `find "@srcdir@" -name '*.pctl' -o -name '*.csl' -o -name '*.xpctl' -o -name '*.xcsl' | sort`; do basefile="`basename $file`" - bfile="`echo \"$basefile\" | sed 's/\.x\?pm$//'`" + bfile="`echo \"$basefile\" | sed 's/\.x\?pctl$//;s/\.x\?csl//'`" echo ">>> Starting the test for $basefile" test_cnt=$((test_cnt + 1)) echo @ECHO_N@ " Parsing $basefile ... " - "@top_builddir@/src/tools/parse-xrm" -i "$file" -o "$outdir/$bfile.aterm" + "@top_builddir@/src/tools/parse-xpctl" -i "$file" -o "$outdir/$bfile.aterm" if [ $? -ne 0 ]; then echo 'FAILED, continuing with the next test...' echo " * $file: parsing FAILED" >> failed_tests.$$ @@ -38,8 +38,8 @@ echo 'OK, no ambiguities found' echo @ECHO_N@ " Pretty printing $basefile ... " - "@top_builddir@/src/tools/pp-xrm" \ - -i "$outdir/$bfile.aterm" -o "$outdir/$bfile.pp.xpm" + "@top_builddir@/src/tools/pp-xpctl" \ + -i "$outdir/$bfile.aterm" -o "$outdir/$bfile.pp.xpctl" if [ $? -ne 0 ]; then echo 'FAILED, continuing with the next test...' echo " * $file: pretty printing FAILED" >> failed_tests.$$ @@ -48,12 +48,12 @@ echo 'OK' echo @ECHO_N@ " Re-Parsing pretty printed file $basefile ... " - "@top_builddir@/src/tools/parse-xrm" \ - -i "$outdir/$bfile.pp.xpm" -o "$outdir/$bfile.pp2aterm" + "@top_builddir@/src/tools/parse-xpctl" \ + -i "$outdir/$bfile.pp.xpctl" -o "$outdir/$bfile.pp2aterm" if [ $? -ne 0 ]; then echo 'FAILED, here is the content of the file:' echo '>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>' - cat -n "$outdir/$bfile.pp.xpm" + cat -n "$outdir/$bfile.pp.xpctl" echo '<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<' echo 'Now continuing with the next test...' echo " * $file: re-parsing FAILED" >> failed_tests.$$ @@ -62,8 +62,8 @@ echo 'OK, no ambiguities found' echo @ECHO_N@ " Re-Pretty printing the re-parsed file $basefile ... " - "@top_builddir@/src/tools/pp-xrm" \ - -i "$outdir/$bfile.pp2aterm" -o "$outdir/$bfile.pp2.xpm" + "@top_builddir@/src/tools/pp-xpctl" \ + -i "$outdir/$bfile.pp2aterm" -o "$outdir/$bfile.pp2.xpctl" if [ $? -ne 0 ]; then echo 'FAILED, continuing with the next test...' echo " * $file: re-pretty printing FAILED" >> failed_tests.$$ @@ -73,7 +73,7 @@ err='' diff -q "$outdir/$bfile.aterm" "$outdir/$bfile.pp2aterm" || err='aterm' - diff -q "$outdir/$bfile.pp.xpm" "$outdir/$bfile.pp2.xpm" || err="$err+pp" + diff -q "$outdir/$bfile.pp.xpctl" "$outdir/$bfile.pp2.xpctl" || err="$err+pp" case $err in *aterm*) @@ -88,7 +88,7 @@ ;; *pp*) echo 'FAILED: the two pretty printing did NOT produce the same source:' - diff -u "$outdir/$bfile.pp.xpm" "$outdir/$bfile.pp2.xpm" + diff -u "$outdir/$bfile.pp.xpctl" "$outdir/$bfile.pp2.xpctl" echo " * $file: both pretty pretty did NIT produce the same source" >> failed_tests.$$ continue ;; Index: tests/Makefile.am --- tests/Makefile.am (revision 61) +++ tests/Makefile.am (working copy) @@ -5,7 +5,7 @@ ## Mail <sigoure.benoit(a)lrde.epita.fr> ## ## Started on Thu Apr 27 16:56:50 2006 SIGOURE Benoit -## Last update Sat Jun 10 05:24:43 2006 SIGOURE Benoit +## Last update Sun Jun 11 03:40:50 2006 SIGOURE Benoit ## #include $(top_srcdir)/config/toplevel.mk @@ -14,9 +14,11 @@ test-parse-prism.sh \ test-parse-pctl.sh \ test-parse-xrm.sh \ + test-parse-xpctl.sh \ test-pp-prism.sh \ test-pp-pctl.sh \ test-pp-xrm.sh \ + test-pp-xpctl.sh \ test-xrm-front.sh # Set the XTC_REPOSITORY environment variable so that we override the XTC @@ -29,9 +31,11 @@ TESTS = test-parse-prism.sh \ test-parse-pctl.sh \ test-parse-xrm.sh \ + test-parse-xpctl.sh \ test-pp-prism.sh \ test-pp-pctl.sh \ test-pp-xrm.sh \ + test-pp-xpctl.sh \ test-xrm-front.sh \ test-summary.sh Index: tests/test-parse-xpctl.sh.in --- tests/test-parse-xpctl.sh.in (revision 61) +++ tests/test-parse-xpctl.sh.in (working copy) @@ -1,6 +1,6 @@ #!/bin/sh ## -## test-parse-xrm.sh for xrm in /home/tsuna/work/xrm/trunk/tests +## test-parse-xpctl.sh for xrm in /home/tsuna/work/xrm/trunk/tests ## ## Made by SIGOURE Benoit ## Mail <sigoure.benoit(a)lrde.epita.fr> @@ -13,9 +13,9 @@ test_pass=0 rm -f failed_tests.$$ -for file in `find "@srcdir@" -name '*.pm' -o -name '*.nm' -o -name '*.sm' -o -name '*.xpm' | sort`; do +for file in `find "@srcdir@" -name '*.pctl' -o -name '*.csl' -o -name '*.xpctl' -o -name '*.xcsl' | sort`; do echo @ECHO_N@ " Parsing `basename $file` ... " - "@top_builddir@/src/tools/parse-xrm" -i "$file" -o /dev/null + "@top_builddir@/src/tools/parse-xpctl" -i "$file" -o /dev/null rv=$? test_cnt=$((test_cnt + 1)) if [ $? -eq 0 ]; then Index: configure.ac --- configure.ac (revision 61) +++ configure.ac (working copy) @@ -5,7 +5,7 @@ ## Mail <sigoure.benoit(a)lrde.epita.fr> ## ## Started on Thu Apr 27 15:55:56 2006 SIGOURE Benoit -## Last update Sat Jun 10 05:25:09 2006 SIGOURE Benoit +## Last update Sun Jun 11 03:38:49 2006 SIGOURE Benoit ## ## --------------- ## @@ -75,6 +75,7 @@ src/syn/prism/Makefile src/syn/pctl/Makefile src/syn/xrm/Makefile + src/syn/xpctl/Makefile src/sig/Makefile src/str/Makefile src/lib/Makefile @@ -84,6 +85,8 @@ src/lib/pctl/pp/Makefile src/lib/xrm/Makefile src/lib/xrm/pp/Makefile + src/lib/xpctl/Makefile + src/lib/xpctl/pp/Makefile src/lib/native/Makefile src/tools/Makefile tests/Makefile @@ -91,10 +94,12 @@ AC_CONFIG_FILES([tests/test-parse-prism.sh], [chmod a=rx tests/test-parse-prism.sh]) -AC_CONFIG_FILES([tests/test-parse-xrm.sh], - [chmod a=rx tests/test-parse-xrm.sh]) AC_CONFIG_FILES([tests/test-parse-pctl.sh], [chmod a=rx tests/test-parse-pctl.sh]) +AC_CONFIG_FILES([tests/test-parse-xrm.sh], + [chmod a=rx tests/test-parse-xrm.sh]) +AC_CONFIG_FILES([tests/test-parse-xpctl.sh], + [chmod a=rx tests/test-parse-xpctl.sh]) AC_CONFIG_FILES([tests/test-pp-prism.sh], [chmod a=rx tests/test-pp-prism.sh]) @@ -102,6 +107,8 @@ [chmod a=rx tests/test-pp-pctl.sh]) AC_CONFIG_FILES([tests/test-pp-xrm.sh], [chmod a=rx tests/test-pp-xrm.sh]) +AC_CONFIG_FILES([tests/test-pp-xpctl.sh], + [chmod a=rx tests/test-pp-xpctl.sh]) AC_CONFIG_FILES([tests/test-xrm-front.sh], [chmod a=rx tests/test-xrm-front.sh]) Index: TODO --- TODO (revision 61) +++ TODO (working copy) @@ -13,6 +13,9 @@ * Add tests using "system ... endsystem" (it's properly not parsed atm) + * Fix the PCTL grammar (see tests/pctl/longuest-exp-match.pctl for a simple + test case) + * Add more tests. Add tests which actually do check that the generated code is correct (which is not done ATM). Factorize current tests with shell functions.

1 0

XRM 61: Fix pretty-printing for PCTL/CSL.
by SIGOURE Benoit 10 Jun '06

10 Jun '06

https://svn.lrde.epita.fr/svn/xrm/trunk Index: ChangeLog from SIGOURE Benoit <sigoure.benoit(a)lrde.epita.fr> Fix pretty-printing for PCTL/CSL. Pretty printing is now fully functional for PCTL/CSL. * src/lib/pctl/pp/pctl-label.str: Fix boxing. * src/syn/pctl/PCTL-Property.sdf: Put correct constructor names. * src/lib/pctl/pp/pctl-property.str: Ditto + take new constructor names into account. * THANKS: Typo. THANKS | 2 +- src/lib/pctl/pp/pctl-label.str | 2 +- src/lib/pctl/pp/pctl-property.str | 18 +++++++++--------- src/syn/pctl/PCTL-Property.sdf | 24 ++++++++++++------------ 4 files changed, 23 insertions(+), 23 deletions(-) Index: src/lib/pctl/pp/pctl-label.str --- src/lib/pctl/pp/pctl-label.str (revision 60) +++ src/lib/pctl/pp/pctl-label.str (working copy) @@ -4,4 +4,4 @@ // "label" "\"" Identifier "\"" "=" Expression ";" -> LabelDef prism-to-box: LabelDef(idf, exp) - -> H hs=1 [ KW["label"] "\"" ~idf "\"" "=" H hs=0 [~exp ";"] ] + -> H hs=1 [ KW["label"] H hs=0["\"" ~idf "\""] "=" H hs=0 [~exp ";"] ] Index: src/lib/pctl/pp/pctl-property.str --- src/lib/pctl/pp/pctl-property.str (revision 60) +++ src/lib/pctl/pp/pctl-property.str (working copy) @@ -60,19 +60,19 @@ -> H hs=1 [ H hs=0[ KW["P"] MATH["=?"] ] "[" ~path ~filter_ "]" ] prism-to-box: - ProbAtLeast(path, None()) + ProbMin(path, None()) -> H hs=1 [ KW["Pmin"] MATH["=?"] "[" ~path "]" ] prism-to-box: - ProbAtLeast(path, Some(filter_)) + ProbMin(path, Some(filter_)) -> H hs=1 [ KW["Pmin"] MATH["=?"] "[" ~path ~filter_ "]" ] prism-to-box: - ProbAtMost(path, None()) + ProbMax(path, None()) -> H hs=1 [ KW["Pmax"] MATH["=?"] "[" ~path "]" ] prism-to-box: - ProbAtMost(path, Some(filter_)) + ProbMax(path, Some(filter_)) -> H hs=1 [ KW["Pmax"] MATH["=?"] "[" ~path ~filter_ "]" ] /* S Operator */ @@ -160,19 +160,19 @@ -> H hs=1 [ H hs=0[ KW["R"] MATH["=?"] ] "[" ~reward ~filter_ "]" ] prism-to-box: - RewardAtLeast(reward, None()) + RewardMin(reward, None()) -> H hs=1 [ KW["Rmin"] MATH["=?"] "[" ~reward "]" ] prism-to-box: - RewardAtLeast(reward, Some(filter_)) + RewardMin(reward, Some(filter_)) -> H hs=1 [ KW["Rmin"] MATH["=?"] "[" ~reward ~filter_ "]" ] prism-to-box: - RewardAtMost(reward, None()) + RewardMax(reward, None()) -> H hs=1 [ KW["Rmax"] MATH["=?"] "[" ~reward "]" ] prism-to-box: - RewardAtMost(reward, Some(filter_)) + RewardMax(reward, Some(filter_)) -> H hs=1 [ KW["Rmax"] MATH["=?"] "[" ~reward ~filter_ "]" ] /* Misc. stuff */ @@ -181,4 +181,4 @@ Init() -> H hs=0 ["\"" KW["init"] "\""] prism-to-box: - Label(s) -> H hs=0 ["\"" s "\""] + Label(idf) -> H hs=0 ["\"" ~idf "\""] Index: src/syn/pctl/PCTL-Property.sdf --- src/syn/pctl/PCTL-Property.sdf (revision 60) +++ src/syn/pctl/PCTL-Property.sdf (working copy) @@ -147,19 +147,19 @@ 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")} + Property "|" Property -> Property {left,cons("Or")} + Property "&" Property -> Property {left,cons("And")} + "!" Property -> Property {cons("Not")} "P" "<" Expression "[" Path Filter? "]" -> Property {cons("ProbLt")} "P" "<=" Expression "[" Path Filter? "]" -> Property {cons("ProbLtEq")} "P" ">" Expression "[" Path Filter? "]" -> Property {cons("ProbGt")} "P" ">=" Expression "[" Path Filter? "]" -> Property {cons("ProbGtEq")} "P" "=?" "[" Path Filter? "]" -> Property {cons("ProbEq")} - "P" "min" "=?" "[" Path Filter? "]" -> Property {cons("ProbAtLeast")} - "Pmin" "=?" "[" Path Filter? "]" -> Property {cons("ProbAtLeast")} - "P" "max" "=?" "[" Path Filter? "]" -> Property {cons("ProbAtMost")} - "Pmax" "=?" "[" Path Filter? "]" -> Property {cons("ProbAtMost")} + "P" "min" "=?" "[" Path Filter? "]" -> Property {cons("ProbMin")} + "Pmin" "=?" "[" Path Filter? "]" -> Property {cons("ProbMin")} + "P" "max" "=?" "[" Path Filter? "]" -> Property {cons("ProbMax")} + "Pmax" "=?" "[" Path Filter? "]" -> Property {cons("ProbMax")} "S" "<" Expression "[" Formula ("{" Formula "}")? "]" -> Property {cons("SteadyLt")} "S" "<=" Expression "[" Formula ("{" Formula "}")? "]" -> Property {cons("SteadyLtEq")} @@ -172,14 +172,14 @@ "R" ">" Expression "[" Reward Filter? "]" -> Property {cons("RewardGt")} "R" ">=" Expression "[" Reward Filter? "]" -> Property {cons("RewardGtEq")} "R" "=?" "[" Reward Filter? "]" -> Property {cons("RewardEq")} - "R" "min" "=?" "[" Reward Filter? "]" -> Property {cons("RewardAtLeast")} - "Rmin" "=?" "[" Reward Filter? "]" -> Property {cons("RewardAtLeast")} - "R" "max" "=?" "[" Reward Filter? "]" -> Property {cons("RewardAtMost")} - "Rmax" "=?" "[" Reward Filter? "]" -> Property {cons("RewardAtMost")} + "R" "min" "=?" "[" Reward Filter? "]" -> Property {cons("RewardMin")} + "Rmin" "=?" "[" Reward Filter? "]" -> Property {cons("RewardMin")} + "R" "max" "=?" "[" Reward Filter? "]" -> Property {cons("RewardMax")} + "Rmax" "=?" "[" Reward Filter? "]" -> Property {cons("RewardMax")} "\"init\"" -> Property {cons("Init")} "\"" Identifier "\"" -> Property {cons("Label")} - Expression -> Property {cons("Exp2Prop")} + Expression -> Property %%{cons("Exp2Prop")}%%DEBUG "(" Property ")" -> Property {bracket} context-free priorities Index: THANKS --- THANKS (revision 60) +++ THANKS (working copy) @@ -10,5 +10,5 @@ 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(a)lrde.epita.fr> +Micha�l Cadilhac <micha(a)lrde.epita.fr> For his beta-testing, his suggestions and many (good) ideas.

1 0

XRM 60: Fix (almost completely) the PCTL/CSL grammar.
by SIGOURE Benoit 10 Jun '06

10 Jun '06

https://svn.lrde.epita.fr/svn/xrm/trunk Index: ChangeLog from SIGOURE Benoit <sigoure.benoit(a)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(a)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(a)acm.org> + For his support on IRC. + +Akim Demaille <akim(a)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(a)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

1 0