• Orch orchName {
•    Role roleName{
•       Main() = Exp1;
•        ...
•    }
•        
• Role roleName1{
•       ...
•   }
• }

1 Variables

Each role can have local variables used inside the role. A variable is defined using the following syntax,

var knight  = 0;

where var is a keyword for defining a variable and knight is the variable name. Initially, knight has the value 0. Semi-colon is used to mark the end of the 'sentence' as above. We remark the input language of PAT is weakly typed and therefore no typing information is required when declaring a variable. Cast between incompatible types may result in a run-time exception. A fixed-size array may be defined as follows,

var board = [3, 5, 6, 0, 2, 7, 8, 4, 1];

where board is the array name and its initial value is specified as the sequence, e.g., board[0] = 3. The following defines an array of size 3.

var leader[3];

All elements in the array are initialized to be 0.

Note for multi-dimentional array: currently only one dimentional array is supported for the performance reason. However, multi-dimentional arraies can be easily simulated using one dimentional array. For example, a 4*3 two dimentional array [[1,1,1], [2,2,2], [3,3,3], [4,4,4]] can be represented easily using a simply array [1,1,1,2,2,2,3,3,3,4,4,4]. You only need to calculate index carefully to access the correct elements.

Variable range specification: users can provide the range of the variables/arrays explicitly by giving lower bound or upper bound or both. In this way, the model checker and simulator can report the out-of-range violation of the variable values to help users to monitor the variable values. The syntax of specifying range values are demonstrated as follows.

• var knight : {0..} = 0;
• var board : {0..10} = [3, 5, 6, 0, 2, 7, 8, 4, 1];
• var leader[N] : {..N-1};  //where N is a constant defined.

2 Processes

Each role expression can be composed by using the following operators.

Stop

The deadlock process is written as follows,

Stop

The process does absolutely nothing.

Skip

The process which terminates immediately is written as follows,

Skip

The process terminates and then behaves exactly the same as Stop.

Service Invoking/Invoked

In orchestration, one role inside the service can invoke the service provided by another role. One example of service invoking/Invoked is the following:

• channel B2S ; //The pre-established channel between the buyer and the seller
•    
• Role Buyer {
•      Main () = B2S!{Bch} -> Bch?Ack -> Skip;
• }
• {
•     Main =  B2S?{ch} -> ch!Ack -> Session();
• }

The above states that role Buyer invokes a service provided by role Seller through channel B2S.  {Bch} is a sequence of session channels which are created for this service invocation only. Note that the set of channel names in service invoking (e.g., {Bch}) needs not to be same as the set in service invoked (e.g., {ch}).  Each pair of service invoking and service invoked are treated as two actions in PAT, which means the service invocation is an asynchronous event.

Channel Input/Output

Once the service channel is established between two roles, the two roles can communication using the channels agreed in the service invocation. The following example demonstrates the idea.

• channel B2S ; //The pre-established channel between the buyer and the seller
•    
• Role Buyer {
•     Main () = B2S!{Bch} -> Bch?Ack.x -> Skip;
• }
• Role Seller {
•     Main =  B2S?{ch} -> ch!Ack.100 -> Session();
• }

In the first example, Seller ouput a message Ack to Buyer using channel ch, and Buyer input the Ack via this channel. Channel messages can be companied with a list of values. The values should be stored in the variables of the channel input.

Assignment

We support the update of the variables of a role. Without loss of generality, we always require that the variables constituting new value and the variable to be updated must be associated with the same role. The following example demonstrated the usage of assignment.

• Role Buyer {
•     var counter = 0;
•     Main () = (counter = 0) -> B2S!{Bch1} -> Bch1?Ack -> Session();
•     Session() = Bch1!QuoteRequest -> (counter = counter+1) -> Skip;
• }

Sequential composition

A sequential composition is written as,

P; Q

where P and Q are processes. In this process, P starts first and Q starts only when P has finished.

Choice

In Web Service module, we have only external choice, which is made by the environment, e.g., the observation of a visible event or the valuation of the variables. An choice is written as follows,

P [] Q

The choice operator [] states that either P or Q may execute. If P performs a visible event first, then P takes control. Otherwise, Q takes control.

The generalized form of choice is written as,

[] x:{1..n}@ P(x)                                - which is equivalent to P(1) [] ... [] P(n)

Conditional Choice

A choice may depend on a Boolean expression which in turn depends on the valuations of the variables. In PAT, we support the classic if-then-else as follows,

if (cond) { P } else { Q }

where cond is a Boolean formula. If cond evaluates to true, the P executes, otherwise Q executes. Notice that the else-part is optional. The process if(false) {P} behaves exactly as process Skip.

Case

A generalized form of conditional choice is written as,

• case {
•     cond1: P1
•     cond2: P2
•     default: P
• }

where case is a key word and cond1, cond2 are Boolean expressions. if cond1 is true, then P1 executes. Otherwise, if cond2 is true, then P2. And if cond1 and cond2 are both false, then P executes by default. The condition is evaluated one by one until a true one is found. In case no condition is true, the default process will be executed. 

Guarded process

A guarded process only executes when its guard condition is satisfied. In PAT, a guard process is written as follows,

[cond] P

where cond is a Boolean formula and P is a process. If cond is true, P executes. Notice that different from conditional choice, if cond is false, the whole process will wait until cond is true and then P executes. 

Interleaving

Two processes which run concurrently without barrier synchronization written as,

P ||| Q

where ||| denotes interleaving. Both P and Q may perform their local actions without referring to each other. Notice that P and Q can still communicate via shared variables or channels. The generalized form of interleaving is written as,

||| x:{0..n} @ P(x)

Recursion

Recursion is achieved through process referencing flexibly. The following process contains mutual recursion.

• P() = a -> Q();
• Q() = b -> P();
• System() = P() || Q();

It is straightforward to use process reference to realize common iterative procedures. For instance, the following process behaves exactly as while (cond) {P()};

Q() = if (cond) {P(); Q()};