填充合金中的一組隨着時間的推移在一個完全連接的網絡

Question

跟進從this question ...

我有一個完全連通圖，這是偉大的。我也加入了時間概念。我現在正在圍繞我的圖傳遞數據的概念而掙扎。

我正在對一個系統進行建模，該系統的任務是確保每個節點都有一份已插入系統的數據副本。我已經掌握瞭如何做到這一點的程序，但是我正在努力將它翻譯成Alloy術語。

一個典型的算法將是這個樣子：

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個屬性：

• 獨特的短信發送（可恰在此時，一個簡單的變量）
• 集收到的消息（包括原始消息）

當所有DataMirrors具有相同的消息集時，系統會得到滿足。

例如，如果我們有：

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

我提前作出任何正式的邏輯電源用戶畏縮道歉......我我試圖在一場試火中學習這個:)。

Answer 1

您在非常低的層次上進行造型 - 如果您抽象，則會更清晰。

在下面的代碼中，我將文檔抽象爲一個簡單的二進制數據。每次所有節點都有數據（開）或不（關）。在下一步它將傳播到圖中的所有鄰居（不需要完成）。

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