alloy - 在完全连接的网络中随时间在 Alloy 中填充一组

Question

来自 this question 的跟进...

我有一个完全连接的图，这很棒。我还添加了时间的概念。我现在正在为围绕我的图表传递数据的概念而苦苦挣扎。

我正在建模一个系统，该系统的任务是确保每个节点都有一个已插入系统的数据副本。我脑子里有关于如何做到这一点的程序，但是我正在努力将其翻译成合金术语。

一个典型的算法看起来像这样:

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

为简单起见，假设每个节点都有一个独特的数据，并且它们必须向所有其他节点提供该数据。由于这是完全连接的，所以它应该相对简单(转换为合金/形式逻辑对我来说有点困难)。

这是我目前所在的位置:

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

从我的运行谓词中，您可以看到我希望在 20 个时间步长内发送所有消息，因此每个 DataMirror 应该有一组由 5 个唯一消息组成的数据。

我很确定我想要做的是让每个 DataMirror 有 2 个属性:

要发送的唯一消息(此时可以只是一个简单的变量)

收到的一组消息(包括原始消息)

当所有 DataMirror 具有相同的消息集时，系统才会满意。

例如，如果我们有:

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

那么系统将在以下情况下得到满足:

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'}

我提前为让任何正式的逻辑 super 用户感到畏缩而道歉......我正在尝试通过火试来学习这一点:)。

Answer 1

你是在一个非常低的层次上建模——如果你抽象的话会更清楚。

在下面的代码中，我将文档抽象为一个简单的二进制数据。每次所有的节点都有数据 (On) 或没有 (Off)。在下一步，它被传播到图中的所有邻居(不需要是完整的)。

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