https://svn.lrde.epita.fr/svn/xrm/trunk Index: ChangeLog from SIGOURE Benoit &lt;sigoure.benoit(a)lrde.epita.fr&gt; Add RIVF's equivalent in XRM meta-code. Usage: xrm-front -i rivf.xpm -o rivf.pm -D -D stands for --desugar (it will add an additional pass after the main pipeline to desugar as much as possible everything and perform constant propagation). This is completely optional. One thing has been omitted here: support for battery_mode=0 (which is basically the same thing but without bothering with b[x][y] and without having to check at every update whether or not we should go in the OFF state because we run out of power). I omitted this for the sake of clarity although it's fairly straightforward to add it (since it's only a matter of commenting out some lines). * tests/xrm/rivf.xpm: New. rivf.xpm | 93 +++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 93 insertions(+) Index: tests/xrm/rivf.xpm --- tests/xrm/rivf.xpm (revision 0) +++ tests/xrm/rivf.xpm (revision 0) @@ -0,0 +1,93 @@ +probabilistic + +const int width = 10; +const int height = 10; + +// coordinates of the sensors 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; + +module timer + t : [0..268435454] init 0; +endmodule + +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 + 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:(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); + 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); + + // 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)); + + // 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); + + // 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); + end + + endmodule + end +end