https://svn.lrde.epita.fr/svn/xrm/trunk J'espère que ça marche... Index: ChangeLog from Akim Demaille &lt;akim(a)lrde.epita.fr&gt; Sync with ISOLA'06. * tests/xrm/rivf.xpm: Update. rivf.xpm | 145 ++++++++++++++++++++++++++++++++++----------------------------- 1 file changed, 79 insertions(+), 66 deletions(-) Index: tests/xrm/rivf.xpm --- tests/xrm/rivf.xpm (revision 75) +++ tests/xrm/rivf.xpm (working copy) @@ -1,87 +1,100 @@ probabilistic -const int width = 10; -const int height = 10; +// ------------ // +// Parameters. // +// ------------ // -// 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; -const int lossage = 0; -const int loss = 76; - -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; +// Grid dimensions. +const int X = 10, Y = 10; + +// Initial energy, percentage of lost cells. +const int power = 15, lossage = 50; + +// States. +const int OFF = 0, SLEEP = 1, SENSE = 2, + LISTEN = 3, BROADCAST = 4; + +// Energy consumption for each state. +const int COST_SLEEP = 1, COST_SENSE = 1, + COST_LISTEN = 3, COST_BROADCAST = 3; + + +// ---------- // +// Formulas. // +// ---------- // + +// Whether X, Y is valid, and broadcasts. +formula broadcasts (int x, int y) + valid (x, y) & s[x][y] = BROADCASTS + +// Whether a neighbor of X, Y is broadcasting. +formula ears (int x, int y) = + broadcasts (x - 1, y) | broadcasts (x + 1, y) + | broadcasts (x, y - 1) | broadcasts (x, y + 1) + +// Whether the event (middle cell) is detected. +formula senses (int x, int Y) = + x = X / 2 & y = Y / 2; + +// Consume C units of power. +formula consume (int x, int y, int c) = + b[x][y]' = b[x][y] < c ? 0 : b[x][y] - c; + +// Reach state ST if energy allows it. +formula set_state (int x, int y, int st) = + s[x][y]' = (0 <= b[x][y]) ? st : OFF; module timer 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); +// Transition to the next state ST, consuming C. +formula transition (int x, int y, int st, int c) = + t' = t+1 & consume(x, y, c) & set_state(x, y, st); -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 +// --------- // +// Sensors. // +// --------- // + +for x from 0 to X - 1 do + for y from 0 to Y - 1 do module sensor[x][y] - s[x][y] : [0..MAX_STATE] init (random_failure ? OFF : SENSE); + s[x][y] : [0..4] 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: 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] = SENSE -> 1: transition (x, y, senses (x, y) ? BROADCAST : LISTEN, COST_SENSE); + [] s[x][y] = LISTEN -> 1: transition (x, y, ears (x, y) ? BROADCAST : SLEEP, COST_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 module + end end - endmodule +// ------------ // +// Properties. // +// ------------ // + +// A broadcast in (x, y..Y - 1)? +formula X_broadcasts (int x, int y) = + valid (x, y) + & (broadcasts (x, y) | X_broadcasts (x, y + 1)); + +// A broadcast in (x..X - 1, y)? +formula Y_broadcasts (int x, int y) = + valid (x, y) + & (broadcasts (x, y) | Y_broadcasts (x + 1, y)); + +// A broadcast in the perimeter? +formula boundary_broadcasts = + X_broadcasts (0, 0) | X_broadcasts (X - 1, 0) + | Y_broadcasts (0, 0) | Y_broadcasts (0, Y - 1); + +properties + for T from 0 to 1200 step 100 do + // Alarmed triggered before instant T? + P =? [ true U (t <= T & boundary_broadcasts) ]; end end