- Projects

Re: XRM 79: Generalize ranges.
by Akim Demaille 19 Jun '06

19 Jun '06

>>> "SIGOURE" == SIGOURE Benoit <sigoure.benoit(a)lrde.epita.fr> writes: Something is rotten in your kingdom. You should factor simultaneously. > @@ -69,8 +24,7 @@ > IntDecNoInit(aa@ArrayAccess(aa_idf, _), low, up) -> int-decl-no-init-list > where <fetch-idf> aa_idf => idf > - ; <desugar-array-access-for-decl> aa > - ; desugar-array-access > + ; <desugar-array-access> aa > ; desugared-array-access-list-to-identifier-list(|idf) > ; map({var-name: > ?var-name > @@ -83,8 +37,7 @@ > IntDec(aa@ArrayAccess(aa_idf, _), low, up, value) -> int-decl-list > where <fetch-idf> aa_idf => idf > - ; <desugar-array-access-for-decl> aa > - ; desugar-array-access > + ; <desugar-array-access> aa > ; desugared-array-access-list-to-identifier-list(|idf) > ; map({var-name: > ?var-name > @@ -99,8 +52,7 @@ > BoolDecNoInit(aa@ArrayAccess(aa_idf, _)) -> bool-decl-no-init-list > where <fetch-idf> aa_idf => idf > - ; <desugar-array-access-for-decl> aa > - ; desugar-array-access > + ; <desugar-array-access> aa > ; desugared-array-access-list-to-identifier-list(|idf) > ; map({var-name: > ?var-name > @@ -113,8 +65,7 @@ > BoolDec(aa@ArrayAccess(aa_idf, _), value) -> bool-decl-list > where <fetch-idf> aa_idf => idf > - ; <desugar-array-access-for-decl> aa > - ; desugar-array-access > + ; <desugar-array-access> aa > ; desugared-array-access-list-to-identifier-list(|idf) > ; map({var-name: > ?var-name > @@ -133,8 +84,7 @@ > ConstInt(aa@ArrayAccess(aa_idf, _), value) -> const-int-decl-list > where <fetch-idf> aa_idf => idf > - ; <desugar-array-access-for-decl> aa > - ; desugar-array-access > + ; <desugar-array-access> aa > ; desugared-array-access-list-to-identifier-list(|idf) > ; map({var-name: > ?var-name > @@ -147,8 +97,7 @@ > ConstIntNoInit(aa@ArrayAccess(aa_idf, _)) -> const-int-decl-no-init-list > where <fetch-idf> aa_idf => idf > - ; <desugar-array-access-for-decl> aa > - ; desugar-array-access > + ; <desugar-array-access> aa > ; desugared-array-access-list-to-identifier-list(|idf) > ; map({var-name: > ?var-name > @@ -163,8 +112,7 @@ > ConstDouble(aa@ArrayAccess(aa_idf, _), value) -> const-double-decl-list > where <fetch-idf> aa_idf => idf > - ; <desugar-array-access-for-decl> aa > - ; desugar-array-access > + ; <desugar-array-access> aa > ; desugared-array-access-list-to-identifier-list(|idf) > ; map({var-name: > ?var-name > @@ -177,8 +125,7 @@ > ConstDoubleNoInit(aa@ArrayAccess(aa_idf, _)) -> const-double-decl-no-init-list > where <fetch-idf> aa_idf => idf > - ; <desugar-array-access-for-decl> aa > - ; desugar-array-access > + ; <desugar-array-access> aa > ; desugared-array-access-list-to-identifier-list(|idf) > ; map({var-name: > ?var-name > @@ -193,8 +140,7 @@ > ConstBool(aa@ArrayAccess(aa_idf, _), value) -> const-bool-decl-list > where <fetch-idf> aa_idf => idf > - ; <desugar-array-access-for-decl> aa > - ; desugar-array-access > + ; <desugar-array-access> aa > ; desugared-array-access-list-to-identifier-list(|idf) > ; map({var-name: > ?var-name > @@ -207,8 +153,7 @@ > ConstBoolNoInit(aa@ArrayAccess(aa_idf, _)) -> const-bool-decl-no-init-list > where <fetch-idf> aa_idf => idf > - ; <desugar-array-access-for-decl> aa > - ; desugar-array-access > + ; <desugar-array-access> aa > ; desugared-array-access-list-to-identifier-list(|idf) > ; map({var-name:

1 0

Re: XRM 77: Add declaration lists.
by Akim Demaille 19 Jun '06

19 Jun '06

>>> "SIGOURE" == SIGOURE Benoit <sigoure.benoit(a)lrde.epita.fr> writes: Hum, nice, and heavily factored. I love that! > 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)

1 0

Re: monoburg 60: Fix the recipient of Vcs' messages
by Akim Demaille 19 Jun '06

19 Jun '06

>>> "Roland" == Roland Levillain <roland(a)lrde.epita.fr> writes: > Vcs' messages go to the projects list instead of the tiger-patches > list, as for Nolimips and HAVM. I prefer tiger-patches for havm. I would vote for tiger-patches for the other two, but I'm not responsible for them.

2 1

XRM 79: Generalize ranges.
by SIGOURE Benoit 18 Jun '06

18 Jun '06

https://svn.lrde.epita.fr/svn/xrm/trunk Index: ChangeLog from SIGOURE Benoit <sigoure.benoit(a)lrde.epita.fr> Generalize ranges. /!\ Backward compatibility broken! In order to declare an array, one MUST now use ranges. Before this commit, declarations such as: const int array[N]; were desugared down to: const int array[0..N-1]; This expansion will no longer take place automatically so one must write const int array[0..N-1] explicitly. Writing const int array[N] will only declare one variable, that is the Nth variable of the array. * src/str/array-decl-desugar.str: Remove automatic desugarisation of array declarations. * src/str/eval-meta-code.str: Remove now useless comments and annotations about substituted meta-vars. * src/str/signatures.str: Remove non longer needed signature. * tests/xrm/exists-eq.xpm, * tests/xrm/array-decl-with-meta-and-non-meta-and-exp.xpm, * tests/xrm/cond-array-access.xpm, * tests/xrm/array-decl_1d.xpm, * tests/xrm/array-decl_3d.xpm, * tests/xrm/priorities-exp-array-subscript.xpm, * tests/xrm/array-decl_dim_exp.xpm, * tests/xrm/array-decl-with-meta-and-non-meta.xpm, * tests/xrm/static-const-arrays-desugar.xpm, * tests/xrm/array-decl_2d.xpm, * tests/xrm/consts.xpm, * tests/xrm/array_with_static_dim.xpm: Update array declarations. * doc/user-guide.txt: Bring up to date. doc/user-guide.txt | 49 +++------- src/str/array-decl-desugar.str | 75 ++-------------- src/str/eval-meta-code.str | 11 -- src/str/signatures.str | 8 - tests/xrm/array-decl-with-meta-and-non-meta-and-exp.xpm | 2 tests/xrm/array-decl-with-meta-and-non-meta.xpm | 2 tests/xrm/array-decl_1d.xpm | 8 - tests/xrm/array-decl_2d.xpm | 8 - tests/xrm/array-decl_3d.xpm | 8 - tests/xrm/array-decl_dim_exp.xpm | 2 tests/xrm/array_with_static_dim.xpm | 2 tests/xrm/cond-array-access.xpm | 2 tests/xrm/consts.xpm | 12 +- tests/xrm/exists-eq.xpm | 4 tests/xrm/priorities-exp-array-subscript.xpm | 4 tests/xrm/static-const-arrays-desugar.xpm | 4 16 files changed, 59 insertions(+), 142 deletions(-) Index: src/str/array-decl-desugar.str --- src/str/array-decl-desugar.str (revision 78) +++ src/str/array-decl-desugar.str (working copy) @@ -9,51 +9,6 @@ module array-decl-desugar imports desugar-array-access -strategies - - /** - ** Desugar dimensions in array declarations in explicit ranges. - ** eg: x[1,2][4] is desugared to x[1,2][0..3] - */ - desugar-array-access-for-decl = - ArrayAccess(try(desugar-array-access-for-decl), try(try-add-range)) - - /** - ** Try to add a range if one of the dimensions is a simple Int - */ - try-add-range = - if ?[single-elem] then // we might need to add a range (x[4] -> x[0..3]) - /* in the current term (including subterms), we're collecting all the - * annotations that match Generated(_) which means that the dimensions - * has been generated by eval-meta-code and must no be transformed into - * a range */ - where(collect-all({a*:?_{a*};<fetch(?Generated(_))> a*}) => genlist) - ; prism-desugar - ; if !genlist => [] then // the dimension wasn't generated: - add-range // we can (try to) expand it in a range - end - else // no need to add a range, simply desugar the array access - prism-desugar - end - -rules - - /** @internal Rewrite simple dimensions with ranges (x[4] -> x[0..3]). */ - add-range: - [Int(i)] -> [Range(Int("0"), Int(j))] - where if <eq>(i, "0") then - err-msg(|"array declared with a size of 0 element") - ; debug - ; <xtc-exit> 2 - else - if <ltS>(i, "0") then - err-msg(|"array declared with a negative number of elements") - ; debug - ; <xtc-exit> 2 - end - end - ; <subtS>(i, "1") => j - rules // FIXME: Try to figure out why concrete syntax fails to work here. // FIXME: Try to put some code in common in order to shorten the rules. @@ -69,8 +24,7 @@ IntDecNoInit(aa@ArrayAccess(aa_idf, _), low, up) -> int-decl-no-init-list where <fetch-idf> aa_idf => idf - ; <desugar-array-access-for-decl> aa - ; desugar-array-access + ; <desugar-array-access> aa ; desugared-array-access-list-to-identifier-list(|idf) ; map({var-name: ?var-name @@ -83,8 +37,7 @@ IntDec(aa@ArrayAccess(aa_idf, _), low, up, value) -> int-decl-list where <fetch-idf> aa_idf => idf - ; <desugar-array-access-for-decl> aa - ; desugar-array-access + ; <desugar-array-access> aa ; desugared-array-access-list-to-identifier-list(|idf) ; map({var-name: ?var-name @@ -99,8 +52,7 @@ BoolDecNoInit(aa@ArrayAccess(aa_idf, _)) -> bool-decl-no-init-list where <fetch-idf> aa_idf => idf - ; <desugar-array-access-for-decl> aa - ; desugar-array-access + ; <desugar-array-access> aa ; desugared-array-access-list-to-identifier-list(|idf) ; map({var-name: ?var-name @@ -113,8 +65,7 @@ BoolDec(aa@ArrayAccess(aa_idf, _), value) -> bool-decl-list where <fetch-idf> aa_idf => idf - ; <desugar-array-access-for-decl> aa - ; desugar-array-access + ; <desugar-array-access> aa ; desugared-array-access-list-to-identifier-list(|idf) ; map({var-name: ?var-name @@ -133,8 +84,7 @@ ConstInt(aa@ArrayAccess(aa_idf, _), value) -> const-int-decl-list where <fetch-idf> aa_idf => idf - ; <desugar-array-access-for-decl> aa - ; desugar-array-access + ; <desugar-array-access> aa ; desugared-array-access-list-to-identifier-list(|idf) ; map({var-name: ?var-name @@ -147,8 +97,7 @@ ConstIntNoInit(aa@ArrayAccess(aa_idf, _)) -> const-int-decl-no-init-list where <fetch-idf> aa_idf => idf - ; <desugar-array-access-for-decl> aa - ; desugar-array-access + ; <desugar-array-access> aa ; desugared-array-access-list-to-identifier-list(|idf) ; map({var-name: ?var-name @@ -163,8 +112,7 @@ ConstDouble(aa@ArrayAccess(aa_idf, _), value) -> const-double-decl-list where <fetch-idf> aa_idf => idf - ; <desugar-array-access-for-decl> aa - ; desugar-array-access + ; <desugar-array-access> aa ; desugared-array-access-list-to-identifier-list(|idf) ; map({var-name: ?var-name @@ -177,8 +125,7 @@ ConstDoubleNoInit(aa@ArrayAccess(aa_idf, _)) -> const-double-decl-no-init-list where <fetch-idf> aa_idf => idf - ; <desugar-array-access-for-decl> aa - ; desugar-array-access + ; <desugar-array-access> aa ; desugared-array-access-list-to-identifier-list(|idf) ; map({var-name: ?var-name @@ -193,8 +140,7 @@ ConstBool(aa@ArrayAccess(aa_idf, _), value) -> const-bool-decl-list where <fetch-idf> aa_idf => idf - ; <desugar-array-access-for-decl> aa - ; desugar-array-access + ; <desugar-array-access> aa ; desugared-array-access-list-to-identifier-list(|idf) ; map({var-name: ?var-name @@ -207,8 +153,7 @@ ConstBoolNoInit(aa@ArrayAccess(aa_idf, _)) -> const-bool-decl-no-init-list where <fetch-idf> aa_idf => idf - ; <desugar-array-access-for-decl> aa - ; desugar-array-access + ; <desugar-array-access> aa ; desugared-array-access-list-to-identifier-list(|idf) ; map({var-name: ?var-name Index: src/str/eval-meta-code.str --- src/str/eval-meta-code.str (revision 78) +++ src/str/eval-meta-code.str (working copy) @@ -10,13 +10,6 @@ ** fact that the `&' is lazy and that s[x-1] won't be expanded for invalid ** values of x. ** -** The code generated is annotated with the Generated("s") annotation where -** s is the name of the strategy which generated the code (can be useful for -** debugging). -** We annotate generated code because the rest of the pipeline might need to -** know what has been generated and what comes from the user to take -** different actions depending on that (eg: in array-decl-desugar.str). -** ** NOTE: This is a tricky part so debugging stuff have been kept and ** commented out instead of being deleted. Hopefully this will make ** debugging easier. This might also make the code easier to understand. @@ -160,7 +153,7 @@ ///*DEBUG*/; printf(|" i = ", i) ///*DEBUG*/; say(!" <<< gen-meta-for -- propagating meta-var's value <<< ") ; !body - ; topdown(try(?meta-var; !Int(i){Generated("gen-meta-for")})) + ; topdown(try(?meta-var; !Int(i))) ///*DEBUG*/; debug ///*DEBUG*/; say(!" ~~~ gen-meta-for: now recursing") ; eval-meta-code => generated-code @@ -196,7 +189,7 @@ ///*DEBUG*/; printf(|" exp-to-replace = ", exp-to-replace) ///*DEBUG*/; say(!" <<< gen-meta-forin -- propagating meta-var's value <<< ") ; !body - ; topdown(try(?meta-var; !exp-to-replace{Generated("gen-meta-forin")})) + ; topdown(try(?meta-var; !exp-to-replace)) ///*DEBUG*/; debug ///*DEBUG*/; say(!" ~~~ gen-meta-forin: now recursing") ; eval-meta-code => generated-code Index: src/str/signatures.str --- src/str/signatures.str (revision 78) +++ src/str/signatures.str (working copy) @@ -14,11 +14,3 @@ */ signature constructors FIXME : FIXME - -/** -** used in eval-meta-code.str -** annotation to indicate generated code which must not go through further -** expansions. -*/ -signature constructors - Generated : String -> Generated Index: tests/xrm/exists-eq.xpm --- tests/xrm/exists-eq.xpm (revision 78) +++ tests/xrm/exists-eq.xpm (working copy) @@ -1,8 +1,8 @@ formula N = 4; module test - x[N] : [0..42]; - y[4][4] : [0..42] init 0; + x[0..N] : [0..42]; + y[0..4][0..4] : [0..42] init 0; [] x[3]?=0 -> true; [] y[3][2]?=0 -> true; Index: tests/xrm/array-decl-with-meta-and-non-meta-and-exp.xpm --- tests/xrm/array-decl-with-meta-and-non-meta-and-exp.xpm (revision 78) +++ tests/xrm/array-decl-with-meta-and-non-meta-and-exp.xpm (working copy) @@ -1,5 +1,5 @@ for i from 0 to 4 do for j in 0, 1 do - const int N[i+2+j][3] = 0; + const int N[i+2+j][0..3] = 0; end end Index: tests/xrm/cond-array-access.xpm --- tests/xrm/cond-array-access.xpm (revision 78) +++ tests/xrm/cond-array-access.xpm (working copy) @@ -1,4 +1,4 @@ module test - x[4] : [0..42] init 0; + x[0..4] : [0..42] init 0; [] x[-1<0?0:-1]=0 -> true; endmodule Index: tests/xrm/array-decl_1d.xpm --- tests/xrm/array-decl_1d.xpm (revision 78) +++ tests/xrm/array-decl_1d.xpm (working copy) @@ -1,8 +1,8 @@ // should be expanded in x_0 x_1 x_2 x_3 module arrays - x[4] : [0..42]; - y[4] : [0..42] init 0; - b[4] : bool; - c[4] : bool init true; + x[0..4] : [0..42]; + y[0..4] : [0..42] init 0; + b[0..4] : bool; + c[0..4] : bool init true; endmodule Index: tests/xrm/array-decl_3d.xpm --- tests/xrm/array-decl_3d.xpm (revision 78) +++ tests/xrm/array-decl_3d.xpm (working copy) @@ -1,8 +1,8 @@ // should be expanded in x_0_0_0 x_0_0_1 x_0_0_2 x_0_0_3 ... module arrays - x[4][3][2] : [0..42]; - y[4][3][2] : [0..42] init 0; - b[4][3][2] : bool; - c[4][3][2] : bool init true; + x[0..4][0..3][0..2] : [0..42]; + y[0..4][0..3][0..2] : [0..42] init 0; + b[0..4][0..3][0..2] : bool; + c[0..4][0..3][0..2] : bool init true; endmodule Index: tests/xrm/priorities-exp-array-subscript.xpm --- tests/xrm/priorities-exp-array-subscript.xpm (revision 78) +++ tests/xrm/priorities-exp-array-subscript.xpm (working copy) @@ -1,7 +1,7 @@ module test - x[3] : bool init false; + x[0..3] : bool init false; y : bool init true; - x[4] : [0..42] init 0; + x[0..4] : [0..42] init 0; //[] true -> x[1|1]'=true; [] x[true?2:3]=0 -> true; Index: tests/xrm/array-decl_dim_exp.xpm --- tests/xrm/array-decl_dim_exp.xpm (revision 78) +++ tests/xrm/array-decl_dim_exp.xpm (working copy) @@ -1,5 +1,5 @@ // should be equivalent as declaring x[8] module arrays - x[4+4] : [0..42]; + x[0..4+4] : [0..42]; endmodule Index: tests/xrm/array-decl-with-meta-and-non-meta.xpm --- tests/xrm/array-decl-with-meta-and-non-meta.xpm (revision 78) +++ tests/xrm/array-decl-with-meta-and-non-meta.xpm (working copy) @@ -1,3 +1,3 @@ for i from 0 to 4 do - const int N[i][3] = 0; + const int N[i][0..3] = 0; end Index: tests/xrm/static-const-arrays-desugar.xpm --- tests/xrm/static-const-arrays-desugar.xpm (revision 78) +++ tests/xrm/static-const-arrays-desugar.xpm (working copy) @@ -1,8 +1,8 @@ const int N = 3; -const int array[N] = 42; +const int array[0..N] = 42; module test - x[N] : [0..N] init array[N]; + x[0..N] : [0..N] init array[N]; [] x[array[N]]=0 -> (x[array[N]]'=1); endmodule Index: tests/xrm/array-decl_2d.xpm --- tests/xrm/array-decl_2d.xpm (revision 78) +++ tests/xrm/array-decl_2d.xpm (working copy) @@ -3,8 +3,8 @@ // x_0_2 x_1_2 x_2_2 x_3_2 module arrays - x[4][3] : [0..42]; - y[4][3] : [0..42] init 0; - b[4][3] : bool; - c[4][3] : bool init true; + x[0..4][0..3] : [0..42]; + y[0..4][0..3] : [0..42] init 0; + b[0..4][0..3] : bool; + c[0..4][0..3] : bool init true; endmodule Index: tests/xrm/consts.xpm --- tests/xrm/consts.xpm (revision 78) +++ tests/xrm/consts.xpm (working copy) @@ -2,9 +2,9 @@ const int x[i] = 2*i; end -const int y[5]; -const z[5] = 42; -const double d[3] = 3.14; -rate c[4] = 42 > 3.14; -probe d[4]; -const bool b[3] = true; +const int y[0..5]; +const z[0..5] = 42; +const double d[0..3] = 3.14; +rate c[0..4] = 42 > 3.14; +probe d[0..4]; +const bool b[0..3] = true; Index: tests/xrm/array_with_static_dim.xpm --- tests/xrm/array_with_static_dim.xpm (revision 78) +++ tests/xrm/array_with_static_dim.xpm (working copy) @@ -1,5 +1,5 @@ const int N = 10; module test - s[N] : [0..1]; + s[0..N] : [0..1]; endmodule Index: doc/user-guide.txt --- doc/user-guide.txt (revision 78) +++ doc/user-guide.txt (working copy) @@ -37,6 +37,7 @@ Once Nix is installed, use the following commands (you might need to be root depending on how you installed nix): $ nix-channel --add http://nix.cs.uu.nl/dist/stratego/channels-v3/strategoxt-unstable + $ nix-env -u '*' $ nix-env --install aterm sdf2-bundle strategoxt There you are! Add the following line to your .bashrc/.zshrc: @@ -159,11 +160,11 @@ variables. Everywhere a variable declaration was allowed in PRISM, an array declaration is allowed in XRM. o Arrays can be declared like in C, eg: - x[4] : [0..1] init 0; + x[0..4] : [0..1] init 0; will declare an array of 4 elements: x[0], x[1], x[2] and x[3]. So it's all like in C (access from to 0 through N-1) o It's possible to declare multidimensional arrays, eg: - x[3][4] : [0..1] init 0; + x[0..3][0..4] : [0..1] init 0; Again this is *almost* like C with the exception for multidimensional arrays that intermediate dimensions are not accessible (simply because they don't exist). So the former declaration will declare: @@ -176,11 +177,8 @@ x[2..4][0,3..5] will declare only: x[2][0], x[2][3], x[2][4], x[2][5], x[3][0], x[3][3], x[3][4], x[3][5], x[4][0], x[4][3], x[4][4], x[4][5] - So basically, when one of the dimensions of an array declaration is a - simple integer, eg: x[N] it is expansed in x[0..N-1]. Then the Cartesian - product of all the dimensions of the array is used to compute the set of - accessible variables. - o Dimensions of size zero are not allowed, eg: x[0] : [0..1]; + The Cartesian product of all the dimensions of the array is used to + compute the set of accessible variables. o Arrays can also be implicitly declared using for loops (see below, the section about for loops in XRM). o Array accesses can be found (nearly) everywhere a simple variable @@ -196,6 +194,14 @@ [] x[N+3]=0 -> ...; // valid: N+3 can be worked out at compile time. [] x[i+3]=0 -> ...; // invalid: the value of `i' is dynamic and unknown // at compile time. + o NOTE: In XRM 1.0 and before, it was possible to declare arrays like in C, + eg: + const int array[N]; + was automatically desugared to: + const int array[0..N-1]; + This is no longer true since XRM 1.1, one must now explicitly write + const int array[0..N-1] and const int array[N] leads to the declaration + of a single variable, that is, the Nth variable of the array. + TODO: Array accesses with dynamic subscripts. # XRM Meta-code @@ -238,38 +244,19 @@ endmodule end will generate 3 modules: dummy[1], dummy[2] and dummy[3]. - Of course, since each module has its own unique variables too, the - variables declared in that generated module will also have to be suffixed - by an array access with the meta-var. - In this case though, when `i' gets replaced by its successive values, we - have the following modules: - module dummy[1] - x[1] : [0..1] init 0; // not an array declaration - endmodule - module dummy[2] - x[2] : [0..1] init 0; // ditto - endmodule - module dummy[3] - x[3] : [0..1] init 0; // ditto - endmodule - But fortunately, this will not create 3 times an array called `x'. In - this very special case, the numerical values will not be expansed as - x[0..1] for dummy[1], x[0..2] for dummy[2] and x[0..3] for dummy[3] - because the integer in the array subscript comes from the expansion of a - meta-var and won't be further expanded. Thus in this case you get 3 different modules, each with their own single unique variable `x'. If you wish to provide each module with an array of, say 6 elements, then do the following: for i from 1 to 3 do module dummy[i] - x[i][5] : [0..1] init 0; + x[i][0..5] : [0..1] init 0; endmodule end In this case the first dimensions (`i') will first be expansed by the loop unrolling, which will equip each generated module with its own - unique variable `x' and then the second dimension will be expansed to - 0..5 which will create an array of 6 elements for each generated module. + unique variable `x' and then the second dimension will create an array of + 6 elements for each generated module. o Meta-for loops can also be used to declare arrays implicitely: module ImplicitArray for i from 0 to 3 do @@ -437,8 +424,8 @@ x[1..3]?=0 => x_1=0 | x_2=0 | x_3=0 - Dynamic array accesses, eg: x[i] where `i' is not known at compile-time. - Array initializations a la C: - x[3] : [0..4] init {0, 1, 2}; - const int array[3] = {0, 1, 2}; + x[0..3] : [0..4] init {0, 1, 2}; + const int array[0..3] = {0, 1, 2}; - Better error messages (with the location of error). **************

1 0

XRM 78: Add lazy and/or evaluation at the meta-level.
by SIGOURE Benoit 18 Jun '06

18 Jun '06

https://svn.lrde.epita.fr/svn/xrm/trunk Index: ChangeLog from SIGOURE Benoit <sigoure.benoit(a)lrde.epita.fr> Add lazy and/or evaluation at the meta-level. One can now rely on laziness of logical operators to prevent what could be an error at the meta-level, eg: x > 0 & s[x-1]=0 * src/str/eval-meta-code.str (eval-meta-code): Add lazy and/or evaluation. * src/str/eval-meta-code.meta: New. * tests/xrm/formula-amb.xpm: New. Failing test case (ticket #25). * tests/xrm/rivf.xpm: Use the lazyness. src/str/eval-meta-code.str | 29 +++++++++++++++++++++++++++++ tests/xrm/formula-amb.xpm | 1 + tests/xrm/rivf.xpm | 2 +- 3 files changed, 31 insertions(+), 1 deletion(-) Index: src/str/eval-meta-code.str --- src/str/eval-meta-code.str (revision 77) +++ src/str/eval-meta-code.str (working copy) @@ -3,6 +3,13 @@ ** XRM modules can contain meta for loops as well as meta if statements ** which have to evaluated and transformed in PRISM source code. ** +** NOTE: We also evaluate normal if statements if possible because they can +** be used as a short way of writing meta-if statements. We also perform a +** lazy evaluation of and's (`&') and or's (`|') because they can be used to +** protect potentially invalid meta code, eg: x > 0 & s[x-1]=0 relies on the +** fact that the `&' is lazy and that s[x-1] won't be expanded for invalid +** values of x. +** ** The code generated is annotated with the Generated("s") annotation where ** s is the name of the strategy which generated the code (can be useful for ** debugging). @@ -29,6 +36,8 @@ eval-meta-code = eval-meta-if + <+ lazy-eval-and + <+ lazy-eval-or <+ unroll-meta-for <+ unroll-meta-forin <+ (expand-pformulas; eval-meta-code) // try again on expansed code. @@ -72,6 +81,26 @@ end end + lazy-eval-and = + ?|[ e1 & e2 ]| + ; <prism-desugar> e1 + ; try(LitToBool) => e1' + ; if !e1' => False() then + !False() + else + fail + end + + lazy-eval-or = + ?|[ e1 | e2 ]| + ; <prism-desugar> e1 + ; try(LitToBool) => e1' + ; if !e1' => True() then + !True() + else + fail + end + strategies unroll-meta-for = Index: tests/xrm/formula-amb.xpm --- tests/xrm/formula-amb.xpm (revision 0) +++ tests/xrm/formula-amb.xpm (revision 0) @@ -0,0 +1 @@ +formula amb = true; Index: tests/xrm/rivf.xpm --- tests/xrm/rivf.xpm (revision 77) +++ tests/xrm/rivf.xpm (working copy) @@ -32,7 +32,7 @@ // 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; + valid (x, y) & s[x][y] = BROADCAST; // Whether a neighbor of (x, y) is broadcasting. formula ears (int x, int y) =

1 0

XRM 77: Add declaration lists.
by SIGOURE Benoit 18 Jun '06

18 Jun '06

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

1 0

opposition hamster
by Monica Barrera 17 Jun '06

17 Jun '06

1 0

XRM 76: Sync with ISOLA'06.
by Akim Demaille 16 Jun '06

16 Jun '06

https://svn.lrde.epita.fr/svn/xrm/trunk J'espère que ça marche... Index: ChangeLog from Akim Demaille <akim(a)lrde.epita.fr> Sync with ISOLA'06. * tests/xrm/rivf.xpm: Update. rivf.xpm | 145 ++++++++++++++++++++++++++++++++++----------------------------- 1 file changed, 79 insertions(+), 66 deletions(-) Index: tests/xrm/rivf.xpm --- tests/xrm/rivf.xpm (revision 75) +++ tests/xrm/rivf.xpm (working copy) @@ -1,87 +1,100 @@ probabilistic -const int width = 10; -const int height = 10; +// ------------ // +// Parameters. // +// ------------ // -// coordinates of the sensor where the alert is first seen. -const int event_x = 5; -const int event_y = 5; - -//const int battery_mode = 1; // 0=no-battery, 1=battery -const int power = 15; -const int length = 1200; -const int lossage = 0; -const int loss = 76; - -const int OFF = 0; -const int SLEEP = 1; -const int SENSE = 2; -const int LISTEN = 3; -const int BROADCAST = 4; -const int MAX_STATE = BROADCAST; - -const int COST_SLEEP = 1; -const int COST_SENSE = 1; -const int COST_LISTEN = 3; -const int COST_BROADCAST = 3; +// Grid dimensions. +const int X = 10, Y = 10; + +// Initial energy, percentage of lost cells. +const int power = 15, lossage = 50; + +// States. +const int OFF = 0, SLEEP = 1, SENSE = 2, + LISTEN = 3, BROADCAST = 4; + +// Energy consumption for each state. +const int COST_SLEEP = 1, COST_SENSE = 1, + COST_LISTEN = 3, COST_BROADCAST = 3; + + +// ---------- // +// Formulas. // +// ---------- // + +// Whether X, Y is valid, and broadcasts. +formula broadcasts (int x, int y) + valid (x, y) & s[x][y] = BROADCASTS + +// 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) + +// Whether the event (middle cell) is detected. +formula senses (int x, int Y) = + x = X / 2 & y = Y / 2; + +// Consume C units of power. +formula consume (int x, int y, int c) = + b[x][y]' = b[x][y] < c ? 0 : b[x][y] - c; + +// Reach state ST if energy allows it. +formula set_state (int x, int y, int st) = + s[x][y]' = (0 <= b[x][y]) ? st : OFF; module timer t : [0..268435454] init 0; endmodule -// Whether a neighbor is broadcasting. -formula neighbor_broadcasts(int x, int y) = - (x != 0 ? s[x-1][y] = BROADCAST : false) - | (x != width - 1 ? s[x+1][y] = BROADCAST : false) - | (y != 0 ? s[x][y-1] = BROADCAST : false) - | (y != height - 1 ? s[x][y+1] = BROADCAST : false); - -// Consume some power. -formula consume (int x, int y, int value) = - b[x][y]' = b[x][y] < value ? 0 : b[x][y] - value; - -// Reach state STATE if energy allows it. -formula set_state (int x, int y, int state) = - s[x][y]' = (0 <= b[x][y]) ? state : OFF; - -// Transition to the next STATE, consuming COST. -formula transition (int x, int y, int state, int cost) = - t' = t + 1 & consume (x, y, cost) & set_state (x, y, state); +// Transition to the next state ST, consuming C. +formula transition (int x, int y, int st, int c) = + t' = t+1 & consume(x, y, c) & set_state(x, y, st); -formula random_failure = - lossage != 0 & static_rand(0, 100) < lossage; -for x from 0 to width - 1 do - for y from 0 to height - 1 do +// --------- // +// Sensors. // +// --------- // + +for x from 0 to X - 1 do + for y from 0 to Y - 1 do module sensor[x][y] - s[x][y] : [0..MAX_STATE] init (random_failure ? OFF : SENSE); + s[x][y] : [0..4] init (static_rand (0, 100) < lossage) ? OFF : SENSE; b[x][y] : [0..power] init power; - if x = event_x & y = event_y then - // this node is the node broadcasting the alert - // rule 1: SENSE -> BROADCAST - [] s[x][y] = SENSE -> 1: transition (x, y, BROADCAST, COST_SENSE); - // rule 2: BROADCAST -> BROADCAST - [] s[x][y] = BROADCAST -> 1: transition (x, y, BROADCAST, COST_BROADCAST); - else // !event - - // rule 1: SENSE -> LISTEN - [] s[x][y] = SENSE -> 1: transition (x, y, LISTEN, COST_SENSE); - - // rule 2: LISTEN -> BROADCAST if neighbors broadcasts | SLEEP - [] s[x][y] = LISTEN -> 1: transition (x, y, - neighbor_broadcasts(x, y) ? BROADCAST : SLEEP, - COST_LISTEN); - - // rule 3: SLEEP -> SENSE | LISTEN + [] s[x][y] = SENSE -> 1: transition (x, y, senses (x, y) ? BROADCAST : LISTEN, COST_SENSE); + [] s[x][y] = LISTEN -> 1: transition (x, y, ears (x, y) ? BROADCAST : SLEEP, COST_LISTEN); [] s[x][y] = SLEEP -> 0.5: transition (x, y, SENSE, COST_SLEEP) + 0.5: transition (x, y, LISTEN, COST_LISTEN); - - // rule 4: BROADCAST -> BROADCAST [] s[x][y] = BROADCAST -> 1: transition (x, y, BROADCAST, COST_BROADCAST); + end module + end end - endmodule +// ------------ // +// Properties. // +// ------------ // + +// A broadcast in (x, y..Y - 1)? +formula X_broadcasts (int x, int y) = + valid (x, y) + & (broadcasts (x, y) | X_broadcasts (x, y + 1)); + +// A broadcast in (x..X - 1, y)? +formula Y_broadcasts (int x, int y) = + valid (x, 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); + +properties + for T from 0 to 1200 step 100 do + // Alarmed triggered before instant T? + P =? [ true U (t <= T & boundary_broadcasts) ]; end end

1 0

XRM 75: Factor common code between different parsers.
by SIGOURE Benoit 16 Jun '06

16 Jun '06

https://svn.lrde.epita.fr/svn/xrm/trunk Index: ChangeLog from SIGOURE Benoit <sigoure.benoit(a)lrde.epita.fr> Factor common code between different parsers. * src/tools/parse-pctl.str, * src/tools/parse-xrm.str, * src/tools/parse-prism.str, * src/tools/parse-xpctl.str: Move redundant code ... * src/tools/parser-common.str: ... here. * TODO: Bring up to date. TODO | 26 ++++++++++++++++++++++++++ src/tools/parse-pctl.str | 43 +++++-------------------------------------- src/tools/parse-prism.str | 43 +++++-------------------------------------- src/tools/parse-xpctl.str | 43 +++++-------------------------------------- src/tools/parse-xrm.str | 43 +++++-------------------------------------- src/tools/parser-common.str | 38 +++++++++++++++++++++++++++++++++++++- 6 files changed, 83 insertions(+), 153 deletions(-) Index: src/tools/parse-pctl.str --- src/tools/parse-pctl.str (revision 74) +++ src/tools/parse-pctl.str (working copy) @@ -1,5 +1,3 @@ -// Code mostly from parse-java by Martin Bravenboer <martin(a)cs.uu.nl> - module parse-pctl imports libxtclib // FIXME: import libstratego-xtc for strc 0.17 @@ -10,37 +8,13 @@ main-parse-pctl = // xtc-io-wrap(extra-opts, usage, about, deps, s) xtc-io-wrap( - parse-pctl-options - , parse-pctl-usage + parser-options + , parser-usage , parser-about , !["sglr", "implode-asfix", "PCTL.tbl", "pp-aterm"] - , parse-pctl + , parser-main ) - parse-pctl-options = - symbol-option - + preserve-comments-option - + preserve-positions-option - + pp-aterm-option - + allow-amb-option - -strategies - - 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 - xtc-transform(!"asfix-anno-comments", pass-verbose) - end - ; if must-preserve-positions then - xtc-transform(!"addPosInfo", !["-p", input-file-name - | <pass-verbose>()]) - end - ; xtc-implode-asfix - ; if must-pp-aterm then - xtc-transform(!"pp-aterm", pass-verbose) - end - strategies symbol-option = @@ -77,12 +51,5 @@ */ strategies - parse-pctl-usage = - <tool-doc> - [ Usage("parse-pctl [OPTIONS]") - , Summary( - "Parses a PCTL source file to an abstract syntax - tree in the ATerm format.") - , OptionUsage() - , AutoReportBugs() - ] + parser-usage = + template-parser-usage(|"parse-pctl", "PCTL") Index: src/tools/parse-xrm.str --- src/tools/parse-xrm.str (revision 74) +++ src/tools/parse-xrm.str (working copy) @@ -1,5 +1,3 @@ -// Code mostly from parse-java by Martin Bravenboer <martin(a)cs.uu.nl> - module parse-xrm imports libxtclib // FIXME: import libstratego-xtc for strc 0.17 @@ -10,37 +8,13 @@ main-parse-xrm = // xtc-io-wrap(extra-opts, usage, about, deps, s) xtc-io-wrap( - parse-xrm-options - , parse-xrm-usage + parser-options + , parser-usage , parser-about , !["sglr", "implode-asfix", "XRM.tbl", "pp-aterm"] - , parse-xrm + , parser-main ) - parse-xrm-options = - symbol-option - + preserve-comments-option - + preserve-positions-option - + pp-aterm-option - + allow-amb-option - -strategies - - parse-xrm = - where(?FILE(input-file-name) + !"stdin" => input-file-name) - ; xtc-sglr-no-heuristics(get-parse-table, get-start-symbol) - ; if must-preserve-comments then - xtc-transform(!"asfix-anno-comments", pass-verbose) - end - ; if must-preserve-positions then - xtc-transform(!"addPosInfo", !["-p", input-file-name - | <pass-verbose>()]) - end - ; xtc-implode-asfix - ; if must-pp-aterm then - xtc-transform(!"pp-aterm", pass-verbose) - end - strategies symbol-option = @@ -77,12 +51,5 @@ */ strategies - parse-xrm-usage = - <tool-doc> - [ Usage("parse-xrm [OPTIONS]") - , Summary( - "Parses an eXtended Reactive Module source file to an abstract syntax - tree in the ATerm format.") - , OptionUsage() - , AutoReportBugs() - ] + parser-usage = + template-parser-usage(|"parse-xrm", "eXtended Reactive Modules") Index: src/tools/parse-prism.str --- src/tools/parse-prism.str (revision 74) +++ src/tools/parse-prism.str (working copy) @@ -1,5 +1,3 @@ -// Code mostly from parse-java by Martin Bravenboer <martin(a)cs.uu.nl> - module parse-prism imports libxtclib // FIXME: import libstratego-xtc for strc 0.17 @@ -10,37 +8,13 @@ main-parse-prism = // xtc-io-wrap(extra-opts, usage, about, deps, s) xtc-io-wrap( - parse-prism-options - , parse-prism-usage + parser-options + , parser-usage , parser-about , !["sglr", "implode-asfix", "PRISM.tbl", "pp-aterm"] - , parse-prism + , parser-main ) - parse-prism-options = - symbol-option - + preserve-comments-option - + preserve-positions-option - + pp-aterm-option - + allow-amb-option - -strategies - - parse-prism = - where(?FILE(input-file-name) + !"stdin" => input-file-name) - ; xtc-sglr-no-heuristics(get-parse-table, get-start-symbol) - ; if must-preserve-comments then - xtc-transform(!"asfix-anno-comments", pass-verbose) - end - ; if must-preserve-positions then - xtc-transform(!"addPosInfo", !["-p", input-file-name - | <pass-verbose>()]) - end - ; xtc-implode-asfix - ; if must-pp-aterm then - xtc-transform(!"pp-aterm", pass-verbose) - end - strategies symbol-option = @@ -77,12 +51,5 @@ */ strategies - parse-prism-usage = - <tool-doc> - [ Usage("parse-prism [OPTIONS]") - , Summary( - "Parses a PRISM source file to an abstract syntax - tree in the ATerm format.") - , OptionUsage() - , AutoReportBugs() - ] + parser-usage = + template-parser-usage(|"parse-prism", "PRISM") Index: src/tools/parser-common.str --- src/tools/parser-common.str (revision 74) +++ src/tools/parser-common.str (working copy) @@ -1,9 +1,35 @@ -// used by parse-prism and parse-xrm to factorize common strategies +// used by parse-* to factor common strategies module parser-common strategies + parser-main = + where(?FILE(input-file-name) + !"stdin" => input-file-name) + ; xtc-sglr-no-heuristics(get-parse-table, get-start-symbol) + ; if must-preserve-comments then + xtc-transform(!"asfix-anno-comments", pass-verbose) + end + ; if must-preserve-positions then + xtc-transform(!"addPosInfo", !["-p", input-file-name + | <pass-verbose>()]) + end + ; xtc-implode-asfix + ; if must-pp-aterm then + xtc-transform(!"pp-aterm", pass-verbose) + end + +strategies + + parser-options = + symbol-option + + preserve-comments-option + + preserve-positions-option + + pp-aterm-option + + allow-amb-option + +strategies + /* sglr options: ** -fi: heuristic: injection count ** -fe: heuristic: eagerness @@ -84,6 +110,16 @@ */ strategies + template-parser-usage(|parser-name, language) = + <tool-doc> + [ Usage(<concat-strings>[parser-name, " [OPTIONS]"]) + , Summary(<concat-strings>[ + "Parses a ", language, " source file to an abstract syntax + tree in the ATerm format."]) + , OptionUsage() + , AutoReportBugs() + ] + parser-about = <tool-doc> [ AutoProgram() Index: src/tools/parse-xpctl.str --- src/tools/parse-xpctl.str (revision 74) +++ src/tools/parse-xpctl.str (working copy) @@ -1,5 +1,3 @@ -// Code mostly from parse-java by Martin Bravenboer <martin(a)cs.uu.nl> - module parse-xpctl imports libxtclib // FIXME: import libstratego-xtc for strc 0.17 @@ -10,37 +8,13 @@ main-parse-xpctl = // xtc-io-wrap(extra-opts, usage, about, deps, s) xtc-io-wrap( - parse-xpctl-options - , parse-xpctl-usage + parser-options + , parser-usage , parser-about , !["sglr", "implode-asfix", "XPCTL.tbl", "pp-aterm"] - , parse-xpctl + , parser-main ) - parse-xpctl-options = - symbol-option - + preserve-comments-option - + preserve-positions-option - + pp-aterm-option - + allow-amb-option - -strategies - - 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 - xtc-transform(!"asfix-anno-comments", pass-verbose) - end - ; if must-preserve-positions then - xtc-transform(!"addPosInfo", !["-p", input-file-name - | <pass-verbose>()]) - end - ; xtc-implode-asfix - ; if must-pp-aterm then - xtc-transform(!"pp-aterm", pass-verbose) - end - strategies symbol-option = @@ -77,12 +51,5 @@ */ strategies - parse-xpctl-usage = - <tool-doc> - [ Usage("parse-xpctl [OPTIONS]") - , Summary( - "Parses an eXtended Properties source file to an abstract syntax - tree in the ATerm format.") - , OptionUsage() - , AutoReportBugs() - ] + parser-usage = + template-parser-usage(|"parse-xpctl", "eXtended Properties") Index: TODO --- TODO (revision 74) +++ TODO (working copy) @@ -103,6 +103,23 @@ end end + * Fix the rand builtin. Instead of generating an extra module to host the + random variable and generate random numbers, host the random variable in + the module that called rand. Update the random variable each time it's + accessed to ensure good randomness, eg: + module random => module random + x : [0..51] init 0; => x : [0..51] init 0; + [] true -> x'=rand(42); => __rand_0 : [0..42]; // no init here + endmodule => [] true -> x'=__rand_0 + + => 1/43:(__rand_0'=0) + ... + + => 1/43:(__rand_0'=42); + => endmodule + + * Generalize the ranges. Instead of writing rand (42, 51), write: + rand (42 .. 51) + So that rand (42) always returns 42 and rand (42, 51) returns either 42 + or 51. + ## -------------- ## ## Desugarisation ## ## -------------- ## @@ -177,6 +194,15 @@ loops and then later try to group them? Would there be cases where grouping gets tricky? What about d_2 above? + * Don't use external parsers/pretty-printers in xrm-front. This leads to + many /tmp files and implies a great performance penalty on big + inputs/outputs. Instead, factor each parser in an external library linked + to xrm-front (preferably a static library because dynamic libraries must + be installed in the right path or require messing up with + LD_LIBRARY_PATH). This way, no external process will be involved. See if + we can also get rid of pp-aterm by using it directly through + libstratego-gpp. + ## ----- ## ## Notes ## ## ----- ##

1 0

monoburg 60: Fix the recipient of Vcs' messages
by Roland Levillain 16 Jun '06

16 Jun '06

Vcs' messages go to the projects list instead of the tiger-patches list, as for Nolimips and HAVM. https://svn.lrde.epita.fr/svn/monoburg ChangeLog | 7 +++++++ vcs/monoburg.rb | 2 +- 2 files changed, 8 insertions(+), 1 deletion(-) Index: ChangeLog from Roland Levillain <roland(a)lrde.epita.fr> Fix the recipient of Vcs' messages. * vcs/monoburg.rb (Vcs::monoburg_commit): Send messages to projects(a)lrde.epita.fr. 2006-06-16 Roland Levillain <roland(a)lrde.epita.fr> Index: vcs/monoburg.rb --- vcs/monoburg.rb (révision 58) +++ vcs/monoburg.rb (copie de travail) @@ -7,7 +7,7 @@ def monoburg_commit! ( *args ) common_commit!("monoburg <%= rev %>: <%= title %>", *args) do |subject| - mail!(:to => %w[tiger-patches(a)lrde.epita.fr], :subject => subject) + mail!(:to => %w[projects(a)lrde.epita.fr], :subject => subject) end end alias_command :mbci, :monoburg_commit

1 0