alloy - 数量子の数え方 - 方法

Question

たとえば、チェッカーボードをモデル化する必要があり、「A」の垂直方向に少なくとも 5 つの正方形が空であると言いたいとします。Alloyでそれを行うにはどうすればよいですか？0 または 1 以外の数値を使用する他の例は適切です。言い換えれば、「一部」が十分に正確でない場合はどうすればよいでしょうか? ありがとう！

Answer 1

カーディナリティ演算子 (#) を使用して、リレーション内のタプルの数に関するアサーションを作成できます。たとえば、

#r >= 5

リレーションrには少なくとも 5 つのタプルが必要です。

カーディナリティ演算子を任意の式で使用することもできます。

#board.cells >= 5

また

#{c: Cell | c in board.cells and ...} >= 5