从这个问题跟进...
我有一个完全连通的图,这很棒。我也加入了时间的概念。我现在正在为围绕我的图表传递数据的概念而苦苦挣扎。
我正在为一个系统建模,该系统的任务是确保每个节点都有一个已插入系统的数据副本。我脑子里有关于如何做到这一点的程序,但是我正在努力将其翻译成合金术语。
一个典型的算法看起来像这样:
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'}
我为让任何形式逻辑的高级用户畏缩而提前道歉......我正试图在试炼中学习这一点:)。