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,
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;