问题标签 [alloy]

无法理解合金代码的输出：

我很好奇输出是否包含（e0，e0）和（b0，b0）。我附上了分析仪的输出，但不知道如何解释它。这是否意味着 (e0,e0) 在解决方案中？

我真的很困惑为什么我的以下断言总是有一个反例。

反例总是显示 1 univ set 中的元素。然而，这不应该是这样，因为我指定会有一些 ~r iff x 不在 y 中并且 y 不在 x 中。唯一的元素不应该满足这个陈述。

然而，为什么该模型总是对我的断言提出反例呢？

非常感谢一些指导！

比方说，我必须对棋盘进行建模，并且我想说“A”垂直上的至少 5 个方格是空的。我如何在合金中做到这一点？任何其他数字不同于 0 或 1 的示例都会很好。换句话说，当“some”不够精确时，我该怎么办？谢谢！

我看到了以下合金定义：

一个信号数 { i:Int[3]}

//Int[3] 是什么意思。我的意思是上述字段'i'的含义是什么

我正在尝试使用 Alloy（对于形式逻辑也相对较新），并且尝试从完全连接的节点图开始。

从图中可以看出，节点 0 和 1 未连接。我认为我的事实足以让它完全联系起来……但也许我错过了一些东西。

我正在关注 Daniel Jackson 的优秀著作（软件抽象）中的一个示例，特别是他设置令牌环以选举领导者的示例。

我正在尝试扩展此示例（Ring 选举）以确保令牌（而不是仅限于一个）在规定的时间内传递给所有成员（并且每个成员只被选举一次，而不是多次）。但是（主要是由于我对合金缺乏经验），我在找出最佳方法时遇到了问题。最初我认为我可以与一些运算符一起玩（将 - 更改为 + ），但我似乎并没有完全击中头部。

下面是示例中的代码。我已经用问题标记了一些区域......感谢任何和所有帮助。我正在使用合金 4.2。

从这个问题跟进...

我有一个完全连通的图，这很棒。我也加入了时间的概念。我现在正在为围绕我的图表传递数据的概念而苦苦挣扎。

我正在为一个系统建模，该系统的任务是确保每个节点都有一个已插入系统的数据副本。我脑子里有关于如何做到这一点的程序，但是我正在努力将其翻译成合金术语。

一个典型的算法看起来像这样：

为简单起见，假设每个节点都有一个唯一的数据，它们必须将该数据提供给所有其他节点。由于这是完全连接的，它应该相对简单（翻译成合金/形式逻辑对我来说有点困难）。

这是我目前所在的位置：

从我的运行谓词中，您可以看到我希望在 20 个时间步内发送所有消息，因此到那时每个 DataMirror 都应该有一组由 5 个唯一消息组成的数据。

我很确定我想做的是让每个 DataMirror 有 2 个属性：

• 要发送的唯一消息（此时可以只是一个简单的变量）
• 收到的消息集（包括原始消息）

当所有 DataMirror 具有相同的消息集时，系统会感到满意。

例如，如果我们有：

那么系统将在以下情况下完成：

我为让任何形式逻辑的高级用户畏缩而提前道歉......我正试图在试炼中学习这一点:)。

以下是我迄今为止的部分工作。由于某种原因，我的线路和从消息到线路的单一连接之间存在循环和双向连接。我不明白为什么线路连接的消息永远不会超过一条。我的事实可能（很可能）有点错误。谢谢您的帮助。

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

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

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

编辑：

所以，我按照建议做了并遇到了以下错误：
我很困惑，因为我认为邻居和节点仍然是集合？

这是我更新的代码：

我是合金新手。我正在尝试制定允许的模拟电话线规格。这是我的 FSM 图。

我编写了一个示例代码来说明状态转换。我的转换表是事实，但是输出乘数是合金语法中的一个问题。我无法运行此代码。

你会说我有什么问题吗。有什么建议吗？