Anyway we prepare for auction protocols: now an auction has a lot of constructs in it (unicasting, multicasting, loop, perhaps a global escape, choice, ...) so perhaps it's a good idea to introduce each of the basic constructs one by one. Our simplest protocol so far is one for the "hello world":
protocol GreetWorld {where we declare this is the protocol, we declare its name (GreetWorld), then we declare participants we shall use as pure names so that models and programs can bind later, and we declare a channel we use.
participant You, World;
channel chWorld @ World;
chWorld.greetings(string) from You to World;
}
Recall @ indicates the locatedness:
channel chWorld @ World;says that (1) we use the channel chWorld and that channel is located at World: World is the participant who can receive messages from this channel.
When a channel is declared, it will not be bound to anything later: a declared channel is entirely a logical entity inside a conversation (if you are familiar with the pi-calculus it corresponds to declaring a channel with "new"). This is like a method name (selector) is a pure name and is logically independent from any external entities. Or perhaps better it is like a locally declared variable which gets generated when a method is called and discarded when the method returns. So declaring a channel as above means specifying this channel is local to a conversation which will materialise this protocol.
This is subtlety of channel, how it is different from participants, and that which is important when we consider a protocol which allows the description of unbounded conversation structure.
Once we have everything declared we can have an interaction --- we formally call this interaction signature as distinct from conversation signature, but let's be simple --- which is:
chWorld.greetings(string) from You to World;The interaction says You (in fact somebody who is bound to You) will send a greeting to World via the channel chWorld. As we have discussed, we are assuming asynchronous messaging which will travel through some network infrastructure --- that expanse. The phrases such as from You and to World can be changed heir positions so we can say
to World from You if you like. Sometimes uniformity does pay for a quick understanding though.
To leave no stones unturned let's see what this
greetings(string)which is the message You will send to World. Here greetings is an operator name --- or a selector, quite like a method name --- and string is its argument type. Like method names, operator names are internal to a protocol. So a message (logically) in this interaction will/should consist of an envelope which is this operator name and its content which is a string.
But what is the use of this operator name? In OOPL we had a method dispatch table and we need to go to an appropriate code: but how does the operator name have use in interaction? Just as the mechanism of dynamics in OOPL, logically or as embodied in the design of VM (in the sense of JVM, not VM as in Xen), this operator name is closely tied to a key mechanism of conversation-based interaction which is a finite state automata which governs conversation behaviour. In brief an operator name serves as a transition label in FSA. So when a state in a FSA has several choices it is different labels which are used for this purpose. Of course logically (just like method names) it serves as a way to indicate what this message is about.
We shall come back to this point later. Here we note there is a simple way to go without an operator name and it is using a type name instead of an operator name, like (presenting the whole interaction):
chWorld.string from You to World;where we specify only the type, not a selector. This works well especially when you are sending a specific message type as in:
chWorld.Greetings from You to World;In such a case the name Greetingsserves as both the operator name and the message content.
To this topic we shall also come back later. I think this is enough as detailed examination of these basic constructs.
My original purpose was to introduce the next most basic constructs, sequencing and choice, after I briefly examined what we introduced already, but this prelude took long: I will continue with sequencing and choice in a new post, perhaps a couple of hours later.
