\||||||||||||||||||/
		   --- Welcome to Maude ---
		     /||||||||||||||||||\
	    Maude 2.3 built: Feb 14 2007 17:53:50
	    Copyright 1997-2007 SRI International
		   Fri Nov  2 04:25:54 2007

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

	  Real-Time Maude 2.3 extension May 2, 2007

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

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

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

rewrites: 40702 in 83ms cpu (83ms real) (484622 rewrites/second)
Introduced module OGDC-COVERAGE-OPERATIONS

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

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

rewrites: 29063 in 44ms cpu (44ms real) (645930 rewrites/second)

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

rewrites: 72482 in 149ms cpu (149ms real) (483284 rewrites/second)

Introduced timed module: OGDC

rewrites: 51143 in 108ms cpu (108ms real) (469270 rewrites/second)

Introduced timed module: OGDC-RTM

rewrites: 86055 in 171ms cpu (171ms real) (500395 rewrites/second)

Introduced timed module: OGDC-ANALYSIS

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

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

rewrites: 207745295 in 277295ms cpu (277364ms real) (749182 rewrites/second)

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

Result:	{< Random : RandomNGen | seed : 10158 > < -301 . -723 : 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 f f f f f f f f f f f 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 : 1999946000,roundTimer : 999900,status : on,
    uncoveredCrossings : none,volunteerProb : 200 > < -1244 . -327 : 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 t t t t ' ' | 
| ' ' ' ' ' ' ' ' ' ' f f f f t t t t t t ' | 
| ' ' ' ' ' ' ' ' ' ' f f f t t t t t t t ' | 
| ' ' ' ' ' ' ' ' ' ' f f t t t t t t t t ' | 
| ' ' ' ' ' ' ' ' ' ' f 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 ' ' ' | 
| ' ' ' ' ' ' ' ' ' ' f t t t t t t ' ' ' ' | 
| ' ' ' ' ' ' ' ' ' ' f t t t t ' ' ' ' ' ' | 
| ' ' ' ' ' ' ' ' ' ' ' ' ' ' ' ' ' ' ' ' ' |),hasVolunteered : false,neighbors
    : -301 . -723 starting true,remainingPower : 1999946000,roundTimer :
    999900,status : on,uncoveredCrossings : none,volunteerProb : 400 > < 434 .
    -561 : 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 ' ' | 
| ' t t t t t t t t t t t t t t t t t t ' ' | 
| ' t t t t t t t t t t t t t t t t t t ' ' | 
| t t t t t t t t t t t t t t t t t t t ' ' | 
| ' t t t t t t t t t t t t t t t t t t ' ' | 
| ' t t t t t t t t t t t t t t t t t t ' ' | 
| ' t t t t t t t t t t t t t t t t t t ' ' | 
| ' t t t t t t t t t t t t t t t t t t ' ' | 
| ' ' t t t t t t t t t t 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
    :((-301 . -723 starting true)(-1244 . -327 starting false)(918 . -650
    starting false)950 . -61 starting true),remainingPower : 1999960000,
    roundTimer : 999900,status : off,uncoveredCrossings :((950 . -61 x -301 .
    -723 in -6 . 233)950 . -61 x -301 . -723 in 655 . -1016),volunteerProb :
    400 > < 918 . -650 : 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 t t t t t t t t t t t t ' ' ' ' ' ' ' | 
| ' t t t t t t t t t t t t t ' ' ' ' ' ' ' | 
| ' t t t t t t t t t 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 f f ' ' ' ' ' ' ' | 
| ' ' t t t t t f f f f f f f ' ' ' ' ' ' ' | 
| ' ' t t t t t f f f f f f f ' ' ' ' ' ' ' | 
| ' ' ' ' ' ' ' ' ' ' ' ' ' ' ' ' ' ' ' ' ' | 
| ' ' ' ' ' ' ' ' ' ' ' ' ' ' ' ' ' ' ' ' ' | 
| ' ' ' ' ' ' ' ' ' ' ' ' ' ' ' ' ' ' ' ' ' | 
| ' ' ' ' ' ' ' ' ' ' ' ' ' ' ' ' ' ' ' ' ' |),hasVolunteered : false,neighbors
    :((-301 . -723 starting true)950 . -61 starting true),remainingPower :
    1999946000,roundTimer : 999900,status : on,uncoveredCrossings : 950 . -61 x
    -301 . -723 in 655 . -1016,volunteerProb : 400 > < 950 . -61 : 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 : 1999946000,roundTimer : 999900,status : on,
    uncoveredCrossings : none,volunteerProb : 200 >(msg powerOnWithDirection -1
    from 918 . -650 to -301 . -723)msg powerOnWithDirection -1 from 918 . -650
    to 950 . -61} in time 100

rewrites: 20889049 in 53457ms cpu (53467ms real) (390757 rewrites/second)

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

Result:	{dly(msg powerOnWithDirection -1 from -1244 . -327 to -301 . -723,
    7)dly(msg powerOnWithDirection -1 from -1244 . -327 to 434 . -561,7)<
    Random : RandomNGen | seed : 3453 > < -301 . -723 : WSNode | backoffTimer :
    INF,bitmap :(
| ' ' ' ' ' ' ' ' ' ' f ' ' ' ' ' ' ' ' ' ' | 
| ' ' ' ' ' ' f f f f f t t t t ' ' ' ' ' ' | 
| ' ' ' ' f f f f f f t t t t t t t ' ' ' ' | 
| ' ' ' f f f f f f t t t t t t t t t ' ' ' | 
| ' ' f f f 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 t t t ' ' | 
| ' f f f f f f f t t t t t t t t t t t t ' | 
| ' f f f f f f f t t t t t t t t t t t t ' | 
| ' f f f f f f f t t t t t t t t t t t t ' | 
| ' f f f f f f f t t t t t t t t t t t t ' | 
| ' f f f f f f f t t t t t t t t t t t t t | 
| ' f f f f f f f t t t t t t t t t t t t ' | 
| ' f f f f f f f f t t t t t t t t t t t ' | 
| ' f f f f f f f f t t t t t t t t t t t ' | 
| ' f f f f f f f f f t t t t t t t t t t ' | 
| ' ' f f f f f f f f t t t t t t t t t ' ' | 
| ' ' ' ' ' ' ' ' ' ' ' ' ' ' ' ' ' ' ' ' ' | 
| ' ' ' ' ' ' ' ' ' ' ' ' ' ' ' ' ' ' ' ' ' | 
| ' ' ' ' ' ' ' ' ' ' ' ' ' ' ' ' ' ' ' ' ' | 
| ' ' ' ' ' ' ' ' ' ' ' ' ' ' ' ' ' ' ' ' ' | 
| ' ' ' ' ' ' ' ' ' ' ' ' ' ' ' ' ' ' ' ' ' |),hasVolunteered : false,neighbors
    :((434 . -561 starting true)(918 . -650 starting false)950 . -61 starting
    true),remainingPower : 1999288800,roundTimer : 998257,status : on,
    uncoveredCrossings : none,volunteerProb : 400 > < -1244 . -327 : 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 t t t t ' ' | 
| ' ' ' ' ' ' ' ' ' ' f f f f t t t t t t ' | 
| ' ' ' ' ' ' ' ' ' ' f f f t t t t t t t ' | 
| ' ' ' ' ' ' ' ' ' ' f f t t t t t t t t ' | 
| ' ' ' ' ' ' ' ' ' ' f 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 ' ' ' | 
| ' ' ' ' ' ' ' ' ' ' f t t t t t t ' ' ' ' | 
| ' ' ' ' ' ' ' ' ' ' f t t t t ' ' ' ' ' ' | 
| ' ' ' ' ' ' ' ' ' ' ' ' ' ' ' ' ' ' ' ' ' |),hasVolunteered : false,neighbors
    :((-301 . -723 starting false)434 . -561 starting true),remainingPower :
    1999288800,roundTimer : 998257,status : on,uncoveredCrossings : none,
    volunteerProb : 400 > < 434 . -561 : 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 f f f f f f f f f ' ' | 
| ' ' f f f f f f f f f f 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 : 1999288800,roundTimer : 998257,status : on,
    uncoveredCrossings : none,volunteerProb : 200 > < 918 . -650 : 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 t t t t t t t t t t t t ' ' ' ' ' ' ' | 
| ' t t t t t t t t t t t t t ' ' ' ' ' ' ' | 
| ' t t t t t t t t t t t t t ' ' ' ' ' ' ' | 
| ' t t t t t t t t t t t t t ' ' ' ' ' ' ' | 
| ' t t t t t t t t t t t t 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 ' ' ' ' ' ' ' | 
| ' ' ' ' ' ' ' ' ' ' ' ' ' ' ' ' ' ' ' ' ' | 
| ' ' ' ' ' ' ' ' ' ' ' ' ' ' ' ' ' ' ' ' ' | 
| ' ' ' ' ' ' ' ' ' ' ' ' ' ' ' ' ' ' ' ' ' | 
| ' ' ' ' ' ' ' ' ' ' ' ' ' ' ' ' ' ' ' ' ' |),hasVolunteered : false,neighbors
    :((434 . -561 starting true)950 . -61 starting true),remainingPower :
    1999288800,roundTimer : 998257,status : on,uncoveredCrossings : 434 . -561
    x 950 . -61 in 1342 . -981,volunteerProb : 400 > < 950 . -61 : 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 : 1999288800,roundTimer : 998257,status : on,
    uncoveredCrossings : none,volunteerProb : 200 >} in time 1743

Bye.