<div dir="ltr"><div dir="ltr">TLA plus might suit you! I've actually had some success going back and forth between copattern style code and TLA specs, its not easy and not perfect, but it works<div><br></div><div>i've been slowly experimenting with modelling protocols as coinductive / copattern style trick </div><div><a href="https://www.reddit.com/r/haskell/comments/4aju8f/simple_example_of_emulating_copattern_matching_in/">https://www.reddit.com/r/haskell/comments/4aju8f/simple_example_of_emulating_copattern_matching_in/</a> is a small toy exposition i did<br></div><div><br></div><div>i am messing around with some reusable abstractions, though its definitely a challenging problem </div></div></div><br><div class="gmail_quote"><div dir="ltr" class="gmail_attr">On Mon, Mar 4, 2019 at 2:05 AM P Orrifolius <<a href="mailto:porrifolius@gmail.com">porrifolius@gmail.com</a>> wrote:<br></div><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex">Hi,<br>
<br>
this will probably be a somewhat rambling, open-ended question... my<br>
apologies in advance.<br>
There are some concrete questions after I explain what I'm trying to<br>
achieve, and some of them may even make sense!<br>
<br>
I'm planning on writing a multi-party, distributed protocol. I would<br>
like to informally model the protocol itself and the environment it<br>
would run in and then simulate it to see if it achieves what I expect.<br>
Then it would need to be implemented and tested of course.<br>
I think a formal, mathematical model of the protocol would be beyond<br>
my abilities.<br>
<br>
I'm looking for any advice or tool/library recommendations I can get<br>
on the modelling and simulating part of the process and how that work<br>
could be leveraged in the implementation to reduce the work and help<br>
ensure correctness.<br>
<br>
<br>
I have some ideas of how this could work, but I don't know if I'm<br>
approaching it with a suitably Haskell-like mindset...<br>
What I envisage at the moment is defining the possible behaviour of<br>
each party, who are not homogeneous, as well as things which form the<br>
external environment of the parties but will impact their behaviour.<br>
By external things I mean, for example, communication links which may<br>
drop or reorder packets, storage devices which may lose or corrupt<br>
data, machines that freeze or slew their clock... that sort of thing.<br>
I'm also picturing a 'universal coordinator' that controls interaction<br>
of the parties/environment during simulation.<br>
<br>
Modelling each party and external as a Harel-like statechart seems<br>
plausible. Perhaps some parts could be simpler FSMs, but I think many<br>
will be reasonably complex and involve internal state.<br>
<br>
It would be nice if the simulation could, to the limit of given<br>
processing time, exhaustively check the model rather than just<br>
randomly, as per quickcheck.<br>
If at each point the universal coordinator got a list of possible next<br>
states from each party/external it could simulate the<br>
simultaneity/sequencing of events by enumerating all combinations, of<br>
every size, of individual party/external transitions and then<br>
recursing with each separate combination applied as being the next set<br>
of simultaneous state transitions.<br>
<br>
To reduce the space to exhaustively search it would be nice if any<br>
values that the parties used, and were being tested by, were<br>
abstracted. Not sure what the technical term is but I mean asserting<br>
relationships between variables in a given domain, rather than their<br>
actual value.<br>
For example, imagine a distributed vote between two nodes where each<br>
node must vote for a random integer greater than their last vote.<br>
Each node is a party in the protocol.<br>
In the current branch of the exhaustive search of the protocol a<br>
relation between node 1's existing vote, v1, and node 2's existing<br>
vote, v2, has already been asserted: v1>v2.<br>
So when the coordinator enumerates the possibilities for sets of<br>
next-state transitions, with each node n asserting vn'>vn in their<br>
individual party state transition, it will prune any search branch<br>
which doesn't satisfy the union of the assertions (v1>v2, v1'>v1,<br>
v2'>v2), and recurse into the search branch alternatives with v1'<v2',<br>
or v1'=v2', or v1'>v2'.<br>
<br>
<br>
<br>
So, some questions...<br>
<br>
Is what I'm suggesting even vaguely sensible way to approach the<br>
problem in Haskell? Or am I getting carried away and some neat tricks<br>
zipping list monoids or something will get the job done?<br>
<br>
Is there some fantastic tool/library which already does everything I want?<br>
<br>
Are there any good tools or libraries in Haskell for defining and<br>
manipulating statecharts?<br>
<br>
The sessiontypes, and sessiontypes-distributed, libraries are cool,<br>
representing the protocol at the type level... but these only handle<br>
point-to-point, two-party protocols, right?<br>
I expect that extending them would be a _serious_ amount of work.<br>
<br>
Can quickcheck do the sort of exhaustive coverage testing that I'd like?<br>
<br>
Again, not sure of the correct terminology but can quickcheck generate<br>
tests at a variable-relation assertion level? I.e. inspect the<br>
operators and boolean tests over a domain (+, ==, >=, append, length,<br>
contains, etc) and explore test cases according to whether certain<br>
relations between variables hold.<br>
<br>
Any feelings/opinions about whether Oleg Kiselyov's Typed Tagless<br>
Final Interpreter (<a href="http://okmij.org/ftp/tagless-final/index.html" rel="noreferrer" target="_blank">http://okmij.org/ftp/tagless-final/index.html</a>) work<br>
might be a useful mechanism to define the behaviour of parties within<br>
the protocol (the statecharts, basically) and then have different<br>
interpreters that enable both the testing and implementation of the<br>
protocol, to keep them more closely aligned?<br>
I read that work years ago and have wanted to try it out ever since,<br>
so I may be overlooking the fact that it's totally unsuitable!<br>
Perhaps superseded now, but if it can allow more of the protocol to be<br>
expressed at the type level that would be good.<br>
<br>
<br>
Yeah, rambling. Sorry about that.<br>
<br>
<br>
Thanks!<br>
porrifolius<br>
_______________________________________________<br>
Haskell-Cafe mailing list<br>
To (un)subscribe, modify options or view archives go to:<br>
<a href="http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe" rel="noreferrer" target="_blank">http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe</a><br>
Only members subscribed via the mailman list are allowed to post.</blockquote></div>