//This file was generated from (Academic) UPPAAL 4.0.8 (rev. 4276), March 2009 /* */ A[] not deadlock /* */ //NO_QUERY /* */ nodes(1).UpdateEnergy --> nodes(2).UpdateNeighbour /* */ nodes(2).UpdateEnergy --> (nodes(1).UpdateNeighbour and nodes(3).UpdateNeighbour and nodes(4).UpdateNeighbour) /* */ nodes(3).UpdateEnergy --> nodes(2).UpdateNeighbour /* */ nodes(4).UpdateEnergy --> nodes(2).UpdateNeighbour /* */ //NO_QUERY /* Check that all packages are eventually routed to sink old: (nodes(1).Application and nodes(1).Route) --> basestation.Collect */ (nodes(1).Application) --> basestation.Collect /* Check that all packages are eventually routed to sink */ (nodes(2).Application) --> basestation.Collect /* Check that all packages are eventually routed to sink */ (nodes(3).Application) --> basestation.Collect /* Check that all packages are eventually routed to sink */ (nodes(4).Application) --> basestation.Collect /* */ //NO_QUERY /* */ A[] not outOfPower /* */ //NO_QUERY /* */ A<> nodes(1).UpdateEnergy /* */ A<> nodes(2).UpdateEnergy /* */ A<> nodes(3).UpdateEnergy /* */ A<> nodes(4).UpdateEnergy /* */ (nodes(1).UpdateEnergy --> (nodes(2).UpdateNeighbour)) /* */ (nodes(2).UpdateEnergy --> (nodes(1).UpdateNeighbour and nodes(3).UpdateNeighbour and nodes(4).UpdateNeighbour)) /* */ (nodes(3).UpdateEnergy --> (nodes(2).UpdateNeighbour)) /* */ (nodes(4).UpdateEnergy --> (nodes(2).UpdateNeighbour)) /* A[] (nodes(1).UpdateNeighbour imply E<> nodes(2).AugmentNeighbour) */ //NO_QUERY /* */ A[] (nodes(1).Application or nodes(1).UpdateEnergy or nodes(1).RouteReceive or nodes(1).RouteSend) imply (nodes(2).Idle and nodes(3).Idle and nodes(4).Idle) /* */ A[] (nodes(2).Application or nodes(2).UpdateEnergy or nodes(2).RouteReceive or nodes(2).RouteSend) imply (nodes(1).Idle and nodes(3).Idle and nodes(4).Idle) /* */ A[] (nodes(3).Application or nodes(3).UpdateEnergy or nodes(3).RouteReceive or nodes(3).RouteSend) imply (nodes(1).Idle and nodes(2).Idle and nodes(4).Idle) /* */ A[] (nodes(4).Application or nodes(4).UpdateEnergy or nodes(4).RouteReceive or nodes(4).RouteSend) imply (nodes(1).Idle and nodes(2).Idle and nodes(3).Idle) /* */ //NO_QUERY /* */ E<> (nodes(1).UpdateNeighbour and not nodes(1).hasValidRoute()) /* */ (nodes(1).UpdateNeighbour and not nodes(1).hasValidRoute()) --> nodes(2).UpdateNeighbour /* */ (nodes(2).UpdateNeighbour and not nodes(2).hasValidRoute()) --> (nodes(1).UpdateNeighbour and nodes(3).UpdateNeighbour and nodes(4).UpdateNeighbour) /* */ (nodes(3).UpdateNeighbour and not nodes(3).hasValidRoute()) --> nodes(2).UpdateNeighbour /* */ (nodes(4).UpdateNeighbour and not nodes(4).hasValidRoute()) --> nodes(2).UpdateNeighbour /* */ nodes(1).UpdateEnergy --> nodes(1).hasValidRoute() /* */ nodes(2).UpdateEnergy --> nodes(2).hasValidRoute() /* */ nodes(3).UpdateEnergy --> nodes(3).hasValidRoute() /* */ nodes(4).UpdateEnergy --> nodes(4).hasValidRoute() /* */ //NO_QUERY /* */ A[] nodes(1).route == 0 /* */ E<> nodes(2).route != 1 and not nodes(2).Init /* */ A[] nodes(3).route == 2 or nodes(3).Init /* */ A[] nodes(4).route == 2 or nodes(4).Init /* */ //NO_QUERY /* */ E<> nodes(2).route != 1 and nodes(2).RouteSend /* */ //NO_QUERY /* */ //NO_QUERY /* */ //NO_QUERY /* */ //NO_QUERY /* */ //NO_QUERY