合金關係事實

以下是我迄今工作的一部分。由於某些原因，我在我的線路和從消息到線路的單個連接之間獲得了週期和雙向連接。我不明白爲什麼不會有多條消息到線路連接。我的事實可能（很可能）有點不對。謝謝您的幫助。合金關係事實

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 
}

來源

2012-12-03 mechanicum

還，我可以添加什麼樣的事實，使消息sig將nextLine視爲其形成的行內以及原始行。我可以爲下一行添加一個事實，但是然後我將失去原始行。我應該像第一行一樣添加另一個sig關係嗎？ – mechanicum

你的模型允許每個Line有多個nextLine s，這可能不是你的意圖。這就是爲什麼你的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

（我不知道，你的事實之一是應該這樣做）

如果您想一個Message有超過1行，你應該改變formedOfLines到set的多樣性，即

sig Message { 
    formedOfLines: set Line 
}

來源

2012-12-03 17:33:30

謝謝，它需要一些習慣爲此正確思考。 – mechanicum

btw，'all disj l1，l2：Line |在l1.nextLine中的l2意味着在l2.nextLine中的l1！中斷每個連接之間的循環，但是不超過2個連接。還有循環和循環。我正在尋找解決方案 – mechanicum

我不知道你的意思是「循環」「雙向連接」;我認爲這正是我在Alloy中正式寫的東西。 –

合金關係事實

回答

相關問題