alloy - 合金关系事实

Question

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

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
}

Answer 1

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

all l: Line | l !in l.nextLine

禁止所有循环。

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

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

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

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

sig Message {
  formedOfLines: set Line
}