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
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,
defproc Listener = gossip?(info).Gossiper(info);Finally we define the System which is made of three Listeners and one Gossiper,
defproc System = new secret in ( Gossiper(secret) | Listener | Listener | Listener );This system will clearly evolve at each step by a synchronization between a Listener
check System |= 4 and (<> 3) and (<><> 2) and (<><><>1);We then specify concretely this name sharing property, starting by defining a formula
defprop everywhere(A) = (false || (1 => A));We reuse this last property to define another that states that a given name is present
defprop everybody_knows(secret) = everywhere(@secret);After that we define a property that says that there is a restricted name which will be
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
defprop gossiper_forever = maxfix X.(< gossip! > true and [*]X);Then we specify systems that internally, i.e. underneath all restricted names, are made
defprop all_gossipers = eventually inside everywhere(gossiper_forever);Finally we check to see if our system satisfies this specification.
check System |= all_gossipers;