「複数の人がいて、時系列で状態が変化しつつインタラクションする」っていうのをやろうと思ったんだけど(具体的には既婚・未婚状態が変わりながら男女が結婚したり離婚したりするってものを作って、最初は制約が足りなくて重婚が起きてしまい、それを修正す…

Alloyになにか適当なパズルを解かせてみようと思って、最初に思いついたものが「SとKの組み合わせでIを作れ」だったので実装してみたが、Iを探す以前に、制約なしでもfactを満たす解が見つからない。何故だ？ abstract sig Bird{ apply: Bird -> Bird } one …

Alloyのallの意味がよくわからない。 enum X {A, B, C} check { all r: X{ one r } }これは反例が見つからない。つまり「all r: X {foo}」は「すべての集合Xの 要素 についてfooが成立する」なわけだ。しかし、このXをX -> Xに置き換えてみると挙動が違う。 …