*contributed by Christian Krause*

The example requires Henshin 0.9.3 or higher.
It shows how to use nested rules to match subpatterns and how to generate and analyze state spaces. The example is known as the *Gossiping Girls Problem*. The metamodel is very simple: it consists of a class *Girl* and a class *Secret*. Girls know those secrets to which they have a reference to. Two girls can exchange their secrets by making a phone call with each other. For example, if girl A knows the secrets 1 and 2, and girl B knows the secrets 3 and 4, then after the phone call both girls know the secrets 1,2,3,4.

The problem to solve is as follows. Given N girls each knowing a secret that no other girl knows. How many phone calls are necessary so that every girl knows all the secrets?

This problem can be modeled nicely in Henshin. We only need one rule for modeling phone calls, and one rule for adding girls and secrets (for creating initial configurations). The two rules are shown below.

The rule *addGirl* creates a new girl and a new secret that only she knows. The annotation *@Container* says that the two created objects should be added to the contents of an existing object of type *Container*. By invoking this rule N times, we can create the initial configuration for N girls.

The rule *exchangeSecrets(g1,g2)* is used to model phone calls. The parameters *g1,g2* identify the girls which make the phone calls. If these parameters are not set, Henshin nondeterministically selects two arbitrary girls. The rule has one nested rules to describe the *for-all* semantics for exchanging secrets. That means, for girl *g1* all of her secrets which girl *g2* does not know will be matched (ensured using the forbid* edge). Analogously for girl *g2*. The application of the rule then adds between every pair of girl and secrets (that she doesn't know) a new edge between them. Thus, after applying this rule, both girls know all secrets (their owns and the ones from the other girl).

To solve the gossiping girls problem, we generate the state space with Henshin and search for the shortest path leading to a state where all girls know all secrets. The state space generation can be done in the State Space Explorer or in Java as done in the GossipingGirls class. The figure below shows the state space for 4 girls generated in the state space explorer.

The green state is the initial state. State 12 is the target state in which all girls know all secrets. We use the following OCL constraint to identify the target states:

girls->forAll(g : Girl | g.secrets->size()=girls->size())

which basically says that for all girls it holds that the number of secrets that she knows is equal to the number of girls there exists. To determine the minimum number of phone calls required, select the validation tool

The table below shows the number of states and transitions and the minimum number of phone calls as computed by Henshin. The benchmark was conducted on a Intel(R) Xeon(R) CPU @ 2.50GHz with 8GB of main memory. Note that it is important to set the state space property *ignoreDuplicateTransitions* to true here to be able to get to level 8.

Girls | States | Transitions | Calls | Generation Time | Checking Time |
---|---|---|---|---|---|

2 | 2 | 2 | 1 | 59ms | 3ms |

3 | 4 | 6 | 3 | 88ms | 4ms |

4 | 13 | 31 | 4 | 221ms | 5ms |

5 | 52 | 198 | 6 | 733ms | 12ms |

6 | 357 | 2,092 | 8 | 2,891ms | 66ms |

7 | 3,689 | 33,392 | 10 | 12,545ms | 721ms |

8 | 62,857 | 827,963 | 12 | 510s | 430s |