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
You received this message because you are subscribed to the Google Groups "tlaplus" group.
To unsubscribe from this group and stop receiving emails from it, send an email to
.