/* GOSSIPING SYSTEM */

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

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

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

/* PROPERTIES */

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

/***/

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

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

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

check System |= everybody_gets_to_know;

/* ---------- */

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

defprop all_gossipers = eventually inside everywhere(gossiper_forever);

check System |= all_gossipers;