3

是否可以对合金中的随机故障进行建模？

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

我试图建模的软件处理不确定性。基本上，节点之间的链接可能会失败，并且软件会沿着另一条路径重新路由。我想在合金中尝试做的是在某些时间步长（最好是随机的）有一些链接到“死”的设施。在最重要的事实中，我有能力使图完全连接，因此，如果一个链接死掉，另一个可能会弥补这一缺陷（因为 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, ....}

您将需要重新表达关于每个时间点的邻居的对称性等事实。这很容易通过在 Time 签名的不变部分中完成：

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

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

于 2012-12-05T06:10:32.557 回答