[Haskell-cafe] Informal modelling and simulation of protocols

[P Orrifolius]

On Fri, 8 Mar 2019 at 02:28, MarLinn <monkleyon at gmail.com> wrote:

> AFAIK in existing general-purpose simulation frameworks the type of
> simulation you need for this type of problem is typically implemented in
> a way that very closely resembles "classical" FRP, particularly it's
> definition of events. The framework basically manages huge queues of
> time-action-pairs.

Interesting.  So it's possible that the Spin model checker takes a
similar approach, along with all sorts of state-space compression
tricks and such like.

> So several of the FRP libraries might be a good candidate. I haven't had
> a chance to experiment with MSF's yet, but seeing as they are a
> development in FRP space, Ivan's approach sounds like quite a good idea.

I am coming (back) around to some sort of FRP modelling... it'd be
hubris to expect to top Spin, but as long as I'm learning it's fine I
suppose.
It appears to me now that a FRP network of streams may allow quite a
lot of re-use between protocol modelling and implementation... it may
be pretty straight forward to substitute the 2 alternative
sub-networks of the modelling FRP that carried out "receive (good|bad)
message -> emit message count+(1|0)" with the implementation "receive
message -> check signature -> write to disk -> etc -> emit message
count+(1|0)".

And it occurs to me now that using CRDTs, and Lamport or vector
clocks, to manage variables/state on the individual simulation runs
could provide quite an effective state-space compression, collapse the
tree of runs down to a graph.


Thanks for the 2 cents.