3

Alloy で偶発的な故障をモデル化することは可能ですか?

たとえば、現在、さまざまな時間ステップでデータを隣接グラフに渡す接続グラフがあります。私がやろうとしているのは、モデルがリンクをランダムに強制終了できるようにする方法を見つけ出し、そうすることで、その目標を達成することです (すべてのノードのデータ状態がオンに設定されていることを確認する)。

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 
}
fact { 
  neighbours = ~neighbours   -- symmetric
  no iden & neighbours          -- no loops
  all n : Node | Node in n.*neighbours -- connected
  --  all n : Node | (Node - n) in n.neighbours -- comp. connected
}
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 5 Time, 10 Node

私がモデリングしようとしているソフトウェアは、不確実性を扱っています。基本的に、ノード間のリンクが失敗する可能性があり、ソフトウェアは別のパスに沿って再ルーティングします。私が Alloy でやりたいと思っていることは、リンクが特定のタイムステップで (できればランダムに) '死ぬ' ための機能を持たせることです。最上位の事実として、私はグラフを完全に接続する機能を持っているため、リンクが停止した場合、別のリンクがたるみを拾う可能性があります (simple_change が Datum の状態を On に切り替えるため)。接続されているすべてのネイバー)。

編集：

それで、提案されたとおりに実行したところ、次のエラーが発生しました。タイプエラー
隣人とノードがまだ設定されていると思っていたので、混乱していますか?

これが私の更新されたコードです：

open util/ordering[Time]
open util/relation

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

sig Time{
  neighbours : Node->Node,
  state:Node->one Datum         // at each time we have a network state
}{
  symmetric[neighbours, Node]
}
abstract sig Node{
  neighbours:set Node
}

fact { 
  neighbours = ~neighbours   -- symmetric
  no iden & neighbours          -- no loops
--  all n : Node | (Node - n) in n.neighbours -- comp. connected
  all n : Node | Node in n.*neighbours -- connected
}

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

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

  all t:Time-last | next[t].neighbours in t.neighbours
  all t:Time-last | lone t.neighbours - next[t].neighbours
}

run {} for 10 Time, 3 Node
4

1 に答える 1

3

近傍の定義を Time に移動します。

sig Time {neighbours : Node->Node, ....}

各時点に対する近隣の対称性などに関する事実を再表現する必要があります。これは、拍子記号の不変部分で実行することによって最も簡単に実行できます。

sig Time {
  neighbours : Node->Node,
  ...
}{
  symmetric[neighbours, Node],
  ....
}

open util/relation(などの便利な定義をロードするには、 を使用することをお勧めしますsymmetric。)

次に、次のsimple_changeような事実を追加することにより、時間ステップを複雑にすることができます

next[t].neighbours in t.neighbours

任意に多くのアークを捨てることができます。

各ステップで破棄されるアークの数を制限したい場合は、次のような事実をさらに追加できます。

lone t.neighbours - next[t].neighbours

これにより、処分が最大 1 つのアークに制限されます。

于 2012-12-05T06:10:32.557 に答える