Gossiping girls

In my class on UPPAAL (a modeling and analysis tool for communicating FAs aka CFAs), I gave the following (classic) exercise:

A number of girls initially know one distinct secret each. Each girl has access to a phone which can be used to call another girl to share their secrets. Each time two girls talk to each other they always exchange all secrets with each other (thus after the phone call they both know all secrets they knew together before the phone call). The girls can communicate only in pairs (no conference calls) but it is possible that different pairs of girls talk concurrently.

Sounds like fun, right? Before, I discuss a sample solution in UPPAAL, let's consider some alternative frameworks which we could use to code up the above problem.

Here's a solution using CHR (Constraint Handling Rules):

  Girl(name1,secrets1), Girl(name2,secrets2) <==> 
         newSecrets(secrets1,secrets1) | let s=shareSecrets(secrets1,secrets2)
                                         in Girl(name1,s)
                                            Girl(name2,s)

What about using Join-patterns extended with guards and synchronous method calls:

   Girl(name1,secrets1) & Girl(name,secrets2) = do 
                              secrets1 := secrets1 `union` secrets2
                              secrets2 := secrets2 `union` secrets2

Okay, so finally my UPPAAL solution. First, the declarations plus description. The actual CFA is displayed below.

// =========================
// == Global declarations ==

// We introduce two channels. First, I thought we can do with just
// one channel but then I believe things will get really messy.

chan call, call2;

// We assume that there are three secrets: one, two and three

// To pass secrets among girls we introduce three (global) variables, 
// one for each secret.
// The value 0 indicates that the secret is not present (ie known).
// The value 1 indicates that the secret is known.

int var_s1, var_s2, var_s3;

// The actual transmission of values is performed in two steps:
//  1. First the caller tranfers her secrets
//  2. Then, it's the callee's turn to transfer her secrets.
// We must guarantee that this step happens atomically between
// two parties. We can either (a) use the UPPAAL feature of
// committed locations or (b) we simply transmit the callers identity 
// which then the callee transmits back for verification. 
// Option (a) sounds too easy, almost cheating :),
// so we'll pursue option (b). 

// To transmit the callers identity, we'll need another "message-passing" variable.

int var_id;

// WARNING: We use here the initial_secret as a unique identifier
// which implies that we only supports girls which initially now
// a distinct secret.

// Please check the declarations of the girl template which
// describes the ideas and functionality of the CFA.

// =======================================
// == Declarations of the girl template ==

// Three variables to represent the girl's knowledge/status about
// the three secrets.

// We will initialize the variables when instantiating
// the girl template. The input parameter initial_secret
// refers to the secret that's initially known.

int s1, s2, s3;

// local variables to store the transmitted messages (secrets and caller id)

int in1, in2, in3, in_id;

// The first step of the girl CFA is to record (locally) the initially known
// secret. View as programming if-then-else statements using CFA transitions.
// If initial_secret == 1 then s1 = 1, s2 = 0, s3 = 0
// else and so on

// It gets interesting once we reach the "Start" state.
// In the first stage, we can either make a call, via "call!", or receive a call via "call?".
// In case we're the caller, we transmit our secrets and our identity (in form of the
// initial_secret). In case we're the receiver of the call, we're storing the
// transmitted values. Then, in the second stage, the roles switch and the caller 
// becomes the receive and vice versa. Notice the use of a different channel.
// This is to avoid that a caller of the first stage can interact with a receiver
// of the second stage. We yet need to check that the caller and receiver of the
// first stage are still the same for the second stage. We perform this check
// in state "Verify" by comparing the transmited identify with our own (the initial_secret).
// A point to note is that this check is only performed by the receiver
// of the second stage.
// States "Update_Secrets1" and "Update_Secrets2" then update the secrets after the
// exchange. The formula (x+y) - (x*y) evaluates to 1 or 0 for values 0 and 1.
// Sure, this could be done smarter using bit operations or simply using UPPAAL's
// C-style array.

// =========================
// == System declarations ==

girl1 = Girl(1);
girl2 = Girl(2);
girl3 = Girl(3);

// List one or more processes to be composed into a system.
system girl1, girl2, girl3;

And finally the CFA:
Girl

Get your own at Scribd or explore others:

So, which solution do you prefer? To be fair, UPPAAL is not meant for programming, it has its strength in analyzing CFAs via its expressive query language and model checker.