I made this change to let MonoBURG distcheck on the build farm.
https://svn.lrde.epita.fr/svn/monoburg
ChangeLog | 4 ++++
NEWS | 7 +++++++
2 files changed, 11 insertions(+)
Index: ChangeLog
from Roland Levillain <roland(a)lrde.epita.fr>
* NEWS: Update.
Index: NEWS
--- NEWS (révision 58)
+++ NEWS (copie de travail)
@@ -1,3 +1,7 @@
+* New in 1.0.5a:
+
+
+
* New in 1.0.5, 2006-02-01:
** Rework MonoBURG options
@@ -29,6 +33,7 @@
#line 1 "./tree.brg"
+
* 1.0.4
** Support named subtree with multi rules
@@ -39,6 +44,7 @@
Moreover, Name3 could be renamed Name1. The only restriction
is that Name4 couldn't be named Name1 nor Name3.
+
* 1.0.3
** Add --with-line option
@@ -53,6 +59,7 @@
Depths of `%namespace' and `%include' are no more limited.
+
* 1.0.2a
** Reoganization of the sources
>>> "SIGOURE" == SIGOURE Benoit <sigoure.benoit(a)lrde.epita.fr> writes:
> + If you wish, it is possible to specify properties directly in XRM files.
> + You can add property sections to your XRM files. Property sections can be
> + found everywhere a module declaration can be found. A property section is
> + specified as:
> + properties
> + // XPCTL code here
> + end
> + If you use property sections, you will need to pass an additional argument
> + to xrm-front to specify the PCTL property file where the options must be
> + saved. The option switch is --p-output f or -po f (where `f' is a path).
> + However, this option is not mandatory. If you specify property sections but
> + omit this switch, xrm-front will discard the properties and issue a warning
> + about that.
Many thanks!
>>> "SIGOURE" == SIGOURE Benoit <sigoure.benoit(a)lrde.epita.fr> writes:
> https://svn.lrde.epita.fr/svn/xrm/trunk
> Index: ChangeLog
> from SIGOURE Benoit <sigoure.benoit(a)lrde.epita.fr>
> Extend parametrized formula to updates.
> See rivf.xpm to see what this enables.
Nice. And nice verbose errors too.
https://svn.lrde.epita.fr/svn/xrm/trunk
Index: ChangeLog
from SIGOURE Benoit <sigoure.benoit(a)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
