alloy - 合金関係事実

Question

以下は、これまでの私の作品の一部です。なんらかの理由で、回線間の双方向の接続と、メッセージから回線への単一の接続が発生しています。回線接続へのメッセージが 1 つしかない理由がわかりません。私の事実は、おそらく (ほとんどの場合) 少し間違っています。助けてくれてありがとう。

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が複数nextLineの を持つことができますが、これはあなたの意図ではないかもしれません。が複数含まれていて、NoNextLineIsSelfそのうちの 1 つが. その事実を次のように書き換えることができますl.nextLine != ll.nextLineLinel

all l: Line | l !in l.nextLine

すべてのループを禁止します。

行間の「双方向接続」を禁止するには、次のように記述できます

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

（あなたの事実のどれがそうするはずだったのかわかりません）

Messageaに複数の行を持たせたい場合は、 formedOfLinestoの多重度を変更する必要がありますset。つまり、

sig Message {
  formedOfLines: set Line
}