Index: tests/xrm/rivf.xpm
===================================================================
--- tests/xrm/rivf.xpm	(revision 67)
+++ tests/xrm/rivf.xpm	(working copy)
@@ -32,60 +32,52 @@
 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;

+      // Whether a neighbor is broadcasting.
+      formula neighbor_broadcasts =
+          (  (x != 0          & s[x-1][y] = BROADCAST)
+	   | (x != width - 1  & s[x+1][y] = BROADCAST)
+	   | (y != 0          & s[x][y-1] = BROADCAST)
+	   | (y != height - 1 & s[x][y+1] = BROADCAST))
+
+      // Consume some power.
+      formula consume (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 state) =
+        s[x][y] '= (0 <= b[x][y]) ? state : OFF
+
+      // Transition to the next STATE, consuming COST.
+      formula transition (int state, int cost) =
+         t '= t + 1
+	 & consume (cost)
+	 & set_state (state)
+
       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 (BROADCAST, COST_SENSE);
+        // rule 2: BROADCAST -> BROADCAST
+        [] s[x][y] = BROADCAST -> 1: transition (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 (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 (neighbor_broadcasts () ? 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 (SENSE, COST_SLEEP)
+                            + 0.5: transition (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 (BROADCAST, COST_BROADCAST);
       end

     endmodule
