[erlang-questions] Looking for tricky protocol examples for verification research

[zxq9]

On Wednesday 05 November 2014 13:24:43 Jonathan Schuster wrote:
> On Fri, Oct 31, 2014 at 12:20 PM, zxq9 <zxq9@REDACTED> wrote:
> > Erlang processes can be thought of the same way if we accept that in
> > Erlang
> > "process" means something much closer to what languages like Python mean
> > by
> > "object" than is commonly imagined. If I have a game character process it
> > might have an AI controller, or it might have a player controller. The
> > character process doesn't need to know or care, and we could actively swap
> > out
> > AI for player control on the fly and the character process wouldn't care,
> > so
> > long as all controllers, regardless of subtype (if we decide to use this
> > term
> > "type"), adhere to the "controller" protocol.
> 
> Yes, this is exactly the sort of abstraction I'm looking for. The main
> questions I have right now are (1) where are the real-life examples of such
> protocols, and (2) what is the most useful enforcement mechanism? A type
> system would probably be the most familiar to programmers, but it's not
> necessarily the most practical. Question 2 is really a research question,
> and the answer to question 1 should help me solve question 2.
> 
> I haven't had a chance yet to look into the examples already mentioned on
> this thread, but hopefully there are examples there or in other programs
> I'm examining (e.g. ejabberd probably has several instances of this kind of
> problem).
> 
> I agree that behaviors might be a good place to look. This does seem to be
> the closest thing Erlang has to built-in protocol specifications, so maybe
> I can extend those in an interesting way.

I'm working on a demonstration system right now that is full of this 
particular case. Actually, its the source of the AI/player controller swap-out 
example. The protocols are dead simple, though, but even so a verification 
mechanism would be nice.

While writing my own system I'm confident I won't mess up an easy protocol that 
I'm intimately familiar with (and if I do I'll know immediately), but game 
system operators who want to extend existing games by writing new AIs, 
interesting game items, new mobs, etc. will have to write new modules. These 
modules will have to adhere to the protocols that already exist, and having a 
way to declare them in code and having the compiler check that they do receive 
and send the correct protocol would be nice.

Indication of protocol compliance must permit pluralities. An AI only adheres 
to the "mob controller" protocol, but a player controller must adhere to the 
network messaging, chat system and mob controller protocols at once (and more 
if the system is extended in almost any way).

One trick to verification is synchronous messaging with a third-process 
response. For example, how to verify that: A sends B a synchronous message 
{From, Ref, Message}. Process B does something with it, and passes {From, Ref, 
Data} on to process C. Process C responds to A with {Ref, Response2} which 
satisfies A's synchronous response expectation.

>From A's perspective this is synchronous, to B and C it is not. This case does 
not occur in function returns, so I don't think it has been thought through 
much in terms of external type or protocol assignment -- at least I've never 
seen it mentioned before.

Good luck with your project. Let me know if you make any progress -- it would 
be a good tool when writing software in teams or writing code intended for 
extension by other Erlangers (and being a wizard should not be a requirement 
to extend code written for this purpose!).

-Craig