Re: XRM 68: Extend parametrized formula to updates.

"SIGOURE" == SIGOURE Benoit <sigoure.benoit@lrde.epita.fr> writes:
Index: tests/xrm/rivf.xpm --- tests/xrm/rivf.xpm (revision 67) +++ tests/xrm/rivf.xpm (working copy)
| probabilistic | | const int width = 10; | const int height = 10; | | // coordinates of the sensor where the alert is first seen. | const int event_x = 5; | const int event_y = 5; | | //const int battery_mode = 1; // 0=no-battery, 1=battery | const int power = 15; | const int length = 1200; Useless. | const int lossage = 0; | const int loss = 76; Useless. | const int OFF = 0; | const int SLEEP = 1; | const int SENSE = 2; | const int LISTEN = 3; | const int BROADCAST = 4; | const int MAX_STATE = BROADCAST; | | const int COST_SLEEP = 1; | const int COST_SENSE = 1; | const int COST_LISTEN = 3; | const int COST_BROADCAST = 3; Can't we use an array above? | module timer | t : [0..268435454] init 0; MAX_INT would be nice. | 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); | | 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 (random_failure ? 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: 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: transition (x, y, LISTEN, COST_SENSE); | | // rule 2: LISTEN -> BROADCAST if neighbors broadcasts | 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: transition (x, y, SENSE, COST_SLEEP) | + 0.5: transition (x, y, LISTEN, COST_LISTEN); | | // rule 4: BROADCAST -> BROADCAST | [] s[x][y] = BROADCAST -> 1: transition (x, y, BROADCAST, COST_BROADCAST); | end | | endmodule How about adding "end" "module" as sugar for "endmodule"? | end | end

On 2006-06-14, Akim Demaille <akim@lrde.epita.fr> wrote:
How about adding "end" "module" as sugar for "endmodule"?
I agree for a simple `end' (to be consistent with for loops, if statements etc.) but why on earth do you want to write "end module" :P Why not "for ... end for" then? (omg I would never want to write that :P) IMHO a simple "end" is clear, concise, consistent if used everywhere, etc. -- SIGOURE Benoit aka Tsuna _____ /EPITA\ Promo 2008.CSI Rock & tRoll

"Tsuna" == Tsuna <tsuna@warszawa.lrde.epita.fr> writes:
On 2006-06-14, Akim Demaille <akim@lrde.epita.fr> wrote:
How about adding "end" "module" as sugar for "endmodule"?
I agree for a simple `end' (to be consistent with for loops, if statements etc.) but why on earth do you want to write "end module" :P Why not "for ... end for" then? (omg I would never want to write that :P)
IMHO a simple "end" is clear, concise, consistent if used everywhere, etc.
In Ada you may, at your option, qualify or not the end (with for, module etc.). The added feature is that you are more checked by the compiler, and the reader may appreciate where he is in the code when looking a longuish sources. That's already what people do with long cpp ifs.
participants (2)
-
Akim Demaille
-
Tsuna