2cents: 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. 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. Cheers. On 05/03/2019 14.29, Ivan Perez 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.
Ivan
[1] https://github.com/ivanperez-keera/dunai [2] https://arc.aiaa.org/doi/abs/10.2514/6.2019-1187