This example choreography appears in the paper "AIOCJ: A Choreographic Framework for Safe Adaptive Distributed Applications". In the program, Bob and Alice want to find a free day to meet, scheduling an event for that day (e.g., going to the cinema).
include isFreeDay from "socket://localhost:8000"
include getTicket from "socket://localhost:8001"
preamble { starter: bob }
aioc {
end@bob = false;
while( !end )@bob{
scope @bob {
free_day@bob = getInput( "Insert your free day" );
proposal: bob( free_day ) -> alice( bob_free_day );
is_free@alice = isFreeDay( bob_free_day )
} prop { N.scope_name = "matching day"};
if( is_free )@alice {
scope @bob {
proposal: bob( "cinema" ) -> alice( event );
agreement@alice = getInput( "Bob proposes " + event +
", do you agree?[y/n]");
if( agreement == "y" )@alice{
end@bob = true;
book: bob( bob_free_day ) -> cinema( book_day );
ticket@cinema = getTicket( book_day );
{ notify: cinema( ticket ) -> bob( ticket )
| notify: cinema( ticket ) -> alice( ticket ) }
}
} prop { N.scope_name = "event selection" }
};
if( !end )@bob {
_r@bob = getInput( "Alice refused. Try to propose another day?[y/n]" );
if( _r != "y" )@bob{
end@bob = true
}
}
}
}
The code starts with some deployment information (Lines 1-4, discussed later).
The description of the behaviour starts at Line 6. The program is made by a cycle where Bob first checks when Alice is available and then invites her to the cinema. Before starting the cycle, Bob initialises the variable end to the boolean value false (Line 7). The variable is used to control the exit from the cycle. Note the annotation @bob, meaning that end is a local variable of Bob. The first instructions of the while cycle are enclosed in a scope (Lines 11-15), meaning that this part of the program may be adapted in the future. The first operation within the scope is the call to the primitive function getInput that asks to Bob a day where he is free and stores this date into the local variable free_day. At Line 13 the content of free_day is sent to Alice via operation proposal. Alice stores it in its local variable bob_free_day. Then, at Line 14, Alice calls the external function isFreeDay that checks whether she is available on bob_free_day. If she is available (Line 17) then Bob sends to her the invitation to go to the cinema via the operation proposal (Line 19). Alice, reading from the input, accepts or refuses the invitation (Line 20). If Alice accepts the invitation then Bob first sets the variable end to true to end the cycle. Then, he sends to the cinema the booking request via operation book. The cinema generates the tickets using the external function getTicket and sends them to Alice and Bob via operation notify. The two notifications are done in parallel using the parallel operator | (until now we composed statements using the sequential operator ;). Lines 18-28 are enclosed in a second scope with property N.scope_name = "event selection". If the agreement is not reached, Bob decides, reading from the input, if he wants to stop inviting Alice. If so, the program exits setting the variable end to true.
We remark the different meanings of the annotations @bob and @alice. When prefixed by a variable, they identify the owner of the variable. Prefixed by the boolean guard of conditionals and cycles, they identify the role that evaluates the guard. Prefixed by the keyword scope, they identify the process coordinating the adaptation of that scope. A scope, besides the code, may also include some properties describing the current implementation. These can be specified using the keyword prop and are prefixed by N. For instance, each scope of the example includes the property scope_name, that can be used to distinguish its functionality.
AIOCJ can interact with external services, seen as functions. This allows both to interact with real services and to have easy access to libraries from other languages. To do that, one must specify the address and protocol used to interact with them. For instance, the external function isFreeDay used in Line 14 is associated to the service deployed at the location "socket://localhost", reachable though port 8000 (Line 1). External functions are declared with the keyword include. To preserve deadlock freedom, external services must be non-blocking. After function declaration, in a preamble section, it is possible to declare the locations where processes are deployed. The keyword starter is mandatory and defines which process must be started first. The starter makes sure all other processes are ready before the execution of the choreography begins.
Now suppose that Bob, during summer, prefers to invite Alice to a picnic more than to the cinema, provided that the weather forecasts are good. This can be obtained by adding the following adaptation rule to one of the adaptation servers. This may even be done while the application is running, e.g., while Bob is sending an invitation. In this case, if Bob first try is unsuccessful, in the second try he will propose a picnic.
rule {
include getWeather from "socket://localhost:8002"
include getTicket from "socket://localhost:8001"
on { N.scope_name == "event selection"
and ( E.month > 6 or E.month < 9 ) }
do {
forecast@bob = getWeather( free_day );
if( forecast == "Clear" )@bob{
eventProposal: bob( "picnic" ) -> alice( event )
} else {
eventProposal: bob( "cinema" ) -> alice( event )
};
agreement@alice = getInput( "Bob proposes " + event + ", do you agree?[y/n]");
if( agreement == "y" )@alice{
end@bob = true |
if( event == "cinema" )@alice {
book: bob( bob_free_day ) -> cinema( book_day );
ticket@cinema = getTicket( book_day );
{ notify: cinema( ticket ) -> bob( ticket )
| notify: cinema( ticket ) -> alice( ticket ) }
}
}}}
A rule specifies its applicability condition and the new code to execute. In general, the applicability condition may depend only on properties of the scope, environment variables, and variables belonging to the coordinator of the scope. The condition of the rule above, introduced by the keyword on(Line 4), makes the rule applicable to scopes having the property scope_name equal to the string "event selection" and only during summer. This last check relies on an environment variable month that contains the current month. Environment variables are prefixed by E. When the rule applies, the new code to execute is defined using the keyword do (Line 6). In this case, the forecasts can be retrieved calling an external function getWeather (Line 7) that queries a weather forecasts service. This function is declared in Line 2. If the weather is clear, Bob proposes to Alice a picnic, the cinema otherwise. Booking (Lines 16-20) is needed only if Alice accepts the cinema proposal.
Click on the buttons below to download the code of this example.