--- Real-Time Maude 2.2 specification of the OGDC algorithm. --- October 18, 2006. --- First: load real-time-maude. You may need to also take the directory --- into account: load real-time-maude --- Remember when executing: please also change the sensing area size --- and the value of the constant 'n' around lines 926 to 929, so --- that 'n' equals the number of nodes. This latter is not crucial, as it --- "only" affects the probability that a node volunteers to be a starting --- node. ****( TUNABLE PARAMETERS )**** (omod OGDC-PARAMETERS is protecting CONVERSION . protecting NAT-TIME-DOMAIN-WITH-INF . op max : TimeInf Int -> TimeInf [ditto] . --- new in RTM 2.2 ---( Constants )--- --- Number of nodes in network op n : -> Nat . --- Size of sensor area in meters op sensingAreaSize : -> Nat . --- Round time in ms op roundTime : -> Nat . eq roundTime = 1000000 . --- If a node does not volunteer it sets it's timer to this value op nonVolunteerTimer : -> Time . eq nonVolunteerTimer = 1000 . --- Upper bound for the volunteer timer op volunteerTimeBound : -> Time . eq volunteerTimeBound = 10 . --- Timer is set to this value when a node receives a power-on --- message and all crossings within range are covered and --- there are no starting neighbors op tc : -> Time . eq tc = 200 . --- Sensing range in centimeters op sensingRange : -> Nat . eq sensingRange = 1000 . --- Transmission range in centimeters op transmissionRange : -> Nat . eq transmissionRange = 2 * sensingRange . --- Transmission time in ms (originally 6.8) op transmissionDelay : -> Nat . eq transmissionDelay = 7 . --- Backoff scale op c : -> Rat . eq c = 10 / (sensingRange * sensingRange) . ---( Power related constants )--- --- Power ratio = transmit:idle:sleep = 5:1:0.0025 --- One power unit (pu) is the amount of power needed --- to stay idle for one millisecond op powerUnit : -> Nat . eq powerUnit = 400 . --- Startup power, lifetime op lifetime : -> Nat . eq lifetime = 5000000 * powerUnit . --- Power threshold - minimum power required to volunteer--- op powerThreshold : -> Nat . eq powerThreshold = 900000 * powerUnit . --- Power required to transmit one power-on message op transPower : -> Nat . eq transPower = powerUnit * 5 * transmissionDelay . --- Power required to sleep one millisecond op sleepPower : -> Nat . eq sleepPower = powerUnit * (25 / 10000) . --- Power required to stay idle for one millisecond op idlePower : -> Nat . eq idlePower = powerUnit . endom) ****( BASIC SORTS AND FUNCTIONS )**** (omod OGDC-SORTS is protecting OGDC-PARAMETERS . including BOOL . sorts LocationSet Location Status VolunteeredStatus NeighborSet Neighbor . subsort Location < Oid LocationSet . subsort Neighbor < NeighborSet . subsort Bool < VolunteeredStatus . --- A location is represented by its coordinates op _._ : Rat Rat -> Location [ctor] . --- Definition of a set of locations and some basic function on this set op none : -> LocationSet [ctor] . op _;_ : LocationSet LocationSet -> LocationSet [ctor assoc comm id: none] . op _minus_ : LocationSet LocationSet -> LocationSet . op remove : LocationSet Oid -> LocationSet . --- A node can have one of three statuses op on : -> Status [ctor format ( g o )] . op off : -> Status [ctor format ( r o )] . op undecided : -> Status [ctor] . --- A node can have one of three volunteered statuses; undecided, true, or false op undecided : -> VolunteeredStatus [ctor] . --- A neighbor is represented by it's coordinate and whether it's a starting node op _starting_ : Location Bool -> Neighbor . op none : -> NeighborSet [ctor] . op __ : NeighborSet NeighborSet -> NeighborSet [ctor assoc comm id: none] . --- RandomNGen object name op Random : -> Oid . --- Basic functions for computing and checking distances op isInSensingArea : Location -> Bool . op vectorLengthSq : Location Location -> Rat . op _withinSensingRangeOf_ : Location Location -> Bool . op _withinTwiceTheSensingRangeOf_ : Location Location -> Bool . op _withinTransmissionRangeOf_ : Location Location -> Bool . vars L L' : Location . vars LS LS' : LocationSet . vars X X' Y Y' : Rat . var SASIZE : Nat . ceq isInSensingArea(X . Y) = (abs(X) <= SASIZE) and (abs(Y) <= SASIZE) if SASIZE := sensingAreaSize / 2 . eq vectorLengthSq(X . Y, X' . Y') = ((X - X') * (X - X')) + ((Y - Y') * (Y - Y')) . eq L withinSensingRangeOf L' = vectorLengthSq(L, L') <= (sensingRange * sensingRange) . eq L withinTwiceTheSensingRangeOf L' = vectorLengthSq(L, L') <= (4 * sensingRange * sensingRange) . eq L withinTransmissionRangeOf L' = vectorLengthSq(L, L') <= (transmissionRange * transmissionRange) . eq LS minus none = LS . eq none minus LS = none . eq LS minus (L ; LS') = remove(LS, L) minus LS' . eq remove(none, L) = none . eq remove((LS ; L), L') = (if (L == L') then remove(LS, L') else remove(LS, L') ; L fi) . endom) ****( BITMAP DEFINITION **** (omod OGDC-BITMAP is protecting OGDC-SORTS . sorts Bitmap BitList Bit . subsort Bit < BitList . --- A cell in the bitmap is either true (t) false (f) or not in use (') op t : -> Bit [ctor format ( g o )] . op f : -> Bit [ctor format ( r o )] . op ' : -> Bit [ctor format ( y o )] . --- Collect bit's into a list op nil : -> BitList [ctor] . op __ : BitList BitList -> BitList [ctor assoc id: nil format ( o s o )] . --- Incapsulate one row in the bitmap with | | starting on a --- separate line to give more intuitive formatting op |_| : BitList -> Bitmap [ctor format ( ni o o o )] . --- Collect rows into a bitmap op nil : -> Bitmap [ctor] . op __ : Bitmap Bitmap -> Bitmap [ctor assoc id: nil format ( o s o )] . --- Define the distance between each bit op gridInc : -> Nat . eq gridInc = 100 . --- Determine how many rows and columns the bitmap will have op gridCounter : -> Nat . eq gridCounter = ceiling((2 * sensingRange) / gridInc) + if (gridInc divides (2 * sensingRange)) then 1 else 0 fi . --- Initialize bitmap op initBitmap : Location -> Bitmap . op makeColumnBitmap : Location Location Nat Nat -> Bitmap . op makeRowBitmap : Location Location Nat Nat -> BitList . --- Update bitmap op updateBitmap : Location Bitmap Location -> Bitmap . op updateBitmap : Bitmap Location Location Nat -> Bitmap . op updateBitList : BitList Location Location Nat -> BitList . --- Check if sensor area is completely covered op coverageAreaCovered : Bitmap -> Bool . vars L L' : Location . vars BM : Bitmap . var BITL : BitList . vars X X' Y Y' : Rat . var BIT : Bit . vars I N : Nat . --- Start making the bitmap from the top left corner eq initBitmap(X . Y) = makeColumnBitmap(X . Y, X - sensingRange . Y + sensingRange, gridInc, gridCounter) . --- Make bitmap centered in L, with N rows and columns and increment I eq makeColumnBitmap(L, X . Y, I, N) = if N > 0 then | makeRowBitmap(L, X . Y, I, gridCounter) | makeColumnBitmap(L, X . Y - I, I, N - 1) else nil fi . eq makeRowBitmap(X' . Y', X . Y, I, N) = if N > 0 then (if ((X' . Y') withinSensingRangeOf (X . Y)) and isInSensingArea(X . Y) then f else ' fi) makeRowBitmap(X' . Y', X + I . Y, I, N - 1) else nil fi . --- Update the bitmap from the top left corner eq updateBitmap(X . Y, BM, L) = updateBitmap(BM, L, X - sensingRange . Y + sensingRange, gridInc) . eq updateBitmap(nil, L', L, I) = nil . eq updateBitmap(| BITL | BM, L', X . Y, I) = | updateBitList(BITL, L', X . Y, I) | updateBitmap(BM, L', X . Y - I, I) . --- Update one row of the bitmap eq updateBitList(nil, L', L, I) = nil . eq updateBitList(BIT BITL, L', X . Y, I) = if (BIT =/= f) then BIT else if L' withinSensingRangeOf (X . Y) then t else f fi fi updateBitList(BITL, L', X + I . Y, I) . --- Check if sensing area is completely covered after updated --- with the latest neighbor's position ---( stian's solution: eq coverageAreaCovered(nil) = true . eq coverageAreaCovered(| nil | BM) = coverageAreaCovered(BM) . eq coverageAreaCovered(| BIT BITL | BM) = (BIT =/= f) and coverageAreaCovered(| BITL | BM) . )--- ---Is it more efficient with 'owise'??? var BM' : Bitmap . var BITL' : BitList . eq coverageAreaCovered(BM | BITL f BITL' | BM') = false . eq coverageAreaCovered(BM) = true [owise] . endom) ****( COMPUTATION OF CROSSINGS **** (omod OGDC-COVERAGE-OPERATIONS is protecting OGDC-SORTS . sorts Crossing CrossingSet . subsort Crossing < CrossingSet . --- A crossing between two sensing areas is represented by the location of the two nodes --- that create the crossing and the coordinates of the crossing op _x_in_ : Location Location Location -> Crossing [ctor] . op none : -> CrossingSet [ctor] . op __ : CrossingSet CrossingSet -> CrossingSet [ctor assoc comm id: none] . --- Find all crossings created by a node at a given location and a list of neighbors op newCrossings : Location Location NeighborSet -> CrossingSet . op findCrossings : Location NeighborSet -> CrossingSet . --- Update a list of uncovered crossings op updateUncoveredCrossings : Location Location NeighborSet CrossingSet -> CrossingSet . --- Extract uncovered crossings op listUncoveredCrossings : LocationSet CrossingSet -> CrossingSet . op crossingIsUncovered : LocationSet Crossing -> Bool . --- Extract crossings that are within range of a given location op extractValidCrossings : Location CrossingSet -> CrossingSet . --- Determine whether a location creates the closest crossing to another location op _createsClosestCrossing__ : Location Location CrossingSet -> Bool . op closestCrossing : Location CrossingSet -> Crossing . --- Find closest starting neighbor op findClosestStartingNeighbor : Location NeighborSet -> Location . --- Determine wether there exists a starting neighbor in a list of neighbors op existsStartingNeighbor : NeighborSet -> Bool . --- Extract all starting neighbors op listStartingNeighbors : NeighborSet -> LocationSet . --- Find the closest neighbor to a location op findClosestNeighbor : Location NeighborSet -> Location . op compareNeighbors : Location LocationSet -> Location . --- Compute the crossings between two nodes op findPairCrossings : Location Location -> CrossingSet . op calcLinearCrossing : Location Location Bool -> Location . --- Auxiliary operators to calculate a crossing point op sqrt : Rat -> Rat . ops delta u v a b c : Location Location -> Rat . ops y x : Location Location Bool -> Rat . --- Other auxiliary functions op extractLocation : NeighborSet -> LocationSet . op locationCreatesCrossing : Location Crossing -> Bool . op extractCrossing : Crossing -> Location . var B : Bool . vars LS : LocationSet . vars L L' L'' L''' L1' L1'' L1''' : Location . vars X X' Y Y' R : Rat . vars C : Crossing . vars CS : CrossingSet . var NBS : NeighborSet . eq sqrt(R) = rat(sqrt(float(R))) . eq L' createsClosestCrossing L CS = locationCreatesCrossing(L', closestCrossing(L, CS)) . --- Find closest crossing eq closestCrossing(L, none) = none . eq closestCrossing(L, C) = C . eq closestCrossing(L, (L' x L'' in L''') (L1' x L1'' in L1''') CS) = if vectorLengthSq(L, L''') < vectorLengthSq(L, L1''') then closestCrossing(L, (L' x L'' in L''') CS) else closestCrossing(L, (L1' x L1'' in L1''') CS) fi . --- Update the list of uncovered crossings eq updateUncoveredCrossings(L, L', NBS, CS) = listUncoveredCrossings(L', CS) listUncoveredCrossings(extractLocation(NBS), newCrossings(L, L', NBS)) . eq newCrossings(L, L', NBS) = extractValidCrossings(L, findCrossings(L', NBS)) . eq findCrossings(L, none) = none . eq findCrossings(L, (L' starting B) NBS) = (if L withinTwiceTheSensingRangeOf L' then findPairCrossings(L, L') else none fi) findCrossings(L, NBS) . --- Only keep crossings that are uncovered by a third node eq listUncoveredCrossings(LS, none) = none . eq listUncoveredCrossings(LS, (L x L' in L'') CS) = if crossingIsUncovered(LS minus (L ; L'), (L x L' in L'')) then (L x L' in L'') else none fi listUncoveredCrossings(LS, CS) . --- Determine if a crossing is within range of the nodes in LS eq crossingIsUncovered(none, C) = true . eq crossingIsUncovered(L ; LS, (L' x L'' in L''')) = (not L withinSensingRangeOf L''') and crossingIsUncovered(LS, (L' x L'' in L''')) . ---Only keep the crossings within sensor range of L eq extractValidCrossings(L, none) = none . eq extractValidCrossings(L, (L' x L'' in L''') CS) = if L withinSensingRangeOf L''' then (L' x L'' in L''') else none fi extractValidCrossings(L, CS) . --- Find the crossings between two nodes eq findPairCrossings(X . Y, X' . Y') = if X =/= X' then (X . Y x X' . Y' in x(X . Y, X' . Y', true) . y(X . Y, X' . Y', true)) (X . Y x X' . Y' in x(X . Y, X' . Y', false) . y(X . Y, X' . Y', false)) else (X . Y x X' . Y' in calcLinearCrossing(X . Y, X' . Y', true)) (X . Y x X' . Y' in calcLinearCrossing(X . Y, X' . Y', false)) fi . --- Special case where the one node is directly above the other eq calcLinearCrossing(X . Y, X' . Y', true) = ((2 * X + sqrt( (((4 * sensingRange * sensingRange) - (Y' * Y')) + (2 * Y * Y')) - (Y * Y))) / 2 . (Y + Y') / 2) . eq calcLinearCrossing(X . Y, X' . Y', false) = ((2 * X - sqrt( (((4 * sensingRange * sensingRange) - (Y' * Y')) + (2 * Y * Y')) - (Y * Y))) / 2 . (Y + Y') / 2) . --- Compute the x and y coordinate eq y(L, L', true) = ceiling((- b(L, L') + delta(L, L')) / (2 * a(L, L'))) . eq y(L, L', false) = ceiling((- b(L, L') - delta(L, L')) / (2 * a(L, L'))) . eq x(L, L', B) = ceiling((- u(L, L') * y(L, L', B)) - v(L, L')) . eq delta(L, L') = sqrt((b(L, L') * b(L, L')) - (4 * a(L, L') * c(L, L'))) . eq u(X . Y, X' . Y') = (Y - Y') / (X - X') . eq v(X . Y, X' . Y') = (((X' * X') + (Y' * Y')) - ((X * X) + Y * Y)) / (2 * (X - X')) . --- ay2 + by + c = 0 eq a(L, L') = 1 + (u(L, L') * u(L, L')) . eq b(L, X' . Y') = 2 * u(L, X' . Y') * (X' + v(L, X' . Y')) - (2 * Y') . eq c(L, X' . Y') = ((Y' * Y') + ((v(L, X' . Y') + X') * (v(L, X' . Y') + X'))) - (sensingRange * sensingRange) . --- Determine if a starting neighbor exists eq existsStartingNeighbor(none) = false . eq existsStartingNeighbor((X . Y starting B) NBS) = B or existsStartingNeighbor(NBS) . --- Find the closest starting neighbor to L in NBS eq findClosestStartingNeighbor(L, NBS) = compareNeighbors(L, listStartingNeighbors(NBS)) . --- List all starting neighbors eq listStartingNeighbors(none) = none . eq listStartingNeighbors((X . Y starting B) NBS) = if B then X . Y else none fi ; listStartingNeighbors(NBS) . --- Find the closest neighbor to L in NBS eq findClosestNeighbor(L, NBS) = compareNeighbors(L, extractLocation(NBS)) . --- Find the closest neighbor to L in LS eq compareNeighbors(L, L') = L' . eq compareNeighbors(L, L' ; L'' ; LS) = if vectorLengthSq(L, L') < vectorLengthSq(L, L'') then compareNeighbors(L, L' ; LS) else compareNeighbors(L, L'' ; LS) fi . eq extractLocation(none) = none . eq extractLocation((L starting B) NBS) = L ; extractLocation(NBS) . eq locationCreatesCrossing(L, L' x L'' in L''') = L == L' or L == L'' . eq extractCrossing(L x L' in L'') = L'' . endom) ****( RANDOM NUMBER GENERATOR )**** (omod RANDOM is including NAT . class RandomNGen | seed : Nat . op random : Nat -> Nat . --- random(x) generates the next random number vars N N' : Nat . eq random(N) = ((104 * N) + 7921) rem 10609 . --- Obeys Knuths criteria for a "good" random function --- The seed may be modified by applying the random function many times: op repeatRandom : Nat Nat -> Nat . --- repeatRandom(seed, noOfReps) eq repeatRandom(N, s N') = repeatRandom(random(N), N') . eq repeatRandom(N, 0) = N . endom) ****( BACKOFF TIMER COMPUTATIONS )**** (omod OGDC-TC is protecting OGDC-COVERAGE-OPERATIONS . protecting RANDOM . op setTa : Location Nat CrossingSet -> Time . --- Angle between optimal location and location of receiver node op dAlphaTa : Location Crossing -> Rat . op dAlphaTaSingleCrossing : Location Crossing -> Rat . ---Distance from receiver to closest crossing point op dTa : Location Crossing -> Rat . op setTb : Location Location Nat NeighborSet Nat -> Time . --- Angle between desired node position and receiver node op dAlphaTb : Location Location Nat -> Rat . ---Distance from receiver to sender--- op dTb : Location Location -> Rat . op acos : Rat -> Rat . eq acos(R:Rat) = rat(acos(float(R:Rat))) . op pi : -> Rat . eq pi = rat(pi) . op negY : Location -> Bool . --- Calculate the angle the vector created by the two locations and the x-axis op angle : Location Location -> Rat . --- Normalize a vector op normalize : Location -> Location . --- Calculate the scalar product of two vectors op dotProd : Location Location -> Rat . --- Random term [0 , 1> op randomU : Nat -> Rat . eq randomU(N:Nat) = (random(N:Nat) rem 100) / 100 . vars R ANGLE X X' Y Y' : Rat . vars N D : Nat . vars C CLOSESTC : Crossing . var CS : CrossingSet . var NBS : NeighborSet . vars L L' VECTOR : Location . ceq setTa(L, N, CS) = ceiling(transmissionDelay * (c * (((sensingRange - dTa(L, CLOSESTC)) * (sensingRange - dTa(L, CLOSESTC))) + (dTa(L, CLOSESTC) * dTa(L, CLOSESTC) * dAlphaTa(L, CLOSESTC) * dAlphaTa(L, CLOSESTC))) + randomU(N))) if CLOSESTC := closestCrossing(L, CS) . --- Distance between receiver node and the closest uncovered crossing point eq dTa(L, C) = sqrt(vectorLengthSq(L, extractCrossing(C))) . ---( Angle between the optimal node location and the location of --- the receiving node )--- eq dAlphaTa(L, C) = dAlphaTaSingleCrossing(L, C) . ceq dAlphaTaSingleCrossing(L, X . Y x X' . Y' in L') = (if ANGLE > pi then 2 * pi - ANGLE else ANGLE fi) if ANGLE := abs(angle(L', L) - angle(((X' + X) / 2 . (Y' + Y) / 2), L')) . eq setTb(L, L', D, NBS, N) = ceiling(transmissionDelay * (c * (((sqrt(3) * sensingRange - dTb(L, L')) * (sqrt(3) * sensingRange - dTb(L, L'))) + (dTb(L, L') * dTb(L, L') * dAlphaTb(L, L', D) * dAlphaTb(L, L', D))) + randomU(N))) . --- Distance from sender to receiver eq dTb(L, L') = sqrt(vectorLengthSq(L, L')) . --- Angle between the desired direction in which the node should be --- located and the direction from the sender to the receiver ceq dAlphaTb(L, L', D) = (if ANGLE > pi then 2 * pi - ANGLE else ANGLE fi) if ANGLE := abs(angle(L', L) - ((D / 180) * pi)) . --- Angle between the vector from (X . Y) to (X' . Y') and the x-axis ceq angle(X . Y, X' . Y') = (if negY(VECTOR) then 2 * pi - acos(dotProd(VECTOR, 1 . 0)) else acos(dotProd(VECTOR, 1 . 0)) fi) if VECTOR := normalize((X' - X) . (Y' - Y)) . eq normalize(X . Y) = ((X / (sqrt((X * X) + (Y * Y)))) . (Y / (sqrt((X * X) + (Y * Y))))) . eq dotProd(X . Y, X' . Y') = (X * X') + (Y * Y') . eq negY(X . Y) = Y < 0 . endom) ****( NODE AND MESSGAE DEFINITIONS )**** (tomod OGDC-NODE-AND-MESSAGE-DEFINITIONS is protecting OGDC-BITMAP . protecting OGDC-TC . --- Messages msg broadcast`from_withDirection_ : Oid Int -> Msg . msg power-onMsgFrom_to_withDirection_ : Oid Oid Int -> Msg . op dly : Msg TimeInf -> Msg [ctor right id: 0] . --- Wireless Sensor Node class WSNode | backoffTimer : TimeInf, bitmap : Bitmap, hasVolunteered : VolunteeredStatus, neighbors : NeighborSet, uncoveredCrossings : CrossingSet, remainingPower : Nat, roundTimer : TimeInf, status : Status, volunteerProb : Rat . endtom) ****( THE OGDC ALGORITHM )**** (tomod OGDC is protecting OGDC-NODE-AND-MESSAGE-DEFINITIONS . --- Message distribution op distributeMsg : Oid Nat Configuration -> Configuration [frozen (3)] . --- Auxiliary fuctions --- Double the probability for volunteering op doubleProb : Rat -> Rat . --- [0, 1000> op randomProb : Nat -> Nat . --- [0, td> op randomTimer : Nat -> Time . --- [0, 360> op randomDirection : Nat -> Nat . vars O O' : Oid . var D : Int . vars M N : Nat . var P : NzNat . vars R : Rat . var L : Location . var BM : Bitmap . var NB : Neighbor . var NBS : NeighborSet . var CS : CrossingSet . vars T : Time . var S : Status . var C : Configuration . var MSG : Msg . --- Message broadcasting eq {< O : WSNode | > (broadcast from O withDirection D) C} = {< O : WSNode | > distributeMsg(O, D, C)} . --- Break down the broadcast message to single messages for nodes which --- are within transmission range eq distributeMsg(O, D, none) = none . eq distributeMsg(O, D, MSG C) = MSG distributeMsg(O, D, C) . eq distributeMsg(O, D, < Random : RandomNGen | > C) = < Random : RandomNGen | > distributeMsg(O, D, C) . eq distributeMsg(O, D, < O' : WSNode | > C) = < O' : WSNode | > distributeMsg(O, D, C) (if O withinTransmissionRangeOf O' then dly((power-onMsgFrom O to O' withDirection D), transmissionDelay) else none fi) . eq doubleProb(R) = if R >= 1000 / 2 then 1000 else 2 * R fi . eq randomProb(N) = random(N) rem 1000 . eq randomTimer(N) = random(N) rem volunteerTimeBound . eq randomDirection(N) = random(N) rem 360 . ---( Dynamic behavior in OGDC )--- ---( A node volunteers with probability N )--- rl [volunteer] : < O : WSNode | remainingPower : P, volunteerProb : R, hasVolunteered : undecided > < Random : RandomNGen | seed : M > => (if (randomProb(M) < R) and (P > powerThreshold or R == 1000) then < O : WSNode | backoffTimer : randomTimer(random(M)), hasVolunteered : true > else < O : WSNode | backoffTimer : nonVolunteerTimer, hasVolunteered : false, volunteerProb : doubleProb(R) > fi) < Random : RandomNGen | seed : repeatRandom(M, 3) > . --- If the nonVolunteerTimer timer expires, volunteer again with the volunteer --- probability doubled rl [repeatVolunteering] : < O : WSNode | backoffTimer : 0, neighbors : none, volunteerProb : R, remainingPower : P, hasVolunteered : false > < Random : RandomNGen | seed : M > => (if (randomProb(M) < R) and (P > powerThreshold or R == 1000) then < O : WSNode | backoffTimer : randomTimer(random(M)), hasVolunteered : true > else < O : WSNode | backoffTimer : nonVolunteerTimer, volunteerProb : doubleProb(R) > fi) < Random : RandomNGen | seed : repeatRandom(M, 3) > . --- Power on and send out a message when the timer expires rl [startingNodePowerOn] : < O : WSNode | remainingPower : P, backoffTimer : 0, hasVolunteered : true > < Random : RandomNGen | seed : M > => < O : WSNode | remainingPower : P monus transPower, backoffTimer : INF, status : on > < Random : RandomNGen | seed : random(M) > broadcast from O withDirection randomDirection(M) . --- become active as starting node --- Power on and send out a message when the timer expires rl [nonStartingNodePowerOn] : < O : WSNode | remainingPower : P, backoffTimer : 0, neighbors : NB NBS, hasVolunteered : false > => < O : WSNode | remainingPower : P monus transPower, backoffTimer : INF, status : on > broadcast from O withDirection -1 . --- become active as non-starting node --- Power off if remainingPower : 0 ceq < O : WSNode | status : S, remainingPower : 0 > = < O : WSNode | backoffTimer : INF, roundTimer : INF, status : off, hasVolunteered : false > if S =/= off . --- Power off if O's neighbors completely cover its sensing area crl [recPowerOnMsgAndSwichOff] : (power-onMsgFrom O' to O withDirection D) < O : WSNode | status : undecided, neighbors : NBS, bitmap : BM, remainingPower : P > => < O : WSNode | status : off, neighbors : NBS (O' starting (D >= 0)), bitmap : updateBitmap(O, BM, O'), backoffTimer : INF > if O withinTwiceTheSensingRangeOf O' /\ coverageAreaCovered(updateBitmap(O, BM, O')) . --- Update timer to Ta if O' creates closest uncovered crossing crl [recPowerOnWithUncoveredCrossings] : (power-onMsgFrom O' to O withDirection D) < O : WSNode | remainingPower : P, status : undecided, backoffTimer : T, neighbors : NBS, uncoveredCrossings : CS, bitmap : BM > < Random : RandomNGen | seed : M > => < O : WSNode | backoffTimer : (if O' createsClosestCrossing O (updateUncoveredCrossings(O, O', NBS, CS)) then setTa(O, M, updateUncoveredCrossings(O, O', NBS, CS)) else T fi), neighbors : NBS (O' starting (D >= 0)), uncoveredCrossings : updateUncoveredCrossings(O, O', NBS, CS), bitmap : updateBitmap(O, BM, O') > < Random : RandomNGen | seed : random(M) > if O withinTwiceTheSensingRangeOf O' /\ updateUncoveredCrossings(O, O', NBS, CS) =/= none /\ not coverageAreaCovered(updateBitmap(O, BM, O')) . --- Update timer to Tb if all crossings are covered and --- O' is the closest starting neighbor crl [recPowerOnWithStartingNeighbors] : (power-onMsgFrom O' to O withDirection D) < O : WSNode | remainingPower : P, status : undecided, backoffTimer : T, neighbors : NBS, uncoveredCrossings : CS, bitmap : BM > < Random : RandomNGen | seed : M > => < O : WSNode | backoffTimer : (if O' == findClosestStartingNeighbor(O, NBS (O' starting (D >= 0))) then setTb(O, O', D, NBS (O' starting (D >= 0)), M) else T fi), neighbors : NBS (O' starting (D >= 0)), uncoveredCrossings : none, bitmap : updateBitmap(O, BM, O') > < Random : RandomNGen | seed : random(M) > if O withinTwiceTheSensingRangeOf O' /\ existsStartingNeighbor(NBS (O' starting (D >= 0))) /\ updateUncoveredCrossings(O, O', NBS, CS) == none /\ not coverageAreaCovered(updateBitmap(O, BM, O')) . --- Update timer to TC if all crossings are covered and --- there's no starting neighbor and --- O' is the closest neighbor crl [recPowerOnWithNeighbors] : (power-onMsgFrom O' to O withDirection D) < O : WSNode | remainingPower : P, status : undecided, backoffTimer : T, neighbors : NBS, uncoveredCrossings : CS, bitmap : BM > => < O : WSNode | backoffTimer : (if O' == findClosestNeighbor(O, NBS (O' starting (D >= 0))) then tc else T fi), neighbors : NBS (O' starting (D >= 0)), uncoveredCrossings : none, bitmap : updateBitmap(O, BM, O') > if O withinTwiceTheSensingRangeOf O' /\ not existsStartingNeighbor(NBS (O' starting (D >= 0))) /\ updateUncoveredCrossings(O, O', NBS, CS) == none /\ not coverageAreaCovered(updateBitmap(O, BM, O')) . --- Discard/ignore power-on messages received after powered on crl [discard] : (power-onMsgFrom O' to O withDirection D) < O : WSNode | status : S > => < O : WSNode | > if S =/= undecided or not O withinTwiceTheSensingRangeOf O' . --- Discard/ignore power-on messages if the node is dead eq (power-onMsgFrom O' to O withDirection D) < O : WSNode | status : off, remainingPower : 0 > = < O : WSNode | > . --- Restart the node when the round is over rl [restart] : < O : WSNode | roundTimer : 0, remainingPower : P > => < O : WSNode | status : undecided, neighbors : none, uncoveredCrossings : none, bitmap : initBitmap(O), hasVolunteered : undecided, backoffTimer : INF, roundTimer : roundTime, volunteerProb : 1000 / n > . endtom) ****************************************** ********* REAL TIME BEHAVIOR ************* ****************************************** (tomod OGDC-RTM is protecting OGDC . var O : Oid . vars T T' : Time . vars TI TI' : TimeInf . var P : NzNat . var N : Nat . var R : Rat . var S : Status . var V : VolunteeredStatus . var M : Msg . crl [tick] : {C:Configuration} => {delta(C:Configuration, T)} in time T if T <= mte(C:Configuration) [nonexec] . ---( Delta )--- op delta : Configuration Time -> Configuration [frozen (1)] . eq delta(none, T') = none . eq delta(NEC:NEConfiguration NEC':NEConfiguration, T') = delta(NEC:NEConfiguration, T') delta(NEC':NEConfiguration, T') . eq delta(< O : WSNode | remainingPower : N, status : S, backoffTimer : TI, roundTimer : TI' >, T) = < O : WSNode | remainingPower : if S == on then N monus (idlePower * T) else N monus (sleepPower * T) fi, backoffTimer : TI monus T, roundTimer : TI' monus T > . eq delta(< Random : RandomNGen | >, T') = < Random : RandomNGen | > . eq delta(dly(M, TI), T') = dly(M, TI monus T') . ---( Maximum Time Elapse )--- op mte : Configuration -> TimeInf [frozen (1)] . eq mte(none) = INF . eq mte(NEC:NEConfiguration NEC':NEConfiguration) = min(mte(NEC:NEConfiguration), mte(NEC':NEConfiguration)) . eq mte(< O : WSNode | remainingPower : 0, status : S >) = if S == off then INF else 0 fi . eq mte(< O : WSNode | backoffTimer : TI, roundTimer : T, remainingPower : P, hasVolunteered : true, status : S >) = min(TI, T, if S == on then ceiling(P / powerUnit) else P fi) . eq mte(< O : WSNode | backoffTimer : TI, roundTimer : T, remainingPower : P, hasVolunteered : false, status : S >) = min(TI, T, if S == on then ceiling(P / powerUnit) else P fi) . eq mte(< O : WSNode | hasVolunteered : undecided >) = 0 . eq mte(< Random : RandomNGen | >) = INF . eq mte(dly(M, TI)) = TI . endtom) ****************************************** ********* ANALYSIS *********************** ****************************************** (tomod OGDC-ANALYSIS is protecting OGDC-RTM . including TIMED-MODEL-CHECKER . --- The size of the sensing area in cm (5000 denotes 50mx50m area) eq sensingAreaSize = 5000 . --- The number of nodes in the system eq n = 200 . vars M N N' P : Nat . var NL : NatList . var D : Int . var T : Time . var BIT : Bit . var BITL : BitList . var BM : Bitmap . var LS : LocationSet . var O : Oid . var L : Location . var S : Status . var NB : Neighbor . var NBS : NeighborSet . var SYSTEM : Configuration . var MSG : Msg . ---( Definition of analysis messages )--- --- List of natural numbers sort NatList . subsort Nat < NatList . op nil : -> NatList . op _++_ : NatList NatList -> NatList [ctor assoc id: nil] . --- The analysis messages msg activeNodes : NatList -> Msg . msg coveragePercentage : NatList -> Msg . msg totalRemainingPower : NatList -> Msg . rl [computeActiveNodes] : {activeNodes(NL) SYSTEM} => {dly(activeNodes(NL ++ numActiveNodes(SYSTEM)), roundTime) SYSTEM} . rl [computeSensingCoverage] : {coveragePercentage(NL) SYSTEM} => {dly(coveragePercentage(NL ++ coveragePercentage(SYSTEM)), roundTime) SYSTEM} . rl [computeTotalPower] : {totalRemainingPower(NL) SYSTEM} => {dly(totalRemainingPower(NL ++ calcTotalRemainingPower(SYSTEM)), roundTime) SYSTEM} . --- Compute the number of active nodes in the system op numActiveNodes : Configuration -> Nat [frozen (1)] . op countNodes : Configuration -> Nat [frozen (1)] . --- Compute the percentage of coverage in the system op coveragePercentage : Configuration -> Nat [frozen (1)] . op calcCoveragePercentage : Bitmap Nat Nat -> Nat . --- Compute the total remaining power in the system op calcTotalRemainingPower : Configuration -> Nat [frozen (1)] . eq numActiveNodes(SYSTEM) = countNodes(extractActiveNodes(SYSTEM)) . eq countNodes(none) = 0 . eq countNodes(< O : WSNode | > SYSTEM) = 1 + countNodes(SYSTEM) . eq coveragePercentage(SYSTEM) = calcCoveragePercentage(updateArea(sensingArea, SYSTEM), 0, 0) . eq calcCoveragePercentage(nil, N, M) = ceiling((N * 100) / M) . eq calcCoveragePercentage(| nil | BM, N, M) = calcCoveragePercentage(BM, N, M) . eq calcCoveragePercentage(| BIT BITL | BM, N, M) = if (BIT == f) then calcCoveragePercentage(| BITL | BM, N, M + 1) else calcCoveragePercentage(| BITL | BM, N + 1, M + 1) fi . eq calcTotalRemainingPower(none) = 0 . eq calcTotalRemainingPower(< O : RandomNGen | > SYSTEM) = calcTotalRemainingPower(SYSTEM) . eq calcTotalRemainingPower(MSG SYSTEM) = calcTotalRemainingPower(SYSTEM) . eq calcTotalRemainingPower(< O : WSNode | remainingPower : P > SYSTEM) = P + calcTotalRemainingPower(SYSTEM) . --- Generation of a random generator object and a given number of nodes op genInitConf : Nat Nat -> Configuration . --- seed numNodes op genInitConf : Nat Nat Nat -> Configuration . eq genInitConf(N, N') = genInitConf(N, N', N') . ceq genInitConf(M, s(N), N') = < L : WSNode | remainingPower : lifetime, status : undecided, neighbors : none, bitmap : initBitmap(L), uncoveredCrossings : none, backoffTimer : INF, roundTimer : roundTime, volunteerProb : 1000 / N', hasVolunteered : undecided > (if N == 0 then < Random : RandomNGen | seed : repeatRandom(M, 3) > else genInitConf(repeatRandom(M, 3), N, N') fi) if L := random(M) rem sensingAreaSize - (sensingAreaSize / 2) . random(random(M)) rem sensingAreaSize - (sensingAreaSize / 2) . --- Top left corner of the entire sensing area, which is symetric around (0 . 0) op cornerOfSensingArea : -> Location . eq cornerOfSensingArea = ((- sensingAreaSize / 2) . (sensingAreaSize / 2)) . --- A bitmap of the sensing area of size sensingAreaSize op sensingArea : -> Bitmap . op makeAreaColumns : Nat Nat -> Bitmap . op makeAreaRows : Nat -> BitList . eq sensingArea = makeAreaColumns(sensingAreaSize / 100, sensingAreaSize / 100) . eq makeAreaColumns(N, N') = if N > 0 then | makeAreaRows(N') | makeAreaColumns(N - 1, N') else nil fi . eq makeAreaRows(N) = if N > 0 then f makeAreaRows(N - 1) else nil fi . --- Check if a bitmap is covered by the nodes in the system op _coveredBy_ : Bitmap Configuration -> Bool . --- Update the bits in a bitmap to t if it is within the sensing range --- of an active node in the system op updateArea : Bitmap Configuration -> Bitmap . eq BM coveredBy SYSTEM = coverageAreaCovered(updateArea(BM, SYSTEM)) . eq updateArea(BM, none) = BM . eq updateArea(BM, < O : RandomNGen | > SYSTEM) = updateArea(BM, SYSTEM) . eq updateArea(BM, MSG SYSTEM) = updateArea(BM, SYSTEM) . eq updateArea(BM, < O : WSNode | status : S > SYSTEM) = updateArea((if S == on then updateBitmap(BM, O, cornerOfSensingArea, 100) else BM fi), SYSTEM) . --- Check if the system is in the steady state phase op steadyStatePhase : Configuration -> Bool [frozen (1)] . eq steadyStatePhase(none) = true . eq steadyStatePhase(< O : RandomNGen | > SYSTEM) = steadyStatePhase(SYSTEM) . eq steadyStatePhase(MSG SYSTEM) = steadyStatePhase(SYSTEM) . eq steadyStatePhase(< O : WSNode | status : S > SYSTEM) = (S =/= undecided) and steadyStatePhase(SYSTEM) . --- Extract the active nodes from the system op extractActiveNodes : Configuration -> Configuration [frozen (1)] . eq extractActiveNodes(none) = none . eq extractActiveNodes(< O : RandomNGen | > SYSTEM) = extractActiveNodes(SYSTEM) . eq extractActiveNodes(MSG SYSTEM) = extractActiveNodes(SYSTEM) . eq extractActiveNodes(< O : WSNode | status : S > SYSTEM) = if S == on then < O : WSNode | status : S > else none fi extractActiveNodes(SYSTEM) . op sensor-area-covered : -> Prop [ctor] . eq { SYSTEM } |= sensor-area-covered = coverageAreaCovered(updateArea(sensingArea, SYSTEM)) . op steady-state-phase : -> Prop [ctor] . eq { SYSTEM } |= steady-state-phase = steadyStatePhase(SYSTEM) . endtom) (set tick max def roundTime .) *************************************** ***** ANALYSIS: ***** ***** TEST REWRITES AND SEARCHES ***** *************************************** --- Please notice that the commands take long time to execute --- and that the output can be large with many nodes. Please consider --- fewer nodes and fewer rounds for quick results, and consider --- to pipe the output to file or another program. --- Also don'r forget the parameters on lines 926-929! --- ACTIVE NODES AND COVERAGE VS DEPLOYED NODES, one round: ---(tfrew {genInitConf(1, 400) dly(activeNodes(nil),roundTime - 1) dly(coveragePercentage(nil),roundTime - 1)} in time < roundTime .) --- On Intel 3.6 GHz Xeon: --- 200 nodes: res: (for n=200) 32, in 180 seconds, 85-->151MB mem --- 400 nodes: res: (for n=400) 38, in 1243 sec, 100MB most of time, 231 --- 600 nodes: res: (for n=600) 45, in 5034 s, 112MB memory most of time --- COVERAGE AND POWER VS TIME, 50 rounds: ---(tfrew {genInitConf(313, 200) dly(coveragePercentage(nil),roundTime - 1) dly(totalRemainingPower(nil),roundTime - 1)} in time < roundTime * 50 .) --- On 'buri', Intel Xeon 3.6GHz: --- 200 nodes in 50X50: 4931 sec, 90MB most of time --- ALPHA LIFETIME VS DEPLOYED NODES --- Note that these take long to execute. Use e.g. 20 nodes and 5 rounds --- for fairly quick results. ---(tfrew {genInitConf(1, 64) dly(coveragePercentage(nil), roundTime - 1) } in time <= roundTime * 200 .) ---(tfrew {genInitConf(45, 80) dly(coveragePercentage(nil), roundTime - 1) } in time <= roundTime * 200 .) ---(tfrew {genInitConf(35, 20) dly(coveragePercentage(nil), roundTime - 1) } in time <= roundTime * 200 .) ---(tfrew {genInitConf(8921, 125) dly(coveragePercentage(nil), roundTime - 1) } in time <= roundTime * 200 .) --- STEADY STATE PHASE ---(find latest {genInitConf(75, 6)} =>* { C:Configuration } such that steadyStatePhase(C:Configuration) in time <= roundTime .) --- result: {...} in time 372, 4187sec, 525MB ---(find earliest {genInitConf(791, 5)} =>* { C:Configuration } such that steadyStatePhase(C:Configuration) .) ---(mc {genInitConf(341,5)} |=t (steady-state-phase => [] steady-state-phase) in time < roundTime .) --- 26 seconds using 147MB --- STEADY STATE PHASE AND COVERAGE ---(mc {genInitConf(95,5)} |=t [] (steady-state-phase -> sensor-area-covered) in time <= roundTime .) ---(mc {genInitConf(5,5)} |=t [] (steady-state-phase -> sensor-area-covered) in time < roundTime * 5 .) ---(tsearch [1] {genInitConf(7197,5)} =>* {C:Configuration} such that steadyStatePhase(C:Configuration) /\ not coverageAreaCovered(updateArea(sensingArea, C:Configuration)) in time < roundTime .) --- for area 20x20: for seed 7197, everything should be covered by 5 nodes --- for seed 1, even 8 nodes cannot cover ... --- crashes both for 7 and 8 nodes --- try 6: ---(tsearch [1] {genInitConf(1,6)} =>* {C:Configuration} such that steadyStatePhase(C:Configuration) /\ not coverageAreaCovered(updateArea(sensingArea, C:Configuration)) in time < roundTime .) --- finds state in 679 sec using 1.3GB memory ---(tsearch [1] {genInitConf(7197,5)} =>* {C:Configuration} such that steadyStatePhase(C:Configuration) /\ not coverageAreaCovered(updateArea(sensingArea, C:Configuration)) in time < roundTime .) --- 'No solution' in 227 sec using 430 MB of memory ---(tsearch [1] {genInitConf(1,5)} =>* { < O:Oid : WSNode | status : on, bitmap : BM:Bitmap, ATTS:AttributeSet > C:Configuration } such that BM:Bitmap coveredBy C:Configuration in time <= roundTime .) ---q