Gossips
Contribution of this section
use of sets,
exercise with abstract datatypes, and
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 indicates 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 a girl owning the process gets updates, it now
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
, andfinish 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.
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.
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 . 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.
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.
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
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 ofN
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.
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 ofall_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 theall_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 theall_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.
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.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].