合金函数输出二元关系

【问题标题】：Alloy Function output binary relation合金函数输出二元关系
【发布时间】：2013-03-10 19:09:43
【问题描述】：

谁能告诉我如何使用 Alloy 中的函数输出二元关系？例如，学生与老师链接，学生也与课程链接。如何以学生为输入，输出教师与课程的二元关系？

【问题讨论】：

【解决方案1】：

这样的？

sig Course {}
sig Teacher {}
sig Student {
  teacher: one Teacher, 
  course: some Course
}

fun binrel [s: Student]: Teacher -> Course {
  s.teacher -> s.course
}

run {
  some s: Student | (#binrel[s] > 2)
}

从函数返回二元关系没有特殊规则。我认为您的问题更多是关于关系乘积运算符 (->)，在这种情况下您需要使用它来从两个标量（或两个一元关系）构造二元关系

【讨论】：

谢谢，这正是我想要的^_^