>>> "SIGOURE" == SIGOURE Benoit <sigoure.benoit(a)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
