//$ Original protocol

//$ timed global protocol HandleDNSRequest(role Handler, role Regional) {
//$     rec QueryResolution {
//$         FindNearestZone(DomainName) from Handler to Regional within [0;1] using a and resetting ();
//$         choice at Regional {
//$             ZoneResponse(ZonePID) from Regional to Handler within [0;1] using a and resetting ();
//$             Handler initiates GetZoneData(Handler, new Data) within [0;1] using a and resetting ();
//$             continue QueryResolution within [0;1] using a and resetting ();
//$         } or {
//$             InvalidZone() from Regional to Handler within [0;1] using a and resetting ();
//$         }

//$     }

//$ }

//$ timed global protocol GetZoneData(role Handler, role Data) {
//$     ZoneDataRequest() from Handler to Data within [0;1] using a and resetting ();
//$     ZoneDataResponse(RRTree) from Data to Handler within [0;1] using a and resetting ();
//$ }

//$ Modified protocol

timed global protocol HandleDNSRequest(role Handler, role Regional, role Data) {
    rec QueryResolution {
        FindNearestZone(DomainName) from Handler to Regional within [0;1] using a and resetting ();
        choice at Regional {
            ZoneResponse(ZonePID) from Regional to Handler within [0;1] using a and resetting ();
            ZoneDataRequest() from Handler to Data within [0;1] using a and resetting ();
            ZoneDataResponse(RRTree) from Data to Handler within [0;1] using a and resetting ();
            continue QueryResolution within [0;1] using a and resetting ();
        } or {
            InvalidZone() from Regional to Handler within [0;1] using a and resetting ();
            InvalidZone() from Handler to Data within [0;1] using a and resetting ();
            Received() from Data to Handler
        }
    }
}