June 2006 - Projects

Re: XRM 68: Extend parametrized formula to updates.
by Akim Demaille 14 Jun '06

14 Jun '06

>>> "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.

1 0

XRM 71: Add the -s|--seed option.
by SIGOURE Benoit 13 Jun '06

13 Jun '06

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

1 0

XRM 70: Use nodist_pkgdata_DATA instead of pkgdata_DATA_built.
by SIGOURE Benoit 13 Jun '06

13 Jun '06

https://svn.lrde.epita.fr/svn/xrm/trunk Index: ChangeLog from SIGOURE Benoit <sigoure.benoit(a)lrde.epita.fr> Use nodist_pkgdata_DATA instead of pkgdata_DATA_built. * src/syn/pctl/Makefile.am, * src/syn/prism/Makefile.am, * src/syn/xpctl/Makefile.am, * src/syn/xrm/Makefile.am: Use nodist_pkgdata_DATA instead of pkgdata_DATA_built. pctl/Makefile.am | 8 ++++---- prism/Makefile.am | 8 ++++---- xpctl/Makefile.am | 8 ++++---- xrm/Makefile.am | 8 ++++---- 4 files changed, 16 insertions(+), 16 deletions(-) Index: src/syn/pctl/Makefile.am --- src/syn/pctl/Makefile.am (revision 69) +++ src/syn/pctl/Makefile.am (working copy) @@ -19,7 +19,7 @@ -I $(STRATEGO_FRONT)/share/sdf/stratego-front \ -I $(top_srcdir)/src/syn/prism -pkgdata_DATA_built = \ +nodist_pkgdata_DATA = \ PCTL.def \ PCTL.tbl \ PCTL.rtg \ @@ -29,11 +29,11 @@ StrategoPCTL.def \ StrategoPCTL.tbl -pkgdata_DATA = $(pkgdata_DATA_built) -sdfdata_DATA = $(pkgdata_DATA_built) +pkgdata_DATA = $(nodist_pkgdata_DATA) +sdfdata_DATA = $(nodist_pkgdata_DATA) nobase_sdfdata_DATA = PCTL-Prefixed.sdf $(SDFS) -CLEANFILES = $(pkgdata_DATA_built) \ +CLEANFILES = $(nodist_pkgdata_DATA) \ $(wildcard *.dep) \ PCTL.{c,str,c.dep} \ PCTL-StartSymbols.def \ Index: src/syn/prism/Makefile.am --- src/syn/prism/Makefile.am (revision 69) +++ src/syn/prism/Makefile.am (working copy) @@ -17,7 +17,7 @@ STRINCLUDES = -I $(srcdir) SDFINCLUDES = -I $(srcdir) -I $(STRATEGO_FRONT)/share/sdf/stratego-front -pkgdata_DATA_built = \ +nodist_pkgdata_DATA = \ PRISM.def \ PRISM.tbl \ PRISM.rtg \ @@ -27,11 +27,11 @@ StrategoPRISM.def \ StrategoPRISM.tbl -pkgdata_DATA = $(pkgdata_DATA_built) -sdfdata_DATA = $(pkgdata_DATA_built) +pkgdata_DATA = $(nodist_pkgdata_DATA) +sdfdata_DATA = $(nodist_pkgdata_DATA) nobase_sdfdata_DATA = PRISM-Prefixed.sdf $(SDFS) -CLEANFILES = $(pkgdata_DATA_built) \ +CLEANFILES = $(nodist_pkgdata_DATA) \ $(wildcard *.dep) \ PRISM.{c,str,c.dep} \ PRISM-StartSymbols.def \ Index: src/syn/xpctl/Makefile.am --- src/syn/xpctl/Makefile.am (revision 69) +++ src/syn/xpctl/Makefile.am (working copy) @@ -21,7 +21,7 @@ -I $(top_srcdir)/src/syn/xrm \ -I $(top_srcdir)/src/syn/pctl -pkgdata_DATA_built = \ +nodist_pkgdata_DATA = \ XPCTL.def \ XPCTL.tbl \ XPCTL.rtg \ @@ -31,11 +31,11 @@ StrategoXPCTL.def \ StrategoXPCTL.tbl -pkgdata_DATA = $(pkgdata_DATA_built) -sdfdata_DATA = $(pkgdata_DATA_built) +pkgdata_DATA = $(nodist_pkgdata_DATA) +sdfdata_DATA = $(nodist_pkgdata_DATA) nobase_sdfdata_DATA = XPCTL-Prefixed.sdf $(SDFS) -CLEANFILES = $(pkgdata_DATA_built) \ +CLEANFILES = $(nodist_pkgdata_DATA) \ $(wildcard *.dep) \ XPCTL.{c,str,c.dep} \ XPCTL-StartSymbols.def \ Index: src/syn/xrm/Makefile.am --- src/syn/xrm/Makefile.am (revision 69) +++ src/syn/xrm/Makefile.am (working copy) @@ -19,7 +19,7 @@ -I $(STRATEGO_FRONT)/share/sdf/stratego-front \ -I $(top_srcdir)/src/syn/prism -pkgdata_DATA_built = \ +nodist_pkgdata_DATA = \ XRM.def \ XRM.tbl \ XRM.rtg \ @@ -29,11 +29,11 @@ StrategoXRM.def \ StrategoXRM.tbl -pkgdata_DATA = $(pkgdata_DATA_built) -sdfdata_DATA = $(pkgdata_DATA_built) +pkgdata_DATA = $(nodist_pkgdata_DATA) +sdfdata_DATA = $(nodist_pkgdata_DATA) nobase_sdfdata_DATA = XRM-Prefixed.sdf $(SDFS) -CLEANFILES = $(pkgdata_DATA_built) \ +CLEANFILES = $(nodist_pkgdata_DATA) \ $(wildcard *.dep) \ XRM.{c,str,c.dep} \ XRM-StartSymbols.def \

1 0

XRM 69: Use $srcdir instead of @srcdir@.
by SIGOURE Benoit 13 Jun '06

13 Jun '06

https://svn.lrde.epita.fr/svn/xrm/trunk Index: ChangeLog from SIGOURE Benoit <sigoure.benoit(a)lrde.epita.fr> Use $srcdir instead of @srcdir@. * tests/test-parse-pctl.sh.in, * tests/test-parse-prism.sh.in, * tests/test-parse-xpctl.sh.in, * tests/test-parse-xrm.sh.in, * tests/test-pp-pctl.sh.in, * tests/test-pp-prism.sh.in, * tests/test-pp-xpctl.sh.in, * tests/test-pp-xrm.sh.in, * tests/test-xrm-front.sh.in: Use $srcdir instead of @srcdir@. test-parse-pctl.sh.in | 3 ++- test-parse-prism.sh.in | 3 ++- test-parse-xpctl.sh.in | 3 ++- test-parse-xrm.sh.in | 3 ++- test-pp-pctl.sh.in | 3 ++- test-pp-prism.sh.in | 3 ++- test-pp-xpctl.sh.in | 3 ++- test-pp-xrm.sh.in | 3 ++- test-xrm-front.sh.in | 3 ++- 9 files changed, 18 insertions(+), 9 deletions(-) Index: tests/test-parse-pctl.sh.in --- tests/test-parse-pctl.sh.in (revision 68) +++ tests/test-parse-pctl.sh.in (working copy) @@ -11,9 +11,10 @@ test_cnt=0 test_pass=0 +srcdir="@srcdir@" rm -f failed_tests.$$ -for file in `find "@srcdir@" -name '*.pctl' -o -name '*.csl' | sort`; do +for file in `find "$srcdir" -name '*.pctl' -o -name '*.csl' | sort`; do echo @ECHO_N@ " Parsing `basename $file` ... " "@top_builddir@/src/tools/parse-pctl" -i "$file" -o /dev/null rv=$? Index: tests/test-parse-prism.sh.in --- tests/test-parse-prism.sh.in (revision 68) +++ tests/test-parse-prism.sh.in (working copy) @@ -11,9 +11,10 @@ test_cnt=0 test_pass=0 +srcdir="@srcdir@" rm -f failed_tests.$$ -for file in `find "@srcdir@" -name '*.pm' -o -name '*.nm' -o -name '*.sm' | sort`; do +for file in `find "$srcdir" -name '*.pm' -o -name '*.nm' -o -name '*.sm' | sort`; do echo @ECHO_N@ " Parsing `basename $file` ... " "@top_builddir@/src/tools/parse-prism" -i "$file" -o /dev/null rv=$? Index: tests/test-parse-xpctl.sh.in --- tests/test-parse-xpctl.sh.in (revision 68) +++ tests/test-parse-xpctl.sh.in (working copy) @@ -11,9 +11,10 @@ test_cnt=0 test_pass=0 +srcdir="@srcdir@" rm -f failed_tests.$$ -for file in `find "@srcdir@" -name '*.pctl' -o -name '*.csl' -o -name '*.xpctl' -o -name '*.xcsl' | sort`; do +for file in `find "$srcdir" -name '*.pctl' -o -name '*.csl' -o -name '*.xpctl' -o -name '*.xcsl' | sort`; do echo @ECHO_N@ " Parsing `basename $file` ... " "@top_builddir@/src/tools/parse-xpctl" -i "$file" -o /dev/null rv=$? Index: tests/test-parse-xrm.sh.in --- tests/test-parse-xrm.sh.in (revision 68) +++ tests/test-parse-xrm.sh.in (working copy) @@ -11,9 +11,10 @@ test_cnt=0 test_pass=0 +srcdir="@srcdir@" rm -f failed_tests.$$ -for file in `find "@srcdir@" -name '*.pm' -o -name '*.nm' -o -name '*.sm' -o -name '*.xpm' | sort`; do +for file in `find "$srcdir" -name '*.pm' -o -name '*.nm' -o -name '*.sm' -o -name '*.xpm' | sort`; do echo @ECHO_N@ " Parsing `basename $file` ... " "@top_builddir@/src/tools/parse-xrm" -i "$file" -o /dev/null rv=$? Index: tests/test-pp-pctl.sh.in --- tests/test-pp-pctl.sh.in (revision 68) +++ tests/test-pp-pctl.sh.in (working copy) @@ -11,6 +11,7 @@ test_cnt=0 test_pass=0 +srcdir="@srcdir@" target_dir='output-pp-pctl' rm -f failed_tests.$$ @@ -21,7 +22,7 @@ outdir="`pwd`" cd .. -for file in `find "@srcdir@" -name '*.pctl' -o -name '*.csl' | sort`; do +for file in `find "$srcdir" -name '*.pctl' -o -name '*.csl' | sort`; do basefile="`basename $file`" bfile="`echo \"$basefile\" | sed 's/\.x\?pm$//'`" Index: tests/test-pp-prism.sh.in --- tests/test-pp-prism.sh.in (revision 68) +++ tests/test-pp-prism.sh.in (working copy) @@ -11,6 +11,7 @@ test_cnt=0 test_pass=0 +srcdir="@srcdir@" target_dir='output-pp-prism' rm -f failed_tests.$$ @@ -21,7 +22,7 @@ outdir="`pwd`" cd .. -for file in `find "@srcdir@" -name '*.pm' -o -name '*.nm' -o -name '*.sm' | sort`; do +for file in `find "$srcdir" -name '*.pm' -o -name '*.nm' -o -name '*.sm' | sort`; do basefile="`basename $file`" bfile="`echo \"$basefile\" | sed 's/\.pm$//'`" Index: tests/test-pp-xpctl.sh.in --- tests/test-pp-xpctl.sh.in (revision 68) +++ tests/test-pp-xpctl.sh.in (working copy) @@ -11,6 +11,7 @@ test_cnt=0 test_pass=0 +srcdir="@srcdir@" target_dir='output-pp-xpctl' rm -f failed_tests.$$ @@ -21,7 +22,7 @@ outdir="`pwd`" cd .. -for file in `find "@srcdir@" -name '*.pctl' -o -name '*.csl' -o -name '*.xpctl' -o -name '*.xcsl' | sort`; do +for file in `find "$srcdir" -name '*.pctl' -o -name '*.csl' -o -name '*.xpctl' -o -name '*.xcsl' | sort`; do basefile="`basename $file`" bfile="`echo \"$basefile\" | sed 's/\.x\?pctl$//;s/\.x\?csl//'`" Index: tests/test-pp-xrm.sh.in --- tests/test-pp-xrm.sh.in (revision 68) +++ tests/test-pp-xrm.sh.in (working copy) @@ -11,6 +11,7 @@ test_cnt=0 test_pass=0 +srcdir="@srcdir@" target_dir='output-pp-xrm' rm -f failed_tests.$$ @@ -21,7 +22,7 @@ outdir="`pwd`" cd .. -for file in `find "@srcdir@" -name '*.pm' -o -name '*.nm' -o -name '*.sm' -o -name '*.xpm' | sort`; do +for file in `find "$srcdir" -name '*.pm' -o -name '*.nm' -o -name '*.sm' -o -name '*.xpm' | sort`; do basefile="`basename $file`" bfile="`echo \"$basefile\" | sed 's/\.x\?pm$//'`" Index: tests/test-xrm-front.sh.in --- tests/test-xrm-front.sh.in (revision 68) +++ tests/test-xrm-front.sh.in (working copy) @@ -11,6 +11,7 @@ test_cnt=0 test_pass=0 +srcdir="@srcdir@" target_dir='output-xrm-front' rm -f failed_tests.$$ @@ -21,7 +22,7 @@ outdir="`pwd`" cd .. -for file in `find "@srcdir@" -name '*.xpm' | sort`; do +for file in `find "$srcdir" -name '*.xpm' | sort`; do basefile="`basename $file`" bfile="`echo \"$basefile\" | sed 's/\.x\?pm$//'`"

1 0

XRM 68: Extend parametrized formula to updates.
by SIGOURE Benoit 13 Jun '06

13 Jun '06

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. * src/str/flatten-array-access.str: Yield better error messages. * src/str/desugar-array-access.str: Ditto. * src/str/xrm-to-prism.str: Don't expand parameterized formula here... * src/str/eval-meta-code.str: ... but do it here instead. * src/syn/xrm/XRM-Formula.sdf: Formulas can now contain updates. * src/syn/xrm/XRM-Expression.sdf: Parameterized formulas can be used where an update is expected. * tests/xrm/rivf.xpm: New nice version using the latest features. Written by Akim Demaille. * TODO: More things to do. TODO | 6 +++ src/str/desugar-array-access.str | 12 ++++-- src/str/eval-meta-code.str | 16 ++++++++ src/str/flatten-array-access.str | 32 +++++++++++++---- src/str/xrm-to-prism.str | 11 +----- src/syn/xrm/XRM-Expression.sdf | 2 + src/syn/xrm/XRM-Formula.sdf | 4 +- tests/xrm/rivf.xpm | 71 +++++++++++++++++---------------------- 8 files changed, 94 insertions(+), 60 deletions(-) Index: src/str/flatten-array-access.str --- src/str/flatten-array-access.str (revision 67) +++ src/str/flatten-array-access.str (working copy) @@ -32,31 +32,49 @@ /* Now the access must only contain a simple Int(..) * So we can remove the Int() constructor. */ - ; (\ Int(i) -> i \ <+ invalid-array-access) + ; (\ Int(i) -> i \ <+ invalid-array-access(|idf, subscript)) /* Now we have an int in a string such as: "1" * Check that the subscript is not negative */ - ; try(string-to-int; neg; invalid-array-access) + ; try(string-to-int; neg; invalid-array-access(|idf, subscript)) /* Produce the final identifier: eg: idf_1 */ ; <concat-strings> [idf, "_" | [<id>]] /** ** @internal + ** Report invalid array accesses and exit 5. + */ + invalid-array-access(|idf) = + wrapped-invalid-array-access(|idf) + ; <xtc-exit> 5 + + /** + ** @internal + ** Report invalid array accesses and exit 5. + */ + invalid-array-access(|idf, subscript) = + wrapped-invalid-array-access(|idf) + ; err-msg(|["original subscript:"]) + ; <debug> subscript + ; <xtc-exit> 5 + + /** + ** @internal ** Report invalid array accesses. */ - invalid-array-access = + wrapped-invalid-array-access(|idf) = if ?Identifier(i) then - err-msg(|["undeclared meta-variable: ", i]) + err-msg(|["undeclared meta-variable used in an array access on `", + idf, "': ", i]) else if (is-int; neg) then - err-msg(|"negative array subscript detected:") + err-msg(|["negative array subscript detected on array `", idf, "':"]) ; debug else - err-msg(|"invalid array access:") + err-msg(|["invalid array access on array `", idf, "':"]) ; debug ; err-msg(|["array subscripts must be evaluable ", "down to constant positive integers."]) end end - ; <xtc-exit> 5 Index: src/str/xrm-to-prism.str --- src/str/xrm-to-prism.str (revision 67) +++ src/str/xrm-to-prism.str (working copy) @@ -114,20 +114,13 @@ // FIXME: can we make this more efficient than a complete innermost? ; if <is-module-file> start-symbol then log-timed( - innermost( - flatten-array-access - <+ expand-pformulas - ) + innermost(flatten-array-access) | "Desugaring array accesses", 2) else /* NOTE: for XPCTL files we also need to expand use of XRM-Formulas * because the original definition has been removed. */ log-timed( - innermost( - flatten-array-access - <+ expand-pformulas - <+ ExpandFormulas - ) + innermost(flatten-array-access <+ ExpandFormulas) | "Desugaring array accesses", 2) end Index: src/str/prism-desugar.str Index: src/str/eval-meta-code.str --- src/str/eval-meta-code.str (revision 67) +++ src/str/eval-meta-code.str (working copy) @@ -31,6 +31,7 @@ eval-meta-if <+ unroll-meta-for <+ unroll-meta-forin + <+ (expand-pformulas; eval-meta-code) // try again on expansed code. <+ all(eval-meta-code) strategies @@ -56,6 +57,21 @@ end end + /** Try also on normal if statements... */ + eval-meta-if = + ?If(condition, then-part, else-part) + ; where(<prism-desugar> condition + ; try(LitToBool) => condition-value) + ; if !condition-value => True() then + <eval-meta-code> then-part + else + if !condition-value => False() then + <eval-meta-code> else-part + else + fail + end + end + strategies unroll-meta-for = Index: src/str/desugar-array-access.str --- src/str/desugar-array-access.str (revision 67) +++ src/str/desugar-array-access.str (working copy) @@ -37,7 +37,8 @@ ** dimension. */ desugar-subscripts = - collect-all(?ArrayAccess(_, <id>), conc) // collect gives us the list... + ?array-access // save the current term + ; collect-all(?ArrayAccess(_, <id>), conc) // collect gives us the list... ; reverse // ... with deepest array accesses first (we want the opposite) ; prism-desugar ; map( // traverse the list of dimensions @@ -45,18 +46,23 @@ if ?Int(_) then (\ Int(i) -> i \ // get rid of Int() constructor ; where(string-to-int; not(neg))) // ensure that i>=0 - <+ invalid-array-access // if anything above failed, report it + <+ <report-invalid-array-access> array-access else if ?Range(_, _) then desugar-range else // we are neither on an Int nor on a Range => invalid - invalid-array-access + <report-invalid-array-access> array-access end end ) // end inner map ; flatten-list // because Ranges create nested lists ) // end outer map + /* TODO: check that this strategy actually works :s */ + report-invalid-array-access = + fetch-idf => idf + ; invalid-array-access(|idf) + strategies /** Create the Cartesian product of all possible array subscripts. Index: src/syn/xrm/XRM-Formula.sdf --- src/syn/xrm/XRM-Formula.sdf (revision 67) +++ src/syn/xrm/XRM-Formula.sdf (working copy) @@ -21,8 +21,10 @@ -> FormulaDef {cons("FormulaDef")} context-free syntax - "formula" Identifier "(" {Argument ","}* ")" "=" Expression ";" + "formula" Identifier "(" {Argument ","}* ")" "=" (Expression|Updates) ";" -> FormulaDef {cons("PFormulaDef")} + "formula" Identifier "=" Updates ";" + -> FormulaDef {cons("FormulaDef")} sorts Argument context-free syntax Index: src/syn/xrm/XRM-Expression.sdf --- src/syn/xrm/XRM-Expression.sdf (revision 67) +++ src/syn/xrm/XRM-Expression.sdf (working copy) @@ -45,6 +45,8 @@ %% "Function" calls (parametrized formulas) Identifier "(" {Expression ","}+ ")" -> Expression {cons("PFormulaCall")} + Identifier "(" {Expression ","}+ ")" + -> Update {cons("PFormulaCall")} %% Ranges in XRM with different priority (for array accesses) sorts XRMRange Index: tests/xrm/rivf.xpm --- tests/xrm/rivf.xpm (revision 67) +++ tests/xrm/rivf.xpm (working copy) @@ -29,63 +29,54 @@ 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); + 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 + + s[x][y] : [0..MAX_STATE] 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:(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); + [] 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:(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); + [] s[x][y] = SENSE -> 1: transition (x, y, LISTEN, COST_SENSE); // 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)); + [] s[x][y] = LISTEN -> 1: transition (x, y, + neighbor_broadcasts(x, y) ? BROADCAST : SLEEP, + COST_LISTEN); // 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); + [] 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:(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); + [] s[x][y] = BROADCAST -> 1: transition (x, y, BROADCAST, COST_BROADCAST); end endmodule Index: TODO --- TODO (revision 67) +++ TODO (working copy) @@ -50,6 +50,12 @@ * Add a sanity check after xrm-front has finished to generate everything in order to ensure that each module/var decl has a unique name. + * Transform PRISM's If into a MetaIf if the condition has meta-vars (do + this before the check-meta-vars pass) + + * Add partial evaluation for Expressions which contain meta-vars. eg: + x != 0 & array[x-1]=0 // prevent array[-1] + * Add bound checking. (extension of the previous point) Dirty way: check that each variable is declared somewhere. Hard way: detect and register array declarations and detect the bounds of

1 0

Re: [Projects] Vcs cassé sur brasilia
by Roland Levillain 13 Jun '06

13 Jun '06

Roland Levillain <roland(a)lrde.epita.fr> writes: > "Nicolas Pouillard" <nicolas.pouillard(a)gmail.com> writes: > >> essaye de revenir à activesupport 1.2.5 > > J'ai l'impression que ça n'a pas changé grand'chose : > > brasilia ~ % vcs-svn 16:07 #235 > /usr/lib/ruby/gems/1.8/gems/core_ex-0.5.6.2/lib/core_ex/lazy_loading.rb:120:in `result': uninitialized constant Commands::Runners::Runner::Datas (NameError) > from /usr/lib/ruby/gems/1.8/gems/core_ex-0.5.6.2/lib/core_ex/lazy_loading.rb:71:in `load' > from /usr/lib/ruby/gems/1.8/gems/core_ex-0.5.6.2/lib/core_ex/lazy_loading.rb:133:in `load' > from /usr/lib/ruby/gems/1.8/gems/core_ex-0.5.6.2/lib/core_ex/lazy_loading.rb:149:in `const_missing' > from /usr/lib/ruby/gems/1.8/gems/activesupport-1.2.5/lib/active_support/binding_of_caller.rb:80:in `of_caller' > from /usr/lib/ruby/gems/1.8/gems/core_ex-0.5.6.2/lib/core_ex/lazy_loading.rb:147:in `const_missing' > from /usr/lib/ruby/gems/1.8/gems/ruby_ex-0.4.6.2/lib/commands/runners/runner.rb:42:in `initialize' > from /usr/lib/ruby/gems/1.8/gems/ruby_ex-0.4.6.2/lib/concrete.rb:18:in `new' > from /usr/lib/ruby/gems/1.8/gems/ruby_ex-0.4.6.2/lib/uri/generic_ex.rb:37 > ... 29 levels... > from /usr/lib/ruby/gems/1.8/gems/vcs-0.5.2.4/bin/../lib/vcs/app.rb:17 > from /usr/local/lib/site_ruby/1.8/rubygems/custom_require.rb:21:in `require' > from /usr/lib/ruby/gems/1.8/gems/vcs-0.5.2.4/bin/vcs-svn:7 > from /usr/bin/vcs-svn:18 La ligne où Ruby échoue est indiquée ci-dessous : class LazyLoader # ... def result if succeeded? return @result else -> return @module.original_core_ex_const_missing(const) end end # ... end J'ai l'impression que c'est core_ex le coupable, mais j'ai pas eu le temps d'investiguer plus loin.

2 3

Re: XRM 64: Use --verbose instead of --statistics.
by Akim Demaille 13 Jun '06

13 Jun '06

>>> "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> > Use --verbose instead of --statistics. > This cancels the note of the previous commit. What made you change your mind? Efficiency?

2 1

Re: XRM 59: Add (buggy) support for PCTL/CSL formulas.
by Akim Demaille 13 Jun '06

13 Jun '06

>>> "SIGOURE" == SIGOURE Benoit <sigoure.benoit(a)lrde.epita.fr> writes: > Index: tests/test-pp-pctl.sh.in > --- tests/test-pp-pctl.sh.in (revision 58) > +++ tests/test-pp-pctl.sh.in (working copy) > @@ -1,6 +1,6 @@ > #!/bin/sh > ## > -## test-pp-xrm.sh for xrm in /home/tsuna/work/xrm/trunk/tests > +## test-pp-pctl.sh for xrm in /home/tsuna/work/xrm/trunk/tests > ## > ## Made by SIGOURE Benoit > ## Mail <sigoure.benoit(a)lrde.epita.fr> > @@ -11,7 +11,7 @@ > test_cnt=0 > test_pass=0 > -target_dir='output-pp-xrm' > +target_dir='output-pp-pctl' > rm -f failed_tests.$$ > test ! -d $target_dir && { mkdir $target_dir \ > @@ -21,7 +21,7 @@ > outdir="`pwd`" > cd .. > -for file in `find "@srcdir@" -name '*.pm' -o -name '*.nm' -o -name '*.sm' -o -name '*.xpm' | sort`; do > +for file in `find "@srcdir@" -name '*.pctl' -o -name '*.csl' -o -name '*.xpctl' -o -name '*.xcsl' | sort`; do > basefile="`basename $file`" > bfile="`echo \"$basefile\" | sed 's/\.x\?pm$//'`" Too much code duplication. Use functions! for God sakes...

2 1

Re: XRM 59: Add (buggy) support for PCTL/CSL formulas.
by Akim Demaille 13 Jun '06

13 Jun '06

>>> "SIGOURE" == SIGOURE Benoit <sigoure.benoit(a)lrde.epita.fr> writes: > + %% FIXME: Some priorities are probably missing here > + context-free priorities > + { > + Property "=>" Property -> Property > + } > + > { > + Property "|" Property -> Property > + } > + > { > + Property "&" Property -> Property > + } > + > { > + "!" Property -> Property > + } > + > { > + Expression -> Property > + } I thought it was mandatory to keep the annotations in the rules here? It isn't the case? For instance, in some old Tiger.sdf modules, I read: module Tiger-Statements imports Tiger-Expressions exports context-free syntax LValue ":=" Exp -> Exp {cons("Assign")} "Label" IntConst Exp -> Exp {cons("ExpLabel")} "(" {Exp ";"}* ")" -> Exp {cons("Seq")} "if" Exp "then" Exp "else" Exp -> Exp {cons("If")} "if" Exp "then" Exp -> Exp {cons("IfThen")} "while" Exp "do" Exp -> Exp {cons("While")} "repeat" Exp "whilst" Exp -> Exp {cons("DoWhile")} "for" Var ":=" Exp "to" Exp "do" Exp -> Exp {cons("For")} "break" -> Exp {cons("Break")} "for" Var ":=" Exp "to" Exp "in" Exp "do" Exp -> Exp {cons("ForStride")} "[" {LValue ","}* "]" ":=" "[" {Exp ","}* "]" -> Exp {cons("ParAssign")} "label" Id -> Exp {cons("Label")} "goto" Id -> Exp {cons("Goto")} "if" Exp "goto" Id -> Exp {cons("IfGoto")} %% "(" {Exp "||"}2+ ")" -> Exp {cons("Par")} context-free priorities Exp "|" Exp -> Exp {left,cons("Or")} > LValue ":=" Exp -> Exp {cons("Assign")} > "Label" IntConst Exp -> Exp {cons("ExpLabel")} > {right: "if" Exp "then" Exp "else" Exp -> Exp {cons("If")} "if" Exp "then" Exp -> Exp {cons("If")} "while" Exp "do" Exp -> Exp {cons("While")} "repeat" Exp "whilst" Exp -> Exp {cons("DoWhile")} "for" Var ":=" Exp "to" Exp "do" Exp -> Exp {cons("For")} } > {Exp ";"}+ ";" {Exp ";"}+ -> {Exp ";"}+ Note that they preciously kept the annotations.

2 1

Re: XRM 59: Add (buggy) support for PCTL/CSL formulas.
by Akim Demaille 13 Jun '06

13 Jun '06

>>> "SIGOURE" == SIGOURE Benoit <sigoure.benoit(a)lrde.epita.fr> writes: > + prism-to-box: > + Cumul(exp) -> H hs=0 [ KW["C"] MATH["<="] ~exp ] > + > + prism-to-box: > + Inst(exp) -> H hs=0 [ KW["I"] MATH["="] ~exp ] > + > + prism-to-box: > + Reach(formula) -> H hs=1 [ KW["F"] ~formula ] Why don't you use concrete syntax?

2 1