факты отношения сплава

Ниже часть моей работы на данный момент. По какой-то причине я получаю циклы и двусторонние соединения между моими линиями и одиночные соединения из сообщений в строки. Я не понимаю, почему никогда не бывает более одного сообщения для линейных соединений. Мои факты, вероятно (скорее всего), немного неверны. Спасибо за помощь.

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
}

alloy
person mechanicum    schedule 03.12.2012    source источник
comment
Кроме того, какой факт я могу добавить, чтобы Message sig видел следующую строку как в пределах своих сформированных строк, так и в исходной строке. Я могу добавить факт для следующей строки, но тогда я потеряю исходную строку. Должен ли я добавить еще одно отношение sig, например, первую строку?   -  person mechanicum    schedule 03.12.2012

Ответы (1)


arrow_upward
0
arrow_downward

Ваша модель позволяет каждому Line иметь несколько nextLine, что может не соответствовать вашим намерениям. Вот почему ваш факт 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
}
person Aleksandar Milicevic    schedule 03.12.2012
comment
спасибо, для этого нужно привыкнуть думать правильно. - person mechanicum; 06.12.2012
comment
Кстати, all disj l1, l2: Line | l2 in l1.nextLine implies l1 !in l2.nextLine разрывает циклы между каждым соединением, но не более чем на 2 соединения. Есть еще циклы и петли. Я ищу решение - person mechanicum; 13.01.2013
comment
Я не знал, что вы имеете в виду петли под двусторонними соединениями; Я предположил, что это означает именно то, что я официально написал в Alloy. - person Aleksandar Milicevic; 15.01.2013