[Projects] XRM 76: Sync with ISOLA'06.

16 Jun 2006

https://svn.lrde.epita.fr/svn/xrm/trunk


J'espère que ça marche...


Index: ChangeLog
from  Akim Demaille  <akim@lrde.epita.fr>

	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

    