[Haskell-cafe] Informal modelling and simulation of protocols

[P Orrifolius]

On Wed, 6 Mar 2019 at 02:30, Ivan Perez <ivanperezdominguez at gmail.com> wrote:
>
> Hi
>
> Partly related; for recent work we did two things:
>
> - Model part of the collision avoidance logic of a satellite as a state machine, implement it in haskell (14 locs) and use small check to verify that the state transitions fulfill the properties we expect for collision avoidance.
>
> - Model small sats as Monadic Stream Functions [1], implement a communication protocol on top (also using MSFs), and use quickcheck + fault injection to verify distributed consensus in the presence of faults. The next (immediate) step will be to bound the trace length and use smallcheck or something that exhausts the input space. I have also implemented Raft using MSFs, and the idea is to verify properties in a similar way.
>
> I know this is vague. Let me know if you have any questions or want more details.

An appropriately vague response for a vague question! :)

No, that's good, thanks.  I have considered using an FRP library for
the _implementation_ but I couldn't really get my head around how I
would use it for modelling and checking the protocol itself.  I was
considering reflex as it seems to be well regarded, and the
browser/mobile capabilities appear to be good which could prove useful
for me in the future.  I'm not sure how reflex is classified but I
guess it's a 'classic' FRP system, so perhaps the issues I was facing
would be analogous to those when using MSF/dunai.

Your email has made me take a second look at a FRP option, and I think
I was seeing problems where there aren't any.

One difficulty I perceived was the heterogeneity of the participants
in the protocol and the multi-point communications, well beyond a
simple sending/receiving distinction.
That worries me less now.  It seems that if I could come up with a
statechart description of each participant it's probably a fairly
mechanical process to represent that in a FRP network.
Perhaps that explains why I couldn't find many libraries to do with
more 'elaborate' state representations (as in statecharts are more
elaborate than FSM/automata/etc).  Maybe once you reach that
complexity they're not the best way to think about the problem in
Haskell.

The 'complex heterogeneity' reinforced my main problem, which now I
think might just be a case premature optimisation.  It seemed that if
I wanted to enumerate all states while testing the protocol I would
need to 'branch' each participant whenever they changed and
recursively test each temporal alternative... and that probably
involved building, modifying, reorganising, restoring networks on the
fly.  Maybe achievable, but I couldn't immediately see how.  But a
simple succession of root-to-tip searches/executions of that tree
could be perfectly adequate.
Just have to try it out but I think I was getting carried away.

Anyway, after that additional vagueness... a bit of a tangent. :)
One problem I have with the Haskell ecosystem is I end up falling down
the rabbit-hole whenever I start researching something.  And within
each rabbit-hole I find more
interesting-thing-to-research-rabbit-holes, and within them... etc,
etc.  Soon I'm so deep down the rabbit-holes I'm smothered in quantum
foam and don't know which way is up.
On my last foray I started with MSF and came upon Streamly:
https://hackage.haskell.org/package/streamly-0.6.0
Are you familiar with it?  To my inexperienced eye it seems quite
similar to MSF/dunai, do you have any thoughts on it?  Relative merits
in different use cases?
Reflex appeals to me because of the possibility of learning it and
leveraging it's UI layers in other projects.  But for a protocol
implementation it feels like maybe I should be using something more,
um... stripped back/fundamental.

Again, thanks for the reply.