Projects

projects@lrde.epita.fr

1049 discussions

by SIGOURE Benoit

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).

18 years, 7 months

XRM 66: Add parameterized formulas.

by SIGOURE Benoit

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 *

18 years, 7 months

XRM 65: Add XRM-like formulas in eXtended PCTL.

by SIGOURE Benoit

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 *

18 years, 7 months

XRM 64: Use --verbose instead of --statistics.

by SIGOURE Benoit

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 */

18 years, 7 months

XRM 63: Finish eXtended PCTL integration in xrm-front.

by SIGOURE Benoit

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 * *********************

18 years, 7 months

XRM 62: Add the base for eXtended PCTL.

by SIGOURE Benoit

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.

18 years, 7 months

XRM 61: Fix pretty-printing for PCTL/CSL.

by SIGOURE Benoit

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.

18 years, 7 months

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

by SIGOURE Benoit

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

18 years, 7 months

XRM 59: Add (buggy) support for PCTL/CSL formulas.

by SIGOURE Benoit

https://svn.lrde.epita.fr/svn/xrm/trunk Index: ChangeLog from SIGOURE Benoit <sigoure.benoit(a)lrde.epita.fr> Add (buggy) support for PCTL/CSL formulas. This commit provides a parser and a pretty printer for PCTL/CSL formulas as used in PRISM. The parser is buggy (several ambiguities to be fixed etc.). The pretty-printer also seems buggy although it seems to be boxing properly the AST, it's (sometimes) rejected by libstratego-gpp for some reason... To be fixed... * src/tools/parse-pctl.str: New. * src/tools/pp-pctl.str: New. * src/tools/Makefile.am: Add parse-pctl and pp-pctl. * src/sig/Makefile.am: Generate signatures for PCTL. * src/lib/pctl: New. * src/lib/pctl/pp: New. * src/lib/pctl/pp/pctl-properties-file.str: New. * src/lib/pctl/pp/pctl-to-abox.str: New. * src/lib/pctl/pp/pctl-path.meta: New. * src/lib/pctl/pp/pctl-label.str: New. * src/lib/pctl/pp/pctl-formula.meta: New. * src/lib/pctl/pp/pctl-property.str: New. * src/lib/pctl/pp/pctl-reward.str: New. * src/lib/pctl/pp/pctl-filter.str: New. * src/lib/pctl/pp/pp-pctl-to-box.str: New. * src/lib/pctl/pp/pctl-properties-file.meta: New. * src/lib/pctl/pp/pctl-path.str: New. * src/lib/pctl/pp/pctl-label.meta: New. * src/lib/pctl/pp/pctl-reward.meta: New. * src/lib/pctl/pp/Makefile.am: New. * src/lib/pctl/pp/pctl-property.meta: New. * src/lib/pctl/pp/pctl-filter.meta: New. * src/lib/pctl/pp/pctl-formula.str: New. * src/lib/pctl/Makefile.am: New. * src/lib/xrm/pp/xrm-to-abox.str: Correct the usage summary. * src/lib/Makefile.am (SUBDIRS): Add pctl. * src/syn/pctl: New. * src/syn/pctl/PCTL-Main.sdf: New. * src/syn/pctl/PCTL-Property.sdf: New. * src/syn/pctl/PCTL-Reward.sdf: New. * src/syn/pctl/PCTL-Filter.sdf: New. * src/syn/pctl/PCTL-Formula.sdf: New. * src/syn/pctl/PCTL-StartSymbols.sdf: New. * src/syn/pctl/StrategoPCTL.sdf: New. * src/syn/pctl/PCTL-Path.sdf: New. * src/syn/pctl/PCTL-PropertiesFile.sdf: New. * src/syn/pctl/Makefile.am: New. * src/syn/pctl/PCTL-Label.sdf: New. * src/syn/pctl/PCTL-MetaCongruences.sdf: New. * src/syn/pctl/PCTL-MetaVars.sdf: New. * src/syn/pctl/PCTL.sdf: New. * src/syn/Makefile.am (SUBDIRS): Add pctl. * src/syn/prism/PRISM-Label.sdf: Remove. * tests/pctl: New. * tests/pctl/man_examples.pctl: New. * tests/test-parse-pctl.sh.in: New. * tests/test-pp-pctl.sh.in: New. * tests/Makefile.am: Add test-parse-pctl and test-pp-pctl. * configure.ac: Ditto. * TODO: New idea (-O option for xrm-front to produce optimized PRISM code). TODO | 49 +++++++ configure.ac | 9 + src/lib/Makefile.am | 4 src/lib/pctl/Makefile.am | 11 + src/lib/pctl/pp/Makefile.am | 38 +++++ src/lib/pctl/pp/pctl-filter.meta | 1 src/lib/pctl/pp/pctl-filter.str | 13 + src/lib/pctl/pp/pctl-formula.meta | 1 src/lib/pctl/pp/pctl-formula.str | 6 src/lib/pctl/pp/pctl-label.meta | 1 src/lib/pctl/pp/pctl-label.str | 7 + src/lib/pctl/pp/pctl-path.meta | 1 src/lib/pctl/pp/pctl-path.str | 22 +++ src/lib/pctl/pp/pctl-properties-file.meta | 1 src/lib/pctl/pp/pctl-properties-file.str | 7 + src/lib/pctl/pp/pctl-property.meta | 1 src/lib/pctl/pp/pctl-property.str | 184 +++++++++++++++++++++++++++ src/lib/pctl/pp/pctl-reward.meta | 1 src/lib/pctl/pp/pctl-reward.str | 15 ++ src/lib/pctl/pp/pctl-to-abox.str | 53 +++++++ src/lib/pctl/pp/pp-pctl-to-box.str | 35 +++++ src/lib/xrm/pp/xrm-to-abox.str | 2 src/sig/Makefile.am | 9 + src/syn/Makefile.am | 4 src/syn/pctl/Makefile.am | 65 +++++++++ src/syn/pctl/PCTL-Filter.sdf | 17 ++ src/syn/pctl/PCTL-Formula.sdf | 24 +++ src/syn/pctl/PCTL-Label.sdf | 5 src/syn/pctl/PCTL-Main.sdf | 4 src/syn/pctl/PCTL-MetaCongruences.sdf | 12 + src/syn/pctl/PCTL-MetaVars.sdf | 11 + src/syn/pctl/PCTL-Path.sdf | 23 +++ src/syn/pctl/PCTL-PropertiesFile.sdf | 22 +++ src/syn/pctl/PCTL-Property.sdf | 203 ++++++++++++++++++++++++++++++ src/syn/pctl/PCTL-Reward.sdf | 19 ++ src/syn/pctl/PCTL-StartSymbols.sdf | 17 ++ src/syn/pctl/PCTL.sdf | 11 + src/syn/pctl/StrategoPCTL.sdf | 26 +++ src/tools/Makefile.am | 10 + src/tools/parse-pctl.str | 38 ++--- src/tools/pp-pctl.str | 27 +-- tests/Makefile.am | 6 tests/pctl/man_examples.pctl | 96 ++++++++++++++ tests/test-parse-pctl.sh.in | 6 tests/test-pp-pctl.sh.in | 14 +- 45 files changed, 1074 insertions(+), 57 deletions(-) Index: src/tools/parse-pctl.str --- src/tools/parse-pctl.str (revision 58) +++ src/tools/parse-pctl.str (working copy) @@ -1,23 +1,23 @@ // Code mostly from parse-java by Martin Bravenboer <martin(a)cs.uu.nl> -module parse-prism +module parse-pctl imports libxtclib // FIXME: import libstratego-xtc for strc 0.17 tool-doc parser-common strategies - main-parse-prism = + main-parse-pctl = // xtc-io-wrap(extra-opts, usage, about, deps, s) xtc-io-wrap( - parse-prism-options - , parse-prism-usage + parse-pctl-options + , parse-pctl-usage , parser-about - , !["sglr", "implode-asfix", "PRISM.tbl", "pp-aterm"] - , parse-prism + , !["sglr", "implode-asfix", "PCTL.tbl", "pp-aterm"] + , parse-pctl ) - parse-prism-options = + parse-pctl-options = symbol-option + preserve-comments-option + preserve-positions-option @@ -26,7 +26,7 @@ strategies - parse-prism = + parse-pctl = 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 (PRISM.tbl) has a - ** single start symbol (ModulesFile) and the other (PRISM-StartSymbols) has + ** We use two parse tables for performances. One of them (PCTL.tbl) has a + ** single start symbol (ModulesFile) 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. */ get-parse-table = - <get-config> "parsetable"; not(?"PRISM.tbl") - <+ if get-start-symbol => "ModulesFile" then - !"PRISM.tbl" + <get-config> "parsetable"; not(?"PCTL.tbl") + <+ if get-start-symbol => "PropertiesFile" then + !"PCTL.tbl" else - !"PRISM-StartSymbols.tbl" + !"PCTL-StartSymbols.tbl" end /** @@ -77,11 +77,11 @@ */ strategies - parse-prism-usage = + parse-pctl-usage = <tool-doc> - [ Usage("parse-prism [OPTIONS]") + [ Usage("parse-pctl [OPTIONS]") , Summary( - "Parses a PRISM source file to an abstract syntax + "Parses a PCTL source file to an abstract syntax tree in the ATerm format.") , OptionUsage() , AutoReportBugs() Index: src/tools/pp-pctl.str --- src/tools/pp-pctl.str (revision 58) +++ src/tools/pp-pctl.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-pctl imports libstratego-lib tool-doc libstratego-gpp - pp-xrm-to-box + pp-pctl-to-box strategies - main-pp-xrm = + main-pp-pctl = // io-stream-wrap(extra-opts, usage, about, s) io-stream-wrap( fail - , pp-xrm-usage - , pp-xrm-about - , pp-xrm + , pp-pctl-usage + , pp-pctl-about + , pp-pctl ) - pp-xrm = + pp-pctl = ?(<read-from-stream>, out-file) - ; pp-xrm-to-abox + ; pp-pctl-to-abox ; box2text-stream(|80, out-file) ; <fputs> ("\n", out-file) @@ -29,17 +29,16 @@ */ strategies - pp-xrm-usage = + pp-pctl-usage = <tool-doc> - [ Usage("pp-xrm [OPTIONS]") - , Summary("Pretty-prints an eXtended Reactive Module abstract syntax - tree in ATerm format to an eXtended Reactive Module source - file.") + [ Usage("pp-pctl [OPTIONS]") + , Summary("Pretty-prints a PCTL abstract syntax tree in ATerm format + to an eXtended Reactive Module source file.") , OptionUsage() , AutoReportBugs() ] - pp-xrm-about = + pp-pctl-about = <tool-doc> [ AutoProgram() , Author(Person("SIGOURE Benoit", "sigoure.benoit(a)lrde.epita.fr")) Index: src/tools/Makefile.am --- src/tools/Makefile.am (revision 58) +++ 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 Fri Jun 2 17:57:09 2006 SIGOURE Benoit +## Last update Sat Jun 10 04:48:43 2006 SIGOURE Benoit ## include $(top_srcdir)/config/Transformers.mk @@ -13,8 +13,10 @@ bin_PROGRAMS = \ parse-prism \ + parse-pctl \ parse-xrm \ pp-prism \ + pp-pctl \ pp-xrm EXTRA_DIST = $(wildcard *.str) $(wildcard *.meta) @@ -25,8 +27,10 @@ -I $(GPP)/share/sdf/gpp \ $(STRATEGO_GPP_STRCFLAGS) \ -I $(top_srcdir)/src/lib/prism/pp \ + -I $(top_srcdir)/src/lib/pctl/pp \ -I $(top_srcdir)/src/lib/xrm/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/sig LDADD += $(SSL_LIBS) @@ -35,6 +39,10 @@ pp_prism_SOURCES = pp-prism.c pp_prism_LDADD = $(STRATEGO_GPP_LIBS) +parse_pctl_SOURCES = parse-pctl.c +pp_pctl_SOURCES = pp-pctl.c +pp_pctl_LDADD = $(STRATEGO_GPP_LIBS) + parse_xrm_SOURCES = parse-xrm.c pp_xrm_SOURCES = pp-xrm.c pp_xrm_LDADD = $(STRATEGO_GPP_LIBS) Index: src/sig/Makefile.am --- src/sig/Makefile.am (revision 58) +++ src/sig/Makefile.am (working copy) @@ -5,16 +5,17 @@ ## Mail <sigoure.benoit(a)lrde.epita.fr> ## ## Started on Mon May 8 18:38:32 2006 SIGOURE Benoit -## Last update Thu May 25 23:41:55 2006 SIGOURE Benoit +## Last update Sat Jun 10 04:43:36 2006 SIGOURE Benoit ## include $(top_srcdir)/config/Transformers.mk pkgdata_DATA = PRISM.rtg PRISM.str \ + PCTL.rtg PCTL.str \ XRM.rtg XRM.str EXTRA_DIST = $(pkgdata_DATA) -CLEANFILES = $(pkgdata_DATA) PRISM.def XRM.def +CLEANFILES = $(pkgdata_DATA) PRISM.def PCTL.def XRM.def SDF2RTG_FLAGS = --main $* @@ -22,6 +23,10 @@ rm -f $@ $(LN_S) $(top_builddir)/src/syn/prism/$@ $@ +PCTL.def: $(top_builddir)/src/syn/pctl/PCTL.def + rm -f $@ + $(LN_S) $(top_builddir)/src/syn/pctl/$@ $@ + XRM.def: $(top_builddir)/src/syn/xrm/XRM.def rm -f $@ $(LN_S) $(top_builddir)/src/syn/xrm/$@ $@ Index: src/lib/pctl/pp/pctl-properties-file.str --- src/lib/pctl/pp/pctl-properties-file.str (revision 0) +++ src/lib/pctl/pp/pctl-properties-file.str (revision 0) @@ -0,0 +1,7 @@ +module pctl-properties-file + +rules + // PropertiesFileSection* -> PropertiesFile + prism-to-box: + PropertiesFile(properties-file-sections) + -> box |[ V vs=1 [ ~*properties-file-sections ] ]| Index: src/lib/pctl/pp/pctl-to-abox.str --- src/lib/pctl/pp/pctl-to-abox.str (revision 0) +++ src/lib/pctl/pp/pctl-to-abox.str (revision 0) @@ -0,0 +1,53 @@ +module pctl-to-abox +imports + libxtclib // FIXME: import libstratego-xtc for strc 0.17 + tool-doc + pp-pctl-to-box + +strategies + + main-pctl-to-abox = + // xtc-io-wrap(extra-opts, usage, about, deps, s) + xtc-io-wrap( + fail + , pctl-to-abox-usage + , pctl-to-abox-about + , ![] + , main-wrapped + ) + + // main wrapped in main-pctl-to-abox + main-wrapped = + // read data from input + read-from + ; pp-pctl-to-abox + ; if <get-config> "-b" then + write-to // write binary output + else + write-to-text // write text output + end + +/** + * Documentation + */ +strategies + + pctl-to-abox-usage = + <tool-doc> + [ Usage("pctl-to-abox [OPTIONS]") + , Summary("Transforms a PCTL abstract syntax tree in ATerm format + to a box representation of the AST for pretty-printing") + , OptionUsage() + , AutoReportBugs() + ] + + pctl-to-abox-about = + <tool-doc> + [ AutoProgram() + , Author(Person("SIGOURE Benoit", "sigoure.benoit(a)lrde.epita.fr")) + , GNU_GPL("2006", "SIGOURE Benoit <sigoure.benoit(a)lrde.epita.fr>") + , Config([ + DefaultXTCRepository() + , CurrentXTCRepository() + ]) + ] Index: src/lib/pctl/pp/pctl-path.meta --- src/lib/pctl/pp/pctl-path.meta (revision 0) +++ src/lib/pctl/pp/pctl-path.meta (revision 0) @@ -0,0 +1 @@ +Meta([Syntax("Stratego-Box")]) Index: src/lib/pctl/pp/pctl-label.str --- src/lib/pctl/pp/pctl-label.str (revision 0) +++ src/lib/pctl/pp/pctl-label.str (revision 0) @@ -0,0 +1,7 @@ +module pctl-label + +rules + // "label" "\"" Identifier "\"" "=" Expression ";" -> LabelDef + prism-to-box: + LabelDef(idf, exp) + -> H hs=1 [ KW["label"] "\"" ~idf "\"" "=" H hs=0 [~exp ";"] ] Index: src/lib/pctl/pp/pctl-formula.meta --- src/lib/pctl/pp/pctl-formula.meta (revision 0) +++ src/lib/pctl/pp/pctl-formula.meta (revision 0) @@ -0,0 +1 @@ +Meta([Syntax("Stratego-Box")]) Index: src/lib/pctl/pp/pctl-property.str --- src/lib/pctl/pp/pctl-property.str (revision 0) +++ src/lib/pctl/pp/pctl-property.str (revision 0) @@ -0,0 +1,184 @@ +module pctl-property + +rules + + prism-to-box: + Implies(lhs, rhs) -> H hs=1 [~lhs MATH["=>"] ~rhs] + + // already imported from PRISM's boxer + //prism-to-box: + // Or(lhs, rhs) -> H hs=1 [~lhs MATH["|"] ~rhs] + + // already imported from PRISM's boxer + //prism-to-box: + // And(lhs, rhs) -> H hs=1 [~lhs MATH["|"] ~rhs] + + // already imported from PRISM's boxer + //prism-to-box: + // Not(exp) -> H hs=0 [ MATH["!"] ~exp ] + + /* P Operator */ + + prism-to-box: + ProbLt(exp, path, None()) + -> H hs=1 [ H hs=0[ KW["P"] MATH["<"] ~exp ] "[" ~path "]" ] + + prism-to-box: + ProbLt(exp, path, Some(filter_)) + -> H hs=1 [ H hs=0[ KW["P"] MATH["<"] ~exp ] "[" ~path ~filter_ "]" ] + + prism-to-box: + ProbLtEq(exp, path, None()) + -> H hs=1 [ H hs=0[ KW["P"] MATH["<="] ~exp ] "[" ~path "]" ] + + prism-to-box: + ProbLtEq(exp, path, Some(filter_)) + -> H hs=1 [ H hs=0[ KW["P"] MATH["<="] ~exp ] "[" ~path ~filter_ "]" ] + + prism-to-box: + ProbGt(exp, path, None()) + -> H hs=1 [ H hs=0[ KW["P"] MATH[">"] ~exp ] "[" ~path "]" ] + + prism-to-box: + ProbGt(exp, path, Some(filter_)) + -> H hs=1 [ H hs=0[ KW["P"] MATH[">"] ~exp ] "[" ~path ~filter_ "]" ] + + prism-to-box: + ProbGtEq(exp, path, None()) + -> H hs=1 [ H hs=0[ KW["P"] MATH[">="] ~exp ] "[" ~path "]" ] + + prism-to-box: + ProbGtEq(exp, path, Some(filter_)) + -> H hs=1 [ H hs=0[ KW["P"] MATH[">="] ~exp ] "[" ~path ~filter_ "]" ] + + prism-to-box: + ProbEq(path, None()) + -> H hs=1 [ H hs=0[ KW["P"] MATH["=?"] ] "[" ~path "]" ] + + prism-to-box: + ProbEq(path, Some(filter_)) + -> H hs=1 [ H hs=0[ KW["P"] MATH["=?"] ] "[" ~path ~filter_ "]" ] + + prism-to-box: + ProbAtLeast(path, None()) + -> H hs=1 [ KW["Pmin"] MATH["=?"] "[" ~path "]" ] + + prism-to-box: + ProbAtLeast(path, Some(filter_)) + -> H hs=1 [ KW["Pmin"] MATH["=?"] "[" ~path ~filter_ "]" ] + + prism-to-box: + ProbAtMost(path, None()) + -> H hs=1 [ KW["Pmax"] MATH["=?"] "[" ~path "]" ] + + prism-to-box: + ProbAtMost(path, Some(filter_)) + -> H hs=1 [ KW["Pmax"] MATH["=?"] "[" ~path ~filter_ "]" ] + + /* S Operator */ + + prism-to-box: + SteadyLt(exp, formula, None()) + -> H hs=1 [ H hs=0[ KW["S"] MATH["<"] ~exp ] "[" ~formula "]" ] + + prism-to-box: + SteadyLt(exp, formula, Some(filter_)) + -> H hs=1 [ H hs=0[ KW["S"] MATH["<"] ~exp ] "[" ~formula "{" ~filter_ "}" "]" ] + + prism-to-box: + SteadyLtEq(exp, formula, None()) + -> H hs=1 [ H hs=0[ KW["S"] MATH["<="] ~exp ] "[" ~formula "]" ] + + prism-to-box: + SteadyLtEq(exp, formula, Some(filter_)) + -> H hs=1 [ H hs=0[ KW["S"] MATH["<="] ~exp ] "[" ~formula "{" ~filter_ "}" "]" ] + + prism-to-box: + SteadyGt(exp, formula, None()) + -> H hs=1 [ H hs=0[ KW["S"] MATH[">"] ~exp ] "[" ~formula "]" ] + + prism-to-box: + SteadyGt(exp, formula, Some(filter_)) + -> H hs=1 [ H hs=0[ KW["S"] MATH[">"] ~exp ] "[" ~formula ~filter_ "]" ] + + prism-to-box: + SteadyGtEq(exp, formula, None()) + -> H hs=1 [ H hs=0[ KW["S"] MATH[">="] ~exp ] "[" ~formula "]" ] + + prism-to-box: + SteadyGtEq(exp, formula, Some(filter_)) + -> H hs=1 [ H hs=0[ KW["S"] MATH[">="] ~exp ] "[" ~formula "{" ~filter_ "}" "]" ] + + prism-to-box: + SteadyEq(formula, None()) + -> H hs=1 [ H hs=0[ KW["S"] MATH["=?"] ] "[" ~formula "]" ] + + prism-to-box: + SteadyEq(formula, Some(filter_)) + -> H hs=1 [ H hs=0[ KW["S"] MATH["=?"] ] "[" ~formula "{" ~filter_ "}" "]" ] + + /* Reward stuff */ + + prism-to-box: + RewardLt(exp, reward, None()) + -> H hs=1 [ H hs=0[ KW["R"] MATH["<"] ~exp ] "[" ~reward "]" ] + + prism-to-box: + RewardLt(exp, reward, Some(filter_)) + -> H hs=1 [ H hs=0[ KW["R"] MATH["<"] ~exp ] "[" ~reward ~filter_ "]" ] + + prism-to-box: + RewardLtEq(exp, reward, None()) + -> H hs=1 [ H hs=0[ KW["R"] MATH["<="] ~exp ] "[" ~reward "]" ] + + prism-to-box: + RewardLtEq(exp, reward, Some(filter_)) + -> H hs=1 [ H hs=0[ KW["R"] MATH["<="] ~exp ] "[" ~reward ~filter_ "]" ] + + prism-to-box: + RewardGt(exp, reward, None()) + -> H hs=1 [ H hs=0[ KW["R"] MATH[">"] ~exp ] "[" ~reward "]" ] + + prism-to-box: + RewardGt(exp, reward, Some(filter_)) + -> H hs=1 [ H hs=0[ KW["R"] MATH[">"] ~exp ] "[" ~reward ~filter_ "]" ] + + prism-to-box: + RewardGtEq(exp, reward, None()) + -> H hs=1 [ H hs=0[ KW["R"] MATH[">="] ~exp ] "[" ~reward "]" ] + + prism-to-box: + RewardGtEq(exp, reward, Some(filter_)) + -> H hs=1 [ H hs=0[ KW["R"] MATH[">="] ~exp ] "[" ~reward ~filter_ "]" ] + + prism-to-box: + RewardEq(reward, None()) + -> H hs=1 [ H hs=0[ KW["R"] MATH["=?"] ] "[" ~reward "]" ] + + prism-to-box: + RewardEq(reward, Some(filter_)) + -> H hs=1 [ H hs=0[ KW["R"] MATH["=?"] ] "[" ~reward ~filter_ "]" ] + + prism-to-box: + RewardAtLeast(reward, None()) + -> H hs=1 [ KW["Rmin"] MATH["=?"] "[" ~reward "]" ] + + prism-to-box: + RewardAtLeast(reward, Some(filter_)) + -> H hs=1 [ KW["Rmin"] MATH["=?"] "[" ~reward ~filter_ "]" ] + + prism-to-box: + RewardAtMost(reward, None()) + -> H hs=1 [ KW["Rmax"] MATH["=?"] "[" ~reward "]" ] + + prism-to-box: + RewardAtMost(reward, Some(filter_)) + -> H hs=1 [ KW["Rmax"] MATH["=?"] "[" ~reward ~filter_ "]" ] + + /* Misc. stuff */ + + prism-to-box: + Init() -> H hs=0 ["\"" KW["init"] "\""] + + prism-to-box: + Label(s) -> H hs=0 ["\"" s "\""] Index: src/lib/pctl/pp/pctl-reward.str --- src/lib/pctl/pp/pctl-reward.str (revision 0) +++ src/lib/pctl/pp/pctl-reward.str (revision 0) @@ -0,0 +1,15 @@ +module pctl-reward + +rules + + prism-to-box: + Cumul(exp) -> H hs=0 [ KW["C"] MATH["<="] ~exp ] + + prism-to-box: + Inst(exp) -> H hs=0 [ KW["I"] MATH["="] ~exp ] + + prism-to-box: + Reach(formula) -> H hs=1 [ KW["F"] ~formula ] + + prism-to-box: + Steady() -> box |[ KW["S"] ]| Index: src/lib/pctl/pp/pctl-filter.str --- src/lib/pctl/pp/pctl-filter.str (revision 0) +++ src/lib/pctl/pp/pctl-filter.str (revision 0) @@ -0,0 +1,13 @@ +module pctl-filter + +rules + + prism-to-box: + Filter(formula, min-max-list) + -> H hs=0 [ "{" ~formula "}" ~*min-max-list ] + + prism-to-box: + ComputeMin() -> H hs=0 [ "{" KW["min"] "}" ] + + prism-to-box: + ComputeMax() -> H hs=0 [ "{" KW["max"] "}" ] Index: src/lib/pctl/pp/pp-pctl-to-box.str --- src/lib/pctl/pp/pp-pctl-to-box.str (revision 0) +++ src/lib/pctl/pp/pp-pctl-to-box.str (revision 0) @@ -0,0 +1,35 @@ +module pp-pctl-to-box +imports + Box + PCTL // signature + PRISM // needed because we use PRISM's Expression etc... + prism-constant + prism-expression + pctl-parenthesize + pctl-properties-file + pctl-label + pctl-formula + pctl-property + pctl-path + pctl-reward + pctl-filter + +strategies + + pp-pctl-to-abox = + pp-pctl-to-abox(prism-to-box) // we keep prism-to-box as rule name + // because we simply extend it + + pp-pctl-to-abox(pprules) = + // strategy from pctl-parenthesize.str generated by sdf2parenthesize + parenthesize-PCTL + ; 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/pctl/pp/pctl-properties-file.meta --- src/lib/pctl/pp/pctl-properties-file.meta (revision 0) +++ src/lib/pctl/pp/pctl-properties-file.meta (revision 0) @@ -0,0 +1 @@ +Meta([Syntax("Stratego-Box")]) Index: src/lib/pctl/pp/pctl-path.str --- src/lib/pctl/pp/pctl-path.str (revision 0) +++ src/lib/pctl/pp/pctl-path.str (revision 0) @@ -0,0 +1,22 @@ +module pctl-path + +rules + + prism-to-box: + Next(formula) -> H hs=1 [ KW["X"] ~formula ] + + prism-to-box: + BoundedUntilLtEq(f1, exp, f2) + -> H hs=1 [ ~f1 H hs=0 [KW["U"] MATH["<="] ~exp] ~f2 ] + + prism-to-box: + BoundedUntilGtEq(f1, exp, f2) + -> H hs=1 [ ~f1 H hs=0 [KW["U"] MATH[">="] ~exp] ~f2 ] + + prism-to-box: + BoundedUntilRange(f1, range-start, range-end, f2) + -> H hs=1 [ ~f1 H hs=0 [KW["U"] "[" ~range-start "," ~range-end "]"] ~f2 ] + + prism-to-box: + Until(f1, f2) + -> H hs=1 [ ~f1 KW["U"] ~f2 ] Index: src/lib/pctl/pp/pctl-label.meta --- src/lib/pctl/pp/pctl-label.meta (revision 0) +++ src/lib/pctl/pp/pctl-label.meta (revision 0) @@ -0,0 +1 @@ +Meta([Syntax("Stratego-Box")]) Index: src/lib/pctl/pp/pctl-reward.meta --- src/lib/pctl/pp/pctl-reward.meta (revision 0) +++ src/lib/pctl/pp/pctl-reward.meta (revision 0) @@ -0,0 +1 @@ +Meta([Syntax("Stratego-Box")]) Index: src/lib/pctl/pp/Makefile.am --- src/lib/pctl/pp/Makefile.am (revision 0) +++ src/lib/pctl/pp/Makefile.am (revision 0) @@ -0,0 +1,38 @@ +## +## Makefile.am for xrm in /home/tsuna/work/xrm/trunk/src/lib/pctl/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 +## + +include $(top_srcdir)/config/toplevel.mk +-include $(wildcard *.dep) + +pkgdata_DATA = pctl-parenthesize.str +libexec_PROGRAMS = pctl-to-abox + +pctl_to_abox_SOURCES = pctl-to-abox.c + +STRINCLUDES = -I $(GPP)/share/sdf/gpp -I $(GPP)/share/gpp \ + -I $(top_srcdir)/src/lib/prism/pp \ + -I $(top_builddir)/src/lib/pctl/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 + +EXTRA_DIST = $(wildcard *.str) $(wildcard *.meta) + +pctl-parenthesize.str: $(top_builddir)/src/syn/pctl/PCTL.def + $(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 Index: src/lib/pctl/pp/pctl-property.meta --- src/lib/pctl/pp/pctl-property.meta (revision 0) +++ src/lib/pctl/pp/pctl-property.meta (revision 0) @@ -0,0 +1 @@ +Meta([Syntax("Stratego-Box")]) Index: src/lib/pctl/pp/pctl-filter.meta --- src/lib/pctl/pp/pctl-filter.meta (revision 0) +++ src/lib/pctl/pp/pctl-filter.meta (revision 0) @@ -0,0 +1 @@ +Meta([Syntax("Stratego-Box")]) Index: src/lib/pctl/pp/pctl-formula.str --- src/lib/pctl/pp/pctl-formula.str (revision 0) +++ src/lib/pctl/pp/pctl-formula.str (revision 0) @@ -0,0 +1,6 @@ +module pctl-formula + +rules + // Property -> Formula + prism-to-box: + Formula(prop) -> prop Index: src/lib/pctl/Makefile.am --- src/lib/pctl/Makefile.am (revision 0) +++ src/lib/pctl/Makefile.am (revision 0) @@ -0,0 +1,11 @@ +## +## Makefile.am for xrm in /home/tsuna/work/xrm/trunk/src/lib/pctl +## +## 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 +## + +SUBDIRS = pp Index: src/lib/xrm/pp/xrm-to-abox.str --- src/lib/xrm/pp/xrm-to-abox.str (revision 58) +++ src/lib/xrm/pp/xrm-to-abox.str (working copy) @@ -35,7 +35,7 @@ xrm-to-abox-usage = <tool-doc> [ Usage("xrm-to-abox [OPTIONS]") - , Summary("Transforms a PRISM abstract syntax tree in ATerm format + , Summary("Transforms an XRM abstract syntax tree in ATerm format to a box representation of the AST for pretty-printing") , OptionUsage() , AutoReportBugs() Index: src/lib/Makefile.am --- src/lib/Makefile.am (revision 58) +++ 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 Thu May 25 18:55:45 2006 SIGOURE Benoit +## Last update Sat Jun 10 03:57:26 2006 SIGOURE Benoit ## -SUBDIRS = prism xrm native +SUBDIRS = prism pctl xrm native Index: src/syn/pctl/PCTL-Main.sdf --- src/syn/pctl/PCTL-Main.sdf (revision 0) +++ src/syn/pctl/PCTL-Main.sdf (revision 0) @@ -0,0 +1,4 @@ +module PCTL-Main +imports + PRISM-Layout + PCTL-PropertiesFile Index: src/syn/pctl/PCTL-Property.sdf --- src/syn/pctl/PCTL-Property.sdf (revision 0) +++ src/syn/pctl/PCTL-Property.sdf (revision 0) @@ -0,0 +1,203 @@ +module PCTL-Property +imports + PRISM-Expression + PRISM-Identifier + PCTL-Formula + PCTL-Path + PCTL-Reward + PCTL-Filter +exports + + %% EBNF Grammar: PCTL Properties + %% + %% Property ::= + %% "true" + %% | "false" + %% | Property "=>" Property + %% | Property "|" Property + %% | Property "&" Property + %% | "!" Property + %% | "P" "<" Expression "[" Path [Filter] "]" + %% | "P" "<=" Expression "[" Path [Filter] "]" + %% | "P" ">" Expression "[" Path [Filter] "]" + %% | "P" ">=" Expression "[" Path [Filter] "]" + %% | "P" "=?" "[" Path [Filter] "]" + %% | Pmin "=?" "[" Path [Filter] "]" + %% | Pmax "=?" "[" Path [Filter] "]" + %% + %% | "S" "<" Expression "[" Formula ["{" Formula "}"] "]" + %% | "S" "<=" Expression "[" Formula ["{" Formula "}"] "]" + %% | "S" ">" Expression "[" Formula ["{" Formula "}"] "]" + %% | "S" ">=" Expression "[" Formula ["{" Formula "}"] "]" + %% | "S" "=?" "[" Formula ("{" Formula "}")? "]" + %% + %% | "R" "<" Expression "[" Reward [Filter] "]" + %% | "R" "<=" Expression "[" Reward [Filter] "]" + %% | "R" ">" Expression "[" Reward [Filter] "]" + %% | "R" ">=" Expression "[" Reward [Filter] "]" + %% | "R" "=?" "[" Reward [Filter] "]" + %% | Rmin "=?" "[" Reward [Filter] "]" + %% | Rmax "=?" "[" Reward [Filter] "]" + %% + %% | "\"init\"" + %% | "\"" + %% | Expression + %% + %% Rmin ::= "R" "min" | "Rmin" + %% Rmax ::= "R" "max" | "Rmax" + + %% EBNF Grammar: PCTL Properties as in PRISM's parser + %% + %% PCTLOr ::= PCTLAnd ["|" PCTLAnd] + %% + %% PCTLAnd ::= PCTLNot ["&" PCTLNot] + %% + %% PCTLNot ::= ["!"] PCTLProb + %% + %% PCTLProb ::= + %% { + %% "P" LtGt Expression + %% | "P" "=" "?" + %% | "P" "min" "=" "?" + %% | "P" "max" "=" "?" + %% | "Pmin" "=" "?" + %% | "Pmax" "=" "?" + %% } "[" + %% { PCTLProbNext | PCTLProbBoundedUntil | PCTLProbUntil } + %% ["{" PCTLFormula "}" { "{" "min" "}" | ( "{" "max" "}" }] + %% "]" + %% | PCTLSS + %% + %% PCTLProbNext ::= "X" PCTLFormula + %% + %% PCTLProbBoundedUntil ::= + %% PCTLFormula "U" "<=" Expression PCTLFormula + %% | PCTLFormula "U" ">=" Expression PCTLFormula + %% | PCTLFormula "U" "[" Expression, Expression "]" PCTLFormula + %% + %% PCTLProbUntil ::= PCTLFormula "U" PCTLFormula + %% + %% PCTLSS ::= + %% { + %% "S" LtGt Expression + %% | "S" "=" "?" + %% } "[" + %% PCTLFormula ["{" PCTLFormula "}"] + %% "]" + %% | PCTLReward + %% + %% PCTLReward ::= + %% { + %% "R" LtGt Expression + %% | "R" "=" "?" + %% | "R" "min" "=" "?" + %% | "R" "max" "=" "?" + %% | "Rmin" "=" "?" + %% | "Rmax" "=" "?" + %% } "[" + %% {PCTLRewardCumul | PCTLRewardInst | PCTLRewardReach | PCTLRewardSS} + %% ["{" PCTLFormula "}" { "{" "min" "}" | "{" "max" "}" }] + %% "]" + %% | PCTLInit + %% + %% PCTLRewardCumul ::= "C" "<=" Expression + %% + %% PCTLRewardInst ::= "I" "=" Expression + %% + %% PCTLRewardReach ::= "F" PCTLFormula + %% + %% PCTLRewardSS ::= "S" + %% + %% PCTLInit ::= + %% "\"" "init" "\"" + %% | PCTLLabel + %% + %% PCTLLabel ::= + %% "\"" Identifier "\"" + %% | PCTLBrackets + %% + %% PCTLBrackets ::= + %% "(" PCTLFormula ")" + %% | PCTLExpression + %% + %% (* Comment from PRISM's parser: + %% * Note that we jump into the middle of the Expression hierarchy. + %% * In practice, this means that Boolean conjunctives in expressions + %% * must be below at least one level of parentheses. Otherwise, the + %% * fact that both PCTLFormulas and Expressions can contain such + %% * operators leads to an ambiguous grammar and a whole world of + %% * associated problems. Chances are the or/and/not will just be + %% * happily parsed as a PCTL operator anyway. Note that this is + %% * not true for the if-then-else operator which is not present in + %% * PCTL but has lower precedence than or/and/not. Oh well. + %% *) + %% PCTLExpression ::= + %% ExpressionRelOpRange + + sorts Property + context-free syntax + %% 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")} + + "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")} + + "S" "<" Expression "[" Formula ("{" Formula "}")? "]" -> Property {cons("SteadyLt")} + "S" "<=" Expression "[" Formula ("{" Formula "}")? "]" -> Property {cons("SteadyLtEq")} + "S" ">" Expression "[" Formula ("{" Formula "}")? "]" -> Property {cons("SteadyGt")} + "S" ">=" Expression "[" Formula ("{" Formula "}")? "]" -> Property {cons("SteadyGtEq")} + "S" "=?" "[" Formula ("{" Formula "}")? "]" -> Property {cons("SteadyEq")} + + "R" "<" Expression "[" Reward Filter? "]" -> Property {cons("RewardLt")} + "R" "<=" Expression "[" Reward Filter? "]" -> Property {cons("RewardLtEq")} + "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")} + + "\"init\"" -> Property {cons("Init")} + "\"" Identifier "\"" -> Property {cons("Label")} + Expression -> Property + "(" Property ")" -> Property {bracket} + + %% FIXME: Some priorities are probably missing here + context-free priorities + { + Property "=>" Property -> Property + } + > { + Property "|" Property -> Property + } + > { + Property "&" Property -> Property + } + > { + "!" Property -> Property + } + > { + Expression -> Property + } + + %% FIXME: This looks a bit weird... + context-free priorities + { + "(" Formula ")" -> Formula + } + > { + "(" Property ")" -> Property + } Index: src/syn/pctl/PCTL-Reward.sdf --- src/syn/pctl/PCTL-Reward.sdf (revision 0) +++ src/syn/pctl/PCTL-Reward.sdf (revision 0) @@ -0,0 +1,19 @@ +module PCTL-Reward +imports + PRISM-Expression +exports + + %% EBNF Grammar: Rewards in PCTL + %% + %% Reward ::= + %% "C" "<=" Expression + %% | "I" "=" Expression + %% | "F" Formula + %% | "S" + + sorts Reward + context-free syntax + "C" "<=" Expression -> Reward {cons("Cumul")} + "I" "=" Expression -> Reward {cons("Inst")} + "F" Formula -> Reward {cons("Reach")} + "S" -> Reward {cons("Steady")} Index: src/syn/pctl/PCTL-Filter.sdf --- src/syn/pctl/PCTL-Filter.sdf (revision 0) +++ src/syn/pctl/PCTL-Filter.sdf (revision 0) @@ -0,0 +1,17 @@ +module PCTL-Filter +imports + PCTL-Formula +exports + + %% EBNF Grammar: PCTL Filters + %% + %% Filter ::= + %% "{" Formula "}" {FilterMinMax} + %% | "{" "min" "}" + %% | "{" "max" "}" + + sorts Filter FilterMinMax + context-free syntax + "{" Formula "}" FilterMinMax* -> Filter {cons("Filter")} + "{" "min" "}" -> FilterMinMax {bracket,cons("ComputeMin")} + "{" "max" "}" -> FilterMinMax {bracket,cons("ComputeMax")} Index: src/syn/pctl/PCTL-Formula.sdf --- src/syn/pctl/PCTL-Formula.sdf (revision 0) +++ src/syn/pctl/PCTL-Formula.sdf (revision 0) @@ -0,0 +1,24 @@ +module PCTL-Formula +imports + PCTL-Property +exports + + %% EBNF Grammar: PCTL Formulas in our parser + %% + %% Formula ::= + %% Property + %% | "(" Formula ")" + + %% EBNF Grammar: PCTL Formulas as in PRISM's parser + %% + %% SinglePCTLFormula ::= PCTLFormula + %% + %% PCTLFormula ::= PCTLImplies + %% + %% PCTLImplies ::= PCTLOr ["=>" PCTLOr] + %% + + sorts Formula + context-free syntax + Property -> Formula {cons("Formula")} + "(" Formula ")" -> Formula {bracket} Index: src/syn/pctl/PCTL-StartSymbols.sdf --- src/syn/pctl/PCTL-StartSymbols.sdf (revision 0) +++ src/syn/pctl/PCTL-StartSymbols.sdf (revision 0) @@ -0,0 +1,17 @@ +%% Multiple start symbols for convenience +%% 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 +imports + PCTL-Main + +exports + context-free start-symbols + PropertiesFile + Expression + LabelDef + ConstantDef + Formula + Property + Path Index: src/syn/pctl/StrategoPCTL.sdf --- src/syn/pctl/StrategoPCTL.sdf (revision 0) +++ src/syn/pctl/StrategoPCTL.sdf (revision 0) @@ -0,0 +1,26 @@ +module StrategoPCTL +imports + StrategoRenamed + PCTL + PCTL-MetaVars + PCTL-MetaCongruences + +exports + context-free start-symbols StrategoModule + + context-free syntax + + "|[" LabelDef "]|" -> StrategoTerm {prefer,cons("ToTerm")} + "|[" ConstantDef "]|" -> StrategoTerm {prefer,cons("ToTerm")} + "|[" Formula "]|" -> StrategoTerm {prefer,cons("ToTerm")} + "|[" Property "]|" -> StrategoTerm {prefer,cons("ToTerm")} + "|[" Label "]|" -> StrategoTerm {prefer,cons("ToTerm")} + "|[" Path "]|" -> StrategoTerm {prefer,cons("ToTerm")} + "|[" Reward "]|" -> StrategoTerm {prefer,cons("ToTerm")} + "|[" Filter "]|" -> StrategoTerm {prefer,cons("ToTerm")} + + context-free syntax + + "~" StrategoTerm -> Expression {prefer,cons("FromTerm")} + "~id:" StrategoTerm -> ID {prefer,cons("FromTerm")} + "~label:" StrategoTerm -> Label {prefer,cons("FromTerm")} Index: src/syn/pctl/PCTL-Path.sdf --- src/syn/pctl/PCTL-Path.sdf (revision 0) +++ src/syn/pctl/PCTL-Path.sdf (revision 0) @@ -0,0 +1,23 @@ +module PCTL-Path +imports + PRISM-Expression + PCTL-Formula +exports + + %% EBNF Grammar: PCTL Paths + %% + %% Path ::= + %% "X" Formula + %% | Formula "U" "<=" Expression Formula + %% | Formula "U" ">=" Expression Formula + %% | Formula "U" "[" Expression "," Expression "]" Formula + %% | Formula "U" Formula + + sorts Path + context-free syntax + "X" Formula -> Path {cons("Next")} + Formula "U" "<=" Expression Formula -> Path {cons("BoundedUntilLtEq")} + Formula "U" ">=" Expression Formula -> Path {cons("BoundedUntilGtEq")} + Formula "U" "[" Expression "," Expression "]" Formula + -> Path {cons("BoundedUntilRange")} + Formula "U" Formula -> Path {cons("Until")} Index: src/syn/pctl/PCTL-PropertiesFile.sdf --- src/syn/pctl/PCTL-PropertiesFile.sdf (revision 0) +++ src/syn/pctl/PCTL-PropertiesFile.sdf (revision 0) @@ -0,0 +1,22 @@ +module PCTL-PropertiesFile +imports + PCTL-Label + PRISM-Constant + PCTL-Formula + +exports + + %% EBNF Grammar: PCTL top level stuff + %% + %% PropertiesFile ::= + %% {LabelDef} + %% | {ConstantDef} + %% | {SinglePCTLFormula} + + sorts PropertiesFile PropertiesFileSection + context-free syntax + PropertiesFileSection* -> PropertiesFile {cons("PropertiesFile")} + + LabelDef -> PropertiesFileSection + ConstantDef -> PropertiesFileSection + Formula -> PropertiesFileSection Index: src/syn/pctl/Makefile.am --- src/syn/pctl/Makefile.am (revision 0) +++ src/syn/pctl/Makefile.am (revision 0) @@ -0,0 +1,65 @@ +## +## Makefile.am for xrm in /home/tsuna/work/xrm/trunk/src/syn/pctl +## +## 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 +## + +include $(top_srcdir)/config/Transformers.mk +-include $(wildcard *.dep) + +PGEN_FLAGS = -m $* +SDF2RTG_FLAGS = -m $* +SCFLAGS = -O 2 +STRINCLUDES = -I $(srcdir) +SDFINCLUDES = -I $(srcdir) \ + -I $(STRATEGO_FRONT)/share/sdf/stratego-front \ + -I $(top_srcdir)/src/syn/prism + +pkgdata_DATA_built = \ + PCTL.def \ + PCTL.tbl \ + PCTL.rtg \ + PCTL.str \ + PCTL-StartSymbols.tbl \ + PCTL-Prefixed.def \ + StrategoPCTL.def \ + StrategoPCTL.tbl + +pkgdata_DATA = $(pkgdata_DATA_built) +sdfdata_DATA = $(pkgdata_DATA_built) +nobase_sdfdata_DATA = PCTL-Prefixed.sdf $(SDFS) + +CLEANFILES = $(pkgdata_DATA_built) \ + $(wildcard *.dep) \ + PCTL.{c,str,c.dep} \ + PCTL-StartSymbols.def \ + PCTL-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 + +EXTRA_DIST = $(SDFS) + +PCTL.def: $(SDFS) +PCTL-StartSymbols.def: $(SDFS) + +StrategoPCTL.def: StrategoPCTL.sdf \ + PCTL-MetaVars.sdf \ + PCTL-MetaCongruences.sdf + +PCTL-Prefixed.sdf: PCTL.def + $(SDF_TOOLS)/bin/gen-renamed-sdf-module -i $< -o $@ \ + --main PCTL --name PCTL-Prefixed --prefix PCTL Index: src/syn/pctl/PCTL-Label.sdf --- src/syn/pctl/PCTL-Label.sdf (revision 0) +++ src/syn/pctl/PCTL-Label.sdf (working copy) @@ -1,13 +1,10 @@ -module PRISM-Label +module PCTL-Label imports PRISM-Expression PRISM-Identifier exports - %% NOTE: Labels are used in properties files which we don't need to support - %% at this time. - %% EBNF Grammar: Labels %% LabelDef ::= "label" "\"" Identifier "\"" "=" Expression ";" Index: src/syn/pctl/PCTL-MetaCongruences.sdf --- src/syn/pctl/PCTL-MetaCongruences.sdf (revision 0) +++ src/syn/pctl/PCTL-MetaCongruences.sdf (revision 0) @@ -0,0 +1,12 @@ +module PCTL-MetaCongruences +exports + + context-free syntax + "|[" LabelDef "]|" -> StrategoStrategy {prefer,cons("ToStrategy")} + "|[" ConstantDef "]|" -> StrategoStrategy {prefer,cons("ToStrategy")} + "|[" Formula "]|" -> StrategoStrategy {prefer,cons("ToStrategy")} + "|[" Property "]|" -> StrategoStrategy {prefer,cons("ToStrategy")} + "|[" Label "]|" -> StrategoStrategy {prefer,cons("ToStrategy")} + "|[" Path "]|" -> StrategoStrategy {prefer,cons("ToStrategy")} + "|[" Reward "]|" -> StrategoStrategy {prefer,cons("ToStrategy")} + "|[" Filter "]|" -> StrategoStrategy {prefer,cons("ToStrategy")} Index: src/syn/pctl/PCTL-MetaVars.sdf --- src/syn/pctl/PCTL-MetaVars.sdf (revision 0) +++ src/syn/pctl/PCTL-MetaVars.sdf (revision 0) @@ -0,0 +1,11 @@ +module PCTL-MetaVars +exports + variables + [ijkln][0-9]* -> LInt {prefer} + [dr][0-9]* -> LDouble {prefer} + [xyzfgh][0-9]* -> ID {prefer} + [e][0-9]* -> Expression {prefer} + [F][0-9]* -> Formula {prefer} + [p][0-9]* -> Path {prefer} + [t][0-9]* -> Filter {prefer} + [R][0-9]* -> Reward {prefer} Index: src/syn/pctl/PCTL.sdf --- src/syn/pctl/PCTL.sdf (revision 0) +++ src/syn/pctl/PCTL.sdf (revision 0) @@ -0,0 +1,11 @@ +%% Single start symbol for faster parsing +%% 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 +imports + PCTL-Main + +exports + context-free start-symbols + PropertiesFile Index: src/syn/Makefile.am --- src/syn/Makefile.am (revision 58) +++ 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 Thu May 25 18:44:17 2006 SIGOURE Benoit +## Last update Fri Jun 9 19:16:48 2006 SIGOURE Benoit ## -SUBDIRS = prism xrm +SUBDIRS = prism pctl xrm Index: tests/pctl/man_examples.pctl --- tests/pctl/man_examples.pctl (revision 0) +++ tests/pctl/man_examples.pctl (revision 0) @@ -0,0 +1,96 @@ +P>=1 [ true U terminate ] +// the algorithm eventually terminates successfully with probability 1 + +"init" => P<0.1 [ true U<=100 num_errors > 5 ] +// from an initial state, the probability that more than 5 errors occur within +// the first 100 me units is less than 0.1 + +"down" => P>0.75 [ !"fail" U[1,2] "up" ] +// when a shutdown occurs, the probability of system recovery being completed +// in between and 2 hours without further failures occurring is greater than +// 0.75 + +S<0.01 [ num_sensors < min_sensors ] +// in the long-run, the probability that an inadequate number of sensors are +// operational is less than 0.01 + +P=? [ !proc2_terminate U proc1_terminate ] +// the probability that process 1 terminates before process 2 does + +Pmax=? [ true U<=T messages_lost > 10 ] +// the maximum probability that more than 10 messages have been lost by time T + +S=? [ queue_size / max_size > 0.75 ] +// the long-run probability that the queue is more than 75% full + +P<0.01 [ X y=1 ] +// the probability of the expression y=1 being true in the next state is less +// than 0.01. + +P>0.5 [ true U z=2 ] +// the probability that z is eventually equal to 2 is greater than 0.5 + +P>=0.98 [ true U<=7 y=4 ] +// the probability of y being equal to 4 within 7 time steps is greater than +// or equal to 0.98 + +P>=0.25 [ y<=1 U<=6.5 y>1 ] +P<0.4 [ y<=1 U>=5.5 y>1 ] + +P>0 [ y<=1 U[5.5,6.5] y>1 ] +// the probability that y first exceeds 1 the time interval [5.5, 6.5] is +// greater than zero + +S<0.05 [ queue_size / max_size > 0.75 ] +// the long-run probability of the queue being more than 75% full is less +// than 0.05. + +"init" => P>=1 [ true U leader_elected=true ] + +P=? [ true U x=5&y=5 ] +// returns the probability of, from the initial state, reaching a state +// satisfying x=5&y=5 + +P=? [ true U x=5&y=5 {x=1&y=2} ] +// returns the probability of, from the state (1,2) (i.e. x=1 and y=2), +// reaching a state satisfying x=5&y=5 + +P=? [ true U x=5&y=5 {y=2}{min} ] +P=? [ true U x=5&y=5 {y=2}{max} ] +// return the minimum and maximum probability, respectively, of reaching a +// state satisfying x=5&y=5 from all the states satisfying y=2. In addition, +// PRISM will report the states of the model in which the minimum or maximum +// probability is attained. + +P=? [ true U x=5&y=5 {y=2}{min}{max} ] +// both the minimum and maximum value are computed simultaneously + +P>0.5 [ true U x=5&y=5 {y=2} ] +// will return a Boolean value, depending whether the property is true in all +// states of the model or not, but the probability of path property true U +// x=5&y=5 being satisfied will be displayed for all states where y=2. + +const int k = 7; +const double T = 9.5; +const double p = 0.01; +P<p [ true U<=T x=k ] + +label "safe" = temp<=100 | alarm=true; +label "fail" = temp>100 & alarm=false; +P>=0.99 [ "safe" U "fail" ] + +"init" => P>=0.99 [ "safe" U "fail" ] + +R<=9.5 [ F z=2 ] +// the expected time taken to reach, from s, a state where z equals 2 is less +// than or equal to 9.5 + +R=? [ C<=15.5 ] +// the expected number of lost requests within 15.5 time units of operation. + +R<4.4 [ I=100 ] +// starting from s, the expected queue size exactly 100 time units later is +// less than 4.4 + +R<=0.7 [ S ] +// starting from s, the long-run average power consumption is less than 0.7 Index: tests/test-parse-pctl.sh.in --- tests/test-parse-pctl.sh.in (revision 58) +++ tests/test-parse-pctl.sh.in (working copy) @@ -1,6 +1,6 @@ #!/bin/sh ## -## test-parse-prism.sh for xrm in /home/tsuna/work/xrm/trunk/tests +## test-parse-pctl.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' | sort`; do +for file in `find "@srcdir@" -name '*.pctl' -o -name '*.csl' | sort`; do echo @ECHO_N@ " Parsing `basename $file` ... " - "@top_builddir@/src/tools/parse-prism" -i "$file" -o /dev/null + "@top_builddir@/src/tools/parse-pctl" -i "$file" -o /dev/null rv=$? test_cnt=$((test_cnt + 1)) if [ $rv -eq 0 ]; then Index: tests/Makefile.am --- tests/Makefile.am (revision 58) +++ tests/Makefile.am (working copy) @@ -5,15 +5,17 @@ ## Mail <sigoure.benoit(a)lrde.epita.fr> ## ## Started on Thu Apr 27 16:56:50 2006 SIGOURE Benoit -## Last update Thu May 25 17:29:32 2006 SIGOURE Benoit +## Last update Sat Jun 10 05:24:43 2006 SIGOURE Benoit ## #include $(top_srcdir)/config/toplevel.mk dist_check_SCRIPTS = \ test-parse-prism.sh \ + test-parse-pctl.sh \ test-parse-xrm.sh \ test-pp-prism.sh \ + test-pp-pctl.sh \ test-pp-xrm.sh \ test-xrm-front.sh @@ -25,8 +27,10 @@ TESTS_ENVIRONMENT = XTC_REPOSITORY="$(BUILD_REPOSITORY)" TESTS = test-parse-prism.sh \ + test-parse-pctl.sh \ test-parse-xrm.sh \ test-pp-prism.sh \ + test-pp-pctl.sh \ test-pp-xrm.sh \ test-xrm-front.sh \ test-summary.sh Index: tests/test-pp-pctl.sh.in --- tests/test-pp-pctl.sh.in (revision 58) +++ tests/test-pp-pctl.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-pctl.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-pctl' rm -f failed_tests.$$ test ! -d $target_dir && { mkdir $target_dir \ @@ -21,7 +21,7 @@ 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$//'`" @@ -29,7 +29,7 @@ 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-pctl" -i "$file" -o "$outdir/$bfile.aterm" if [ $? -ne 0 ]; then echo 'FAILED, continuing with the next test...' echo " * $file: parsing FAILED" >> failed_tests.$$ @@ -38,7 +38,7 @@ echo 'OK, no ambiguities found' echo @ECHO_N@ " Pretty printing $basefile ... " - "@top_builddir@/src/tools/pp-xrm" \ + "@top_builddir@/src/tools/pp-pctl" \ -i "$outdir/$bfile.aterm" -o "$outdir/$bfile.pp.xpm" if [ $? -ne 0 ]; then echo 'FAILED, continuing with the next test...' @@ -48,7 +48,7 @@ echo 'OK' echo @ECHO_N@ " Re-Parsing pretty printed file $basefile ... " - "@top_builddir@/src/tools/parse-xrm" \ + "@top_builddir@/src/tools/parse-pctl" \ -i "$outdir/$bfile.pp.xpm" -o "$outdir/$bfile.pp2aterm" if [ $? -ne 0 ]; then echo 'FAILED, here is the content of the file:' @@ -62,7 +62,7 @@ echo 'OK, no ambiguities found' echo @ECHO_N@ " Re-Pretty printing the re-parsed file $basefile ... " - "@top_builddir@/src/tools/pp-xrm" \ + "@top_builddir@/src/tools/pp-pctl" \ -i "$outdir/$bfile.pp2aterm" -o "$outdir/$bfile.pp2.xpm" if [ $? -ne 0 ]; then echo 'FAILED, continuing with the next test...' Index: configure.ac --- configure.ac (revision 58) +++ 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 Fri Jun 2 17:52:40 2006 SIGOURE Benoit +## Last update Sat Jun 10 05:25:09 2006 SIGOURE Benoit ## ## --------------- ## @@ -73,12 +73,15 @@ src/Makefile src/syn/Makefile src/syn/prism/Makefile + src/syn/pctl/Makefile src/syn/xrm/Makefile src/sig/Makefile src/str/Makefile src/lib/Makefile src/lib/prism/Makefile src/lib/prism/pp/Makefile + src/lib/pctl/Makefile + src/lib/pctl/pp/Makefile src/lib/xrm/Makefile src/lib/xrm/pp/Makefile src/lib/native/Makefile @@ -90,9 +93,13 @@ [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-pp-prism.sh], [chmod a=rx tests/test-pp-prism.sh]) +AC_CONFIG_FILES([tests/test-pp-pctl.sh], + [chmod a=rx tests/test-pp-pctl.sh]) AC_CONFIG_FILES([tests/test-pp-xrm.sh], [chmod a=rx tests/test-pp-xrm.sh]) Index: TODO --- TODO (revision 58) +++ TODO (working copy) @@ -124,6 +124,55 @@ [] x=3 -> ... // x=3 is impossible [] x=0 -> (x'=3) // x=3 is not in the definition range of x + ## ------------- ## + ## Optimizations ## + ## ------------- ## + + * If there are some optimization(s) available in xrm-front add a -O option + to enable them (and thus, leave them off by default). If there is more + than one level of optimization, try to add different optimization levels + (pretty much like in GCC): + -O 0 = no optimizations + -O 1 = little optimizations -or- safe optimizations + -O 2 = many optimizations -or- include rarely unsafe optimizations + -O 3 = all optimizations -or- include unsafe optimizations + + * Group variable declarations (Idea from Micha). Goal: reduce the size of the + output file by grouping declarations. When several modules declare the same + variable (such as var[i]) the same way, declarations could be grouped + together and then multiplied using variable renaming. This also seems to + produce more optimized C source (to be confirmed). + for i from 0 to 2 do => module test_0 + module test[i] => // code using a_0, b_0 + a[i]: [0..1] init 0; => endmodule + b[i]: [0..1] init 0; => module test_1 + if i = 2 then => // code using a_1. b_1 + d[i]: [0..1] init 0; => endmodule + end => module test_2 + // code => d_2: [0..1] init 0; + endmodule => // code using a_2, b_2, d_2 + end => endmodule + => module __vars_0 + => a_0: [0..1] init 0; + => b_0: [0..1] init 0; + => endmodule + => module __vars_1 + => = __vars_0 [a_0=a_1, b_0=b_1] + => endmodule + => module __vars_2 + => = __vars_0 [a_0=a_2, b_0=b_2] + => endmodule + With many definitions this can save quite a lot of space because variable + renaming is shorter than copying definitions over and over. + How to do this? Do we do this (partially?) before loops are unrolled? Or + do we do it at the very end of the pipeline (which implies that we have to + collect declarations, see which declarations could go together etc... + seems to be quite a mess since doing this sounds like recovering + information lost when unrolling loops). + Should we try to spot potential redundant declarations when unrolling + loops and then later try to group them? Would there be cases where + grouping gets tricky? What about d_2 above? + ## ----- ## ## Notes ## ## ----- ##

18 years, 7 months

XRM 58: Add ConstantDef in concrete syntax.

by SIGOURE Benoit

https://svn.lrde.epita.fr/svn/xrm/trunk Index: ChangeLog from SIGOURE Benoit <sigoure.benoit(a)lrde.epita.fr> Add ConstantDef in concrete syntax. * src/syn/prism/PRISM-ModulesFile.sdf: Remove useless comment. * src/syn/prism/StrategoPRISM.sdf: Add ConstantDef in concrete syntax. PRISM-ModulesFile.sdf | 6 ------ StrategoPRISM.sdf | 1 + 2 files changed, 1 insertion(+), 6 deletions(-) Index: src/syn/prism/PRISM-ModulesFile.sdf --- src/syn/prism/PRISM-ModulesFile.sdf (revision 57) +++ src/syn/prism/PRISM-ModulesFile.sdf (working copy) @@ -37,9 +37,3 @@ SystemComp -> ModulesFileSection RewardStruct -> ModulesFileSection Init -> ModulesFileSection - -%% At this time we don't need to be able to parse property files... - -%% LabelDef* -> PropertiesFile {cons("PropertiesFile")} -%% ConstantDef* -> PropertiesFile {cons("PropertiesFile")} -%% SinglePCTLFormula* -> PropertiesFile {cons("PropertiesFile")} Index: src/syn/prism/StrategoPRISM.sdf --- src/syn/prism/StrategoPRISM.sdf (revision 57) +++ src/syn/prism/StrategoPRISM.sdf (working copy) @@ -15,6 +15,7 @@ "|[" Expression "]|" -> StrategoTerm {prefer,cons("ToTerm")} "|[" Declaration "]|" -> StrategoTerm {prefer,cons("ToTerm")} "|[" Command "]|" -> StrategoTerm {prefer,cons("ToTerm")} + "|[" ConstantDef "]|" -> StrategoTerm {prefer,cons("ToTerm")} context-free syntax

18 years, 7 months

Jump to page:

2025

2024

2023

2022

2021

2020

2019

2018

2017

2016

2015

2014

2013

2012

2011

2010

2009

2008

2007

2006

2005

2004

Projects