Alloy: 二項関係の性質

p.220の問題をとく上で、univ0とかuniv1と表示されている集合にenumみたいにわかりやすい名前を付けたいななどと思った。

そしてやってみた結果、今回重要なのは矢印の形なので箱に名前がついてもあんまり意味がなかったｗ

fact {
 #univ = 4
}
sig A {}
sig B {}
sig C {}
sig D {}
fact {
  #A = 1 && #B = 1 && #C = 1 && #D = 1
}

run {
   some r: univ -> univ {
    some r
    r.r in r
    no iden & r
    ~r in r
    ~r.r in iden
    r.~r in iden
   univ in r.univ
   univ in univ.r
  }
} for 4

なるほどねぇ、関係が対称的なときに推移律を認めたら必然的に反射的になるか。たしかにそれ大昔に勉強したような気がするけど、実際に手元で動いていると感慨深いものがあるなぁ。