合金关系事实答案

【问题标题】：alloy relation facts合金关系事实
【发布时间】：2012-12-03 08:14:34
【问题描述】：

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

some sig Line{  
    nextLine: some Line,
}

sig Message{
    formedOfLines: Line,
}
fact MessageHasMoreThan1LineHasNextLine{
    all m:Message|#m.formedOfLines>1 implies #m.formedOfLines.nextLine>0
}
fact NoNextLineIsSelf
{
   all l1,l2:Line | l1=l2 implies l1.nextLine!=l2
}
fact LineBelongsToSomeMessage
{
    all l:Line | l in Message.formedOfLines
}

【问题讨论】：

另外，我可以添加什么样的事实以使 Message sig 在其formedOfLines 以及原始 Line 中看到 nextLine。我可以为下一行添加一个事实，但我会丢失原来的行。我应该像第一行一样添加另一个 sig 关系吗？

标签： alloy

【解决方案1】：

您的模型允许每个Line 有多个nextLine，这可能不是您的意图。这就是为什么您的NoNextLineIsSelf 事实实际上并不能防止循环，因为如果l.nextLine 包含多个Line 并且其中之一是l，l.nextLine != l 可能为真。你可以把这个事实改写为

all l: Line | l !in l.nextLine

禁止所有循环。

要禁止行之间的“双向连接”，你可以写类似

all disj l1, l2: Line | l2 in l1.nextLine implies l1 !in l2.nextLine

（我不确定你的哪个事实应该这样做）

如果您希望 Message 有超过 1 行，则应将 formedOfLines 的多重性更改为 set，即

sig Message {
  formedOfLines: set Line
}

【讨论】：

谢谢，这需要一些时间来正确思考。
顺便说一句，all disj l1, l2: Line | l2 in l1.nextLine implies l1 !in l2.nextLine 打破每个连接之间的循环，但不超过 2 个连接。仍然有循环和循环。我正在寻找解决方案
我不知道你的意思是“双向连接”的“循环”；我认为这正是我在 Alloy 中正式写的内容。