DataXfer Protocol PDL Description:
[ simple data transfer protocol in PDL with timeouts, retry, and no error recovery ]
dataxfer { InitialState = Idle;

[ Idle state - no connections have been established ]
state Idle::
        recv(Connect,Net)      ->      send(Connect,Usr),
                                       StartTimer(Tconn)       >> SetupReceive;
        recv(Connect,Usr)      ->      send(Connect,Net),
                                       StartTimer(Tconn)       >> SetupSend;

[ SetupReceive state - network has requested a connection with the user ]
state SetupReceive::
        timeout(Tconn)        |
        recv(Refuse,Usr)       ->      send(Refuse,Net),
                                       StopTimer(Tconn)        >> Idle;
        recv(Accept,Usr)       ->      send(Accept,Net),
                                       StopTimer(Tconn),
                                       StartTimer(Trecv)       >> Receiving;
        macro EventDisc;

[ Receiving state - user has accepted a connection request from the network, ]
[                   network to user transmission is in progress              ]
state Receiving::
        timeout(Trecv)         ->      macro ActionError;
        recv(Disconnect,Net)   ->      send(Disconnect,Usr),
                                       StopTimer(Trecv)        >> Idle;
        recv(Message,Net)      ->      CheckMsg{
                                              MsgOK ->         send(Message,Usr),
                                                               send(Ack,Net),
                                                               RestartTimer(Trecv);
                                              MsgBad ->        send(NotAck,Net);
                        };
        macro EventDisc;

[ SetupSend state - user has requested a connection to the network ]
state SetupSend::
        timeout(Tconn)        |
        recv(Refuse,Net)       ->      send(Refuse,Usr),
                                       StopTimer(Tconn)        >> Idle;
        recv(Accept,Net)       ->      send(Accept,Usr),
                                       StopTimer(Tconn),
                                       StartTimer(Tsend)       >> Sending;
        macro EventDisc;

[ Sending state - network has accepted user connection request,   ]
[                 user to network transmission is in progress.    ]
state Sending::
        timeout(Tsend)         ->      macro ActionError;
        recv(Disconnect,Usr)   ->      send(Disconnect,Net),
                                       StopTimer(Tsend)        >> Idle;
        recv(Message,Usr)      ->      send(Message,Net),
                                       send(Ack,Usr),
                                       StopTimer(Tsend),
                                       RetryReset,
                                       StartTimer(Tack)        >> WaitAck ;
        macro EventDisc;

[ WaitAck state - user transmission to network is waiting for acknowledgement     ]
[                 from network with the condition of the last message received    ]
state WaitAck::
        timeout(Tack)          ->      macro ActionError;
        recv(Ack,Net)          ->      StopTimer(Tack),
                                       StartTimer(Tsend)       >> Sending;
        recv(NotAck,Net)       ->      Retry{
                                              YesRetry ->      ResendMessage,
                                                               RestartTimer(Tack);
                                              NoRetry ->       macro ActionError;
                        };
        macro EventDisc;

[ EventDisc event macro -      either side of the connection may request disconnection,        ]
[                      option is only available in connected states            ]
event macro EventDisc:
        recv(Disc,Net)         ->      send(Disc,Usr),
                                       StopAllTimers           >> Idle;
        recv(Disc,Usr)         ->      send(Disc,Net),
                                       StopAllTimers           >> Idle;

[ ActionError action macro -   an error simply aborts and disconnects ]
action macro ActionError:
                                       send(Abort,Usr),
                                       send(Abort,Net),
                                       StopAllTimers           >> Idle;
}