Alloyガール1、Alloyガール2の続き。JS: あれれ？おかしいな？ 僕: ん、どうしたの？ JS: Alloyちゃんはこの2つ等価だって言ってたけど出てくるものが違うよ？ sig StateManager { state: set State } sig State {} run { one StateManager }one sig StateMa…

Alloyガール1の続き。僕: ただいまー Alloy: あら、随分長い間保健室にいたのね。何してたの 僕: それはもうJavaScriptとイチャイチャと…って何言わすねん Alloy: 冗談よ。 僕: …。 JS: ねえねえ、StateManagerが2個ある問題を解決しようよー 僕: そうだった…

僕: 普通にAlloyさんのことを説明してもイマイチ反応がないんだよね Alloy: 「普通」の定義があいまいね 僕: …で、とりあえず会話形式にしてみたらいいんじゃないかと思ったんだ！ Alloy: 論理が飛躍しすぎね。まったく何を言っているのかわからないわ。 僕:…

Alloyは「関係」が言語の基本的な構成要素なので、やっぱり身近な関係として「人間関係」を使うとわかりやすいですね。というわけで檜山さんのAlloyで人生モデリング その2：時間軸を設定する - 檜山正幸のキマイラ飼育記の続編を勝手に作ってみました。orde…

今回は項書換え的な書き方にしてみた。まずKコンビネータから。 open util/ordering[Term] some abstract sig Term {} one sig K extends Term {} sig Apply extends Term { f, g: Term } fact { all x, y: Term | (x -> y) in (f + g) => y not in (x.prevs…

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

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に置き換えてみると挙動が違う。 …

関係が言語の基本構成部品になっているalloy、やっぱり身近な「関係」を使って解説しようということで「人間関係」を例にあげることが多い。だけどman3とwoman1の間のロマンスとか砂を噛むようで味気ないよね。というわけで与えた選択肢の中からオブジェクト…

p.220の問題をとく上で、univ0とかuniv1と表示されている集合にenumみたいにわかりやすい名前を付けたいななどと思った。そしてやってみた結果、今回重要なのは矢印の形なので箱に名前がついてもあんまり意味がなかったｗ fact { #univ = 4 } sig A {} sig B…

4.2.2章の記法はもちろん間違いじゃないけど、理解するまで結構悩んだ。 sig A {f: e}こう書かれるとfとeは似た種類のものだと思うじゃない？で、 f in A -> eという制約がfactに入っているのと同じ、と続いて、さらにそれは all this: A | this.f in eと同…

とりあえず教科書が届いたのでざっくり読んでみた。ここからどうやって勉強していくかなー。とりあえず既に存在しているソフトウェアをモデリングしてみて、自分がどこまでできてどこでつまずくかを確認してみるか。んー、じゃ、Gitをモデリングする。とりあ…