- Projects

XRM 57: Fix boxing of meta-if at Expression level.
by SIGOURE Benoit 10 Jun '06

10 Jun '06

https://svn.lrde.epita.fr/svn/xrm/trunk Index: ChangeLog from SIGOURE Benoit <sigoure.benoit(a)lrde.epita.fr> Fix boxing of meta-if at Expression level. The new test fails because of an ambiguity. This ambiguity is a bit tricky and (IMHO) must be resolved at the grammar level. Basically we have: test1 ? test1-true : test2 ? test2-true : test2-false The ambiguity is: (test1 ? test1-true : test2) ? test2-true : test2-false -or- test1 ? test1-true : (test2 ? test2-true : test2-false) The second choice seems more natural and that's how it works in C. Obviously we can't keep this ambiguity in the grammar. * tests/xrm/amb-if-exp.xpm: New. * src/lib/xrm/pp/xrm-meta-if.str: Fix boxing of meta-if. src/lib/xrm/pp/xrm-meta-if.str | 29 +++++++++++++++++++++++++++++ tests/xrm/amb-if-exp.xpm | 14 ++++++++++++++ 2 files changed, 43 insertions(+) Index: tests/xrm/amb-if-exp.xpm --- tests/xrm/amb-if-exp.xpm (revision 0) +++ tests/xrm/amb-if-exp.xpm (revision 0) @@ -0,0 +1,14 @@ +for y from 0 to height - 1 do + module sensor + [] true -> (s'=test1 ? test1-true : test2 ? test2-true : test2-false); + endmodule +end + +// amb + +//bad: +// (test1 ? test1-true : test2) ? test2-true : test2-false + +//good: +// test1 ? test1-true : (test2 ? test2-true : test2-false) +//at least that's how it works in C and it feels more natural. Index: src/lib/xrm/pp/xrm-meta-if.str --- src/lib/xrm/pp/xrm-meta-if.str (revision 56) +++ src/lib/xrm/pp/xrm-meta-if.str (working copy) @@ -2,11 +2,16 @@ rules + /* Boxing for if statements at top level or inside modules. + * Their then-part and else-part are lists. + */ + prism-to-box: MetaIf(condition, then-part) -> V[ V is=2 [ H hs=1 [ KW["if"] ~condition KW["then"] ] ~*then-part ] KW["end"]] + where <is-list> then-part prism-to-box: MetaIf(condition, then-part, else-part) @@ -14,3 +19,27 @@ ~*then-part ] V is=2 [ KW["else"] ~*else-part ] KW["end"]] + where <is-list> then-part + ; <is-list> else-part + + /* Boxing for if statements at the Expression level. + * Their then-part and else-part are not list but instead simple elements. + * This is due to the fact that the language as no way to express + * statements nor expression sequences at Expression level. + */ + + prism-to-box: + MetaIf(condition, then-part) + -> V[ V is=2 [ H hs=1 [ KW["if"] ~condition KW["then"] ] + ~then-part ] + KW["end"]] + where <not(is-list)> then-part + + prism-to-box: + MetaIf(condition, then-part, else-part) + -> V[ V is=2 [ H hs=1 [ KW["if"] ~condition KW["then"] ] + ~then-part ] + V is=2 [ KW["else"] ~else-part ] + KW["end"]] + where <not(is-list)> then-part + ; <not(is-list)> else-part

1 0

XRM 56: Minor cleanups in the grammar.
by SIGOURE Benoit 10 Jun '06

10 Jun '06

https://svn.lrde.epita.fr/svn/xrm/trunk Index: ChangeLog from SIGOURE Benoit <sigoure.benoit(a)lrde.epita.fr> Minor cleanups in the grammar. * src/syn/prism/PRISM-MetaCongruences.sdf: Add ConstantDef in concrete syntax. * src/syn/prism/PRISM-Main.sdf: Remove useless imports. * src/syn/prism/PRISM-StartSymbols.sdf: Remove useless start symbol (Identifier). * src/syn/xrm/XRM-StartSymbols.sdf: Ditto. * src/syn/prism/Makefile.am: Don't generate .pp tables (they're not used anyway). Don't use PRISM-Label (in fact, this is for PCTL). * src/syn/xrm/Makefile.am: Ditto. prism/Makefile.am | 5 +---- prism/PRISM-Main.sdf | 16 ---------------- prism/PRISM-MetaCongruences.sdf | 1 + prism/PRISM-StartSymbols.sdf | 1 - xrm/Makefile.am | 4 +--- xrm/XRM-StartSymbols.sdf | 1 - 6 files changed, 3 insertions(+), 25 deletions(-) Index: src/syn/prism/PRISM-MetaCongruences.sdf --- src/syn/prism/PRISM-MetaCongruences.sdf (revision 55) +++ src/syn/prism/PRISM-MetaCongruences.sdf (working copy) @@ -7,3 +7,4 @@ "|[" Expression "]|" -> StrategoStrategy {prefer,cons("ToStrategy")} "|[" Declaration "]|" -> StrategoStrategy {prefer,cons("ToStrategy")} "|[" Command "]|" -> StrategoStrategy {prefer,cons("ToStrategy")} + "|[" ConstantDef "]|" -> StrategoStrategy {prefer,cons("ToStrategy")} Index: src/syn/prism/PRISM-Main.sdf --- src/syn/prism/PRISM-Main.sdf (revision 55) +++ src/syn/prism/PRISM-Main.sdf (working copy) @@ -1,20 +1,4 @@ module PRISM-Main imports - PRISM-Command - PRISM-Constant - PRISM-Declaration - PRISM-Expression - PRISM-Formula - PRISM-Global - PRISM-Identifier - PRISM-Init - PRISM-Label PRISM-Layout - PRISM-Literals - PRISM-Module PRISM-ModulesFile - PRISM-ModulesFileType - PRISM-Reward - PRISM-SystemComposition - PRISM-Update - Index: src/syn/prism/PRISM-StartSymbols.sdf --- src/syn/prism/PRISM-StartSymbols.sdf (revision 55) +++ src/syn/prism/PRISM-StartSymbols.sdf (working copy) @@ -13,7 +13,6 @@ Command Expression Updates - Identifier SystemComp RewardStruct ModulesFileSection Index: src/syn/prism/Makefile.am --- src/syn/prism/Makefile.am (revision 55) +++ src/syn/prism/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 May 26 02:12:29 2006 SIGOURE Benoit +## Last update Sat Jun 10 00:22:28 2006 SIGOURE Benoit ## include $(top_srcdir)/config/Transformers.mk @@ -20,8 +20,6 @@ pkgdata_DATA_built = \ PRISM.def \ PRISM.tbl \ - PRISM.pp \ - PRISM.pp.af \ PRISM.rtg \ PRISM.str \ PRISM-StartSymbols.tbl \ @@ -49,7 +47,6 @@ PRISM-Identifier.sdf \ PRISM-Init.sdf \ PRISM-Keywords.sdf \ - PRISM-Label.sdf \ PRISM-Layout.sdf \ PRISM-Literals.sdf \ PRISM-Main.sdf \ Index: src/syn/xrm/Makefile.am --- src/syn/xrm/Makefile.am (revision 55) +++ 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 Fri May 26 02:12:42 2006 SIGOURE Benoit +## Last update Sat Jun 10 00:20:27 2006 SIGOURE Benoit ## include $(top_srcdir)/config/Transformers.mk @@ -22,8 +22,6 @@ pkgdata_DATA_built = \ XRM.def \ XRM.tbl \ - XRM.pp \ - XRM.pp.af \ XRM.rtg \ XRM.str \ XRM-StartSymbols.tbl \ Index: src/syn/xrm/XRM-StartSymbols.sdf --- src/syn/xrm/XRM-StartSymbols.sdf (revision 55) +++ src/syn/xrm/XRM-StartSymbols.sdf (working copy) @@ -13,7 +13,6 @@ Command Expression Updates - Identifier SystemComp RewardStruct ModulesFileSection

1 0

Re: test
by Tsuna 08 Jun '06

08 Jun '06

On 2006-06-08, SIGOURE Benoit <sigoure.benoit(a)lrde.epita.fr> wrote: > test > Pour une raison qui m'échappe, mes commits ne parviennent plus sur lrde.proj (XRM 49 à XRM 54) oO -- SIGOURE Benoit aka Tsuna _____ /EPITA\ Promo 2008.CSI Rock & tRoll

1 0

XRM 55: Add documentation draft for XRM.
by SIGOURE Benoit 08 Jun '06

08 Jun '06

https://svn.lrde.epita.fr/svn/xrm/trunk Index: ChangeLog from SIGOURE Benoit <sigoure.benoit(a)lrde.epita.fr> Add documentation draft for XRM. * src/str/desugar-array-access.str: Add an ICE condition. * tests/xrm/static_rand.xpm: New. * TODO: Bring up to date. * doc: New. * doc/user-guide.txt: New. TODO | 16 - doc/user-guide.txt | 392 +++++++++++++++++++++++++++++++++++++++ src/str/desugar-array-access.str | 7 tests/xrm/static_rand.xpm | 1 4 files changed, 398 insertions(+), 18 deletions(-) Index: src/str/desugar-array-access.str --- src/str/desugar-array-access.str (revision 54) +++ src/str/desugar-array-access.str (working copy) @@ -35,17 +35,12 @@ ** NOTE: we have a 2D list. The first level of lists represents the ** dimension, the second level, the subscripts accessed for that ** dimension. - ** NOTE: If the subscripts contain at least one meta-var, we completely - ** discard this array-access (by failing) and let the eval-meta-code - ** part take care of it. This is a *dirty* hack to allow declarations - ** using meta-vars. This implies that it's impossible to declare - ** something only partially using meta-vars. :| */ desugar-subscripts = 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 fail end // see the 2nd NOTE above. + ; 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 Index: tests/xrm/static_rand.xpm --- tests/xrm/static_rand.xpm (revision 0) +++ tests/xrm/static_rand.xpm (revision 0) @@ -0,0 +1 @@ +const int N = static_rand(0, 100); Index: TODO --- TODO (revision 54) +++ TODO (working copy) @@ -13,8 +13,6 @@ * Add tests using "system ... endsystem" (it's properly not parsed atm) - * Write some sort of formal descriptions of the extensions offered. - * 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. @@ -63,8 +61,6 @@ x[1..3]?=0 => x_1=0 | x_2=0 | x_3=0 - NOTE: x[5]?=0 should be considered as an error. - * Add non-static array accesses (as suggested by Micha). For instance: module test x[4] : [0..5]; @@ -145,14 +141,7 @@ ## Documentation ## ## ------------- ## - * Document the return values of xrm-front. - - 1: rewriting failed - - 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)) - - 5: invalid array access (eg: subscript is not a positive integer) - - 42: internal compiler error - - 51: not yet implemented + see in the doc/ folder. ## ---- ## ## DONE ## @@ -224,3 +213,6 @@ * Add a sanity check before check-meta-vars to collect all statically declared variables (globals, formulas, local declarations etc.) and ensure (in check-meta-vars) that their identifiers are unique. + + * Write some sort of formal descriptions of the extensions offered. + => see under /doc Index: doc/user-guide.txt --- doc/user-guide.txt (revision 0) +++ doc/user-guide.txt (revision 0) @@ -0,0 +1,392 @@ + ooooooo ooooo ooooooooo. ooo ooooo + `8888 d8' `888 `Y88. `88. .888' + Y888..8P 888 .d88' 888b d'888 + `8888' 888ooo88P' 8 Y88. .P 888 + .8PY888. 888`88b. 8 `888' 888 + d8' `888b 888 `88b. 8 Y 888 + o888o o88888o o888o o888o o8o o888o + eXtended Reactive Modules + + ~ Users' Guide ~ + // FIXME: LaTeXise me + + **************** + * Introduction * + **************** + + // FIXME: An introduction about PRISM and what is/isn't XRM is missing + // here. + + **************** + * Installation * + **************** + + - Requirements: + o Stratego/XT 0.17M1 (at least revision 15278 committed Mon, 29 May 2006) + because of libstratego-gpp (added in Stratego/XT 0.17M1 rev 15278). + o Any version of gcc (3.x or 4.x will do). + o Machine with executable stack (Beware of problems with MacIntel). + o ATerm 2.4.2 or newer. + o SDF2-Bundle 2.3.4 or newer. + + - Using Nix: + Nix is a package management system that ensures safe and complete + installation of packages. + You can get Nix from http://www.cs.uu.nl/wiki/Trace/Nix (pick up the + latest unstable release). + 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 --install aterm sdf2-bundle strategoxt + There you are! + Add the following line to your .bashrc/.zshrc: + [ -r /nix/etc/profile.d/nix.sh ] && source /nix/etc/profile.d/nix.sh + That's it! + + - Without Nix: + Install ATerm, SDF2 Bundle and Stratego/XT from: + http://www.stratego-language.org/Stratego/ContinuousDistribution + Additional install instructions can be found there. + + - Installing XRM: + o Uncompress the tarball: gunzip -c xrm-version.tar.gz | tar -xf - + o Use the following command to setup a build-tree: + $ cd xrm-version && mkdir _build && cd _build + o Invoke configure to generate the Makefiles + If you use Nix, simply use `../configure' + If you don't use Nix, use `PKG_CONFIG_PATH=P ../configure' where + `P' stands for the path(s) to the directory(ies) where the .pc + files of your Stratego/XT installation were installed. eg: + /usr/lib/pkgconfig/aterm.pc + /usr/lib/pkgconfig/sdf2-bundle.pc + /usr/lib/pkgconfig/stratego*.pc + o Then simply type `make all check' then `make install' + + *************************** + * Tools provided with XRM * + *************************** + + - xrm-front: The front-end provided by XRM will take as input an XRM source + code and will transform it into a standard PRISM source code. + - parse-prism: Parse a PRISM source code and yield an AST in ATerms. + - parse-xrm: Ditto with XRM source code. + - pp-prism: Pretty print ("unparse") a PRISM AST as PRISM source code. + - pp-xrm: Ditto but for XRM. + - prism-to-abox: Transform a PRISM AST into a Box AST for pretty printing. + - xrm-to-abox: Ditto but for XRM. + + ******************* + * Using xrm-front * + ******************* + + xrm-front is the main tool of the XRM package. It will transform a source + written in XRM into a standard PRISM source. + + # Common options + -------------- + The options can be reviewed by invoking xrm-front with the --help argument. + Common options include: + -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. + + # Return value + ------------ + xrm-front will return 0 if it succeeds and non zero if an error occured. + Possible return values are: + - 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)) + - 5: invalid array access (eg: subscript is not a positive integer) + - 42: internal compiler error (please send a bug report) + - 51: not yet implemented + + ******************** + * The XRM language * + ******************** + + # Introduction + ------------ + + The specification of the base language is documented in PRISM's manual (a + copy is available in the prism/ directory). + + The XRM language is 100% PRISM compliant and only offers extension to the + language. + + Numerous of the constructs in XRM are `meta' because they cannot be + translated in the PRISM language, thus we must evaluate them at + compile-time (this is xrm-front's job) in order to break them down to + simpler PRISM constructs. + + # XRM Modules + ----------- + + Within XRM modules, it is not mandatory to specify declarations before + commands. They can be freely intertwined in any particular order (whereas + in plain PRISM, declarations must come first and then commands will follow). + The following module is valid in XRM: + + module OutOfOrder + [] x=0 -> (x'=1); + x : [0..1] init 0; + endmodule + + The last step of xrm-front's pipeline is to group all declarations together + at the beginning of the module so that the module will be valid standard + PRISM. + + # XRM Expressions + --------------- + + o XRM has arrays (see below). Array accesses are expressions. + o XRM introduces two operators: "<<" and ">>" which have the same semantics + as in C. They are desugared using calls to the builtin pow. + + TODO: "?=" and "?!=" operators for arrays. + + # XRM Arrays + ---------- + + o It is possible to declare an array of variables instead of a several + 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; + 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; + 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: + x[0][0], x[0][1], x[0][2], x[0][3], + x[1][0], x[1][1], x[1][2], x[1][3], + x[2][0], x[2][1], x[2][2], x[2][3] + But in this case accessing x[0] for example doesn't make sense. + o It is also possible to specify manually the dimensions of an array using + lists and ranges, eg: + 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]. 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]; + 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 + identifier is allowed in PRISM. + o Update of values in arrays is illustrated in the following example: + [] x[N][M]=0 -> (x[N][M]'=1); + Notice that the prime (') comes after the dimensions of the array access. + o All the subscripts in array accesses must be evaluable down to a simple + positive integer at compile time, eg: + const int N = 3; + // ... + i : [0..42] init 0; // declaration of `i'. + [] 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. + + TODO: Array accesses with dynamic subscripts. + + # XRM Meta-code + ------------- + + XRM introduces meta-for loops and meta-if statements in the language. + These constructs are said to be `meta' because they are evaluated by + xrm-front and lead to code generation. + + o Meta-for loops can be found in only 2 places within a XRM source file: + * Where we could expect a module declaration. + * Where we could expect a declaration or a command, within a module. + This implies that meta-for loops can only be used to generate modules (or + other file sections, such as formulas, globals, etc.) or commands and + declarations within modules. + o There exists 2 flavors of for loops: + * For loops a la Pascal + * For loops a la Shell + Example: + for i from 0 to 3 do ... end // Pascal-like + for i from 0 to 10 step 2 do ... end // Pascal-like + for i in a, 1+2, N do .. end // Shell-like + 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 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'. + o For-loops are unrolled by copying the body of the loop and replacing + every match of the identifier of the meta-var by its successive values. + o For-loops are the only way of declaring a meta-var at the moment. + o For-loops can be used to create new modules. Since each module must have + a unique name, it will have to be suffixed by an array access using a + meta-var, eg: + for i from 1 to 3 do + module dummy[i] + x[i] : [0..1] init 0; + 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; + 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. + o Meta-for loops can also be used to declare arrays implicitely: + module ImplicitArray + for i from 0 to 3 do + x[i] : [0..i] init i; + end + endmodule + In this case the module ImplicitArray will have a single array named `x' + of 4 elements. This method offers a greater control on how each element + of the array is declared. + + o Meta-if statements can be found in only 3 places within a XRM source file: + * Where we could expect a module declaration. + * Where we could expect a declaration or a command, within a module. + * Where we would expect an expression. + However the latter case has a restriction that the two formers don't have: + the then-part and the else-part of the if statements cannot contain more + than one expression. + o The syntax for meta-if statements is illustrated in the following example: + if true then + module alwaysGenerated + if 0 = 42 - 21 then + neverGenerated : [0..42] init 0; + else + alwaysGeneratedToo : [0..42] init 0; + end + endmodule + end + o The condition of the meta-if statements must be evaluable at compile + time. It must either be evaluable down to true or false, or down to a + simple integer/double. If that integer/double is 0, the condition will be + false, otherwise it will be true (like in C). Comparison on reals are + done with a precision of 10^-7 which means that if the condition is + reduced down to 0.00000001 (for instance) it will be evaluated as being + false. + + # XRM builtins + ------------ + + XRM introduces two new builtins for generating random numbers: rand and + static_rand. + + 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 + argument (an integer equal to zero) is added. If the single argument + is positive, the zero is added before it, otherwise it's added after + it, eg: + rand(3) will be desugared to rand(0, 3) + rand(-3) will be desugared to rand(-3, 0) + o static_rand(low, hi) will be transformed into a random integer ranging + from `low' to `hi' (included). The random number is obtain with rand(3) + which is seeded with the current UNIX time-stamp when xrm-front starts. + o Calls to static_rand will be evaluated after unrolling of meta-for + loops to ensure that each iteration of the loop gets its own random + number. It will be evaluated earlier if it happens to be used where + a statically evaluable value is required more early in the pipeline + (eg: in meta-if statements' condition, in the fields `from', `to' or + `step' of a meta-for loop, etc.) + o Bear in mind that the random numbers generated by static_rand are + constant from one run to another unless you re-generate the PRISM + source (with xrm-front) each time before running. + o rand(low, hi) will be transformed into a new variable (each call to + rand will generate a new unique variable) which will be controlled by + an external module with a single command: + module testRand => module testRand + x : [0..42] init 0; => x : [0..42] init 0; + [] x=0 -> x'=rand(42); => [] x=0 -> x'=__rand_0; + endmodule => endmodule + => module __rand_0 + => __rand_0 : [0..42]; + => [] true -> 1/43:(__rand_0'=0) + => + 1/43:(__rand_0'=1) + => ... + => + 1/43:(__rand_0'=42); + => endmodule + /!\ This is not a reliable random number generator! + + TODO: The current implementation of rand will be renamed (maybe as + bad_rand or old_rand) and a new reliable implementation will be + provided as a replacement. In this implementation, the random variable + won't be hosted in a foreign module anymore, it will be hosted directly + in the module which called rand. The variable will be updated each time + it's accessed to ensure real random numbers. + + ********************* + * Incoming features * + ********************* + + The following features are not yet implemented (or only partially + implemented or broken). They are ordered in term of the estimated time + needed to successfully implement them. For a complete list of things to be + done please review the TODO file. + - More sanity checks for all declarations at different stages of the + pipeline to ensure that everything is well defined. (variables used have + been declared somewhere etc.) + - Possibility to import another module, eg: import common.pm + - Parameterized formulas. (Pretty much like macro-functions in C) + - Scopes for meta variables (allow redefinitions/shadowing). + - Bound/Type checking (ensure that variables are properly used according to + their type/domain definition). + - Conditional tests on arrays. "?=" and "?!=" operators for arrays. eg: + x[1..3]=0 => x_1=0 & x_2=0 & x_3=0 + 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}; + - Better error messages (with the location of error). + + ************** + * Known bugs * + ************** + + - The construct "system ... endsystem" (for system compositions) is broken + at the moment (meaning: using it will result in a parse error). It's + probably a simple problem with the base SDF grammar. I've never seen a + PRISM source using this construct so this has been in the TODO list since + the beginning but with a very low priority. + - Unary operators are allowed in the base language whereas they should not + (because they are not allowed in the original PRISM parser). + - There is nearly no warranty that the generated code will work in PRISM. + Generally speaking, if the input XRM source is correct, the output PRISM + source will also be correct. However, at this stage of the development, + the front-end is still pretty fragile and I am sure it's quite easy to + generate invalid PRISM code without having any error reported by + xrm-front (in this case please report the bug). + What we clearly need to thwart this is: + - Type checking. + - Bound checking. + - Probably many other things. (run make check and see the tests that fail).

1 0

XRM 54: Add RIVF's equivalent in XRM meta-code.
by SIGOURE Benoit 08 Jun '06

08 Jun '06

https://svn.lrde.epita.fr/svn/xrm/trunk Index: ChangeLog from SIGOURE Benoit <sigoure.benoit(a)lrde.epita.fr> Add RIVF's equivalent in XRM meta-code. Usage: xrm-front -i rivf.xpm -o rivf.pm -D -D stands for --desugar (it will add an additional pass after the main pipeline to desugar as much as possible everything and perform constant propagation). This is completely optional. One thing has been omitted here: support for battery_mode=0 (which is basically the same thing but without bothering with b[x][y] and without having to check at every update whether or not we should go in the OFF state because we run out of power). I omitted this for the sake of clarity although it's fairly straightforward to add it (since it's only a matter of commenting out some lines). * tests/xrm/rivf.xpm: New. rivf.xpm | 93 +++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 93 insertions(+) Index: tests/xrm/rivf.xpm --- tests/xrm/rivf.xpm (revision 0) +++ tests/xrm/rivf.xpm (revision 0) @@ -0,0 +1,93 @@ +probabilistic + +const int width = 10; +const int height = 10; + +// coordinates of the sensors 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; + +module timer + t : [0..268435454] init 0; +endmodule + +for x from 0 to width - 1 do + for y from 0 to height - 1 do + module sensor[x][y] + if lossage != 0 & static_rand(0, 100) < lossage then + s[x][y] : [0..MAX_STATE] init OFF; + else + s[x][y] : [0..MAX_STATE] init SENSE; + end + 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:(t'=t+1) & + (b[x][y]'=b[x][y] < COST_SENSE ? 0 : b[x][y]-COST_SENSE) & + (s[x][y]'=0 <= b[x][y] ? BROADCAST : OFF); + // rule 2: BROADCAST -> BROADCAST | OFF if no more battery + [] s[x][y] = BROADCAST -> 1:(t'=t+1) & + (b[x][y]'=b[x][y] < COST_BROADCAST ? 0 : b[x][y]-COST_BROADCAST) & + (s[x][y]'=0 <= b[x][y] ? BROADCAST : OFF); + else // !event + + // rule 1: SENSE -> LISTEN + [] s[x][y] = SENSE -> 1:(t'=t+1) & + (b[x][y]'=b[x][y] < COST_SENSE ? 0 : b[x][y]-COST_SENSE) & + (s[x][y]'=0 <= b[x][y] ? LISTEN : OFF); + + // rule 2: LISTEN -> BROADCAST if neighbors broadcasts | SLEEP + [] s[x][y] = LISTEN -> 1:(t'=t+1) & + (b[x][y]'=b[x][y] < COST_LISTEN ? 0 : b[x][y]-COST_LISTEN) & + (s[x][y]'=b[x][y] < COST_BROADCAST ? 0 : + (if x != 0 then + s[x-1][y]=BROADCAST + else false end + | if x != width - 1 then + s[x+1][y]=BROADCAST + else false end + | if y != 0 then + s[x][y-1]=BROADCAST + else false end + | if y != height - 1 then + s[x][y+1]=BROADCAST + else false end + ? BROADCAST : SLEEP)); + + // rule 3: SLEEP -> SENSE | LISTEN + [] s[x][y] = SLEEP -> 0.5:(t'=t+1) & + (b[x][y]'=b[x][y] < COST_SLEEP ? 0 : b[x][y]-COST_SLEEP) & + (s[x][y]'=0 <= b[x][y] ? SENSE : OFF) + + 0.5:(t'=t+1) & + (b[x][y]'=b[x][y] < COST_LISTEN ? 0 : b[x][y]-COST_LISTEN) & + (s[x][y]'=0 <= b[x][y] ? LISTEN : OFF); + + // rule 4: BROADCAST -> BROADCAST + [] s[x][y] = BROADCAST -> 1:(t'=t+1) & + (b[x][y]'=b[x][y] < COST_BROADCAST ? 0 : b[x][y]-COST_BROADCAST) & + (s[x][y]'=0 <= b[x][y] ? BROADCAST : OFF); + end + + endmodule + end +end

1 0

XRM 53: Add meta-if at Expression level.
by SIGOURE Benoit 08 Jun '06

08 Jun '06

https://svn.lrde.epita.fr/svn/xrm/trunk Index: ChangeLog from SIGOURE Benoit <sigoure.benoit(a)lrde.epita.fr> Add meta-if at Expression level. So basically, it is now possible to have a meta-if statement everywhere we can find an Expression. /!\ NOTE: meta-if statements at Expression level are restricted to one single expressions in the then-part and else-part. eg: if some-condition then exp1 exp2 end is *invalid* at Expression level because neither the base language nor the extended language provide real statements/sequences of expressions. Other improvements: PRISM-If statements (cond ? then-part : else-part) are now evaluated by prism-desugar when possible. It is also possible to reduce the condition of a meta-if statement down to a simple Int(_) or Double(_). If that Int(_) or Double(_) is zero, the condition will evaluate as False() otherwise True() [like in C]. NOTE: for Double(_) all tests are performed with a precision of 10^-7 in other words if 0.000000001 then ... else /*executed*/ end will be false. * src/str/prism-desugar.str: Add EvalIf and LitToBool. * src/str/eval-meta-code.str: Allow if statements to evaluate as integer/real. In this case the behavior is the same as in C: 0 means false and all the other values mean true. * src/str/xrm-front.str: Change a debug message to be a notice. * src/syn/xrm/XRM-Arrays.sdf: Use XRMRange for array subscripts. * src/syn/xrm/XRM-MetaIf.sdf: Add meta-if at the Expression level. Correct EBNF grammar. * src/syn/xrm/XRM-MetaFor.sdf: Remove trailing whitespaces. * src/syn/xrm/XRM-Expression.sdf: Add XRMRange. This basically just a simple range but it has a different priority in the grammar than the original Range from the base grammar. It is used for array subscripts. Actually XRMRange might not be a wise name for this sorts. * tests/xrm/desugar-if.xpm: New. * tests/xrm/if-exp.xpm: New. * tests/xrm/cond-array-access.xpm: New. * tests/xrm/priorities-exp-array-subscript.xpm: New. src/str/eval-meta-code.str | 4 +- src/str/prism-desugar.str | 46 +++++++++++++++++++++++++++ src/str/xrm-front.str | 3 - src/syn/xrm/XRM-Arrays.sdf | 16 ++++----- src/syn/xrm/XRM-Expression.sdf | 27 +++++++++++++++ src/syn/xrm/XRM-MetaIf.sdf | 44 ++++++++++++++++++++++--- tests/xrm/cond-array-access.xpm | 4 ++ tests/xrm/desugar-if.xpm | 15 ++++++++ tests/xrm/if-exp.xpm | 7 ++++ tests/xrm/priorities-exp-array-subscript.xpm | 9 +++++ 10 files changed, 158 insertions(+), 17 deletions(-) Index: src/str/prism-desugar.str --- src/str/prism-desugar.str (revision 52) +++ src/str/prism-desugar.str (working copy) @@ -27,6 +27,7 @@ <+ EvalAnd <+ EvalOr <+ EvalMin <+ EvalMax <+ EvalFloor <+ EvalCeil <+ EvalPow <+ EvalMod <+ (EvalStaticRand; IntToDouble) + <+ EvalIf ) ; topdown(try(SimplifyDoubles <+ TruncateDouble)) @@ -305,6 +306,28 @@ /* ** ## ============= ## +** ## If statements ## +** ## ============= ## +*/ + +rules + + EvalIf: + |[ true ? e1 : e2 ]| -> |[ e1 ]| + + EvalIf: + |[ false ? e1 : e2 ]| -> |[ e2 ]| + + EvalIf: + |[ d ? e1 : e2 ]| -> |[ e1 ]| + where <not(compare(real-eq))>(d, 0) + + EvalIf: + |[ d ? e1 : e2 ]| -> |[ e2 ]| + where <compare(real-eq)>(d, 0) + +/* +** ## ============= ## ** ## Eval Builtins ## ** ## ============= ## ** @@ -348,3 +371,26 @@ else <modS> (i, j) => r end + +/* +** ## =========== ## +** ## Misc. stuff ## +** ## =========== ## +*/ + +rules + + LitToBool: + |[ 0 ]| -> |[ false ]| + + LitToBool: + |[ i ]| -> |[ true ]| + where <not(eq)>(i, "0") + + LitToBool: + |[ d ]| -> |[ false ]| + where <compare(real-eq)>(d, 0) + + LitToBool: + |[ d ]| -> |[ true ]| + where <not(compare(real-eq))>(d, 0) Index: src/str/eval-meta-code.str --- src/str/eval-meta-code.str (revision 52) +++ src/str/eval-meta-code.str (working copy) @@ -23,6 +23,7 @@ imports ice signatures + prism-desugar strategies @@ -38,7 +39,8 @@ ?MetaIf(condition, then-part, else-part) ///*DEBUG*/; say(!" @@@ eval-meta-if: starting:") ///*DEBUG*/; printf(|" condition = ", condition) - ; where(<prism-desugar> condition => condition-value) + ; where(<prism-desugar> condition + ; try(LitToBool) => condition-value) ///*DEBUG*/; printf(|" condition-value = ", condition-value) ; if !condition-value => True() then <eval-meta-code> then-part Index: src/str/xrm-front.str --- src/str/xrm-front.str (revision 52) +++ src/str/xrm-front.str (working copy) @@ -42,10 +42,9 @@ notice-msg(|"transformation pipeline starting") ; where(<set-random-seed> (<time>)) ; xrm-to-prism - ; dbg(|"xrm-to-prism finished") ; if must-desugar then prism-desugar - ; dbg(|"prism-desugar finished") + ; notice-msg(|"prism-desugar finished") end /** list of available options for xrm-front */ Index: src/syn/xrm/XRM-Arrays.sdf --- src/syn/xrm/XRM-Arrays.sdf (revision 52) +++ src/syn/xrm/XRM-Arrays.sdf (working copy) @@ -6,21 +6,21 @@ %% EBNF Grammar: Arrays %% ArrayAccess ::= - %% Identifier "[" Range {"," Range} "]" - %% | ArrayAccess "[" Range {"," Range} "]" + %% Identifier "[" XRMRange {"," XRMRange} "]" + %% | ArrayAccess "[" XRMRange {"," XRMRange} "]" %% %% ArrayAccessPrime ::= - %% Identifier "[" Range {"," Range} "]" "'" - %% | ArrayAccess "[" Range {"," Range} "]" "'" + %% Identifier "[" XRMRange {"," XRMRange} "]" "'" + %% | ArrayAccess "[" XRMRange {"," XRMRange} "]" "'" sorts ArrayAccess context-free syntax - Identifier "[" {Range ","}+ "]" -> ArrayAccess {cons("ArrayAccess")} - ArrayAccess "[" {Range ","}+ "]" -> ArrayAccess {cons("ArrayAccess")} + Identifier "[" {XRMRange ","}+ "]" -> ArrayAccess {cons("ArrayAccess")} + ArrayAccess "[" {XRMRange ","}+ "]" -> ArrayAccess {cons("ArrayAccess")} sorts ArrayAccessPrime context-free syntax - ArrayAccess "[" {Range ","}+ "]" "'" + ArrayAccess "[" {XRMRange ","}+ "]" "'" -> ArrayAccessPrime {cons("ArrayAccessPrime")} - Identifier "[" {Range ","}+ "]" "'" + Identifier "[" {XRMRange ","}+ "]" "'" -> ArrayAccessPrime {cons("ArrayAccessPrime")} Index: src/syn/xrm/XRM-MetaIf.sdf --- src/syn/xrm/XRM-MetaIf.sdf (revision 52) +++ src/syn/xrm/XRM-MetaIf.sdf (working copy) @@ -7,23 +7,37 @@ %% EBNF Grammar: Meta if-then-else %% (* if-then-else at top-level *) %% ModulesFileSection ::= - %% "if" Expression "then" ModulesFileSection {ModulesFileSection} "end" + %% "if" Expression "then" {ModulesFileSection} "end" %% | "if" Expression "then" - %% ModulesFileSection {ModulesFileSection} + %% {ModulesFileSection} %% "else" - %% ModulesFileSection {ModulesFileSection} + %% {ModulesFileSection} %% "end" %% %% (* if-then-else inside modules *) %% DeclarationOrCommand ::= - %% "if" Expression "then" DeclarationOrCommand {DeclarationOrCommand} "end" + %% "if" Expression "then" {DeclarationOrCommand} "end" %% | "if" Expression "then" - %% DeclarationOrCommand {DeclarationOrCommand} + %% {DeclarationOrCommand} %% "else" - %% DeclarationOrCommand {DeclarationOrCommand} + %% {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")} @@ -36,6 +50,7 @@ "end" -> ModulesFileSection {cons("MetaIf")} context-free syntax + %% if-then within modules "if" Expression "then" DeclarationOrCommand* "end" -> DeclarationOrCommand {cons("MetaIf")} @@ -46,3 +61,20 @@ "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/XRM-MetaFor.sdf Index: src/syn/xrm/XRM-Expression.sdf --- src/syn/xrm/XRM-Expression.sdf (revision 52) +++ src/syn/xrm/XRM-Expression.sdf (working copy) @@ -18,6 +18,9 @@ %% (* builtin functions calls using the "func" notation *) %% | "func" "(" "rand" "," Expression {"," Expression} ")" %% | "func" "(" "static_rand" "," Expression {"," Expression} ")" + %% + %% (* Ranges in XRM with different priority (for array accesses) *) + %% XRMRange ::= Expression | Expression ".." Expression context-free syntax ArrayAccess -> Expression @@ -39,6 +42,12 @@ "func" "(" "static_rand" "," {Expression ","}+ ")" -> Expression {cons("StaticRand")} + %% Ranges in XRM with different priority (for array accesses) + sorts XRMRange + context-free syntax + Expression -> XRMRange + Expression ".." Expression -> XRMRange {cons("Range")} + %% NOTE: remember: priorities are transitive in SDF. %% The following priorities are marked either with "inherited" or "new". %% The former means that these priorities are inherited from the base @@ -71,3 +80,21 @@ > { %% inherited Expression -> Range } + > { %% inherited + "!" Expression -> Expression + } + > {left: %% inherited + Expression "&" Expression -> Expression + } + > {left: %% inherited + Expression "|" Expression -> Expression + } + > { %% inherited + Expression "?" Expression ":" Expression -> Expression + } + > {non-assoc: %% new + Expression ".." Expression -> XRMRange + } + > { %% new + Expression -> XRMRange + } Index: tests/xrm/desugar-if.xpm --- tests/xrm/desugar-if.xpm (revision 0) +++ tests/xrm/desugar-if.xpm (revision 0) @@ -0,0 +1,15 @@ +if 0=1?0:2 then + const int success1 = 1; + if 0=1?0:2 then + const int success2 = 1; + if false?0:0 then + const int fail1 = 1; + else + const int success3 = 1; + end + else + const int fail2 = 1; + end +else + const int fail3 = 1; +end Index: tests/xrm/if-exp.xpm --- tests/xrm/if-exp.xpm (revision 0) +++ tests/xrm/if-exp.xpm (revision 0) @@ -0,0 +1,7 @@ +const int N = 3; +const int success = 1; + +module test + x : [if true then 0 end..if false then 0 else 42 end]; + [] x=0 -> x'=if 42 then success else -1 end; +endmodule Index: tests/xrm/cond-array-access.xpm --- tests/xrm/cond-array-access.xpm (revision 0) +++ tests/xrm/cond-array-access.xpm (revision 0) @@ -0,0 +1,4 @@ +module test + x[4] : [0..42] init 0; + [] x[-1<0?0:-1]=0 -> true; +endmodule Index: tests/xrm/priorities-exp-array-subscript.xpm --- tests/xrm/priorities-exp-array-subscript.xpm (revision 0) +++ tests/xrm/priorities-exp-array-subscript.xpm (revision 0) @@ -0,0 +1,9 @@ +module test + x[3] : bool init false; + y : bool init true; + x[4] : [0..42] init 0; + + //[] true -> x[1|1]'=true; + [] x[true?2:3]=0 -> true; + [] true -> x[0..1&1]'=true; +endmodule

1 0

XRM 52: Add -a|--allow-amb option for parse-prism/parse-xrm.
by SIGOURE Benoit 08 Jun '06

08 Jun '06

https://svn.lrde.epita.fr/svn/xrm/trunk Index: ChangeLog from SIGOURE Benoit <sigoure.benoit(a)lrde.epita.fr> Add -a|--allow-amb option for parse-prism/parse-xrm. This can be useful for debugging. * src/tools/parse-xrm.str: Add -a|--allow-amb option. * src/tools/parse-prism.str: Ditto. * src/tools/parser-common.str: Ditto. parse-prism.str | 1 + parse-xrm.str | 1 + parser-common.str | 25 ++++++++++++++++++++++--- 3 files changed, 24 insertions(+), 3 deletions(-) Index: src/tools/parse-xrm.str --- src/tools/parse-xrm.str (revision 51) +++ src/tools/parse-xrm.str (working copy) @@ -22,6 +22,7 @@ + preserve-comments-option + preserve-positions-option + pp-aterm-option + + allow-amb-option strategies Index: src/tools/parse-prism.str --- src/tools/parse-prism.str (revision 51) +++ src/tools/parse-prism.str (working copy) @@ -22,6 +22,7 @@ + preserve-comments-option + preserve-positions-option + pp-aterm-option + + allow-amb-option strategies Index: src/tools/parser-common.str --- src/tools/parser-common.str (revision 51) +++ src/tools/parser-common.str (working copy) @@ -8,13 +8,15 @@ ** -fi: heuristic: injection count ** -fe: heuristic: eagerness ** -2: use AsFix2 output format - ** -A: ambiguities are treated as errors ** -p <file>: parse table to use ** -s <symbol>: start symbol to use + ** Additionnaly pass-amb might add this option: + ** -A: ambiguities are treated as errors */ xtc-sglr-no-heuristics(tbl, sort) = - xtc-transform(!"sglr", !["-fi", "-fe", "-2A", "-p", <tbl; xtc-find> (), - "-s", <sort> () | <pass-v-verbose> ()]) + xtc-transform(!"sglr", !["-fi", "-fe", "-2", "-p", <tbl; xtc-find> (), + "-s", <sort>(), <pass-amb>() + | <pass-v-verbose>()]) strategies @@ -48,6 +50,7 @@ <get-config> "preserve-positions" => "yes" strategies + pp-aterm-option = Option("-A" + "--pp-aterm" , <set-pp-aterm> "yes" @@ -60,6 +63,22 @@ must-pp-aterm = <get-config> "pp-aterm" => "yes" +strategies + + allow-amb-option = + Option("-a" + "--allow-amb" + , <set-allow-amb> "yes" + , !HelpString("-a | --allow-amb", "Allow ambiguities") + ) + + set-allow-amb = + <set-config> ("allow-amb", <id>) + + must-allow-amb = + <get-config> "allow-amb" => "yes" + + pass-amb = if must-allow-amb then !"" else !"-A" end + /** * Documentation */

1 0

XRM 51: Add static constant propagations in static definitions.
by SIGOURE Benoit 08 Jun '06

08 Jun '06

https://svn.lrde.epita.fr/svn/xrm/trunk Index: ChangeLog from SIGOURE Benoit <sigoure.benoit(a)lrde.epita.fr> Add static constant propagations in static definitions. eg: const int N = 3; const int M = N; // propagation of N in the saved definition for M const int X = M; // ditto => const int X = 3; // and not const int X = N; as it used to be. * src/str/collect-static-const-decl.str: Try to propagate static consts/formulas in the definition of static consts/formulas. * tests/prism/desugar-const.pm: New. src/str/collect-static-const-decl.str | 9 ++++++--- tests/prism/desugar-const.pm | 4 ++++ 2 files changed, 10 insertions(+), 3 deletions(-) Index: src/str/collect-static-const-decl.str --- src/str/collect-static-const-decl.str (revision 50) +++ src/str/collect-static-const-decl.str (working copy) @@ -10,35 +10,38 @@ collect-static-const-decl = ?ConstInt(idf, value) - ; where(!value{Type("int")} => v) ; if <ExpandStaticConsts> idf then cannot-redefine-static-const(|idf) end ; if <ExpandFormulas> idf then cannot-redefine-formula(|idf) end + ; where(<innermost(ExpandStaticConsts + ExpandFormulas)> value => v' + ; !v'{Type("int")} => v) ; rules(ExpandStaticConsts: idf -> v) collect-static-const-decl = ?ConstDouble(idf, value) - ; where(!value{Type("double")} => v) ; if <ExpandStaticConsts> idf then cannot-redefine-static-const(|idf) end ; if <ExpandFormulas> idf then cannot-redefine-formula(|idf) end + ; where(<innermost(ExpandStaticConsts + ExpandFormulas)> value => v' + ; !v'{Type("double")} => v) ; rules(ExpandStaticConsts: idf -> v) collect-static-const-decl = ?ConstBool(idf, value) - ; where(!value{Type("bool")} => v) ; if <ExpandStaticConsts> idf then cannot-redefine-static-const(|idf) end ; if <ExpandFormulas> idf then cannot-redefine-formula(|idf) end + ; where(<innermost(ExpandStaticConsts + ExpandFormulas)> value => v' + ; !v'{Type("bool")} => v) ; rules(ExpandStaticConsts: idf -> v) rules Index: tests/prism/desugar-const.pm --- tests/prism/desugar-const.pm (revision 0) +++ tests/prism/desugar-const.pm (revision 0) @@ -0,0 +1,4 @@ +const int N = 3; +const int M = N; + +const int test = M; // this should become a 3 with xrm-front -D

1 0

XRM 50: Fix static_rand.
by SIGOURE Benoit 08 Jun '06

08 Jun '06

https://svn.lrde.epita.fr/svn/xrm/trunk Index: ChangeLog from SIGOURE Benoit <sigoure.benoit(a)lrde.epita.fr> Fix static_rand. * src/str/xrm-to-prism.str: Evaluate static_rand calls at the end of the transformation pipeline (that is, after meta-code evaluation). * src/str/prism-desugar.str: Evaluate static_rand in prism-desugar. * src/str/builtin-rand.str: Introduce EvalStaticRand. * TODO: Add something to do. TODO | 3 +++ src/str/builtin-rand.str | 2 +- src/str/prism-desugar.str | 2 ++ src/str/xrm-to-prism.str | 2 +- 4 files changed, 7 insertions(+), 2 deletions(-) Index: src/str/xrm-to-prism.str --- src/str/xrm-to-prism.str (revision 49) +++ src/str/xrm-to-prism.str (working copy) @@ -78,7 +78,7 @@ * 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)) + ; topdown(try(array-decl-desugar); try(EvalStaticRand)) ; notice-msg(|"xrm-to-prism: array declarations desugared") /* flatten nested lists */ Index: src/str/prism-desugar.str --- src/str/prism-desugar.str (revision 49) +++ src/str/prism-desugar.str (working copy) @@ -2,6 +2,7 @@ imports PRISM reals + builtin-rand strategies @@ -25,6 +26,7 @@ <+ EvalLt <+ EvalLtEq <+ EvalGt <+ EvalGtEq <+ EvalEq <+ EvalNotEq <+ EvalAnd <+ EvalOr <+ EvalMin <+ EvalMax <+ EvalFloor <+ EvalCeil <+ EvalPow <+ EvalMod + <+ (EvalStaticRand; IntToDouble) ) ; topdown(try(SimplifyDoubles <+ TruncateDouble)) Index: src/str/builtin-rand.str --- src/str/builtin-rand.str (revision 49) +++ src/str/builtin-rand.str (working copy) @@ -66,7 +66,7 @@ /* save this module in a DR for later retrieval */ ; rules(RandGenModules:+ _ -> rand-gen-module) - EvalRand: + EvalStaticRand: StaticRand(args) -> Int(rand-val) where check-rand-args(|"static_rand", args) => (from, to) ; rand(|<string-to-int> from, <string-to-int> to) Index: TODO --- TODO (revision 49) +++ TODO (working copy) @@ -30,6 +30,9 @@ static const int N = -1; will issue an error such as "undeclared meta variable N" whereas the real problem is that array[N] couldn't be expanded. + * Rewrite src/lib/native/rand.c in Stratego. (This has been written in C + because I failed to make it work properly in Stratego :|) + ## ---------- ## ## Extensions ## ## ---------- ##

1 0

XRM 49: Add the static_rand builtin.
by SIGOURE Benoit 08 Jun '06

08 Jun '06

https://svn.lrde.epita.fr/svn/xrm/trunk Index: ChangeLog from SIGOURE Benoit <sigoure.benoit(a)lrde.epita.fr> Add the static_rand builtin. NOTE: Some C was needed to implement rand(from, to) because for some reason I didn't succeed in writing something equivalent in Stratego. For some reason, the numbers I generated were all too small. * src/tools/pp-xrm.str: Remove a FIXME. * src/tools/pp-prism.str: Ditto. * src/lib/xrm/pp/xrm-expression.str: Add boxing for static_rand. * src/lib/native/rand.c: New. * src/lib/native/Makefile.am: Add rand.c. * src/str/prism-desugar.str (prism-desugar-first-pass): Re-order calls and correct a minor bug. * src/str/builtin-rand.str: Handle static_rand. * src/str/xrm-front.str: Set a random seed before the main transformation pipeline starts. * src/syn/xrm/XRM-Expression.sdf: Add static_rand. lib/native/Makefile.am | 5 +- lib/native/rand.c | 27 +++++++++++ lib/xrm/pp/xrm-expression.str | 5 ++ str/builtin-rand.str | 101 ++++++++++++++++++++++++++++++------------ str/prism-desugar.str | 8 +-- str/xrm-front.str | 1 syn/xrm/XRM-Expression.sdf | 9 +++ tools/pp-prism.str | 2 tools/pp-xrm.str | 2 9 files changed, 124 insertions(+), 36 deletions(-) Index: src/tools/pp-xrm.str --- src/tools/pp-xrm.str (revision 48) +++ src/tools/pp-xrm.str (working copy) @@ -22,7 +22,7 @@ ?(<read-from-stream>, out-file) ; pp-xrm-to-abox ; box2text-stream(|80, out-file) - // FIXME: a final \n is missing + ; <fputs> ("\n", out-file) /** * Documentation Index: src/tools/pp-prism.str --- src/tools/pp-prism.str (revision 48) +++ src/tools/pp-prism.str (working copy) @@ -22,7 +22,7 @@ ?(<read-from-stream>, out-file) ; pp-prism-to-abox ; box2text-stream(|80, out-file) - // FIXME: a final \n is missing + ; <fputs> ("\n", out-file) /** * Documentation Index: src/lib/xrm/pp/xrm-expression.str --- src/lib/xrm/pp/xrm-expression.str (revision 48) +++ src/lib/xrm/pp/xrm-expression.str (working copy) @@ -21,3 +21,8 @@ Rand(args) // because func(rand, ...) is just uggly. -> box |[ 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] ")" ] ]| + where <implode-list(|",")> args => args-imploded Index: src/lib/native/rand.c --- src/lib/native/rand.c (revision 0) +++ src/lib/native/rand.c (revision 0) @@ -0,0 +1,27 @@ +/* +** rand.c for str-reals in /home/tsuna/work/xrm/trunk/src/lib/native +** +** Made by SIGOURE Benoit +** Mail <sigoure.benoit(a)lrde.epita.fr> +** +** Started on Tue Jun 6 15:13:53 2006 SIGOURE Benoit +** Last update Tue Jun 6 15:23:57 2006 SIGOURE Benoit +*/ + +#include <stdlib.h> +#include "libstr-reals.h" + +ATerm STR_REALS_rand(ATerm from, ATerm to) +{ + int ifrom; + int ito; + int r; + + if((ATgetType(from) != AT_REAL && ATgetType(from) != AT_INT) || + (ATgetType(to) != AT_REAL && ATgetType(to) != AT_INT)) + return NULL; + NUMERIC_ATERM_TO_REAL(ifrom, from); + NUMERIC_ATERM_TO_REAL(ito, to); + r = ifrom + (unsigned)((float)(ito - ifrom + 1) * rand() / (RAND_MAX + 1.)); + return (ATerm) ATmakeInt(r); +} Index: src/lib/native/Makefile.am --- src/lib/native/Makefile.am (revision 48) +++ src/lib/native/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 20:19:00 2006 SIGOURE Benoit +## Last update Tue Jun 6 15:13:38 2006 SIGOURE Benoit ## include $(top_srcdir)/config/toplevel.mk @@ -16,7 +16,8 @@ libstr_reals_la_SOURCES = $(include_HEADERS) \ ceil.c \ floor.c \ - power.c + power.c \ + rand.c # FIXME: Detect in configure whether -lm needs to be used. libstr_reals_la_LIBADD = $(SSL_LIBS) -lm Index: src/str/prism-desugar.str --- src/str/prism-desugar.str (revision 48) +++ src/str/prism-desugar.str (working copy) @@ -41,13 +41,13 @@ ** formulas and ExpandFormulas. */ prism-desugar-first-pass = - ConstInt(id, prism-desugar) + ?Int(_); IntToDouble + <+ ExpandStaticConsts; prism-desugar-first-pass // we must desugar the + <+ ExpandFormulas; prism-desugar-first-pass // expansed code. + <+ ConstInt(id, prism-desugar) <+ ConstDouble(id, prism-desugar) <+ ConstBool(id, prism-desugar) <+ FormulaDef(id, prism-desugar) - <+ ?Int(_); IntToDouble - <+ ExpandStaticConsts - <+ ExpandFormulas <+ all(prism-desugar-first-pass) rules Index: src/str/builtin-rand.str --- src/str/builtin-rand.str (revision 48) +++ src/str/builtin-rand.str (working copy) @@ -20,48 +20,39 @@ ** rand(x) -> rand(x, 0) if x < 0 */ DesugarRand: Rand([arg]) -> Rand([arg1, arg2]) - where ?current-term + where desugar-rand(|arg) => (arg1, arg2) + + DesugarRand: + StaticRand([arg]) -> StaticRand([arg1, arg2]) + where desugar-rand(|arg) => (arg1, arg2) + +strategies + + desugar-rand(|arg) = + ?current-term ; <prism-desugar> arg => arg' ; if not( !arg' => Int(iarg) ) then <invalid-call-to-rand-non-int> current-term end ; if <ltS>(iarg, "0") then - !Int("0") => arg2 - ; !arg' => arg1 + !(arg', Int("0")) else - !Int("0") => arg1 - ; !arg' => arg2 + !(Int("0"), arg') end +rules + EvalRand: Rand(args) -> Identifier(rand-var) - where ?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: rand", - " takes either one or two arguments"]) - ; !current-term; debug; <xtc-exit> 4 - end - /* desugar (constant propagation) to make both arguments simple Int */ - ; <prism-desugar> from => from' - ; <prism-desugar> to => to' - /* check that both arguments are simple Int */ - ; if not( !from' => Int(ifrom); !to' => Int(ito) ) then - <invalid-call-to-rand-non-int> current-term - end - ; if <gtS>(ifrom, ito) then - err-msg(|<concat-strings>["invalid call to XRM builtin: ", - "rand(x,y) where x > y"]) - ; !current-term; debug; <xtc-exit> 4 - end + where check-rand-args(|"rand", args) => (from, to) /* generate a name for the random variable */ ; <newname> "__rand" => rand-var - /* template: 1/(ito-ifrom+1):(rand-var'=FIXME) */ - ; !ProbUpdate( Div(Int("1"), Int( <addS>(<subtS>(ito, ifrom), "1") )) + /* template: 1/(to-from+1):(rand-var'=FIXME) */ + ; !ProbUpdate( Div(Int("1"), Int( <addS>(<subtS>(to, from), "1") )) , UpdateList([UpdateElement(IdentifierPrime(rand-var), FIXME())])) /* generate the updates by replacing the FIXME */ ; {| RandUpdateList: - for-loop(gen-rand-update-list | ifrom, ito, "1", []) + for-loop(gen-rand-update-list | from, to, "1", []) ; bagof-RandUpdateList |} ; reverse // bagof gives us the list in reverse order @@ -69,12 +60,52 @@ ; !ProbUpdateList(<id>) => u /* inject that node in a module */ ; !|[ module ~id:rand-var - ~id:rand-var : [~int:ifrom..~int:ito]; + ~id:rand-var : [~int:from..~int:to]; [] true -> u; endmodule ]| => rand-gen-module /* save this module in a DR for later retrieval */ ; rules(RandGenModules:+ _ -> rand-gen-module) + EvalRand: + StaticRand(args) -> Int(rand-val) + where check-rand-args(|"static_rand", args) => (from, to) + ; rand(|<string-to-int> from, <string-to-int> to) + ; int-to-string => rand-val + +strategies + + /** + ** Ensure that the arguments passed to rand or static_rand builtin are + ** correct: + ** - It must have exactly two arguments. + ** - Both arguments must be statically evaluable as Int(_). + ** - The first argument must be lesser than or equal to the second. + ** @param builtin-name: String used in error messages + ** @param args: arguments of the builtin call + ** @return (to, from) where to and from are integers. + */ + check-rand-args(|builtin-name, args) = + ?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: ", + builtin-name, " takes either one or two arguments"]) + ; !current-term; debug; <xtc-exit> 4 + end + /* desugar (constant propagation) to make both arguments simple Int */ + ; <prism-desugar> from => from' + ; <prism-desugar> to => to' + /* check that both arguments are simple Int */ + ; if not( !from' => Int(ifrom); !to' => Int(ito) ) then + <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"]) + ; !current-term; debug; <xtc-exit> 4 + end + ; !(ifrom, ito) + strategies gen-rand-update-list(|i, data) = @@ -86,3 +117,17 @@ " arguments must be statically evaluable"]) ; debug ; <xtc-exit> 4 + +strategies + + /** + ** Returns a random integer between `from' and `to' (included). + ** @param from Integer + ** @param to Integer + ** @return Integer + ** @warning You must call <set-random-seed> seed before calling this + ** strategy, otherwise every run will generate the same sequence of + ** random numbers. + */ + rand(|from, to) = + prim("STR_REALS_rand", from, to) Index: src/str/xrm-front.str --- src/str/xrm-front.str (revision 48) +++ src/str/xrm-front.str (working copy) @@ -40,6 +40,7 @@ /** pipeline of transformations performed by xrm-front */ xrm-front-pipeline = notice-msg(|"transformation pipeline starting") + ; where(<set-random-seed> (<time>)) ; xrm-to-prism ; dbg(|"xrm-to-prism finished") ; if must-desugar then Index: src/syn/xrm/XRM-Expression.sdf --- src/syn/xrm/XRM-Expression.sdf (revision 48) +++ src/syn/xrm/XRM-Expression.sdf (working copy) @@ -14,8 +14,10 @@ %% ExpressionFunc ::= %% (* older builtin functions for backwards compat. *) %% "rand" "(" Expression {"," Expression} ")" + %% | "static_rand" "(" Expression {"," Expression} ")" %% (* builtin functions calls using the "func" notation *) %% | "func" "(" "rand" "," Expression {"," Expression} ")" + %% | "func" "(" "static_rand" "," Expression {"," Expression} ")" context-free syntax ArrayAccess -> Expression @@ -27,9 +29,16 @@ ArrayAccess "?=" {Range ","}+ -> Expression {cons("ExistsEq")} ArrayAccess "?!=" {Range ","}+ -> Expression {cons("ExistsNotEq")} + %% rand builtin "rand" "(" {Expression ","}+ ")" -> Expression {cons("Rand")} "func" "(" "rand" "," {Expression ","}+ ")" -> Expression {cons("Rand")} + %% static rand builtin + "static_rand" "(" {Expression ","}+ ")" + -> Expression {cons("StaticRand")} + "func" "(" "static_rand" "," {Expression ","}+ ")" + -> Expression {cons("StaticRand")} + %% NOTE: remember: priorities are transitive in SDF. %% The following priorities are marked either with "inherited" or "new". %% The former means that these priorities are inherited from the base

1 0