Alloy assert check

Question

我想寫一個assert語句，一旦輸入 任何學生的標記，那麼學生總是有該課程的標記（儘管可能 標記可能會改變）。我已經知道如何檢查學生是否有分數，但如果學生沒有任何標記，我不知道該如何去做。另外，我該如何爲這個assert語句編寫一個檢查語句？

sig Student, Tutor, Mark {} 

sig Course { 
    reg : set Student, 
    alloc : Student -> Tutor, 
    result : Student -> Mark 
} 

這就是我想

assert chekmark 
    {all c:Course | let c' = CO/next[c] | 
    some Student.(c.Result) => some Student.(c.Result)} 

check checkmark for 3 

但不知何故，它說：這種表達未能得到typechecked。 我是對還是錯，我如何解決它，如果我是對的？

Answer 1

問題是，在課程排序不會是你的問題的解決方案。使用排序模塊只需在所有課程中放置一個總訂單（因此CO/next [c]只是按順序在c之後返回課程），而您可能希望爲每個（課程，學生）對都有一系列標記。

也許這樣的事情

sig Student, Tutor, Mark {} 

sig Course { 
    reg : set Student, 
    alloc : Student -> Tutor, 
    result : set Grade 
} 

sig Grade { 
    student: one Student, 
    marks: seq Mark 
} 

自動採用合金序列給你你想要的屬性，也就是說，如果marks字段不爲空，那麼它也會包含標記序列所以沒有在中間的空值是可能的。

使用此模型，您可能希望添加一個事實，即每個課程每個學生最多可以強制一個年級。

fact oneGradePerStudentPerCourse { 
    all c: Course { 
    all s: c.reg | 
     lone {g: c.result | g.student = s} 
    } 
}