Проблемы со спецификацией сплава

Question

Ниже приведена так называемая спецификация сплава, которую я недавно закончил для текстовых сообщений мобильного телефона. Это просто основные требования к текстовым сообщениям, и, поскольку это практика, у меня нет строгих требований к соблюдению. Тем не менее, у меня есть некоторые неловкие проблемы, например, почему я не могу получить более 1 пары пар Name-Mobile? Почему 2 MessageSets настойчиво указывают на одно Имя? За исключением вопросов, факты и предикаты очень просты. Пожалуйста, не стесняйтесь критиковать в полной мере, так как мне нужна обратная связь, чтобы изучить сам сплав.

Что я имел в виду, когда делал следующее;

В одном окне сообщений содержится 0 или более наборов сообщений. Набор принадлежит только 1 человеку и ни один набор не является бесплатным. Каждый набор содержит 1 или более сообщений, которые состоят из строк сообщений, клавиш начала и конца, а также строк и расположения курсора. Несколько сообщений могут принадлежать одному человеку, но ни одно сообщение не может принадлежать двум людям одновременно. Каждая строка имеет 1 или более клавиш и имеет свои клавиши начала и конца. Также строка может иметь или не иметь новую строку. Каждый ключ может иметь или не иметь следующий ключ. Клавиши нажимаются через тачпад. Каждое имя имеет номер мобильного телефона, и они записаны в ContactList. У двух имен не может быть одного и того же мобильного телефона, но у человека может быть несколько телефонных номеров.

Благодарю.

    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

почему я не могу получить более 1 пары пар Name-Mobile?

Для устранения подобных проблем вы можете использовать функцию "unsat core". Сначала я добавил #Name > 1 к show предикат, затем я выбрал решатель "MiniSat с Unsat Core" из меню "Опции" и, наконец, выполнил предикат "show". Модель была неудовлетворительной (как и ожидалось), поэтому вместо экземпляра было возвращено ненасыщенное ядро, то есть минимальный набор формул, которые взаимно противоречивы. Другими словами, ядро ​​unsat дает вам причину неудовлетворенности модели, а также, если вы удалите одну из формул в ядре unsat, модель должна стать выполнимой.

В вашем конкретном примере ядро ​​unsat содержало следующие строки:

  contact: Name // field declaration inside the ContactList sig

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

  #Name > 1

Это должно сразу сказать вам, почему модель неудовлетворительная: contact поле объявлено как однозначно Name; следующее ограничение, которое заставляет количество элементов этого поля равным числу Name атомы подразумевают, что может только 1 Name атом, поэтому, когда вы явно просите больше Name атомы (#Name > 1Вы получите противоречие.

Чтобы это исправить, вы можете изменить contact объявление поля в contact: set Name,

Почему 2 MessageSets настойчиво указывают на одно Имя?

Чтобы проверить это, я добавил следующее ограничение к show предикат (после исправления объявления contact как объяснено выше)

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

Действительно, модель была неудовлетворительной. Ядро содержало следующие строки

  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

Опять же, вполне очевидно, в чем проблема. Вы хотите этого не все MessageSetS указывают на то же самое Name (3-я строка), но в вашей модели есть факт (1-я строка), который говорит с точностью до наоборот, то есть для всех ms: MessageSet а также m: Messages, значение ms.isSetOf должен быть таким же и равным m.sentFrom, Единственный способ удовлетворить эти ограничения - это иметь 0 Messages (таким образом, универсальный квантификатор тривиально верен), но в этом случае 2-я строка из несогласованного ядра не может быть удовлетворена.