Gossips

Contribution of this section

  1. use of sets,
  2. exercise with abstract datatypes, and
  3. complicated µ-calculus formulae.

New tools: none.

Initially, each of five teenage schoolgirls Ann, Beth, Carol, Daisy, and Elvy, knows a unique, new, thrilling gossip. They urge to phone each other to exchange all the gossips they know, thus sharing the same gossips right after the phone call. We wonder, what is the minimum number of phone calls that have to take place such that all five girls know all the five new gossips?

In a naive approach for a solution of sharing all gossips, Ann calls Beth, Carol, Daisy and Elvy in a row, collecting all four other gossips. Note that gradually Ann has more gossips to share, because she knows the gossips of the girls she has called so far. For example, finishing her fourth call both Ann and Elvy know all gossips. Next, Ann calls three others, say Daisy, Carol and Beth, to bring them up to date with all the latest news. This takes 7 phone calls in total.

In our modelling below, we choose to index the five gossips by numbers from 1 up to 5. If one girl knows the gossips 1 and 4, and another girl knows gossips 2, 3 and 4, then the two girls both know the gossips 1, 2, 3 and 4 after talking to each other on the phone.

A model using sets of positive integers is given below (also available as gossip-blanks.mcrl2. Dealing with sets, we first introduce constants N and Gossips of type Pos and Set(Pos), respectively. For the definition of the set Gossips we use set comprehension, Gossips comprises all positive k such that 1 < k <= N.

map N: Pos;
    Gossips: *1*;
eqn N = 5;
    Gossips = { k:Pos | 1 <= k  && k <= *2* };

act done, all_done;
    call, answer, exchange: Pos # Pos # Set(Pos) # Set(Pos);

proc Girl(myid:Pos,mygs:Set(Pos)) =
     sum herid:Pos, hergs:Set(Pos) . (
         ( myid != herid ) -> (
             ( call(myid,herid,mygs,hergs)
               + answer(herid,myid,hergs,mygs) ) .
             Girl(myid,mygs + hergs) ) ) +
     ( mygs == Gossips ) -> done . delta;

proc Girl_init(id:Pos) = Girl(id,{id});

init allow({exchange,all_done},
     comm({call|answer -> exchange,
     done|done|done|done|done-> *3* },
       Girl_init(1) || Girl_init(2) || Girl_init(3) || 
       Girl_init(4) || Girl_init(5)
     ));

We distinguish the actions done, that indicate that a particular girl has gathered all gossips, and all_done, that indicates that all girls know all gossips. Furthermore, we have actions call, answer and exchange for initiating a phone call, picking up the phone, and the synchronized execution of these two. Note the type of the latter three actions: Pos # Pos # Set(Pos) # Set(Pos), two identifiers for the caller and callee, two gossip sets to reflect their respective knowledge at that moment.

For each of the girls, we define a process Girl carrying an identifier myid, a positive integer, and the current knowledge of gossips mygs, a set of positive integers, as parameters. Basically, a girl with identifier myid can either phone another executing the action call or answer the phone of another executing the action answer. As the actions have place holders for the identifier and gossips of the other girl, the summation sum herid:Pos, hergs:Set(Pos) quantifies over all possible values, thereby binding the variables herid and hergs. After excuting either a call or answer action, the knowledge of girl owning the process gets update, it know incorporates the knowledge of the other girl too.

As termination condition for one Girl process, we will have equality of the latest gossip knowledge parameter of the process and the set constant Gossips. If all Girl processes are done, i.e. can perform the done action, they can synchronize yielding the action all_done. The delta explicitly terminates the process.

Exercise

Fill in the blanks in gossip-blanks.mcrl2 This means you will have to

  • determine the type of the function Gossips,
  • finish the definition of the equation for Gossips, and
  • finish the communication definition.

Solution

Gossips is a constant of type Set(Pos), with equation Gossips = Gossips = { k:Pos | k >= 1 && k <= N }. The communication enforces the done actions to communicate to all_done.

When these modifications have been made, the specification looks as follows (gossip.mcrl2)

% N Gossiping girls

% Note: when changing N, change the init process accordingly!
map N: Pos;
    Gossips: Set(Pos);
eqn N = 5;
    Gossips = { k:Pos | k >= 1 && k <= N };

act done,all_done;
    call,answer,exchange: Pos # Pos # Set(Pos) # Set(Pos);

proc Girl(id:Pos,knowledge:Set(Pos)) =
       sum i:Pos, s:Set(Pos) . (
         ( id != i ) -> (
           (call(id,i,knowledge,s) + answer(i,id,s,knowledge)) 
           . Girl(id,knowledge + s) )
       )
       +
       (knowledge == Gossips) -> done . Girl(id,knowledge);

proc Girl_init(id:Pos) = Girl(id,{id});

init allow({exchange,all_done},
     comm({call|answer -> exchange,
     done|done|done|done|done->all_done},
       Girl_init(1) || Girl_init(2) || Girl_init(3) || 
       Girl_init(4) || Girl_init(5)
     ));

Exercise

Generate the state space for gossip.mcrl2

Hint

If you think verification takes a long time add the -v flag to lps2lts, this will show you progress messages. If you are on a platform other that Windows, you can also pass the -rjittyc flag to lps2lts to use the compiling rewriter. This is more efficient than the default jitty rewriter.

Solution

We run the following commands:

$ mcrl22lps gossip.mcrl2 gossip.lps
$ lps2lts -v -rjittyc gossip.lps gossip.lts
  [09:02:44.255 verbose] Detected mCRL2 extension.
  [09:02:44.256 verbose] removing unused parts of the data specification.
  [09:02:44.262 verbose] using 'mcrl2compilerewriter' to compile rewriter.
  [09:02:44.274 verbose] compiling rewriter...
  [09:02:46.764 verbose] loading rewriter...
  [09:02:46.765 verbose] writing state space in lts format to 'gossip.lts'.
  [09:02:46.765 verbose] generating state space with 'breadth' strategy...
  [09:02:46.766 verbose] monitor: level 1 done. (1 state, 20 transitions)
  [09:02:46.769 verbose] monitor: level 2 done. (10 states, 200 transitions)
  [09:02:46.795 verbose] monitor: level 3 done. (75 states, 1500 transitions)
  [09:02:46.971 verbose] monitor: level 4 done. (430 states, 8600 transitions)
  [09:02:47.229 verbose] monitor: currently at level 5 with 1000 states and 20000 transitions explored and 3556 states seen.
  [09:02:47.770 verbose] monitor: currently at level 5 with 2000 states and 40000 transitions explored and 5961 states seen.
  [09:02:47.927 verbose] monitor: level 5 done. (1725 states, 34500 transitions)
  [09:02:48.417 verbose] monitor: currently at level 6 with 3000 states and 60000 transitions explored and 6974 states seen.
  [09:02:49.179 verbose] monitor: currently at level 6 with 4000 states and 80000 transitions explored and 7601 states seen.
  [09:02:49.901 verbose] monitor: currently at level 6 with 5000 states and 100000 transitions explored and 8203 states seen.
  [09:02:50.633 verbose] monitor: currently at level 6 with 6000 states and 120000 transitions explored and 8844 states seen.
  [09:02:50.986 verbose] monitor: level 6 done. (4180 states, 83600 transitions)
  [09:02:51.631 verbose] monitor: currently at level 7 with 7000 states and 140001 transitions explored and 9152 states seen.
  [09:02:52.698 verbose] monitor: currently at level 7 with 8000 states and 160001 transitions explored and 9152 states seen.
  [09:02:53.730 verbose] monitor: currently at level 7 with 9000 states and 180001 transitions explored and 9152 states seen.
  [09:02:53.871 verbose] monitor: level 7 done. (2731 states, 54621 transitions)
  [09:02:53.871 verbose] Starting to save file gossip.lts
  [09:03:16.396 verbose] done with state space generation (7 levels, 9152 states and 183041 transitions)

Next we are going to investigate some properties of the gossiping girls.

Exercise

Verify that the model is deadlock free.

Solution

There are several approaches to verifying absence of deadlock. We discuss three of them.

  1. The first approach instructs lps2lts to report deadlocks; if no deadlock is reported, the system is deadlock free, using the -D option. We also instruct the tool to save a trace to the deadlock, and terminate once a deadlock has been found using the option:-t1:

    $ lps2lts -rjittyc -D -t1 gossip.lps
    

    This does not report anything, so the specification is deadlock free.

  2. Assuming we already have the transition system, say in gossip.lts, we can also use the marking facilities of ltsview to check for absence of deadlock. We perform the following steps:

    $ ltsview gossip.lts
    

    Now open the Mark dialog through Tools ‣ Mark.... In this dialog select Mark deadlocks. Now any cluster in the state space containing a deadlock will be coloured red, and the deadlock state is also coloured red.

    This method does not colour any states and clusters for the gossiping girls, so the system is deadlock free.

  3. The third approach uses the µ-calculus to perform the verification. Absence of deadlock can be specified as follows (gossip1.mcf):

    % Deadlock freedom
    
    [true*]<true>true
    

    We can now verify this using lps2pbes and pbes2bool:

    $ lps2pbes -f gossip1.mcf gossip.lps gossip1.pbes
    $ pbes2bool -rjittyc gossip1.pbes
    true
    

Exercse

It is straightforward to see that for N gossiping girls, there is a path of length (N - 1) + (N - 2) states leading to the situation where all girls know all gossips. Simply have the first girl call all other (N-1) girls; then the first and the last girl know all gossips. Then the first girl calls the N - 2 remaining girls.

Verify this claim for N = 5, i.e. show that for 5 gossiping girls, there is a path of 7 phone calss to the situation where all girls know all gossips.

Solution

Again we can pursue various different paths in this verification. We will illustrate three of them.

  1. The first approach uses the µ-calculus to formalise the property. Because we are in the finite case, it is tempting to choose the following formalisation (gossip3.mcf).

    % There is a path of length 7 leading to the situation where all
    % girls know all gossips (true)
    
    <!all_done><!all_done><!all_done><!all_done>
    <!all_done><!all_done><!all_done><all_done>true
    

    This simply says that there is a path of length 7 to a state in which an all_done action can be performed.

    However, if we try to verify this property using:

    $ lps2pbes -f gossip3.mcf gossip.lps | pbes2bool -rjittyc
    

    It seems that lps2pbes is getting stuck. This is caused by the translation of µ-calculus formula with an LPS to a PBES, that has to look ahead 8 levels in the state space, by recursively evaluating the guards in the LPS. This causes a vast blowup in the computations that are performed internally. We can restrict the number of levels that the tool needs to look ahead by introducing fixed points as is done in (gossip3a.mcf):

    % There is a path of length 7 leading to the situation where all
    % girls know all gossips (true)
    
    % This formula has bogus fixed points to make sure lps2pbes does
    % not have to look ahead through the conditions of the entire
    % state space.
    
    mu X1 . <!all_done><!all_done>
    mu X2 . <!all_done><!all_done>
    mu X3 . <!all_done><!all_done>
    mu X4 . <!all_done><all_done>true
    

    Using this formalisation leads to blow up in the number equations in the PBES, hence generating the PBES has become more efficient, but the solving process may be slower, but does succeed:

    $ lps2pbes -f gossip3a.mcf gossip.lps | pbes2bool -rjittyc
    true
    
  2. The µ-calculus formulae in the previous approach must be modified if the value of N is changed, which is, in most cases, undesirable. The µ-calculus used in mCRL2 supports parameterisation with data. We can use this functionality to write a formula for this property for arbitrary values of N as follows (gossip2.mcf).

    % There is a path of length (N - 1) + (N - 2) states
    % leading to the situation where all girls know all gossips (true)
    
    mu X(n:Nat=0) . (val(n <  (N - 1) + (N - 2)) && <!all_done> X(n+1))
                 || (val(n == (N - 1) + (N - 2)) && <all_done> true)
    

    Here the number of actions that has been performed so far is counted by the parameter n of the formula.

    We verify the property using:

    $ lps2pbes -f gossip2.mcf gossip.lps | pbes2bool -rjittyc
    true
    

    Verification of the property using this formula is quick.

  3. As a final approach, we see whether we can use the facilities of lps2lts to search for an action. We use the knowledge that all_done is performed when all girls know all gossips. We store traces to the occurrences of all_done:

    $ lps2lts -rjittyc -aall_done -t gossip.lps
    [13:36:38.405 info]    detect: action 'all_done' found and saved to 'gossip.lps_act_0_all_done.trc'(state index: 6571).
    

    A trace has been saved to gossip.lps_act_0_all_done.trc; we inspect the trace:

    $ tracepp gossip.lps_act_0_all_done.trc
    exchange(4, 5, {4}, {5})
    exchange(3, 4, {3}, {4, 5})
    exchange(2, 1, {2}, {1})
    exchange(2, 3, {1, 2}, {3, 4, 5})
    exchange(3, 5, {1, 2, 3, 4, 5}, {4, 5})
    exchange(4, 1, {3, 4, 5}, {1, 2})
    all_done
    

    We see that the only trace that we stored is six exchanges long, instead of the seven exchanges that we are looking for. The previous approach proved that there is a path of seven exchanges though. This can be explained by the way in which lps2lts generates traces. When searching for an all_done action, the tool will save the trace to the state that is reached with the all_done action. It will, however, only store one trace per state that is reached, i.e. if there is another path to the state doing the all_done action, it will not store this trace. As a result, this approach cannot be used for the verification task at hand.

Exercise

As a last exercise, check whether or not there is a path shorter than (N-1)+(N-2) leading to the situation where all girls know all gossips.

Solution

Again various approaches are possible here. We discuss two of them.

  1. In the previous exercise, we generated a trace to an all_done action using lps2lts. The trace comprised six exchanges, so we easily verify that a trace shorter than 7 exchanges to the situation in which all girls know all gossips is possible.

  2. The second approach formalises this property using the modal µ-calculus. The following, propositional µ-calculus formula (gossip4.mcf) expresses the property.

    % There is no path of length < (N-1)+(N-2) leading to the situation
    % where all girls know all gossips (true)
    
    nu X(n:Nat = 0) . val(n < (N-1)+(N-2)) =>
                        ([true] X(n+1) && [all_done] false)
    

    We verify this using the following commands:

    $ lps2pbes -f gossip4.mcf | pbes2bool -rjittyc
    false
    

    Indeed the property does not hold, as we also observed from the lps2lts output.

Note

In all the verification above, the command pbes2bool can be replaced by pbespgsolve. The latter uses a different algorithm for doing the actual verification; it first translates the pbes into a parity game, and then solves the parity game.

Note

For N >= 4, the minimal number of calls that needs to be made is 2N - 4, as was shown in [Hur00].

[Hur00]C.A.J. Hurkens. Spreading gossip efficiently. Nieuw Archief voor Wiskunde, Vol. 5/1, No. 2, p208-. 2000. (PDF)