合金功能有很多要求

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]] 
}