Hi,
I'm trying to write a specification for an existing system.
I have a server and clients connected through TCP/IP (this is oversimplification, in fact I use ZMQ and IPC channels also can be used).
The protocol is based on serialized C++ structures (protocol bufferes, cereal, whatever, not important, lets abstract that away).
I have couple of questions:
1. How to handle time, timers and timeouts?
I have a monotonic clock on each node (each client and the server). I have implemented a heartbeat. Ping/pong message contains current time. This is what I have at the moment:
ClientStateType ==
[ clock : Nat
, timeout : Nat
, pingResponse : Nat
, interval : Nat
, pingRequest : Nat
... other fields ...
]
ClientInitialState ==
[ clock |-> 0
, timeout |-> 0
, pingResponse |-> 0
, interval |-> 0
, pingRequest |-> 0
... other fields ...
]
ServerTick ==
/\ server' = [ server EXCEPT !.clock = @ + 1 ]
ClientTick ==
/\ client' = [ client EXCEPT !.clock = @ + 1 ]
Next ==
\/ ServerTick
\/ ClientTick
... other actions ...
Is this approach correct?
2. In my API I have setters and gettes. By getters I mean methods/functions that just returns a value, for example:
/// Setup heartbeat.
/**
@param interval How often send PingRequest.
@param timeout How long wait for PingReply.
@warning Should be called before Api::connect or Api::connectAndWait
*/
void setupHeartbeat(uint32_t interval, uint32_t timeout);
/// Get current heartbeat interval.
uint32_t heartbeatInterval() const;
/// Get current heartbeat timeout.
uint32_t heartbeatTimeout() const;
I would like to include heartbeatInterval and heartbeatTimeout in my specification for completness, but I have no idea how these definitions should look like. I can just use UNCHANGED << all my variables >> in definitions, but that feels wrong - useless.
3. My API is based on async handlers. For example I have this:
/// Send SyncVersionInfoRequest message.
/**
@note Async action.
*/
void getVersionInfo(const std::function<void(Error error, std::string info)> &handler);
Info handler is stored in private vector of handlers and it is called when the response is received.
void Api::handleGetVersionInfoResponse(const SyncGetVersionInfoResponse &msg)
{
if(_getVersionInfoResponseHandlers.count(msg.msg) > 0)
{
_getVersionInfoResponseHandlers[msg.msg]({ErrorType::NONE, {}, {}}, msg.data);
_getVersionInfoResponseHandlers.erase(msg.msg);
return;
}
handleUnexpectedResponse();
}
How to model these calls? How to model my handlers? Maybe something like simple counters would do? I would like to know the most common approach.
4. Is there an example of this kind of system/API backed up with implementation?
Thanks,
Emanuel