合金功能有很多要求

Question

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

我希望能夠把課程c作爲輸入;輸出負責一個或多個註冊c但尚未有商標的學生的導師組。

任何人都可以幫助我嗎？

Answer 1

這次你似乎在問如何在Alloy中寫集合理解。然後，您可以使用一組理解來編寫一個函數，該函數針對給定課程返回註冊該課程的所有學生，使其沒有分配標記。之後，可以直接從alloc關係中輕鬆選擇分配給這些學生的導師。

語法在合金集推導如下

{x: expr | condition(x)} 

，它的意思是「選擇屬於設定expr這樣condition(x)持有所有x」。

這裏是如何寫你的問題：

sig Student, Tutor, Mark {} 

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

fun studentsWithNoMarks[c: Course]: set Student { 
    {s: c.reg | no c.result[s]} 
} 

fun tutorsForStudentsWithNoMarks[c: Course]: set Tutor { 
    c.alloc[studentsWithNoMarks[c]] 
}