alloy specification problems

Question

Below is a so-so alloy specification I completed recently for cellphone texting. It's just the basic texting requirements and since it's a practice, i don't have strict requirements to uphold. However, I have some awkward problems such why i can't get more than 1 pair of Name-Mobile pairs? Why 2 MessageSets point to one Name insistently? Other than the questions, the facts and predicates are very straight forward. Please feel free to criticize to the full extent since I need the feedback to learn alloy itself.

What i had in mind while doing the below;

One Message Box has 0 or more MessageSets. A set belongs to only 1 person and no set is free. Each set has 1 or more Messages which consist of message lines, start and end keys and lines and cursor location. Several messages can belong to the same person but no message can belong to 2 people at the same time. Each line has 1 or more keys and have their start and end keys. Also a line may or may not have a new line. Each key may or may not have next key. Keys are pressed through the touchpad. Every name has a mobile number and they are recorded in ContactList. No 2 names can have same mobile but a person can have multiple phone numbers.

Thanks.

    sig Lines{
formedOfKeys:some Keys,
lineStartKey:one Keys,
lineEndKey:one Keys,
nextLine: lone  Lines,
    }

one sig TouchPad{  pressed: set Keys }

sig Keys{ nextKey: one Keys, }

one sig MessageBox{}

    sig MessageSet{
isIn:one MessageBox,
isSetOf: one Name
    }

     sig Messages{
belongsToSet:  one MessageSet,
firstLine: one Lines,
lastLine:one Lines,
lastKey:one Keys,
firstKey: one Keys,
curserLoc: one Keys,
formedOfLines: set Lines,
sentFrom : one Name
   }

sig Name,Mobile {}

    one sig ContactList {
contact: Name, 
mobile: contact -> one Mobile
}

    fact No2NamesBelongingToMessageSetsSame{
//  all ms1,ms2:MessageSet| ms2 = ms1 implies ms1.isSetOf != ms2.isSetOf
    }

    //make it more than 2
fact NameAndMobileNumbersMatchedAndEqual{
//  #Name>2 and #Mobile>2
#Name=#Mobile
    }

    fact MessageSetBelongsToName{
all  ms:MessageSet, m:Messages |ms.isSetOf=m.sentFrom
    }

    fact AllNamesInContactList{
all c:ContactList| #c.contact =#Name
}

    fact NoLastMessageLineWithNextLine{
no l:Lines | l.nextLine not in (Messages.lastLine +Messages.firstLine)
    }

    fact NoNextKeyisSelf{
all k: Keys| k !in k.nextKey
    }

    fact NoNextLineisSelf{
all l: Lines | l !in l.nextLine
    }
    fact No2WayConnectionsBetweenLines{
all disj l1, l2: Lines | l2 in l1.nextLine implies l1 !in l2.nextLine
    }

    fact No2WayConnectionsBetweenKeys{
all disj k1, k2: Keys| k2 in k1.nextKey implies k1 !in k2.nextKey
    }

    fact MessageHasMoreThan1LineHasNextLine{
all m:Messages|#m.formedOfLines>1 implies #m.formedOfLines.nextLine>0
    }

fact LineStartInMessageLines{ all l:Lines| l.lineStartKey in l.formedOfKeys }
fact LineEndInMessageLines{ all l:Lines| l.lineEndKey in l.formedOfKeys }
fact CurserLocInMessageKeys{ all m:Messages| m.curserLoc in m.formedOfLines.formedOfKeys  }
fact FirstKeyInMessageKeys{ all m:Messages| m.firstKey in m.formedOfLines.formedOfKeys  }
fact firstLineInMessageLines{ all m:Messages| m.firstLine in m.formedOfLines }
fact MessageNextLineInMessageLines{ all m:Messages| m.formedOfLines.nextLine in m.formedOfLines }

fact MessageFirstKeyisInLineStartKeySet{ all m:Messages , l:Lines | m.firstKey in l.lineStartKey }

fact MessageLastKeyisInLineEndKeySet{ all m:Messages , l:Lines | l in m.lastLine && l.lineEndKey in m.lastLine.lineEndKey }

fact allKeysArePressed { all k:Keys | k in TouchPad.pressed }

fact NoMessageSetsWithoutMessages{ no ms:MessageSet| ms not in Messages.belongsToSet }

fact NoMessageSetWithoutBox{ no mb:MessageBox| mb not in MessageSet.isIn }

    pred nonReturnKeyPress[k: Keys, l,l':Lines, t:TouchPad]{
//key pressed in message, cursor and line info (new state =original state+1letter)
 l'.formedOfKeys= l.formedOfKeys++(t.pressed)
}

    pred deleteKeyPressed[k: Keys, l,l':Lines, t:TouchPad]{
//key deleted from line. cursor and line info (new state =original state-1key)
l'.formedOfKeys = l.formedOfKeys - (t.pressed)
}

    pred returnKeyPressed[k: Keys, l,l':Lines, t:TouchPad]{
//TODO return key pressed. cursor loc is new line's cursor loc
 l'.formedOfKeys= l.nextLine.formedOfKeys
}
    assert keyPressWorks {
    //TODO check if key press works properly
    }
    pred pressThenDeleteSame {
    all l1,l2,l3: Lines,  t:TouchPad, k: Keys|
    nonReturnKeyPress [k,l1,l2,t] && deleteKeyPressed [k,l2,l3,t]
        => l1.formedOfKeys = l3.formedOfKeys
}

    pred ReceiveThenSendSame {
all ms1,ms2,ms3, m: Messages|
    receive [m,ms1,ms2] && send [m,ms2,ms3]
        => ms1 = ms3
}

    pred findCursorLoc [l:Lines, k:lone Keys]{
//TODO I have a line and a key...How can i check where i am
}

    pred send[m, mS,mS':Messages]{
//final message set is one less than previous
mS'= mS - (m)
}

    pred receive[m, mS,mS':Messages]{
//final message set is one more than previous
mS'= mS++ (m)
}

pred AddContact [cl, cl': ContactList, n: Name, m: Mobile] {
   cl'.mobile = cl.mobile ++ (n->m)
    }

    pred RemoveContact [cl, cl': ContactList, n: Name] {
cl'.mobile = cl.mobile - (n->Mobile)
}

    pred FindContact [cl: ContactList, n: Name, m: Mobile] {
m = cl.mobile[n]
}

    assert AddingContact {
all cl, cl': ContactList, n: Name, m,m': Mobile |
    AddContact [cl,cl',n,m] && FindContact [cl',n,m'] => m = m'
}

    assert AddingThenDeleteSame {
all cl1,cl2,cl3: ContactList, n: Name, m: Mobile|
    AddContact [cl1,cl2,n,m] && RemoveContact [cl2,cl3,n]=> cl1.mobile = cl3.mobile
}

    assert pressThenDeleteSame {
all l1,l2,l3: Lines,  t:TouchPad, k: Keys|
    nonReturnKeyPress [k,l1,l2,t] && deleteKeyPressed [k,l2,l3,t]=> l1.formedOfKeys = l3.formedOfKeys
}

   assert ReceiveThenSendSame {
all ms1,ms2,ms3 , m: Messages|
    receive [m,ms1,ms2] && send [m,ms2,ms3]=> ms1 = ms3
}

//check AddingContact  expect 0
//check AddingThenDeleteSame  expect 1
//check pressThenDeleteSame  expect 0
//check ReceiveThenSendSame  expect 0

pred show{ }

run show 

//for exactly 3 Name,3 Mobile, 4 MessageSet,6 Messages, 5 Lines, 6 Keys  
//for exactly 4 MessageSet,14 Messages, 20 Lines, 40 Keys

Answer 1

why i can't get more than 1 pair of Name-Mobile pairs?

To debug problems like that, you can use the "unsat core" feature. First, I added #Name > 1 to the show predicate, then I selected the "MiniSat with Unsat Core" solver from the "Options" menu, and finally executed the "show" predicate. The model was unsatisfiable (as expected), so instead of an instance, an unsat core was returned, i.e., a minimal set of formulas that are mutually inconsistent. In other words, the unsat core gives you a reason why the model is unsatisfiable, and also, if you remove any one of the formulas in the unsat core, the model should become satisfiable.

In your concrete example, the unsat core contained the following lines:

  contact: Name // field declaration inside the ContactList sig

  all c:ContactList| #c.contact =#Name

  #Name > 1

This should immediately tell you why the model is unsatisfiable: the contact field is declared to point to exactly one Name; the next constraint that forces the cardinality of that field to be equal to the number of Name atoms implies that there can only 1 Name atom, so when you explicitly ask for more Name atoms (#Name > 1) you get contradiction.

To fix this, you can change the contact field declaration to contact: set Name.

Why 2 MessageSets point to one Name insistently?

To test this, I added the following constraint to the show predicate (after fixing the declaration of contact as explained above)

some disj ms1, ms2: MessageSet | ms1.isSetOf != ms2.isSetOf

Indeed, the model was unsatisfiable. The core contained the following lines

  all  ms:MessageSet, m:Messages | ms.isSetOf = m.sentFrom

  no ms:MessageSet | ms not in Messages.belongsToSet 

  some disj ms1, ms2: MessageSet | ms1.isSetOf != ms2.isSetOf

Again, it is pretty obvious what the problem is. You want that not all MessageSets point to the same Name (3rd line) but in your model you have a fact (1st line) that says exactly the opposite, which is that for all ms: MessageSet and m: Messages, the value of ms.isSetOf must be the same and equal to m.sentFrom. The only way to satisfy these constraints is to have 0 Messages (so the universal quantifier is trivially true), but in that case the 2nd line from the unsat core cannot be satisfied.