Alloy

Alloy で整数を使う際のビット幅の件

結論としては、 ・ デフォルトではビット幅が 3 ( -4 〜 3 ) になっている(デフォルトのスコープが Int にも適用される) ・ 指定のビット幅の範囲を超える整数についての式は結果が不定(?) ・ 特にエラー、警告は出ない。 ということのようである。 ※Al…

Alloy の3項関係における多重度指定について

Alloy についてまともに使えるようになろうと、最近ああだこうだやっている。 静的なモデリングについてはほぼ納得できた気がしているのだが、動的なモデリングについては、Timeイディオムあたりでどうも理解が追いつかずに止まってしまっていた。 なぜそこ…