[Haskell-cafe] Informal modelling and simulation of protocols

[P Orrifolius]

On Tue, 5 Mar 2019 at 03:33, Doug McIlroy <doug at cs.dartmouth.edu> wrote:
>
>
> > Is there some fantastic tool/library which already does everything I want?
>
> Have you looked into model checkers like Spin, which was developed
> for the very purpose of exhaustively checking protocols? See spinroot.com

Thanks for lead.  Spin does seem to be an appropriate tool for the job.

I was/am sort of hoping the protocol modelling and implementation
would both be in Haskell to get some reuse, but the consensus seems to
be that Spin's modelling language is pretty easy to use so maybe it
would  be no extra work overall.

I'm sure I've still got the implementation and protocol itself
somewhat confused, so what state is truly required for the protocol is
a bit muddled.  Not certain how I would represent it in spin, just
need to play around with it I guess.
That's partly what I was getting at with my 'modelling operators over
domains' ramble... trying to avoid increasing the state space by
enumerating through all data type values without abstracting the
protocol model by just checking boundary cases.  Or at least
abstracting in a disciplined way that makes me confident all boundary
cases are checked, not just those I happened to think of and model.
But perhaps Spin already has some state space compression tricks of
that nature and I'm worrying over nothing.

Anyway, thanks for the pointer!