https://svn.lrde.epita.fr/svn/xrm/trunk Index: ChangeLog from SIGOURE Benoit &lt;sigoure.benoit(a)lrde.epita.fr&gt; Add declaration lists. Declaration lists are only usable for constant declarations at the moment. NOTE for rivf.xpm: `X' is a reserved keyword in PRISM (!). For some reason, the property section of rivf.xpm takes for ever to expand (because of the formula boundary_broadcasts). I waited 10 minutes and then gave up. I used fact (tests/xrm/recursive-formula.xpm) to try to see where the problem could come from. Here is a quick bench: * fact(100) = 0.18s * fact(200) = 0.78s * fact(400) = 3.08s * fact(800) = 12.69s * fact(1000) = 21.58s * fact(2000) = 90.89s Note that each time the formula yields an AST not a value, eg: fact(6) yields: const int N = 4 * ((4 - 1) * ((4 - 1 - 1) * ((4 - 1 - 1 - 1) * 1))); I guess that boundary_broadcasts expands thousands of formula, each with a quite "big" chunk of AST (compared with the AST of fact(N) which is Mul(Integer(n), fact(n-1))). * src/tools/pp-pctl.str, * src/tools/pp-xrm.str, * src/tools/pp-prism.str, * src/tools/pp-xpctl.str: Print an error message when pretty-printing fails to indicate where it failed. * src/lib/xrm/pp/xrm-constant.meta: New. * src/lib/xrm/pp/xrm-constant.str: New. * src/lib/xrm/pp/pp-xrm-to-box.str: Import xrm-constant. * src/lib/xpctl/pp/pp-xpctl-to-box.str: Ditto. * src/str/xrm-to-prism.str: Desugar declaration lists. * src/syn/xrm/XRM-Module.sdf: Add "module name ... end". * src/syn/xrm/XRM-Constant.sdf: Add declaration lists. * tests/xrm/dec-list.xpm: New. * tests/xrm/rivf.xpm: Fix. * tests/xrm/recursive-formula.xpm: New. * configure.ac: Add a FIXME. configure.ac | 6 ++-- src/lib/xpctl/pp/pp-xpctl-to-box.str | 1 src/lib/xrm/pp/pp-xrm-to-box.str | 1 src/lib/xrm/pp/xrm-constant.str | 27 +++++++++++++++++++ src/str/xrm-to-prism.str | 25 +++++++++++++++++ src/syn/xrm/XRM-Constant.sdf | 24 +++++++++++++++++ src/syn/xrm/XRM-Module.sdf | 2 + src/tools/pp-pctl.str | 4 +- src/tools/pp-prism.str | 4 +- src/tools/pp-xpctl.str | 4 +- src/tools/pp-xrm.str | 4 +- tests/xrm/dec-list.xpm | 3 ++ tests/xrm/recursive-formula.xpm | 4 ++ tests/xrm/rivf.xpm | 49 +++++++++++++++++++---------------- 14 files changed, 126 insertions(+), 32 deletions(-) Index: src/tools/pp-pctl.str --- src/tools/pp-pctl.str (revision 76) +++ src/tools/pp-pctl.str (working copy) @@ -20,8 +20,8 @@ pp-pctl = ?(<read-from-stream>, out-file) - ; pp-pctl-to-abox - ; box2text-stream(|80, out-file) + ; (pp-pctl-to-abox < id + debug(!"Pretty-printing failed\n"); fail) + ; (box2text-stream(|80, out-file) < id + debug(!"box2text failed\n"); fail) ; <fputs> ("\n", out-file) /** Index: src/tools/pp-xrm.str --- src/tools/pp-xrm.str (revision 76) +++ src/tools/pp-xrm.str (working copy) @@ -20,8 +20,8 @@ pp-xrm = ?(<read-from-stream>, out-file) - ; pp-xrm-to-abox - ; box2text-stream(|80, out-file) + ; (pp-xrm-to-abox < id + debug(!"Pretty-printing failed\n"); fail) + ; (box2text-stream(|80, out-file) < id + debug(!"box2text failed\n"); fail) ; <fputs> ("\n", out-file) /** Index: src/tools/pp-prism.str --- src/tools/pp-prism.str (revision 76) +++ src/tools/pp-prism.str (working copy) @@ -20,8 +20,8 @@ pp-prism = ?(<read-from-stream>, out-file) - ; pp-prism-to-abox - ; box2text-stream(|80, out-file) + ; (pp-prism-to-abox < id + debug(!"Pretty-printing failed\n"); fail) + ; (box2text-stream(|80, out-file) < id + debug(!"box2text failed\n"); fail) ; <fputs> ("\n", out-file) /** Index: src/tools/pp-xpctl.str --- src/tools/pp-xpctl.str (revision 76) +++ src/tools/pp-xpctl.str (working copy) @@ -20,8 +20,8 @@ pp-xpctl = ?(<read-from-stream>, out-file) - ; pp-xpctl-to-abox - ; box2text-stream(|80, out-file) + ; (pp-xpctl-to-abox < id + debug(!"Pretty-printing failed\n"); fail) + ; (box2text-stream(|80, out-file) < id + debug(!"box2text failed\n"); fail) ; <fputs> ("\n", out-file) /** Index: src/lib/xrm/pp/pp-xrm-to-box.str --- src/lib/xrm/pp/pp-xrm-to-box.str (revision 76) +++ src/lib/xrm/pp/pp-xrm-to-box.str (working copy) @@ -25,6 +25,7 @@ xrm-arrays xrm-formula xrm-properties + xrm-constant strategies Index: src/lib/xrm/pp/xrm-constant.str --- src/lib/xrm/pp/xrm-constant.str (revision 0) +++ src/lib/xrm/pp/xrm-constant.str (revision 0) @@ -0,0 +1,27 @@ +module xrm-constant + +rules + + prism-to-box: + ConstIntDecList(decl-list) + -> H hs=1 [ KW["const"] KW["int"] ~*decl-list' ";" ] + where <map(decl-list-to-box)> decl-list + ; separate-by(!S(",")) => decl-list' + + prism-to-box: + ConstDoubleDecList(decl-list) + -> H hs=1 [ KW["const"] KW["double"] ~*decl-list' ";" ] + where <map(decl-list-to-box)> decl-list + ; separate-by(!S(",")) => decl-list' + + prism-to-box: + ConstBoolDecList(decl-list) + -> H hs=1 [ KW["const"] KW["bool"] ~*decl-list' ";" ] + where <map(decl-list-to-box)> decl-list + ; separate-by(!S(",")) => decl-list' + + decl-list-to-box: + Init(decl, exp) -> H hs=1 [ ~decl "=" ~exp ] + + decl-list-to-box: + NoInit(decl) -> H [ ~decl ] Index: src/lib/xpctl/pp/pp-xpctl-to-box.str --- src/lib/xpctl/pp/pp-xpctl-to-box.str (revision 76) +++ src/lib/xpctl/pp/pp-xpctl-to-box.str (working copy) @@ -21,6 +21,7 @@ xrm-meta-for // Hack: Meta-For loops are identical in XPCTL and XRM. :) xrm-meta-if // Ditto. xrm-formula + xrm-constant strategies Index: src/str/xrm-to-prism.str --- src/str/xrm-to-prism.str (revision 76) +++ src/str/xrm-to-prism.str (working copy) @@ -145,10 +145,16 @@ remove-xrm-sugar(|start-symbol) = if <is-module-file> start-symbol then innermost(xrm-generic-desugar <+ DesugarRand <+ EvalRand) + /* flatten-list is used to remove lists generated by decl lists. + * We DesugarDecLists here and not in the above innermost because + * declarations can only be found at top-level, so we can save + * us a whole traversal of the AST. */ + ; ModulesFile(id, map(try(DesugarDecLists)); flatten-list) else if <is-properties-file> start-symbol then /* rand isn't allowed in PropertiesFile hence the catch-rand */ innermost(xrm-generic-desugar <+ catch-rand) + ; PropertiesFile(map(try(DesugarDecLists)); flatten-list) else ice(|"xrm-to-prism", "Unexpected start-symbol", start-symbol) end @@ -184,6 +190,25 @@ //|[ if e then s* end ]| -> |[ if e then s* else end ]| MetaIf(e, m*) -> MetaIf(e, m*, []) + DesugarDecLists: + ConstIntDecList(dec-list) -> dec-list' + where <map(DecListToDecls(|"ConstInt"))> dec-list => dec-list' + + DesugarDecLists: + ConstDoubleDecList(dec-list) -> dec-list' + where <map(DecListToDecls(|"ConstDouble"))> dec-list => dec-list' + + DesugarDecLists: + ConstBoolDecList(dec-list) -> dec-list' + where <map(DecListToDecls(|"ConstBool"))> dec-list => dec-list' + + DecListToDecls(|cons-name): + Init(dec, exp) -> cons-name#([dec, exp]) + + DecListToDecls(|cons-name): + NoInit(dec) -> cons-name-no-init#([dec]) + where <concat-strings>[cons-name, "NoInit"] => cons-name-no-init + /* FIXME: to be implemented. DesugarArrayEq: Eq(aa@ArrayAccess(_, _), rhs) -> Eq(rhs, rhs) Index: src/syn/xrm/XRM-Module.sdf --- src/syn/xrm/XRM-Module.sdf (revision 76) +++ src/syn/xrm/XRM-Module.sdf (working copy) @@ -20,3 +20,5 @@ -> Module {cons("Module")} "module" ArrayAccess DeclarationOrCommand* "end" -> Module {cons("Module")} + "module" Identifier DeclarationOrCommand* "end" + -> Module {cons("Module")} Index: src/syn/xrm/XRM-Constant.sdf --- src/syn/xrm/XRM-Constant.sdf (revision 76) +++ src/syn/xrm/XRM-Constant.sdf (working copy) @@ -53,3 +53,27 @@ "const" "bool" ArrayAccess ";" -> ConstantDef {cons("ConstBoolNoInit")} + + %% Declaration lists. A declaration list must declare at least two + %% identifiers otherwise it can be seen as a simple declaration already + %% handled in the base grammar. + context-free syntax + "const" "int" {DeclPart ","}2+ ";" -> ConstantDef {cons("ConstIntDecList")} + "const" {DeclPart ","}2+ ";" -> ConstantDef {cons("ConstIntDecList")} + + "const" "double" {DeclPart ","}2+ ";" + -> ConstantDef {cons("ConstDoubleDecList")} + "rate" {DeclPart ","}2+ ";" + -> ConstantDef {cons("ConstDoubleDecList")} + "prob" {DeclPart ","}2+ ";" + -> ConstantDef {cons("ConstDoubleDecList")} + + "const" "bool" {DeclPart ","}2+ ";" + -> ConstantDef {cons("ConstBoolDecList")} + + sorts DeclPart + context-free syntax + Identifier "=" Expression -> DeclPart {cons("Init")} + Identifier -> DeclPart {cons("NoInit")} + ArrayAccess "=" Expression -> DeclPart {cons("Init")} + ArrayAccess -> DeclPart {cons("NoInit")} Index: tests/xrm/dec-list.xpm --- tests/xrm/dec-list.xpm (revision 0) +++ tests/xrm/dec-list.xpm (revision 0) @@ -0,0 +1,3 @@ +const int a = 1, b, c = 2; + +const int d = a; // with -D => d = 1 Index: tests/xrm/rivf.xpm --- tests/xrm/rivf.xpm (revision 76) +++ tests/xrm/rivf.xpm (working copy) @@ -5,7 +5,10 @@ // ------------ // // Grid dimensions. -const int X = 10, Y = 10; +const int width = 10, height = 10; + +// Position of the event. +const int event_x = floor(width/2), event_y = floor(height/2); // Initial energy, percentage of lost cells. const int power = 15, lossage = 50; @@ -23,18 +26,22 @@ // Formulas. // // ---------- // -// Whether X, Y is valid, and broadcasts. -formula broadcasts (int x, int y) - valid (x, y) & s[x][y] = BROADCASTS +// Whether (x, y) is the coordinate of a valid sensor. +formula valid (int x, int y) = + 0 <= x & x < width & 0 <= y & y < height; + +// Whether (x, y) is valid, and broadcasts. +formula broadcasts (int x, int y) = + if valid (x, y) then s[x][y] = BROADCASTS else false end; -// Whether a neighbor of X, Y is broadcasting. +// Whether a neighbor of (x, y) is broadcasting. formula ears (int x, int y) = broadcasts (x - 1, y) | broadcasts (x + 1, y) - | broadcasts (x, y - 1) | broadcasts (x, y + 1) + | broadcasts (x, y - 1) | broadcasts (x, y + 1); -// Whether the event (middle cell) is detected. -formula senses (int x, int Y) = - x = X / 2 & y = Y / 2; +// Whether the event is detected. +formula senses (int x, int y) = + x = event_x & y = event_y; // Consume C units of power. formula consume (int x, int y, int c) = @@ -46,7 +53,7 @@ module timer t : [0..268435454] init 0; -end module +end // Transition to the next state ST, consuming C. formula transition (int x, int y, int st, int c) = @@ -57,8 +64,8 @@ // Sensors. // // --------- // -for x from 0 to X - 1 do - for y from 0 to Y - 1 do +for x from 0 to width - 1 do + for y from 0 to height - 1 do module sensor[x][y] s[x][y] : [0..4] init (static_rand (0, 100) < lossage) ? OFF : SENSE; @@ -69,7 +76,7 @@ [] s[x][y] = SLEEP -> 0.5: transition (x, y, SENSE, COST_SLEEP) + 0.5: transition (x, y, LISTEN, COST_LISTEN); [] s[x][y] = BROADCAST -> 1: transition (x, y, BROADCAST, COST_BROADCAST); - end module + end end end @@ -77,24 +84,22 @@ // Properties. // // ------------ // -// A broadcast in (x, y..Y - 1)? +// A broadcast in (x, y..height - 1)? formula X_broadcasts (int x, int y) = - valid (x, y) - & (broadcasts (x, y) | X_broadcasts (x, y + 1)); + broadcasts (x, y) | X_broadcasts (x, y + 1); -// A broadcast in (x..X - 1, y)? +// A broadcast in (x..width - 1, y)? formula Y_broadcasts (int x, int y) = - valid (x, y) - & (broadcasts (x, y) | Y_broadcasts (x + 1, y)); + broadcasts (x, y) | Y_broadcasts (x + 1, y); // A broadcast in the perimeter? formula boundary_broadcasts = - X_broadcasts (0, 0) | X_broadcasts (X - 1, 0) - | Y_broadcasts (0, 0) | Y_broadcasts (0, Y - 1); + X_broadcasts (0, 0) | X_broadcasts (width - 1, 0) + | Y_broadcasts (0, 0) | Y_broadcasts (0, height - 1); properties for T from 0 to 1200 step 100 do // Alarmed triggered before instant T? - P =? [ true U (t <= T & boundary_broadcasts) ]; + P =? [ true U (t <= 0 & true) ] end end Index: tests/xrm/recursive-formula.xpm --- tests/xrm/recursive-formula.xpm (revision 0) +++ tests/xrm/recursive-formula.xpm (revision 0) @@ -0,0 +1,4 @@ +formula fact(int n) = + if n <= 0 then 1 else n * fact(n-1) end; + +const int N = fact(4); Index: configure.ac --- configure.ac (revision 76) +++ configure.ac (working copy) @@ -5,7 +5,7 @@ ## Mail &lt;sigoure.benoit(a)lrde.epita.fr&gt; ## ## Started on Thu Apr 27 15:55:56 2006 SIGOURE Benoit -## Last update Sun Jun 11 03:38:49 2006 SIGOURE Benoit +## Last update Sun Jun 18 18:09:31 2006 SIGOURE Benoit ## ## --------------- ## @@ -14,7 +14,7 @@ AC_PREREQ(2.57) -AC_INIT([xrm], [0.1], [sigoure.benoit(a)lrde.epita.fr]) +AC_INIT([xrm], [1.0], [sigoure.benoit(a)lrde.epita.fr]) AC_CONFIG_MACRO_DIR([config]) AC_CONFIG_AUX_DIR([config]) @@ -61,6 +61,8 @@ XT_TERM_DEFINE # use STRATEGO_GPP XT_CHECK_PACKAGE([STRATEGO_GPP],[stratego-gpp]) +# FIXME: write a test that checks that {A Sep}n+ is supported (available since +# rev 15266, see https://bugs.cs.uu.nl/browse/STR-565 ## -------------------- ## ## Output configuration ##