2

この質問からのフォローアップ...

完全に接続されたグラフがあります。これは素晴らしいことです。時間の概念も追加しました。現在、グラフの周りにデータを渡すという概念に苦労しています。

システムに挿入されたデータのコピーが各ノードにあることを確認するタスクを持つシステムをモデル化しています。これを行う方法については頭の中に手順がありますが、それを合金の用語に翻訳するのに苦労しています。

典型的なアルゴリズムは次のようになります。

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

私の run 述語から、すべてのメッセージを 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'}

正式なロジックのパワーユーザーをうんざりさせてしまったことを前もってお詫びします...私は火の試練でこれを学ぼうとしています:)。

4

1 に答える 1

3

あなたは非常に低いレベルでモデリングしています --- 抽象化するとより明確になります。

以下のコードでは、ドキュメントを単純なバイナリ データに抽象化しています。毎回、すべてのノードにデータムがある (オン) か、ない (オフ) かのいずれかです。次のステップで、グラフ内のすべてのネイバーに伝播されます (完全である必要はありません)。

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
于 2012-11-30T16:04:58.653 に答える