- Projects

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

Re: XRM 56: Minor cleanups in the grammar.
by Akim Demaille 13 Jun '06

13 Jun '06

>>> "SIGOURE" == SIGOURE Benoit <sigoure.benoit(a)lrde.epita.fr> writes: > 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 How come they are useless? There were included elsewhere?

2 1

Re: XRM 54: Add RIVF's equivalent in XRM meta-code.
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> > 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). It is really nice. However, the M4 solution remains clearer IMHO. Functions will be most welcome.

2 1