合金功能有很多要求

Question

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

我希望能够将课程 c 作为输入；输出一组导师，他们负责一个或多个在 c 注册但还没有分数的学生。

谁能帮帮我？

Answer 1

这一次您似乎在询问如何在 Alloy 中编写集合推导式。然后，您可以使用集合推导编写一个函数，该函数针对给定课程返回所有注册该课程的学生，这样他们就没有分配分数。之后，很容易直接从alloc 关系中选择分配给这些学生的导师。

Alloy 中集合推导的语法如下

{x: expr | condition(x)}

它的意思是“选择所有属于集合expr的x使得condition(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]]
}