sig X{} sig Y{} pred p[r1, r2: X -> Y]{ #r1 < 3 #r2 < 3 (r1 + r2) != (r1 ++ r2) (r1 ++ r2) != (r2 ++ r1) (r2 ++ r1) != (r1 + r2) no r1 & iden no r2 & iden } run p for 4 int 追記 Alloyは「条件を満たす小さい事例を探す」ってタスクには抜群の使…