| 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