合金功能输出二元关系

Question

谁能告诉我如何使用Alloy中的函数输出二元关系？ 例如，学生与老师关联，学生也与课程相关联。 我怎样才能把学生作为输入，然后输出老师和课程之间的二元关系？

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

从函数返回二元关系没有特别的规则。我假设你的问题更多地是关于你需要在这种情况下使用的关系产品运算符（->）从两个标量（或两个一元关系）构造二元关系