Populating a set over time in Alloy in a completely connected network

Question

Followup from this question...

I have a completely connected graph, which is great. I've also added in the concept of time as well. I am now struggling with the concept of passing data around my graph.

I am modeling a system that has the task of ensuring that each node has a copy of data that has been inserted into the system. I have the procedure in my head as to how to do this, however I'm struggling with translating that into Alloy terminology.

A typical algorithm would look something like this:

For i = 0 to TIME_STEPS:
  For each node in {nodes}:
    Check all other nodes and, if necessary, provide a copy of the data 
    if they do not currently have it

For simplicity sake, lets say that each node has a unique piece of data, and they have to provide that piece of data to all other nodes. Since this is completely connected, it should be relatively straightforward (translating to Alloy/formal logic is a bit more difficult for me).

This is where I'm at currently:

open util/ordering[Time] as TO
module rdm4

----- signatures
sig Time {}

sig DataMirror {
  link: set DataMirror,
  toSend: DataMirror -> Time
}

----- facts

// model network of completely connected data mirrors
fact completely_connected {
      link = ~link          -- symmetrical
      no iden & link     -- no loops
      all n : DataMirror | (DataMirror - n) in n.link -- completely connected
}

// can't send to self
--fact no_self_send {
--  no d: DataMirror | d.toSend = d.link.toSend
--}

------ predicates
pred init [t: Time] {
  all p: DataMirror | p.toSend.t = p
}

pred show() { }
run show for exactly 5 DataMirror, 20 Time

From my run predicate, you can see that I'd like to have all messages sent within 20 time steps, so each DataMirror should have a set of data that is comprised of 5 unique messages by that time.

I'm pretty sure that what I want to do is to have each DataMirror have 2 properties:

• Unique message to send (can be just a simple variable at this point)
• Set of messages received (including original message)

The system would be satisfied when all DataMirrors have the same set of messages.

For example, if we have:

DataMirror1.starting_data = 'a'
DataMirror2.starting_data = 'b'
DataMirror3.starting_data = 'c'
DataMirror4.starting_data = 'd'
DataMirror5.starting_data = 'e'

then the system would be fulfilled when:

DataMirror1.data_set = {'a', 'b', 'c', 'd', 'e'}
DataMirror2.data_set = {'a', 'b', 'c', 'd', 'e'}
DataMirror3.data_set = {'a', 'b', 'c', 'd', 'e'}
DataMirror4.data_set = {'a', 'b', 'c', 'd', 'e'}
DataMirror5.data_set = {'a', 'b', 'c', 'd', 'e'}

I apologize in advance for making any formal logic power-users cringe...I'm trying to learn this in a trial by fire :).

Answer 1

You are modelling at a very low level --- it is clearer if you abstract.

In the code below I abstract the document to a simple binary datum. At each time all of the nodes either have the datum (On) or not (Off). At the next step it is propagated to all neighbours in the graph (which does not need to be complete).

open util/ordering[Time]

enum Datum{Off, On} // A simple representation of the state of each node

sig Time{state:Node->one Datum}// at each time we have a network state

abstract sig Node{
neighbours:set Node
}{
all n : neighbours| this in n.@neighbours} // symmetric

fact start{// At the start exactly one node has the datum
one n:Node|first.state[n]=On}

fact simple_change{ // in one time step all neighbours of On nodes become on
all t:Time-last |
    let t_on = t.state.On |
    next[t].state.On = t_on+t_on.neighbours}

run {} for 9 Time, 4 Node