Gossiping system

This toy example considers a system that illustrates how name passing
can influence the evolution of the structure of a system, and shows how
one can specify simple properties using the spatial logic to observe this
structural evolution.

We start off by defining the simpler kinds of behavior in our system. Firstly
a Gossiper process that is always able to spread some information around,
by means of taking this information as a name parameter and trying to emit
it on public channel gossip, after which continuing with the dissemination intent
considering the same piece of information.

defproc
    Gossiper(info) = gossip!(info).Gossiper(info);

Then we define the Listener process that is eager to learn some information,
using a reception on channel gossip to that end, after which wanting to spread
this received name around and hence becoming a gossiper.

defproc
    Listener = gossip?(info).Gossiper(info);

Finally we define the System which is made of three Listeners and one Gossiper,
considering a restricted name to be the piece of information to be disseminated
by the Gossiper which initially is the only process to know this secret.

defproc
    System =
        new secret in
        ( 
            Gossiper(secret)
            | Listener
            | Listener
            | Listener
        );

This system will clearly evolve at each step by a synchronization between a Listener
and a Gossiper being this secret disclosured to one more Listener at a time. Since the
secret is a restricted name each time that happens the Listener joins in the circle of
trust of the secret, and the spatial bound created by the sharing of a restricted name
makes the processes indivisible. Hence if at the starting point there where 4 distinct
processes after one internal synchronization (<> or < tau >) there are only 3, then 2
after two steps and finally 1 after three steps when all processes share the secret.
We check to see if our system specification satisfies this description.

check System |= 4 and (<> 3) and (<><> 2) and (<><><>1);

We then specify concretely this name sharing property, starting by defining a formula
that states that the argument property is true in every single point of the system.

defprop everywhere(A) = (false || (1 => A));

We reuse this last property to define another that states that a given name is present
everywhere.

defprop everybody_knows(secret) = everywhere(@secret);

After that we define a property that says that there is a restricted name which will be
at some point in time known everywhere in the system. The hidden quantification reveals
the restricted name, i.e. opens up the spatial bound induced by it, therefore allowing
the observation of the inner distinct components that were bound together.

defprop everybody_gets_to_know = 
    hidden secret.eventually everybody_knows(secret);

Finally we check our system specification to see if it satisfies this specification.

check System |= everybody_gets_to_know;

Going one step further we now intend to specify that our system will be, at some point in
time, made exclusively out of Gossipers. We start by defining what is a gossiper and that
amounts to say that it is a process that is always able to emit on channel gossip.

defprop gossiper_forever = maxfix X.(< gossip! > true and [*]X);

Then we specify systems that internally, i.e. underneath all restricted names, are made
exclusively out of Gossipers.

defprop all_gossipers = eventually inside everywhere(gossiper_forever);

Finally we check to see if our system satisfies this specification.

check System |= all_gossipers;