On Wed, 6 Mar 2019 at 02:30, Ivan Perez
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.