On Fri, 8 Mar 2019 at 02:28, MarLinn
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.