alloy relation facts

Question

Below is part of my work so far. I'm getting cycles and both ways connections in between my Lines and single connections from Messages to Lines for some reason. I don't see why there are never more than one message to line connections. My facts are probably (most likely) a little wrong. Thanks for the help.

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
}

also, what kind of a fact can i add to make the Message sig see the nextLine as within its formedOfLines as well as the original Line. I can add a fact for the next line but then i will lose the original line. should i add another sig relation like first line? — mechanicum

Aleksandar Milicevic Aleksandar Milicevic · Accepted Answer · 2012-12-03T17:33:30

Your model allows each Line to have multiple nextLines, which might not be your intention. That's why your NoNextLineIsSelf fact doesn't actually prevent loops, because l.nextLine != l can be true if l.nextLine contains more than one Line and one of them is l. You can rewrite that fact to

all l: Line | l !in l.nextLine

to forbid all loops.

To forbid "two-way connections" between lines, you can write something like

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

(I'm not sure which one of your facts was supposed to do that)

If you want a Message to have more than 1 line, you should change the multiplicity of the formedOfLines to set, i.e.,

sig Message {
  formedOfLines: set Line
}

alloy relation facts

1 Answers