The protocol definition is comprised of a:

• Imports
  A list of import statements that can reference types (messages or other
  protocols) in other namespaces, optionally providing a URL to the
  detailed information about the type.

• Protocol unit
  The protocol definition contains a single top level protocol unit, with
  a name that is scoped to the previously defined namespace.
  The syntax for the process definition is:

( import [ <TypeSystem> ]
			[ "<DataType>" as ] <name>
			( "," [ "<DataType>" as ] <name> )*
			[ from "<Location>" ] ";" )*

protocol <name> [ "at" <Role> ] "(" ( role | <Type> ) <name>
	    ( "," role | <Type> ) <name> )* ")" "{"
    .... ";"
"}"

The import statement is used to define a type that will be used within the protocol definition.
When referenced in the protocol, the type is known by a local name (or alias). If we want to be
able to monitor, or use the protocol definition in any other 'real world' situation, then we
need to bind the concrete type information to this alias.

The import statement can optionally define a type system associated with the imported type.
For example, this could be 'java' if referring to a Java class or interface, or 'xsd'
for an XSD type or element.

Within the type information, we can identify a specific data type, followed by
the 'as' keyword and then the name of the type alias.

The import can optionally specify the location of the type information, by specifying the
'from' keyword followed by a string literal with type system specific location information.

In its simpliest form, the import can just define the type name, which will be represented
without any type system specific information. The next level can introduce a type specific
'data type' value. Finally the most complete version will include the location of the
type information.

Following the import statements is the declaration of the protocol unit
itself. This defines the name of the protocol and whether it is located at
a particular role.

The following represents a 'global' protocol example:

import Customer;

import xsd "{http://www.acme.org/Purchasing}Order" as Order,
	"{http://www.acme.org/Purchasing}Quote" as Quote
	from "../schema/MySchema.xsd";

import java "Order" as Order,
	"Quote" as Quote
	from "org.scribble";

protocol PurchaseGoods (role Buyer) {
    Buyer introduces Seller;
    Order from Buyer to Seller;
    ....
}

This example shows three variations of the import statement.
The first importing a single type based on a
name, without any concrete type information being bound.

The second importing a particular XSD schema, from a
schema location, and referring to two specific types within the schema.
The first being an XSD type, known by the qualified name
{[http://www.acme.org/Purchasing]}Order and
locally referred to using the alias Order.
The second being an XSD element, known by the qualified name
{[http://www.acme.org/Purchasing]}Quote and
locally referred to using the alias Quote.

The third import statement shows the case where two Java classes
are bound to local aliases. The Java package is specified
within the 'from' clause, and the class name is defined prior
to the 'as' keyword in each case.

The global protocol is then defined, named as PurchaseGoods.
This is a global protocol because it does not specify a particular
role at which the definition is located.

A local protocol variation would be:

protocol PurchaseGoods at Buyer (role Buyer) {
    Buyer introduces Seller;
    Order to Seller;
    ....
}

This local representation of the protocol defines the behaviour from the Buyer
role's perspective. That is why the interaction defined within the protocol unit only
include the 'to role' Seller, as this is the role with which the
Buyer is going to communicate. The Buyer role in the interaction is implied from the located role of the local protocol.

The protocol can also be defined with parameters, to allow other protocols to invoke them
with specific values. Below is a variation of the previous example, with the roles
passed into the protocol instead.

protocol PurchaseGoods(role Buyer, role Seller) {
    ....
}

The way in which another protocol can be invoked will be presented in a subsequent
section.