[Projects] XRM 68: Extend parametrized formula to updates.

https://svn.lrde.epita.fr/svn/xrm/trunk Index: ChangeLog from SIGOURE Benoit &lt;sigoure.benoit(a)lrde.epita.fr&gt; 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