formal-methods - 如何显示集合关系的“计数”？

Question

我有这个代码：

taking’ = taking  ∪  {s? → m?} 

如您所见，taking是s映射到的关系的名称m。上面的关系显示了添加过程（联合），我在该关系中添加了一个新的 maptlet。

但是，我需要获取s此关系中可用的数量。我怎么才能得到它？以下是我所做的

#taking = numberOfStudents

但我不确定这一点。

Answer 1

如果你想知道有多少不同的学生正在录取m（不管m是什么）

这很容易：您需要s从taking关系中获得所有可能，然后测量结果集的基数。

就像这样：

numberOfStudents = #(\dom taking)

\dom函数（关系）域在哪里将为您提供关系中的所有学生。