function - 合金功能有很多要求

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

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