alloy - 在 Alloy 的连通图中对随机故障建模

Question

是否可以在 Alloy 中模拟随机故障？

例如，我目前有一个连通图，它在不同的时间步将数据传递给它的邻居。我想做的是找出一些允许模型随机终止链接的方法，并且在这样做的过程中，仍然设法实现其目标(确保所有节点的数据状态都设置为 On)。

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 for所有连接的邻居)。

---

编辑:

所以，我按照建议做了，但遇到了以下错误:
我很困惑，因为我认为邻居和 Node 仍然是固定的？

这是我更新后的代码:

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

Answer 1

将邻居的定义移到时间中:

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

这将处置限制为最多一个弧。