TickerMsg Message Interface¶
TickerMsg Message Constructors¶
TickerMsgIncrement
¶
A TickerMsgIncrement
message instructs the engine to increase the counter.
This message doesn't require any arguments.
TickerMsgCountRequest
¶
A TickerMsgCountRequest
message requests the engine to send the current counter value back to
the requester. This message doesn't require any arguments.
TickerMsgCountReply CountReply
¶
The TickerMsgCountReply
contains the counter value.
type CountReply : Type := mkCountReply@{counter : Nat};
TickerMsg
¶
type TickerMsg :=
| TickerMsgIncrement
| TickerMsgCountRequest
| TickerMsgCountReply CountReply;
There are only two message tags: TickerMsgIncrement
, which increases the counter
state of the ticker, and TickerMsgCount
, which the ticker responds to with the current
counter state.
Ticker Interaction Diagram¶
This diagram represents a simple interaction between a Ticker
engine instance
and another entity sending increment requests and count requests.