合金規格問題

Question

下面是我最近爲手機發短信完成的合金規格。這只是基本的短信要求，由於這是一種做法，我沒有嚴格的要求來維護。但是，我有一些尷尬的問題，例如爲什麼我無法獲得超過1對Name-Mobile對？爲什麼2個MessageSets始終指向一個名稱？除了問題之外，事實和謂詞非常簡單。請隨時批評，因爲我需要反饋來學習合金本身。

在做下面的工作時我想到了什麼;

一個消息框有0個或多個消息集。一套只屬於一個人，沒有一套是免費的。每組有一個或多個消息，它們由消息行，開始和結束鍵以及行和光標位置組成。幾條消息可以屬於同一個人，但不能同時屬於兩個人。每行有一個或多個鍵，並有開始和結束鍵。另外一條線可能有也可能沒有新的線。每個鍵可能有也可能沒有下一個鍵。按鍵通過觸摸板按下。每個名字都有一個手機號碼，它們被記錄在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對名稱-Mobile的對？

要調試這樣的問題，可以使用「不可核心」功能。首先，我將#Name > 1添加到show謂詞中，然後從「Options」菜單中選擇「Unsat Core的MiniSat」解算器，最後執行「show」謂詞。該模型是不可滿足的（如預期的那樣），所以不是一個實例，而是返回一個不合格核心，即一組相互不一致的最小公式。換言之，不飽和核心爲您提供了模型不可滿足的原因，並且，如果刪除不飽和核心中的任何一個公式，該模型應該可以滿足。

在你的具體的例子中，不飽和度的核心包含以下行：

contact: Name // field declaration inside the ContactList sig 

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

    #Name > 1 

這應該立即告訴你爲什麼該模型是不可滿足：在contact字段聲明指向只有一個Name;強制該字段的基數等於原子數目的下一個約束意味着只能有1個原子，所以當你明確要求更多原子時（#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 

再次，這是非常明顯的問題是。你希望不是所有的MessageSet都指向相同的Name（第3行），但在你的模型中，你有一個事實（第1行）完全相反，這就是說，對於所有的ms: MessageSet和m: Messages，ms.isSetOf的值必須是相同並等於m.sentFrom。滿足這些約束條件的唯一方法是具有0 Messages（所以通用量詞是平凡真實的），但是在那種情況下，來自不可核心的第二行不能被滿足。