\||||||||||||||||||/
		   --- Welcome to Maude ---
		     /||||||||||||||||||\
	    Maude 2.3 built: Feb 14 2007 17:53:50
	    Copyright 1997-2007 SRI International
		   Fri Nov  2 00:13:39 2007

	     Full Maude 2.3 `(February 12th`, 2007`)

	  Real-Time Maude 2.3 extension May 2, 2007

rewrites: 17948 in 50ms cpu (50ms real) (351969 rewrites/second)
Introduced module OGDC-PARAMETERS

rewrites: 17795 in 41ms cpu (42ms real) (423751 rewrites/second)
Introduced module OGDC-SORTS

rewrites: 24048 in 51ms cpu (51ms real) (462532 rewrites/second)
Introduced module OGDC-BITMAP

rewrites: 40702 in 85ms cpu (86ms real) (473350 rewrites/second)
Introduced module OGDC-COVERAGE-OPERATIONS

rewrites: 2898 in 8ms cpu (9ms real) (322071 rewrites/second)
Introduced module OUR-RANDOM

rewrites: 33626 in 76ms cpu (76ms real) (436769 rewrites/second)
Introduced module OGDC-TC

rewrites: 29063 in 46ms cpu (45ms real) (618453 rewrites/second)

Introduced timed module: OGDC-NODE-AND-MESSAGE-DEFINITIONS

rewrites: 72482 in 152ms cpu (154ms real) (473809 rewrites/second)

Introduced timed module: OGDC

rewrites: 51143 in 110ms cpu (111ms real) (460818 rewrites/second)

Introduced timed module: OGDC-RTM

rewrites: 86055 in 175ms cpu (175ms real) (489023 rewrites/second)

Introduced timed module: OGDC-ANALYSIS

rewrites: 280 in 17ms cpu (16ms real) (15558 rewrites/second)

Tick mode set to maximal time increase mode with default for INF

rewrites: 198262196 in 272744ms cpu (274231ms real) (726915 rewrites/second)

Find earliest {C:Configuration} in OGDC-ANALYSIS such that 
	{genInitConf(5,1)} =>* {C:Configuration} 
with mode maximal time increase with default roundTime :

Result:	{dly(msg powerOnWithDirection -1 from 814 . -857 to -996 . -755,7)dly(
    msg powerOnWithDirection -1 from 814 . -857 to -1039 . -225,7)dly(msg
    powerOnWithDirection -1 from 814 . -857 to 948 . -150,7)< Random :
    RandomNGen | seed : 5894 > < -728 . 659 : WSNode | backoffTimer : INF,
    bitmap :(
| ' ' ' ' ' ' ' ' ' ' ' ' ' ' ' ' ' ' ' ' ' | 
| ' ' ' ' ' ' ' ' ' ' ' ' ' ' ' ' ' ' ' ' ' | 
| ' ' ' ' ' ' ' ' ' ' ' ' ' ' ' ' ' ' ' ' ' | 
| ' ' ' ' ' ' ' ' ' ' ' ' ' ' ' ' ' ' ' ' ' | 
| ' ' ' ' ' ' ' ' ' ' ' ' ' ' ' ' ' ' ' ' ' | 
| ' ' ' ' ' f f f f f f f f f f f f f f ' ' | 
| ' ' ' ' ' f f f f f f f f f f f f f f f ' | 
| ' ' ' ' ' f f f f f f f f f f f f f f f ' | 
| ' ' ' ' ' f f f f f f f f f f f f f f f ' | 
| ' ' ' ' ' f f f f f f f f f f f f f f f ' | 
| ' ' ' ' ' f f f f f f f f f f f f f f f f | 
| ' ' ' ' ' f f f f f f f f f f f f f f f ' | 
| ' ' ' ' ' f f f f f f f f f f f f f f f ' | 
| ' ' ' ' ' f f f f f f f f f f f f f f f ' | 
| ' ' ' ' ' f f f f f f f f f f f f f f f ' | 
| ' ' ' ' ' f f f f f f f f f f f f f f ' ' | 
| ' ' ' ' ' f f f f f f f f f f f f f f ' ' | 
| ' ' ' ' ' f f f f f f f f f f f f f ' ' ' | 
| ' ' ' ' ' f f f f f f f f f f f f ' ' ' ' | 
| ' ' ' ' ' ' f f f f f f f f f ' ' ' ' ' ' | 
| ' ' ' ' ' ' ' ' ' ' f ' ' ' ' ' ' ' ' ' ' |),hasVolunteered : true,neighbors
    : none,remainingPower : 1999911600,roundTimer : 999814,status : on,
    uncoveredCrossings : none,volunteerProb : 200 > < -996 . -755 : WSNode |
    backoffTimer : INF,bitmap :(
| ' ' ' ' ' ' ' ' ' ' t ' ' ' ' ' ' ' ' ' ' | 
| ' ' ' ' ' ' ' ' t t t t t t t ' ' ' ' ' ' | 
| ' ' ' ' ' ' ' ' t t t t t t t t t ' ' ' ' | 
| ' ' ' ' ' ' ' ' t t t t t t t t t t ' ' ' | 
| ' ' ' ' ' ' ' ' t t t t t t t t t t t ' ' | 
| ' ' ' ' ' ' ' ' t t t t t t t t t t t ' ' | 
| ' ' ' ' ' ' ' ' t t t t t t t t t t t t ' | 
| ' ' ' ' ' ' ' ' t t t t t t t t t t t t ' | 
| ' ' ' ' ' ' ' ' t t t t t t t t t t t t ' | 
| ' ' ' ' ' ' ' ' t t t t t t t t t t t f ' | 
| ' ' ' ' ' ' ' ' t t t t t t t t t t t f f | 
| ' ' ' ' ' ' ' ' t t t t t t t t t t f f ' | 
| ' ' ' ' ' ' ' ' t t t t t t t t t f f f ' | 
| ' ' ' ' ' ' ' ' t t t t t t t t f f f f ' | 
| ' ' ' ' ' ' ' ' t t t t t t f f f f f f ' | 
| ' ' ' ' ' ' ' ' ' ' ' ' ' ' ' ' ' ' ' ' ' | 
| ' ' ' ' ' ' ' ' ' ' ' ' ' ' ' ' ' ' ' ' ' | 
| ' ' ' ' ' ' ' ' ' ' ' ' ' ' ' ' ' ' ' ' ' | 
| ' ' ' ' ' ' ' ' ' ' ' ' ' ' ' ' ' ' ' ' ' | 
| ' ' ' ' ' ' ' ' ' ' ' ' ' ' ' ' ' ' ' ' ' | 
| ' ' ' ' ' ' ' ' ' ' ' ' ' ' ' ' ' ' ' ' ' |),hasVolunteered : false,neighbors
    :((-728 . 659 starting true)-1039 . -225 starting false),remainingPower :
    1999911600,roundTimer : 999814,status : on,uncoveredCrossings : none,
    volunteerProb : 400 > < -1039 . -225 : WSNode | backoffTimer : INF,bitmap
    :(
| ' ' ' ' ' ' ' ' ' ' t ' ' ' ' ' ' ' ' ' ' | 
| ' ' ' ' ' ' ' ' t t t t t t t ' ' ' ' ' ' | 
| ' ' ' ' ' ' ' ' t t t t t t t t t ' ' ' ' | 
| ' ' ' ' ' ' ' ' t t t t t t t t t t ' ' ' | 
| ' ' ' ' ' ' ' ' t t t t t t t t t t t ' ' | 
| ' ' ' ' ' ' ' ' t t t t t t t t t t t ' ' | 
| ' ' ' ' ' ' ' ' t t t t t t t t t t t t ' | 
| ' ' ' ' ' ' ' ' t t t t t t t t t t t t ' | 
| ' ' ' ' ' ' ' ' t t t t t t t t t t t t ' | 
| ' ' ' ' ' ' ' ' t t t t t t t t t t t t ' | 
| ' ' ' ' ' ' ' ' f t t t t t t t t t f f t | 
| ' ' ' ' ' ' ' ' f f f f t t t f f f f f ' | 
| ' ' ' ' ' ' ' ' f f f f f f f f f f f f ' | 
| ' ' ' ' ' ' ' ' f f f f f f f f f f f f ' | 
| ' ' ' ' ' ' ' ' f f f f f f f f f f f f ' | 
| ' ' ' ' ' ' ' ' f f f f f f f f f f f ' ' | 
| ' ' ' ' ' ' ' ' f f f f f f f f f f f ' ' | 
| ' ' ' ' ' ' ' ' f f f f f f f f f f ' ' ' | 
| ' ' ' ' ' ' ' ' f f f f f f f f f ' ' ' ' | 
| ' ' ' ' ' ' ' ' f f f f f f f ' ' ' ' ' ' | 
| ' ' ' ' ' ' ' ' ' ' f ' ' ' ' ' ' ' ' ' ' |),hasVolunteered : false,neighbors
    :((-728 . 659 starting true)948 . -150 starting true),remainingPower :
    1999911600,roundTimer : 999814,status : on,uncoveredCrossings : none,
    volunteerProb : 400 > < 814 . -857 : WSNode | backoffTimer : INF,bitmap :(
| ' ' ' ' ' ' ' ' ' ' t ' ' ' ' ' ' ' ' ' ' | 
| ' ' ' ' ' ' t t t t t t t t t ' ' ' ' ' ' | 
| ' ' ' ' t t t t t t t t t t t ' ' ' ' ' ' | 
| ' ' ' t t t t t t t t t t t t ' ' ' ' ' ' | 
| ' ' t t t t t t t t t t t t t ' ' ' ' ' ' | 
| ' ' t t t t t t t t t t t t t ' ' ' ' ' ' | 
| ' t t t t t t t t t t t t t t ' ' ' ' ' ' | 
| ' t f t t t t t t t t t t t t ' ' ' ' ' ' | 
| ' t f t t t t t t t t t t t t ' ' ' ' ' ' | 
| ' t f f t t t t t t t t t t t ' ' ' ' ' ' | 
| t t f f f t t t t t t t t t t ' ' ' ' ' ' | 
| ' t f f f f t t t t t t t t t ' ' ' ' ' ' | 
| ' t f f f f f f t t t t t t t ' ' ' ' ' ' | 
| ' t f f f f f f f f f f f f f ' ' ' ' ' ' | 
| ' ' ' ' ' ' ' ' ' ' ' ' ' ' ' ' ' ' ' ' ' | 
| ' ' ' ' ' ' ' ' ' ' ' ' ' ' ' ' ' ' ' ' ' | 
| ' ' ' ' ' ' ' ' ' ' ' ' ' ' ' ' ' ' ' ' ' | 
| ' ' ' ' ' ' ' ' ' ' ' ' ' ' ' ' ' ' ' ' ' | 
| ' ' ' ' ' ' ' ' ' ' ' ' ' ' ' ' ' ' ' ' ' | 
| ' ' ' ' ' ' ' ' ' ' ' ' ' ' ' ' ' ' ' ' ' | 
| ' ' ' ' ' ' ' ' ' ' ' ' ' ' ' ' ' ' ' ' ' |),hasVolunteered : false,neighbors
    :((-996 . -755 starting false)(-1039 . -225 starting false)948 . -150
    starting true),remainingPower : 1999911600,roundTimer : 999814,status : on,
    uncoveredCrossings : -996 . -755 x -1039 . -225 in -56 . -412,volunteerProb
    : 400 > < 948 . -150 : WSNode | backoffTimer : INF,bitmap :(
| ' ' ' ' ' ' ' ' ' ' f ' ' ' ' ' ' ' ' ' ' | 
| ' ' ' ' ' ' f f f f f f f f ' ' ' ' ' ' ' | 
| ' ' ' ' f f f f f f f f f f ' ' ' ' ' ' ' | 
| ' ' ' f f f f f f f f f f f ' ' ' ' ' ' ' | 
| ' ' f f f f f f f f f f f f ' ' ' ' ' ' ' | 
| ' ' f f f f f f f f f f f f ' ' ' ' ' ' ' | 
| ' f f f f f f f f f f f f f ' ' ' ' ' ' ' | 
| ' f f f f f f f f f f f f f ' ' ' ' ' ' ' | 
| ' f f f f f f f f f f f f f ' ' ' ' ' ' ' | 
| ' f f f f f f f f f f f f f ' ' ' ' ' ' ' | 
| f f f f f f f f f f f f f f ' ' ' ' ' ' ' | 
| ' f f f f f f f f f f f f f ' ' ' ' ' ' ' | 
| ' f f f f f f f f f f f f f ' ' ' ' ' ' ' | 
| ' f f f f f f f f f f f f f ' ' ' ' ' ' ' | 
| ' f f f f f f f f f f f f f ' ' ' ' ' ' ' | 
| ' ' f f f f f f f f f f f f ' ' ' ' ' ' ' | 
| ' ' f f f f f f f f f f f f ' ' ' ' ' ' ' | 
| ' ' ' f f f f f f f f f f f ' ' ' ' ' ' ' | 
| ' ' ' ' f f f f f f f f f f ' ' ' ' ' ' ' | 
| ' ' ' ' ' ' f f f f f f f f ' ' ' ' ' ' ' | 
| ' ' ' ' ' ' ' ' ' ' f ' ' ' ' ' ' ' ' ' ' |),hasVolunteered : true,neighbors
    : none,remainingPower : 1999911600,roundTimer : 999814,status : on,
    uncoveredCrossings : none,volunteerProb : 200 >} in time 186

rewrites: 22493733 in 65739ms cpu (66127ms real) (342167 rewrites/second)

Find latest {C:Configuration} in OGDC-ANALYSIS such that
	{genInitConf(5,1)} =>* {C:Configuration} 
in time <= roundTime with mode maximal time increase with default roundTime :

Result:	{dly(msg powerOnWithDirection -1 from 948 . -150 to -728 . 659,7)dly(
    msg powerOnWithDirection -1 from 948 . -150 to -1039 . -225,7)dly(msg
    powerOnWithDirection -1 from 948 . -150 to 814 . -857,7)< Random :
    RandomNGen | seed : 5894 > < -728 . 659 : WSNode | backoffTimer : INF,
    bitmap :(
| ' ' ' ' ' ' ' ' ' ' ' ' ' ' ' ' ' ' ' ' ' | 
| ' ' ' ' ' ' ' ' ' ' ' ' ' ' ' ' ' ' ' ' ' | 
| ' ' ' ' ' ' ' ' ' ' ' ' ' ' ' ' ' ' ' ' ' | 
| ' ' ' ' ' ' ' ' ' ' ' ' ' ' ' ' ' ' ' ' ' | 
| ' ' ' ' ' ' ' ' ' ' ' ' ' ' ' ' ' ' ' ' ' | 
| ' ' ' ' ' f f f f f f f f f f f f f f ' ' | 
| ' ' ' ' ' f f f f f f f f f f f f f f f ' | 
| ' ' ' ' ' f f f f f f f f f f f f f f f ' | 
| ' ' ' ' ' f f f f f f f f f f f f f f f ' | 
| ' ' ' ' ' f f f f f f f f f f f f f f f ' | 
| ' ' ' ' ' f f f f f f f f f f f f f f f f | 
| ' ' ' ' ' f f f f f f f f f f f f f f f ' | 
| ' ' ' ' ' f f f f f f f f f f f f f f f ' | 
| ' ' ' ' ' f f f f f f f f f f f f f f f ' | 
| ' ' ' ' ' f f f f f f f f f f f f f f f ' | 
| ' ' ' ' ' f f f f f f f f f f f f f f ' ' | 
| ' ' ' ' ' f f f f f f f f f f f f f f ' ' | 
| ' ' ' ' ' f f f f f f f f f f f f f ' ' ' | 
| ' ' ' ' ' f f f f f f f f f f f f ' ' ' ' | 
| ' ' ' ' ' ' f f f f f f f f f ' ' ' ' ' ' | 
| ' ' ' ' ' ' ' ' ' ' f ' ' ' ' ' ' ' ' ' ' |),hasVolunteered : true,neighbors
    : none,remainingPower : 1999115200,roundTimer : 997823,status : on,
    uncoveredCrossings : none,volunteerProb : 200 > < -996 . -755 : WSNode |
    backoffTimer : INF,bitmap :(
| ' ' ' ' ' ' ' ' ' ' f ' ' ' ' ' ' ' ' ' ' | 
| ' ' ' ' ' ' ' ' f f f f f f f ' ' ' ' ' ' | 
| ' ' ' ' ' ' ' ' f f f f f f f f f ' ' ' ' | 
| ' ' ' ' ' ' ' ' f f f f f f f f f f ' ' ' | 
| ' ' ' ' ' ' ' ' f f f f f f f f f f f ' ' | 
| ' ' ' ' ' ' ' ' f f f f f f f f f f f ' ' | 
| ' ' ' ' ' ' ' ' f f f f f f f f f f f f ' | 
| ' ' ' ' ' ' ' ' f f f f f f f f f f f f ' | 
| ' ' ' ' ' ' ' ' f f f f f f f f f f f f ' | 
| ' ' ' ' ' ' ' ' f f f f f f f f f f f f ' | 
| ' ' ' ' ' ' ' ' f f f f f f f f f f f f f | 
| ' ' ' ' ' ' ' ' f f f f f f f f f f f f ' | 
| ' ' ' ' ' ' ' ' f f f f f f f f f f f f ' | 
| ' ' ' ' ' ' ' ' f f f f f f f f f f f f ' | 
| ' ' ' ' ' ' ' ' f f f f f f f f f f f f ' | 
| ' ' ' ' ' ' ' ' ' ' ' ' ' ' ' ' ' ' ' ' ' | 
| ' ' ' ' ' ' ' ' ' ' ' ' ' ' ' ' ' ' ' ' ' | 
| ' ' ' ' ' ' ' ' ' ' ' ' ' ' ' ' ' ' ' ' ' | 
| ' ' ' ' ' ' ' ' ' ' ' ' ' ' ' ' ' ' ' ' ' | 
| ' ' ' ' ' ' ' ' ' ' ' ' ' ' ' ' ' ' ' ' ' | 
| ' ' ' ' ' ' ' ' ' ' ' ' ' ' ' ' ' ' ' ' ' |),hasVolunteered : true,neighbors
    : none,remainingPower : 1999115200,roundTimer : 997823,status : on,
    uncoveredCrossings : none,volunteerProb : 200 > < -1039 . -225 : WSNode |
    backoffTimer : INF,bitmap :(
| ' ' ' ' ' ' ' ' ' ' t ' ' ' ' ' ' ' ' ' ' | 
| ' ' ' ' ' ' ' ' t t t t t t t ' ' ' ' ' ' | 
| ' ' ' ' ' ' ' ' t t t t t t t t t ' ' ' ' | 
| ' ' ' ' ' ' ' ' t t t t t t t t t t ' ' ' | 
| ' ' ' ' ' ' ' ' t t t t t t t t t t t ' ' | 
| ' ' ' ' ' ' ' ' t t t t t t t t t t t ' ' | 
| ' ' ' ' ' ' ' ' t t t t t t t t t t t t ' | 
| ' ' ' ' ' ' ' ' t t t t t t t t t t t t ' | 
| ' ' ' ' ' ' ' ' t t t t t t t t t t t t ' | 
| ' ' ' ' ' ' ' ' t t t t t t t t t t t t ' | 
| ' ' ' ' ' ' ' ' t t t t t t t t t t t f f | 
| ' ' ' ' ' ' ' ' t t t t t t t t t t t t ' | 
| ' ' ' ' ' ' ' ' t t t t t t t t t t t t ' | 
| ' ' ' ' ' ' ' ' t t t t t t t t t t t t ' | 
| ' ' ' ' ' ' ' ' t t t t t t t t t t t t ' | 
| ' ' ' ' ' ' ' ' t t t t t t t t t t t ' ' | 
| ' ' ' ' ' ' ' ' t t t t t t t t t t t ' ' | 
| ' ' ' ' ' ' ' ' t t t t t t t t t t ' ' ' | 
| ' ' ' ' ' ' ' ' t t t t t t t t t ' ' ' ' | 
| ' ' ' ' ' ' ' ' t t t t t t t ' ' ' ' ' ' | 
| ' ' ' ' ' ' ' ' ' ' t ' ' ' ' ' ' ' ' ' ' |),hasVolunteered : false,neighbors
    :((-728 . 659 starting true)(-996 . -755 starting true)814 . -857 starting
    false),remainingPower : 1999115200,roundTimer : 997823,status : on,
    uncoveredCrossings :((-728 . 659 x -996 . -755 in -181 . -177)(-728 . 659 x
    -996 . -755 in -1547 . 82)814 . -857 x -996 . -755 in -67 . -384),
    volunteerProb : 400 > < 814 . -857 : WSNode | backoffTimer : INF,bitmap :(
| ' ' ' ' ' ' ' ' ' ' f ' ' ' ' ' ' ' ' ' ' | 
| ' ' ' ' ' ' f f f f f f f f f ' ' ' ' ' ' | 
| ' ' ' ' f f f f f f f f f f f ' ' ' ' ' ' | 
| ' ' ' f f f f f f f f f f f f ' ' ' ' ' ' | 
| ' ' f f f f f f f f f f f f f ' ' ' ' ' ' | 
| ' ' f f f f f f f f f f f f f ' ' ' ' ' ' | 
| ' t f f f f f f f f f f f f f ' ' ' ' ' ' | 
| ' t f f f f f f f f f f f f f ' ' ' ' ' ' | 
| ' t f f f f f f f f f f f f f ' ' ' ' ' ' | 
| ' t f f f f f f f f f f f f f ' ' ' ' ' ' | 
| t t f f f f f f f f f f f f f ' ' ' ' ' ' | 
| ' t f f f f f f f f f f f f f ' ' ' ' ' ' | 
| ' t f f f f f f f f f f f f f ' ' ' ' ' ' | 
| ' t f f f f f f f f f f f f f ' ' ' ' ' ' | 
| ' ' ' ' ' ' ' ' ' ' ' ' ' ' ' ' ' ' ' ' ' | 
| ' ' ' ' ' ' ' ' ' ' ' ' ' ' ' ' ' ' ' ' ' | 
| ' ' ' ' ' ' ' ' ' ' ' ' ' ' ' ' ' ' ' ' ' | 
| ' ' ' ' ' ' ' ' ' ' ' ' ' ' ' ' ' ' ' ' ' | 
| ' ' ' ' ' ' ' ' ' ' ' ' ' ' ' ' ' ' ' ' ' | 
| ' ' ' ' ' ' ' ' ' ' ' ' ' ' ' ' ' ' ' ' ' | 
| ' ' ' ' ' ' ' ' ' ' ' ' ' ' ' ' ' ' ' ' ' |),hasVolunteered : false,neighbors
    : -996 . -755 starting true,remainingPower : 1999115200,roundTimer :
    997823,status : on,uncoveredCrossings : none,volunteerProb : 400 > < 948 .
    -150 : WSNode | backoffTimer : INF,bitmap :(
| ' ' ' ' ' ' ' ' ' ' f ' ' ' ' ' ' ' ' ' ' | 
| ' ' ' ' ' ' f f f f f f f f ' ' ' ' ' ' ' | 
| ' ' ' ' f f f f f f f f f f ' ' ' ' ' ' ' | 
| ' ' ' t f f f f f f f f f f ' ' ' ' ' ' ' | 
| ' ' t t f f f f f f f f f f ' ' ' ' ' ' ' | 
| ' ' t f f f f f f f f f f f ' ' ' ' ' ' ' | 
| ' t t f f f f f f f f f f f ' ' ' ' ' ' ' | 
| ' t f f f f f f f f f f f f ' ' ' ' ' ' ' | 
| ' t f f f t t t t t t t t f ' ' ' ' ' ' ' | 
| ' f f t t t t t t t t t t t ' ' ' ' ' ' ' | 
| t f t t t t t t t t t t t t ' ' ' ' ' ' ' | 
| ' t t t t t t t t t t t t t ' ' ' ' ' ' ' | 
| ' t t t t t t t t t t t t t ' ' ' ' ' ' ' | 
| ' t t t t t t t t t t t t t ' ' ' ' ' ' ' | 
| ' t t t t t t t t t t t t t ' ' ' ' ' ' ' | 
| ' ' t t t t t t t t t t t t ' ' ' ' ' ' ' | 
| ' ' t t t t t t t t t t t t ' ' ' ' ' ' ' | 
| ' ' ' t t t t t t t t t t t ' ' ' ' ' ' ' | 
| ' ' ' ' t t t t t t t t t t ' ' ' ' ' ' ' | 
| ' ' ' ' ' ' t t t t t t t t ' ' ' ' ' ' ' | 
| ' ' ' ' ' ' ' ' ' ' t ' ' ' ' ' ' ' ' ' ' |),hasVolunteered : false,neighbors
    :((-728 . 659 starting true)(-1039 . -225 starting false)814 . -857
    starting false),remainingPower : 1999115200,roundTimer : 997823,status :
    on,uncoveredCrossings : none,volunteerProb : 400 >} in time 2177