--- This version uses Maude's built-in random function instead of my --- random function --- remember to set initial seed value: --- maude -random-seed=313 ogdcNewRandom.rtmaude --- Real-Time Maude 2.2/2.3 specification of the OGDC algorithm. --- October 28, 2007. --- Change since Oct 27: --- minor change is function that selects the random initial --- location of a node, so that rightmost edge can be covered --- powerOn is now a message content. --- First: load real-time-maude. You may need to also take the directory --- into account: --- load ../../../../Maude23/real-time-maude 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. Also set later. op noOfNodes : -> Nat . --- Size of sensor area in meters. Set later according --- to desired area. Typically 50 meters, but could be less --- when simulating or model checking with fewer nodes. op sensingAreaSize : -> Nat . --- Round time in ms. One round is supposed to be thousand seconds: 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. The weird names of these constants --- come from the description of OGDC. op tc : -> Time . eq tc = 200 . --- Sensing range in centimeters. 10 meters. op sensingRange : -> Nat . eq sensingRange = 1000 . --- Transmission range in centimeters. op transmissionRange : -> Nat . eq transmissionRange = 2 * sensingRange . --- Transmission time in ms (originally 6.8). We use 7 just to --- avoid having to display rational numbers. It is of course --- equally easy to use rational numbers time domain. Indeed, we have --- done that in previous versions. 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 --- We scale up by 400 so that ... one ms of sleep takes --- 1 power entity. --- One power unit is the amount of power needed --- to stay idle for one millisecond: op powerUnit : -> Nat . eq powerUnit = 400 . op idlePower : -> Nat . eq idlePower = powerUnit . --- Power required to sleep one millisecond op sleepPower : -> Nat . eq sleepPower = 1 . --- Power required to transmit one power-on message. Or ... --- should this be four instead of five? Does this come IN ADDITION --- to the power required to stay idle? op transPower : -> Nat . eq transPower = powerUnit * 5 * transmissionDelay . --- Startup power, lifetime op lifetime : -> Nat . eq lifetime = 5000000 * powerUnit . --- Power threshold - minimum power required to volunteer--- op powerThreshold : -> Nat . eq powerThreshold = 900000 * powerUnit . endom) ****( BASIC SORTS AND FUNCTIONS )**** (omod OGDC-SORTS is including OGDC-PARAMETERS . --- Sorts with self-explaining names: 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 Location -> 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 [ctor] . --- 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 : Rat . --- Notice that origo is in the CENTER of the sensing area! ceq isInSensingArea(X . Y) = (abs(X) <= SASIZE) and (abs(Y) <= SASIZE) if SASIZE := sensingAreaSize / 2 . --- Sufficient to compare SQUARES of lengths to avoid sq root operations: 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) . --- All these owise definistions are new! eq (L ; LS) minus (L ; LS') = LS minus (L ; LS') . eq LS minus LS' = LS [owise] . eq remove((L ; LS), L) = remove(LS, L) . eq remove(LS, L) = LS [owise] . 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 to be one meter: 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 BM' : Bitmap . vars BITL 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 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 )**** --- We try my own random number generator, that existed before Maude --- got it's built-in random number generator. (omod RANDOM-OBJECT is protecting RANDOM . --- random(n) returns the nth random number! class RandomNGen | index : Nat . endom) ****( BACKOFF TIMER COMPUTATIONS )**** --- Computes the various back-off timer values given in the description --- of OGDC. The names of the various function typically correspond --- to the names in that paper. (omod OGDC-TC is protecting OGDC-COVERAGE-OPERATIONS . protecting RANDOM-OBJECT . 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 eq angle(L, L) = 0 . --- the 'vector' is just a point 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)) [owise] . 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] . --- NEW: sort MsgCont . op powerOnWithDirection_ : Int -> MsgCont [ctor] . msg broadcast_from_ : MsgCont Location -> Msg . msg msg_from_to_ : MsgCont Location Location -> 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 : Location MsgCont 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 . vars L 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 . var OBJECT : Object . var MC : MsgCont . --- Message broadcasting eq {< L : WSNode | > (broadcast MC from L) C} = {< L : WSNode | > distributeMsg(L, MC, C)} . --- Break down the broadcast message to single messages for nodes which --- are within transmission range eq distributeMsg(L, MC, none) = none . eq distributeMsg(L, MC, MSG C) = MSG distributeMsg(L, MC, C) . eq distributeMsg(L, MC, OBJECT C) = OBJECT distributeMsg(L, MC, C) [owise] . eq distributeMsg(L, MC, < L' : WSNode | > C) = < L' : WSNode | > distributeMsg(L, MC, C) (if L withinTransmissionRangeOf L' then dly((msg MC from L to L'), transmissionDelay) else none fi) . *** Although very tempting, IN THEORY, the first three equations above *** CANNOT be replaced by the equation below, since the state *** {O broadcast(O) distribute(O to O1 O2 O3 ...)} *** COULD reduce to *** {O distribute(O to distribute(O to O1 O2 O3...))}, which *** with the below equation could be {O distrubute(O to O1 O2 O3 ...)}, *** so that the equations would not be confluent. Of course, due to the *** fact that equations are always reduced before rules are applied, *** we would operationally never reach such a state in the first place. *** But, given that we want have also a theoretically perfect model, *** we do not do this even simpler spec. *** eq distributeMsg(O, D, C) = C [owise] . 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 | index : M > => (if (randomProb(M) < R) and (P > powerThreshold or R == 1000) then < O : WSNode | backoffTimer : randomTimer(M + 1), hasVolunteered : true > else < O : WSNode | backoffTimer : nonVolunteerTimer, hasVolunteered : false, volunteerProb : doubleProb(R) > fi) < Random : RandomNGen | index : M + 2 > . --- 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 | index : M > => (if (randomProb(M) < R) and (P > powerThreshold or R == 1000) then < O : WSNode | backoffTimer : randomTimer(M + 1), hasVolunteered : true > else < O : WSNode | backoffTimer : nonVolunteerTimer, volunteerProb : doubleProb(R) > fi) < Random : RandomNGen | index : M + 2 > . --- Power on and send out a message when the timer expires rl [startingNodePowerOn] : < O : WSNode | remainingPower : P, backoffTimer : 0, hasVolunteered : true > < Random : RandomNGen | index : M > => < O : WSNode | remainingPower : P monus transPower, backoffTimer : INF, status : on > < Random : RandomNGen | index : M + 1 > broadcast (powerOnWithDirection randomDirection(M)) from O . --- 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 (powerOnWithDirection -1) from O . --- 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] : (msg (powerOnWithDirection D) from O' to O) < 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] : (msg (powerOnWithDirection D) from O' to O) < O : WSNode | remainingPower : P, status : undecided, backoffTimer : T, neighbors : NBS, uncoveredCrossings : CS, bitmap : BM > < Random : RandomNGen | index : 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 | index : M + 1 > 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] : (msg (powerOnWithDirection D) from O' to O) < O : WSNode | remainingPower : P, status : undecided, backoffTimer : T, neighbors : NBS, uncoveredCrossings : CS, bitmap : BM > < Random : RandomNGen | index : 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 | index : M + 1 > 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] : (msg (powerOnWithDirection D) from O' to O) < 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] : (msg (powerOnWithDirection D) from O' to O) < O : WSNode | status : S > => < O : WSNode | > if S =/= undecided or not O withinTwiceTheSensingRangeOf O' . --- 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 / noOfNodes > . endtom) ****************************************** ********* REAL TIME BEHAVIOR ************* ****************************************** --- Follows the usual guidelines for OO RTS specification given --- in "Semantics and Pragmatics of Real-Time Maude" (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 =/= off 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 = 2500 . --- The number of nodes in the system eq noOfNodes = 75 . vars M N N' P : Nat . var NL : NatList . var D : Int . var T : Time . var TI : TimeInf . 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 . var OBJECT : Object . ---( Definition of "observer objects" used to compute certain metrics during a simulation )--- --- List of natural numbers sort NatList . subsort Nat < NatList . op nil : -> NatList . op _++_ : NatList NatList -> NatList [ctor assoc id: nil] . --- The record classes: class ObserverObject | timer : TimeInf . class ObserveActiveNodes | activeNodes : NatList . subclass ObserveActiveNodes < ObserverObject . class ObserveCoveragePercentage | coveragePercentage : NatList . subclass ObserveCoveragePercentage < ObserverObject . class ObserveRemainingPower | totalRemainingPower : NatList . subclass ObserveRemainingPower < ObserverObject . --- oid's for these guys: ops o1 o2 o3 : -> Oid [ctor] . --- time definitions for the recording objects: eq delta(< O : ObserverObject | timer : TI >, T) = < O : ObserverObject | timer : TI monus T > . eq mte(< O : ObserverObject | timer : TI >) = TI . rl [computeActiveNodes] : {< O : ObserveActiveNodes | activeNodes : NL, timer : 0 > SYSTEM} => {< O : ObserveActiveNodes | activeNodes : NL ++ numActiveNodes(SYSTEM), timer : roundTime > SYSTEM} . rl [computeSensingCoverage] : {< O : ObserveCoveragePercentage | coveragePercentage : NL, timer : 0 > SYSTEM} => {< O : ObserveCoveragePercentage | coveragePercentage : NL ++ coveragePercentage(SYSTEM), timer : roundTime > SYSTEM} . rl [computeTotalPower] : {< O : ObserveRemainingPower | totalRemainingPower : NL, timer : 0 > SYSTEM} => {< O : ObserveRemainingPower | totalRemainingPower : NL ++ calcTotalRemainingPower(SYSTEM), timer : 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 . --- Quick and almost clean. Not really confluent wrt --- distributeMsg, but that will never cause a problem, --- so we take the luxury of using this dirty version: eq calcTotalRemainingPower(< O : WSNode | remainingPower : P > SYSTEM) = P + calcTotalRemainingPower(SYSTEM) . eq calcTotalRemainingPower(SYSTEM) = 0 [owise] . --- Generation of a random generator object and a given number of nodes op genInitConf : Nat Nat -> Configuration . --- numOfNodes seed op genInitConf : Nat Nat Nat -> Configuration . eq genInitConf(N, N') = genInitConf(N, N', N) . ceq genInitConf(s(M), 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 M == 0 then < Random : RandomNGen | index : N + 2 > else genInitConf(M, N + 2, N') fi) if L := randomLocation(N) . op randomLocation : Nat -> Location . eq randomLocation(N) = (((random(N) rem (sensingAreaSize + 1)) - (sensingAreaSize / 2)) . ((random(N + 1) rem (sensingAreaSize + 1)) - (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, < O : WSNode | status : on > SYSTEM) = updateArea(updateBitmap(BM, O, cornerOfSensingArea, 100), SYSTEM) . eq updateArea(BM, SYSTEM) = BM [owise] . --- Check if the system is in the steady state phase op steadyStatePhase : Configuration -> Bool [frozen (1)] . eq steadyStatePhase(none) = true . eq steadyStatePhase(MSG SYSTEM) = steadyStatePhase(SYSTEM) . eq steadyStatePhase(< O : WSNode | status : S > SYSTEM) = (S =/= undecided) and steadyStatePhase(SYSTEM) . eq steadyStatePhase(OBJECT SYSTEM) = steadyStatePhase(SYSTEM) [owise] . --- Extract the active nodes from the system op extractActiveNodes : Configuration -> Configuration [frozen (1)] . eq extractActiveNodes(none) = none . 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) . eq extractActiveNodes(OBJECT SYSTEM) = extractActiveNodes(SYSTEM) [owise] . 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) *** Time sampling strategy: (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 sensingAreaSize (to 5000 for 50m x 50m) --- and noOfNodes, to the total number of sensor nodes, on lines around 1000 --- ACTIVE NODES AND COVERAGE VS DEPLOYED NODES, one round: ---(tfrew {genInitConf(600, 1) < o1 : ObserveActiveNodes | activeNodes : nil, timer : roundTime - 1 > < o2 : ObserveCoveragePercentage | coveragePercentage : nil, timer : 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(75, 1) < o1 : ObserveCoveragePercentage | coveragePercentage : nil, timer : roundTime - 1 > < o2 : ObserveRemainingPower | totalRemainingPower : nil, timer : roundTime - 1 >} in time < roundTime * 50 .) q --- 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 --- --------------------------------------------------- --- Simulation results and performance --- --------------------------------------------------- ***( Simulation, Real-Time Maude 2.3: * original version: + 200 nodes: -- seed=1 : -- seed=5 :