#define netChanges 2 #define userSuspends 2 mtype = {data,resume,resume_ok,resume_denied,suspend}; typedef ctrlMsg { mtype type; chan addr; } chan recvCtrl[2]; init { /* control channels */ chan point1CtrlRecv[2] = [0] of {ctrlMsg}; chan point2CtrlRecv[2] = [0] of {ctrlMsg}; recvCtrl[0] = point1CtrlRecv[0]; recvCtrl[1] = point2CtrlRecv[0]; /* nameserver channels */ chan point1Name = [0] of {chan}; chan point2Name = [0] of {chan}; /* move channels */ chan point1Move = [0] of {chan}; chan point2Move = [0] of {chan}; /* data synchronization channel */ chan openData = [0] of {mtype}; /* movement indicators */ byte point1Idx = 1; byte point2Idx = 1; /* fixed number of network changes */ int changesLeft = netChanges; /* start processes */ run Nameserver(point1Name, point2Name, point1CtrlRecv[0], point2CtrlRecv[0]); run Endpoint(point1Move, point1Name, point2CtrlRecv[0], openData, 0, 1); run Endpoint(point2Move, point2Name, point1CtrlRecv[0], openData, 1, 0); do :: changesLeft > 0; point1Move!point1CtrlRecv[point1Idx]; point1Idx = (point1Idx + 1) % 2; point2Move!point2CtrlRecv[point2Idx]; point2Idx = (point2Idx + 1) % 2; changesLeft--; :: else; break; od; } proctype Nameserver(chan ns1, ns2, point1Recv, point2Recv) { do :: atomic { ns1?point1Recv; ns1!point2Recv; }; :: atomic { ns2?point2Recv; ns2!point1Recv; }; od; } proctype Endpoint(chan move, ns, sendCtrl, openData; bit myId, otherId) { int suspendsLeft = userSuspends; /* disconnected channel */ chan disconnected = [0] of {ctrlMsg}; /* temporary channel storage */ chan storedRecv; chan storedSend; /* messages */ ctrlMsg recvCtrlMsg; ctrlMsg sendCtrlMsg; ACTIVE: if :: recvCtrl[myId]?recvCtrlMsg; if :: recvCtrlMsg.type == resume; sendCtrl = recvCtrlMsg.addr; /* received resume, send resume_ok */ goto SEND_RESUME_OK; :: recvCtrlMsg.type == resume_ok; /* should not receive resume_ok here */ assert(false); :: recvCtrlMsg.type == resume_denied; /* should not receive resume_denied here */ assert(false); :: recvCtrlMsg.type == suspend; sendCtrl = recvCtrlMsg.addr; /* received suspend, leave active */ goto READY_RESUME; :: else; assert(false); fi; goto ACTIVE; :: suspendsLeft > 0; suspendsLeft--; /* user suspends */ goto SUSPEND; :: sendCtrl != recvCtrl[otherId]; /* failed to send, endpoint unreachable */ goto READY_RESUME; :: sendCtrl != disconnected; /* failed to send, disconnected */ d_step { storedRecv = recvCtrl[myId]; storedSend = sendCtrl; recvCtrl[myId] = disconnected; sendCtrl = disconnected; }; goto READY_RESUME; :: atomic { move?recvCtrl[myId]; /* moved to new network register with name server */ ns!recvCtrl[myId]; ns?sendCtrl; }; goto USER_RESUME; fi; USER_RESUME: skip; d_step { sendCtrlMsg.type = resume; sendCtrlMsg.addr = recvCtrl[myId]; }; if :: sendCtrl!sendCtrlMsg; goto SENT_RESUME; :: sendCtrl != recvCtrl[otherId] && sendCtrl != disconnected; /* failed to send, look up endpoint and retry */ atomic { ns!recvCtrl[myId]; ns?sendCtrl; }; if :: sendCtrl!sendCtrlMsg; goto SENT_RESUME; :: sendCtrl != recvCtrl[otherId]; /* failed to send, unreachable */ goto READY_RESUME; :: sendCtrl != disconnected; /* failed to send, disconnected */ d_step { storedRecv = recvCtrl[myId]; storedSend = sendCtrl; recvCtrl[myId] = disconnected; sendCtrl = disconnected; } goto READY_RESUME; fi; :: sendCtrl != disconnected; /* failed to send, got disconnected */ d_step { storedRecv = recvCtrl[myId]; storedSend = sendCtrl; recvCtrl[myId] = disconnected; sendCtrl = disconnected; } goto READY_RESUME; :: sendCtrl == disconnected; /* disconnected */ goto READY_RESUME; fi; SENT_RESUME: if :: recvCtrl[myId]?recvCtrlMsg; if :: recvCtrlMsg.type == resume; sendCtrl = recvCtrlMsg.addr; if :: myId == 0; /* received resume, initiator */ goto USER_RESUME; :: else; /* received resume, not initiator */ goto READY_RESUME; fi; :: recvCtrlMsg.type == resume_ok; sendCtrl = recvCtrlMsg.addr; /* received resume_ok, go active */ if :: openData!data; goto ACTIVE; :: sendCtrl != recvCtrl[otherId]; /* open connection failed */ goto READY_RESUME; fi; :: recvCtrlMsg.type == resume_denied; sendCtrl = recvCtrlMsg.addr; /* received resume_denied, stop waiting */ goto READY_RESUME; :: recvCtrlMsg.type == suspend; sendCtrl = recvCtrlMsg.addr; /* ignore */ goto SENT_RESUME; :: else; assert(false); fi; :: atomic { move?recvCtrl[myId]; /* moved to new network, register with name server */ ns!recvCtrl[myId]; ns?sendCtrl; }; goto USER_RESUME; fi; READY_RESUME: if :: recvCtrl[myId]?recvCtrlMsg; if :: recvCtrlMsg.type == resume; sendCtrl = recvCtrlMsg.addr; /* send resume_ok */ goto SEND_RESUME_OK; :: recvCtrlMsg.type == resume_ok; sendCtrl = recvCtrlMsg.addr; /* ignore */ goto READY_RESUME; :: recvCtrlMsg.type == resume_denied; sendCtrl = recvCtrlMsg.addr; /* ignore */ goto READY_RESUME; :: recvCtrlMsg.type == suspend; sendCtrl = recvCtrlMsg.addr; /* ignore */ goto READY_RESUME; :: else; assert(false); fi; :: suspendsLeft > 0; suspendsLeft--; /* user suspends */ goto SUSPEND; :: recvCtrl[myId] == disconnected; /* restored connection */ d_step { recvCtrl[myId] = storedRecv; sendCtrl = storedSend; }; goto USER_RESUME; :: atomic { move?recvCtrl[myId]; /* moved to new network, register with name server */ ns!recvCtrl[myId]; ns?sendCtrl; }; goto USER_RESUME; fi; SEND_RESUME_OK: skip; d_step { sendCtrlMsg.type = resume_ok; sendCtrlMsg.addr = recvCtrl[myId]; }; if :: sendCtrl!sendCtrlMsg; /* attempt to receive data connection */ if :: openData?data; goto ACTIVE; :: atomic { move?recvCtrl[myId]; /* moved to new network, register with name server */ ns!recvCtrl[myId]; ns?sendCtrl; }; goto USER_RESUME; fi; :: sendCtrl != recvCtrl[otherId]; /* failed to send, unreachable */ goto READY_RESUME; :: sendCtrl != disconnected; /* failed to send, disconnected */ d_step { storedRecv = recvCtrl[myId]; storedSend = sendCtrl; recvCtrl[myId] = disconnected; sendCtrl = disconnected; } goto READY_RESUME; fi; SUSPEND: skip; d_step { sendCtrlMsg.type = suspend; sendCtrlMsg.addr = recvCtrl[myId]; }; if :: sendCtrl!sendCtrlMsg; goto SUSPENDED; :: sendCtrl != recvCtrl[otherId]; /* failed to send */ goto SUSPENDED; :: sendCtrl != disconnected; /* failed to send, disconnected */ d_step { storedRecv = recvCtrl[myId]; storedSend = sendCtrl; recvCtrl[myId] = disconnected; sendCtrl = disconnected; } goto SUSPENDED; fi; SUSPENDED: if :: recvCtrl[myId]?recvCtrlMsg; if :: recvCtrlMsg.type == resume; sendCtrl = recvCtrlMsg.addr; /* received resume, send resume_denied */ goto SEND_RESUME_DENIED; :: recvCtrlMsg.type == resume_ok; sendCtrl = recvCtrlMsg.addr; /* ignore */ goto SUSPENDED; :: recvCtrlMsg.type == suspend; sendCtrl = recvCtrlMsg.addr; /* ignore */ goto SUSPENDED; :: recvCtrlMsg.type == resume_denied; sendCtrl = recvCtrlMsg.addr; /* ignore */ goto SUSPENDED; :: else; assert(false); fi; :: goto USER_RESUME; /* user resumes */ :: recvCtrl[myId] == disconnected; /* restored connection */ d_step { recvCtrl[myId] = storedRecv; sendCtrl = storedSend; }; goto SUSPENDED; :: atomic { move?recvCtrl[myId]; /* moved to new network, register with name server */ ns!recvCtrl[myId]; ns?sendCtrl; }; goto SUSPENDED; fi; SEND_RESUME_DENIED: skip; d_step { sendCtrlMsg.type = resume_denied; sendCtrlMsg.addr = recvCtrl[myId]; }; if :: sendCtrl!sendCtrlMsg; goto SUSPENDED; :: sendCtrl != recvCtrl[otherId]; /* failed to send */ goto SUSPENDED; :: sendCtrl != disconnected; /* failed to send, disconnected */ d_step { storedRecv = recvCtrl[myId]; storedSend = sendCtrl; recvCtrl[myId] = disconnected; sendCtrl = disconnected; } goto SUSPENDED; fi; }