http://hackage.haskell.org/package/dejafu might do what you want

On Mar 4, 2019, at 10:33 PM, Doug McIlroy 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

Doug McIlroy _______________________________________________ Haskell-Cafe mailing list To (un)subscribe, modify options or view archives go to: http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe Only members subscribed via the mailman list are allowed to post.

On Tue, 5 Mar 2019 at 03:33, Doug McIlroy 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!