https://svn.lrde.epita.fr/svn/xrm/trunk Index: ChangeLog from SIGOURE Benoit <sigoure.benoit@lrde.epita.fr> Add the -s|--seed option. This way it's easy to reproduce twice the same thing. * src/str/prism-desugar.str: Extand EvalIf. * src/str/xrm-front.str: Add the -s|--seed option. * src/syn/xrm/XRM-Formula.sdf: Fix updates in formulas. * tests/xrm/rivf.xpm: Use lossage correctly. * doc/user-guide.txt: Bring up to date. doc/user-guide.txt | 53 ++++++++++++++++++++++++++------------------ src/str/prism-desugar.str | 7 ++++- src/str/xrm-front.str | 27 +++++++++++++++++++++- src/syn/xrm/XRM-Formula.sdf | 4 +-- tests/xrm/rivf.xpm | 7 ++++- 5 files changed, 70 insertions(+), 28 deletions(-) Index: src/str/prism-desugar.str --- src/str/prism-desugar.str (revision 70) +++ src/str/prism-desugar.str (working copy) @@ -346,11 +346,14 @@ EvalIf: |[ d ? e1 : e2 ]| -> |[ e1 ]| - where <not(real-eq)>(d, "0") + where <LitToBool> d => True() EvalIf: |[ d ? e1 : e2 ]| -> |[ e2 ]| - where <real-eq>(d, "0") + where <LitToBool> d => False() + + EvalIf: + |[ d ? e : e ]| -> |[ e ]| /* ** ## ============= ## Index: src/str/xrm-front.str --- src/str/xrm-front.str (revision 70) +++ src/str/xrm-front.str (working copy) @@ -47,7 +47,9 @@ /** pipeline of transformations performed by xrm-front */ xrm-front-pipeline = - where(<set-random-seed> (<time>)) + where(<set-random-seed> (<get-seed-option>) + ; if-verbose3(log(|Info(), "random seed:", <get-seed-option>)) + ) ; log-timed-reentrant(xrm-to-prism | "XRM to PRISM succeeded", 2) ; if must-desugar then log-timed(prism-desugar | "Additionnal desugarisation (-D)", 2) @@ -60,6 +62,7 @@ + keep-attributes-option + desugar-option + parse-pctl-option + + seed-option /** checks the options are consistent */ check-options = @@ -148,6 +151,28 @@ get-parser = must-parse-pctl < !"parse-xpctl" + !"parse-xrm" +strategies + + seed-option = + ArgOption("-s" + "--seed" + , set-seed-option + , !HelpString("-s | --seed", "Set the random seed used for static_rand's + values. Default is the current UNIX + timestamp.") + ) + + set-seed-option = + (string-to-int <+ invalid-seed(|"must be a positive integer")) + ; (not(neg) <+ invalid-seed(|"must be a *positive* integer")) + ; <set-config> ("seed", <id>) + + get-seed-option = + <get-config> "seed" <+ time + + invalid-seed(|msg) = + err-msg(|["Invalid value for --seed: ", msg, "."]) + ; <xtc-exit> 1 + /** * Documentation */ Index: src/syn/xrm/XRM-Formula.sdf --- src/syn/xrm/XRM-Formula.sdf (revision 70) +++ src/syn/xrm/XRM-Formula.sdf (working copy) @@ -21,9 +21,9 @@ -> FormulaDef {cons("FormulaDef")} context-free syntax - "formula" Identifier "(" {Argument ","}* ")" "=" (Expression|Updates) ";" + "formula" Identifier "(" {Argument ","}* ")" "=" (Expression|Update) ";" -> FormulaDef {cons("PFormulaDef")} - "formula" Identifier "=" Updates ";" + "formula" Identifier "=" Update ";" -> FormulaDef {cons("FormulaDef")} sorts Argument Index: tests/xrm/rivf.xpm --- tests/xrm/rivf.xpm (revision 70) +++ tests/xrm/rivf.xpm (working copy) @@ -3,7 +3,7 @@ const int width = 10; const int height = 10; -// coordinates of the sensors where the alert is first seen. +// coordinates of the sensor where the alert is first seen. const int event_x = 5; const int event_y = 5; @@ -48,11 +48,14 @@ formula transition (int x, int y, int state, int cost) = t' = t + 1 & consume (x, y, cost) & set_state (x, y, state); +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 module sensor[x][y] - s[x][y] : [0..MAX_STATE] init (static_rand(0, 100) < lossage) ? OFF : SENSE; + s[x][y] : [0..MAX_STATE] init (random_failure ? OFF : SENSE); b[x][y] : [0..power] init power; if x = event_x & y = event_y then Index: doc/user-guide.txt --- doc/user-guide.txt (revision 70) +++ doc/user-guide.txt (working copy) @@ -54,8 +54,8 @@ $ 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 + If you don't use Nix, use `../configure PKG_CONFIG_PATH=<P>' 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 @@ -72,11 +72,9 @@ - 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. + - parse-xrm, parse-pctl, parse-xpctl: Ditto with XRM/PCTL/XPCTL 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. + - pp-xrm, pp-pctl, pp-xpctl: Ditto with XRM/PCTL/XPCTL source code. ******************* * Using xrm-front * @@ -148,6 +146,10 @@ 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. + o It is possible to disambiguate a double value from an integer by + prefixing the literal value with either `d' or `D' or `f' or `F', eg: + const double p = 1D; // same as 1.0 + This is mainly used internally for concrete syntax. + TODO: "?=" and "?!=" operators for arrays. # XRM Arrays @@ -175,7 +177,7 @@ 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 + 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]; @@ -357,23 +359,32 @@ -------------------------- XRM formulas have been eXtended and can now be parameterized, eg: formula isfree(int i) = p[i]=0..4,6,10; - Parameterized formulas can have 4 kinds of arguments: - o int (as in the example above) - o double - o bool - o exp - With the `exp' type, the formula behaves a bit like C's macro-functions. + o Parameterized formulas can have 4 kinds of arguments: + - int (as in the example above) + - double + - bool + - exp + o With the `exp' type, the formula behaves a bit like C's macro-functions. We can also see that as a void type since no type-checking will be performed on this kind of arguments. - Parameterized formulas definitions will be removed in the output PRISM + o Parameterized formulas definitions will be removed in the output PRISM code. Invoking parameterized formulas is somewhat like calling a function, eg: isfree(2) will be inlined as p[2]=0..4,6,10; - However note that using the PRISM-3 calling style for builtins cannot be - used for formulas, eg: func(isfree, 2) is not supported at the moment. We - _might_ add support for this. - Once a parameterized formula has been defined, it can't be + o Note that using the PRISM-3 calling style for builtins cannot be + used for formulas, eg: func(isfree, 2) is not supported at the moment. + We _might_ add support for this. + o Once a parameterized formula has been defined, it can't be redefined/undefined, just like a normal PRISM formula. + o Parameterized formula can also define updates, not only expressions, eg: + formula consume (int value) = + battery' = battery < value ? 0 : battery - value; + // ... + module sensor + battery : [0..POWER] init POWER; + // ... + [] must_wake_up -> 1:consume(WAKE_UP_COST); + endmodule # XRM Keywords ------------ @@ -391,9 +402,9 @@ It is also possible to define formulas and parameterized formulas in XPCTL files. - ********************* - * Incoming features * - ********************* + ************************ + * Forthcoming features * + ************************ The following features are not yet implemented (or only partially implemented or broken). They are ordered in term of the estimated time