Alloy Analyzer で、あの格言をモデリングする その2〜石の上に何年いればいいのか？〜
前回あつかった「石の上にも三年」のモデリングを再度試みます。
前回まで、
「Alloy で発見されたモデルインスタンスは、つまりそのまま（Happy pathの）テストデータとして
使えるんじゃないか、つまり、Alloy はテストデータ生成器として転用できるんじゃないか」
という期待を持っていたんですが、
整数を使ったモデリングをしてみて、それは無理だとわかりました。
Alloy で発見されたモデルインスタンスをそのままテストデータとして使うのは無理、
なので、テストデータ作成については、
Alloy で発見されたモデルインスタンスに、その後何らかの方法で具体値を割り当てる
ことで実現しよう、というふうに、方策を変えました。
そうなった以上、前回試みたような、ムチャな数値の使い方を、
Alloy の仕様記述に持ち込むのは止めなくては。
Alloy の世界では、数は、Intは、明確に有限でしたね。
"3"といっても、それはもしかしたら、その世界のMax値かもしれない、あるいはmin値かもしれない、
はたまた、範囲外だから表現できないかもしれないわけです。
なので、「"3"そのもの」ではなく、「この仕様内に設定したい、"3"的な何か」を、表現しなければいけない。
数値を抽象化するというのはそういうことなんですね。「"3"そのもの」は、忘れよう、いったん。
さらに、「石の上にも三年」という以上、
そこには、
当年 - 座り始めた年
という、引き算が必須になりますんで、
◎当年 は座り始めた年より大きい
そして
◎当年と座り始めた年との間に、三年未満/三年ちょうど/三年超え、の、みっつを表現できる間隔をあけておく必要がある
わけですね。
てことは、当年と座り始めた年との間には、最低3目盛り、距離でいうと、4離れていないといけないんだ！
ということでまずは、境界線を定義。
※訂正あり→http://d.hatena.ne.jp/nowavailable/20141207/1417950259
one sig MinInterval { val: one Int } { val = 4} one sig Border { val: one Int } { val = 2}
Int は extends できないので、シグニチャのフィールドとして持たせました。
年 も同様にします。
abstract sig Year { val: one Int } one sig ThisYear extends Year {} sig SinceYear extends Year { whose: one Craftman }
そして、石の上にいる人たち、Craftman。等のシグネチャは以下の通り。
sig Craftman { sinceYear: one SinceYear } abstract sig Career { guys: set Craftman } one sig Rookie, FullGrown extends Career {} }
そして、fact です。
fact generic {
// CraftmanのsinceYearとして作用していないSinceYearは、不要。
sinceYear = ~whose
// rookieGuysとfullGrownGuysは互いに素。
disj[Rookie.guys, FullGrown.guys]
// 開始年は過去である。そして開始年と当年の間隔も設定された通りに空いていること。
all sYear:SinceYear, tYear:ThisYear |
tYear.val >= sYear.val &&
tYear.val.minus[sYear.val] >= MinInterval.val
}
fact bizLogic {
all c:Craftman, r:Rookie, f:FullGrown, y:ThisYear, b:Border |
let rGuys = r.guys, fGuys = f.guys |
// 経験年数 b.val 超えなら、FullGrown。それ以外が Rookie 。
y.val.minus[c.sinceYear.val] > b.val implies
c in fGuys else
c in rGuys
}
新しい Alloy 言語のイディオムが登場していますんで、ちょっと解説します。
まず、disj関数。
"disj" というのは、disjointed のことのようです。これは、lone とか、some と同様の
集合に制約をかけるキーワードのひとつとして認識していたんですが、関数もあったんですね！
引数で渡した集合同士が、互いに素であれば、true を返します。これは多用しそうです。
それから、"let"。
let に続く変数定義は、ruby でいうところの、ブロック引数と同じみたいですね。これも使いでがある。
ちなみに、今まで説明なしに使ってきました "|" についても。
これは、"|" の右側が、（rubyでいうところの）ブロックになる、というものです。
本題に戻ります。
今回もっとも肝心な、Int のスコープ設定については、
run {} for 4 Int
としました。2の4乗ぶん、つまり、-8 〜 +8 までの 16ワク確保しました。
実際には、"0" も使うので、-8 〜 +7 までの 16ワクみたいです。
定義した数値の定数は、当年と開始年の最低間隔 "4" と、しきい値 "2"
のふたつなんですが、これをもし、"3 Int" というスコープ指定（2の3乗、-4〜+3 の8ワク）で
run しようとすると、インスタンスで使用する数値が、実際にはワクからあふれてしまいます。
このへんを確認する方法があって、それは、Alloy の
"Options" -> "Forbid Overflow"
を、"Yes" に設定します。そうすると、桁溢れが発生したケースでは、インスタンスは提示されずに、
「No instance found.」が返ってきますんで、それで判ります。これまたありがたい機能。
以上で、モデリングとしては完成です。
ただ、実際に実行してみると、Rookie の実例がなかなか出てきてくれません。。。
しきい値として設定した、"2" という数値が、この仕様世界の数値範囲のなかで、
（たとえば、実例としてでてくる SinceYear と、ThisYear の間隔に比して）
相対的に小さすぎるみたいです。
これを踏まえ、しきい値設定は、 "2" から "4" に変更。
one sig Border { val: one Int } { val = 4 }
そうすると実行例はこんな感じになります。
（※さらにわかりやすくするために、スコープは実際には、"run {} for 4 Int, 4 Craftman, 6 Year" にして、
インスタンスがある程度数表示されるようにしました。）
さて、このモデリングは、「これじゃ、石の上にも"4年" じゃないか。」と読まれてしまう
可能性もありますよね。いやいやこれはモデルなんで、って言うしかありませんが、
まあそういう批判は誤解は甘んじて受けるとして、とはいえ、
このモデルを、モデルでなくテストデータとして見立てたとき、
しきい値として設定した数値リテラルを、どのように実世界の数字に置き換えるか。
というテーマについては、さらに考察するつもりです。
Alloy Analyzer で、あの格言をモデリングする
“石の上にも三年” という格言を Alloy でモデリングします。
まあ、格言は実はどうでもよくて、Alloyにおける、数値（Integer）の扱いについて確認したかったんです。
整数の演算が必要に思えるなら、考え直したほうがいい。
より抽象的に記述したほうが、より問題に適合する記述にできることが多い。
〜（中略）〜
もちろん、数値演算への依存が大きいような問題を扱うのなら整数（あるいはもっと別の数値）
が必要になるだろうが、おそらくその問題は Alloy には向いていない。
と、書いてあります。
- 作者: Daniel Jackson,中島震,今井健男,酒井政裕,遠藤侑介,片岡欣夫
- 出版社/メーカー: オーム社
- 発売日: 2011/07/15
- メディア: 単行本（ソフトカバー）
- 購入: 8人 クリック: 274回
- この商品を含むブログ (35件) を見る
まったくその通りだと思います。
とはいえ、仕様上、数値でもってなんらかのボーダーを設定するケースは勿論有り得るし、
実際数値が入った仕様を Alloy で扱うことは可能ではあるわけで。その場合、内部的には、
問題を解くときに、変数に対してなんらかの数値（Integer）の代入をおこなっているよね？
という仮説にもとづき、Alloy 自体の挙動を観察したかった。今回の目的はそこです。
なんでそんなことを知りたいかというと、Alloyが、式の充足可能性を調べてモデルを発見するときの処理を利用して、
（充足可能成否や、モデルのグラフだけでなく）テストデータの生成ができないかな？と考えているからです。
ではやってみましょう。
“石の上にも三年” のモデリング。
登場人物は、Craftman として表現します。
sig Craftman { startYear: one Int }
startYear が、勤め始めた年です。
3年以上勤めた Craftman は、FullGrown というグループに属し、そうでない連中は Rookie というグループに属します。
one sig Rookie { rMembers: set Craftman } one sig FullGrown { fMembers: set Craftman }
そして、現在が何年であるか、などの条件は、Env というシグネチャの fact として記述しました。
one sig Env { border: one Int, thisYear: one Int, genesisYear: one Int } { border = 3 // 3年 thisYear = 14 // 2014年 genesisYear = 0 // 2000年 すべては2000年以降の話であるとする。 }
年は下二桁で表現しています。
そして、先述の"3年ルール"を表現する fact は
fact {
all c:Craftman, env:Env | c.startYear >= env.genesisYear && c.startYear <= env.thisYear
all c:Craftman, env:Env, rookie:Rookie, full_grown:FullGrown |
env.thisYear.minus[c.startYear] > env.border implies
c in full_grown.fMembers && c not in rookie.rMembers else
c in rookie.rMembers && c not in full_grown.fMembers
}
run {} for 6 Int, 4 Craftman
こうです。では実行結果を見てみましょう。
'09年から勤めている Craftman と、'00年から勤めている Craftman は、FullGrown 組で、
'12年から勤めはじめた Craftman が、Rookie に属しています。
さて、ここまではいいとして。
ここで扱っている「年」を、西暦のフル桁、つまり4桁で扱おうとするとどうなるでしょうか。
その前にふたたび教科書からの引用。
スコープの指定では、シグネチャ Int への指定が整数の最大ビット幅を指定する。
例として、以下のようなスコープを含むコマンドを考える
6 Int
このとき、-32 から +32 までの範囲の整数がシグネチャ Int へと割り当てられる。
えーとつまり、ここでは、2の6乗の範囲の整数を使う例をしめしているんですよね。
じゃあ西暦をフルに表現するには・・・2の13乗の範囲が要るってわけですね。じゃあ上記の式を
thisYear = 2014 genesisYear = 2000
run {} for 13 Int
って書き換えて、実行してみます。・・・・・・・・・・・・・・・・・・・・
・・・・・・・・・・・・・・・・・・・・・・・・・・・・・・・・・・・・
・・・・・・・・・・・・・・（長いな）・・・・・・・・・・・・・・・・・
・・・・・・・・・・・・・・・・・・・・・・・・・・・・・・・・・・・・
・・・・・・・・・・・・・・・・・・・結果：ダメでした。処理完了しません。
と、言われちゃいます。
Fatal Error: the solver ran out of memory!
Try simplifying your model or reducing the scope,
or increase memory under the Options menu.
さらに現象を追うために、先の、"6 Int" でrunしたときに生成された、kodkodファイルを見てみましょう。
kodkodファイルとは？ Alloy では、制約を充足する/しないを判定するために、SATソルバ（sat4j）呼ばれる
証明器を使っているんですが、そのSATソルバの手前に、Kodkod というエージェントがいて、
Kodkod が、SATソルバとのやりとりや、その前処理について受け持っているという形のようです。
で、Kodkod は、Alloy の式を Java コードに変換した中間データを持っています。それがこんな感じの代物です。
public final class Test { public static void main(String[] args) throws Exception { Relation x0 = Relation.unary("Int/min"); Relation x1 = Relation.unary("Int/zero"); Relation x2 = Relation.unary("Int/max"); Relation x3 = Relation.nary("Int/next", 2); Relation x4 = Relation.unary("seq/Int"); Relation x5 = Relation.unary("String"); Relation x6 = Relation.unary("this/Craftman"); Relation x7 = Relation.unary("this/Rookie"); Relation x8 = Relation.unary("this/FullGrown"); Relation x9 = Relation.unary("this/Env"); Relation x10 = Relation.nary("this/Craftman.startYear", 2); Relation x11 = Relation.unary("this/Rookie.rMembers"); Relation x12 = Relation.unary("this/FullGrown.fMembers"); Relation x13 = Relation.unary("this/Env.border"); Relation x14 = Relation.unary("this/Env.thisYear"); Relation x15 = Relation.unary("this/Env.genesisYear"); List<String> atomlist = Arrays.asList( "-1", "-10", "-11", "-12", "-13", "-14", "-15", "-16", "-17", "-18", "-19", "-2", "-20", "-21", "-22", "-23", "-24", "-25", "-26", "-27", "-28", "-29", "-3", "-30", "-31", "-32", "-4", "-5", "-6", "-7", "-8", "-9", "0", "1", "10", "11", "12", "13", "14", "15", "16", "17", "18", "19", "2", "20", "21", "22", "23", "24", "25", "26", "27", "28", "29", "3", "30", "31", "4", "5", "6", "7", "8", "9", "Craftman$0", "Craftman$1", "Env$0", "FullGrown$0", "Rookie$0", "unused0", "unused1" ); Universe universe = new Universe(atomlist); TupleFactory factory = universe.factory(); Bounds bounds = new Bounds(universe); TupleSet x0_upper = factory.noneOf(1); x0_upper.add(factory.tuple("-32")); bounds.boundExactly(x0, x0_upper); TupleSet x1_upper = factory.noneOf(1); x1_upper.add(factory.tuple("0")); bounds.boundExactly(x1, x1_upper); TupleSet x2_upper = factory.noneOf(1); x2_upper.add(factory.tuple("31")); bounds.boundExactly(x2, x2_upper); TupleSet x3_upper = factory.noneOf(2); x3_upper.add(factory.tuple("-32").product(factory.tuple("-31"))); x3_upper.add(factory.tuple("-31").product(factory.tuple("-30"))); x3_upper.add(factory.tuple("-30").product(factory.tuple("-29"))); x3_upper.add(factory.tuple("-29").product(factory.tuple("-28"))); x3_upper.add(factory.tuple("-28").product(factory.tuple("-27"))); x3_upper.add(factory.tuple("-27").product(factory.tuple("-26"))); x3_upper.add(factory.tuple("-26").product(factory.tuple("-25"))); x3_upper.add(factory.tuple("-25").product(factory.tuple("-24"))); x3_upper.add(factory.tuple("-24").product(factory.tuple("-23"))); x3_upper.add(factory.tuple("-23").product(factory.tuple("-22"))); x3_upper.add(factory.tuple("-22").product(factory.tuple("-21"))); x3_upper.add(factory.tuple("-21").product(factory.tuple("-20"))); x3_upper.add(factory.tuple("-20").product(factory.tuple("-19"))); x3_upper.add(factory.tuple("-19").product(factory.tuple("-18"))); x3_upper.add(factory.tuple("-18").product(factory.tuple("-17"))); x3_upper.add(factory.tuple("-17").product(factory.tuple("-16"))); x3_upper.add(factory.tuple("-16").product(factory.tuple("-15"))); x3_upper.add(factory.tuple("-15").product(factory.tuple("-14"))); x3_upper.add(factory.tuple("-14").product(factory.tuple("-13"))); x3_upper.add(factory.tuple("-13").product(factory.tuple("-12"))); x3_upper.add(factory.tuple("-12").product(factory.tuple("-11"))); x3_upper.add(factory.tuple("-11").product(factory.tuple("-10"))); x3_upper.add(factory.tuple("-10").product(factory.tuple("-9"))); x3_upper.add(factory.tuple("-9").product(factory.tuple("-8"))); x3_upper.add(factory.tuple("-8").product(factory.tuple("-7"))); x3_upper.add(factory.tuple("-7").product(factory.tuple("-6"))); x3_upper.add(factory.tuple("-6").product(factory.tuple("-5"))); x3_upper.add(factory.tuple("-5").product(factory.tuple("-4"))); x3_upper.add(factory.tuple("-4").product(factory.tuple("-3"))); x3_upper.add(factory.tuple("-3").product(factory.tuple("-2"))); x3_upper.add(factory.tuple("-2").product(factory.tuple("-1"))); x3_upper.add(factory.tuple("-1").product(factory.tuple("0"))); x3_upper.add(factory.tuple("0").product(factory.tuple("1"))); x3_upper.add(factory.tuple("1").product(factory.tuple("2"))); x3_upper.add(factory.tuple("2").product(factory.tuple("3"))); x3_upper.add(factory.tuple("3").product(factory.tuple("4"))); x3_upper.add(factory.tuple("4").product(factory.tuple("5"))); x3_upper.add(factory.tuple("5").product(factory.tuple("6"))); x3_upper.add(factory.tuple("6").product(factory.tuple("7"))); x3_upper.add(factory.tuple("7").product(factory.tuple("8"))); x3_upper.add(factory.tuple("8").product(factory.tuple("9"))); x3_upper.add(factory.tuple("9").product(factory.tuple("10"))); x3_upper.add(factory.tuple("10").product(factory.tuple("11"))); x3_upper.add(factory.tuple("11").product(factory.tuple("12"))); x3_upper.add(factory.tuple("12").product(factory.tuple("13"))); x3_upper.add(factory.tuple("13").product(factory.tuple("14"))); x3_upper.add(factory.tuple("14").product(factory.tuple("15"))); x3_upper.add(factory.tuple("15").product(factory.tuple("16"))); x3_upper.add(factory.tuple("16").product(factory.tuple("17"))); x3_upper.add(factory.tuple("17").product(factory.tuple("18"))); x3_upper.add(factory.tuple("18").product(factory.tuple("19"))); x3_upper.add(factory.tuple("19").product(factory.tuple("20"))); x3_upper.add(factory.tuple("20").product(factory.tuple("21"))); x3_upper.add(factory.tuple("21").product(factory.tuple("22"))); x3_upper.add(factory.tuple("22").product(factory.tuple("23"))); x3_upper.add(factory.tuple("23").product(factory.tuple("24"))); x3_upper.add(factory.tuple("24").product(factory.tuple("25"))); x3_upper.add(factory.tuple("25").product(factory.tuple("26"))); x3_upper.add(factory.tuple("26").product(factory.tuple("27"))); x3_upper.add(factory.tuple("27").product(factory.tuple("28"))); x3_upper.add(factory.tuple("28").product(factory.tuple("29"))); x3_upper.add(factory.tuple("29").product(factory.tuple("30"))); x3_upper.add(factory.tuple("30").product(factory.tuple("31"))); bounds.boundExactly(x3, x3_upper); TupleSet x4_upper = factory.noneOf(1); x4_upper.add(factory.tuple("0")); x4_upper.add(factory.tuple("1")); x4_upper.add(factory.tuple("2")); x4_upper.add(factory.tuple("3")); bounds.boundExactly(x4, x4_upper); TupleSet x5_upper = factory.noneOf(1); bounds.boundExactly(x5, x5_upper); TupleSet x6_upper = factory.noneOf(1); x6_upper.add(factory.tuple("unused0")); x6_upper.add(factory.tuple("unused1")); x6_upper.add(factory.tuple("Craftman$0")); x6_upper.add(factory.tuple("Craftman$1")); bounds.bound(x6, x6_upper); TupleSet x7_upper = factory.noneOf(1); x7_upper.add(factory.tuple("Rookie$0")); bounds.boundExactly(x7, x7_upper); TupleSet x8_upper = factory.noneOf(1); x8_upper.add(factory.tuple("FullGrown$0")); bounds.boundExactly(x8, x8_upper); TupleSet x9_upper = factory.noneOf(1); x9_upper.add(factory.tuple("Env$0")); bounds.boundExactly(x9, x9_upper); TupleSet x10_upper = factory.noneOf(2); x10_upper.add(factory.tuple("unused0").product(factory.tuple("-32"))); x10_upper.add(factory.tuple("unused0").product(factory.tuple("-31"))); x10_upper.add(factory.tuple("unused0").product(factory.tuple("-30"))); x10_upper.add(factory.tuple("unused0").product(factory.tuple("-29"))); x10_upper.add(factory.tuple("unused0").product(factory.tuple("-28"))); x10_upper.add(factory.tuple("unused0").product(factory.tuple("-27"))); x10_upper.add(factory.tuple("unused0").product(factory.tuple("-26"))); x10_upper.add(factory.tuple("unused0").product(factory.tuple("-25"))); x10_upper.add(factory.tuple("unused0").product(factory.tuple("-24"))); x10_upper.add(factory.tuple("unused0").product(factory.tuple("-23"))); x10_upper.add(factory.tuple("unused0").product(factory.tuple("-22"))); x10_upper.add(factory.tuple("unused0").product(factory.tuple("-21"))); x10_upper.add(factory.tuple("unused0").product(factory.tuple("-20"))); x10_upper.add(factory.tuple("unused0").product(factory.tuple("-19"))); x10_upper.add(factory.tuple("unused0").product(factory.tuple("-18"))); x10_upper.add(factory.tuple("unused0").product(factory.tuple("-17"))); x10_upper.add(factory.tuple("unused0").product(factory.tuple("-16"))); x10_upper.add(factory.tuple("unused0").product(factory.tuple("-15"))); x10_upper.add(factory.tuple("unused0").product(factory.tuple("-14"))); x10_upper.add(factory.tuple("unused0").product(factory.tuple("-13"))); x10_upper.add(factory.tuple("unused0").product(factory.tuple("-12"))); x10_upper.add(factory.tuple("unused0").product(factory.tuple("-11"))); x10_upper.add(factory.tuple("unused0").product(factory.tuple("-10"))); x10_upper.add(factory.tuple("unused0").product(factory.tuple("-9"))); x10_upper.add(factory.tuple("unused0").product(factory.tuple("-8"))); x10_upper.add(factory.tuple("unused0").product(factory.tuple("-7"))); x10_upper.add(factory.tuple("unused0").product(factory.tuple("-6"))); x10_upper.add(factory.tuple("unused0").product(factory.tuple("-5"))); x10_upper.add(factory.tuple("unused0").product(factory.tuple("-4"))); x10_upper.add(factory.tuple("unused0").product(factory.tuple("-3"))); x10_upper.add(factory.tuple("unused0").product(factory.tuple("-2"))); x10_upper.add(factory.tuple("unused0").product(factory.tuple("-1"))); x10_upper.add(factory.tuple("unused0").product(factory.tuple("0"))); x10_upper.add(factory.tuple("unused0").product(factory.tuple("1"))); x10_upper.add(factory.tuple("unused0").product(factory.tuple("2"))); x10_upper.add(factory.tuple("unused0").product(factory.tuple("3"))); x10_upper.add(factory.tuple("unused0").product(factory.tuple("4"))); x10_upper.add(factory.tuple("unused0").product(factory.tuple("5"))); x10_upper.add(factory.tuple("unused0").product(factory.tuple("6"))); x10_upper.add(factory.tuple("unused0").product(factory.tuple("7"))); x10_upper.add(factory.tuple("unused0").product(factory.tuple("8"))); x10_upper.add(factory.tuple("unused0").product(factory.tuple("9"))); x10_upper.add(factory.tuple("unused0").product(factory.tuple("10"))); x10_upper.add(factory.tuple("unused0").product(factory.tuple("11"))); x10_upper.add(factory.tuple("unused0").product(factory.tuple("12"))); x10_upper.add(factory.tuple("unused0").product(factory.tuple("13"))); x10_upper.add(factory.tuple("unused0").product(factory.tuple("14"))); x10_upper.add(factory.tuple("unused0").product(factory.tuple("15"))); x10_upper.add(factory.tuple("unused0").product(factory.tuple("16"))); x10_upper.add(factory.tuple("unused0").product(factory.tuple("17"))); x10_upper.add(factory.tuple("unused0").product(factory.tuple("18"))); x10_upper.add(factory.tuple("unused0").product(factory.tuple("19"))); x10_upper.add(factory.tuple("unused0").product(factory.tuple("20"))); x10_upper.add(factory.tuple("unused0").product(factory.tuple("21"))); x10_upper.add(factory.tuple("unused0").product(factory.tuple("22"))); x10_upper.add(factory.tuple("unused0").product(factory.tuple("23"))); x10_upper.add(factory.tuple("unused0").product(factory.tuple("24"))); x10_upper.add(factory.tuple("unused0").product(factory.tuple("25"))); x10_upper.add(factory.tuple("unused0").product(factory.tuple("26"))); x10_upper.add(factory.tuple("unused0").product(factory.tuple("27"))); x10_upper.add(factory.tuple("unused0").product(factory.tuple("28"))); x10_upper.add(factory.tuple("unused0").product(factory.tuple("29"))); x10_upper.add(factory.tuple("unused0").product(factory.tuple("30"))); x10_upper.add(factory.tuple("unused0").product(factory.tuple("31"))); x10_upper.add(factory.tuple("unused1").product(factory.tuple("-32"))); x10_upper.add(factory.tuple("unused1").product(factory.tuple("-31"))); x10_upper.add(factory.tuple("unused1").product(factory.tuple("-30"))); x10_upper.add(factory.tuple("unused1").product(factory.tuple("-29"))); x10_upper.add(factory.tuple("unused1").product(factory.tuple("-28"))); x10_upper.add(factory.tuple("unused1").product(factory.tuple("-27"))); x10_upper.add(factory.tuple("unused1").product(factory.tuple("-26"))); x10_upper.add(factory.tuple("unused1").product(factory.tuple("-25"))); x10_upper.add(factory.tuple("unused1").product(factory.tuple("-24"))); x10_upper.add(factory.tuple("unused1").product(factory.tuple("-23"))); x10_upper.add(factory.tuple("unused1").product(factory.tuple("-22"))); x10_upper.add(factory.tuple("unused1").product(factory.tuple("-21"))); x10_upper.add(factory.tuple("unused1").product(factory.tuple("-20"))); x10_upper.add(factory.tuple("unused1").product(factory.tuple("-19"))); x10_upper.add(factory.tuple("unused1").product(factory.tuple("-18"))); x10_upper.add(factory.tuple("unused1").product(factory.tuple("-17"))); x10_upper.add(factory.tuple("unused1").product(factory.tuple("-16"))); x10_upper.add(factory.tuple("unused1").product(factory.tuple("-15"))); x10_upper.add(factory.tuple("unused1").product(factory.tuple("-14"))); x10_upper.add(factory.tuple("unused1").product(factory.tuple("-13"))); x10_upper.add(factory.tuple("unused1").product(factory.tuple("-12"))); x10_upper.add(factory.tuple("unused1").product(factory.tuple("-11"))); x10_upper.add(factory.tuple("unused1").product(factory.tuple("-10"))); x10_upper.add(factory.tuple("unused1").product(factory.tuple("-9"))); x10_upper.add(factory.tuple("unused1").product(factory.tuple("-8"))); x10_upper.add(factory.tuple("unused1").product(factory.tuple("-7"))); x10_upper.add(factory.tuple("unused1").product(factory.tuple("-6"))); x10_upper.add(factory.tuple("unused1").product(factory.tuple("-5"))); x10_upper.add(factory.tuple("unused1").product(factory.tuple("-4"))); x10_upper.add(factory.tuple("unused1").product(factory.tuple("-3"))); x10_upper.add(factory.tuple("unused1").product(factory.tuple("-2"))); x10_upper.add(factory.tuple("unused1").product(factory.tuple("-1"))); x10_upper.add(factory.tuple("unused1").product(factory.tuple("0"))); x10_upper.add(factory.tuple("unused1").product(factory.tuple("1"))); x10_upper.add(factory.tuple("unused1").product(factory.tuple("2"))); x10_upper.add(factory.tuple("unused1").product(factory.tuple("3"))); x10_upper.add(factory.tuple("unused1").product(factory.tuple("4"))); x10_upper.add(factory.tuple("unused1").product(factory.tuple("5"))); x10_upper.add(factory.tuple("unused1").product(factory.tuple("6"))); x10_upper.add(factory.tuple("unused1").product(factory.tuple("7"))); x10_upper.add(factory.tuple("unused1").product(factory.tuple("8"))); x10_upper.add(factory.tuple("unused1").product(factory.tuple("9"))); x10_upper.add(factory.tuple("unused1").product(factory.tuple("10"))); x10_upper.add(factory.tuple("unused1").product(factory.tuple("11"))); x10_upper.add(factory.tuple("unused1").product(factory.tuple("12"))); x10_upper.add(factory.tuple("unused1").product(factory.tuple("13"))); x10_upper.add(factory.tuple("unused1").product(factory.tuple("14"))); x10_upper.add(factory.tuple("unused1").product(factory.tuple("15"))); x10_upper.add(factory.tuple("unused1").product(factory.tuple("16"))); x10_upper.add(factory.tuple("unused1").product(factory.tuple("17"))); x10_upper.add(factory.tuple("unused1").product(factory.tuple("18"))); x10_upper.add(factory.tuple("unused1").product(factory.tuple("19"))); x10_upper.add(factory.tuple("unused1").product(factory.tuple("20"))); x10_upper.add(factory.tuple("unused1").product(factory.tuple("21"))); x10_upper.add(factory.tuple("unused1").product(factory.tuple("22"))); x10_upper.add(factory.tuple("unused1").product(factory.tuple("23"))); x10_upper.add(factory.tuple("unused1").product(factory.tuple("24"))); x10_upper.add(factory.tuple("unused1").product(factory.tuple("25"))); x10_upper.add(factory.tuple("unused1").product(factory.tuple("26"))); x10_upper.add(factory.tuple("unused1").product(factory.tuple("27"))); x10_upper.add(factory.tuple("unused1").product(factory.tuple("28"))); x10_upper.add(factory.tuple("unused1").product(factory.tuple("29"))); x10_upper.add(factory.tuple("unused1").product(factory.tuple("30"))); x10_upper.add(factory.tuple("unused1").product(factory.tuple("31"))); x10_upper.add(factory.tuple("Craftman$0").product(factory.tuple("-32"))); x10_upper.add(factory.tuple("Craftman$0").product(factory.tuple("-31"))); x10_upper.add(factory.tuple("Craftman$0").product(factory.tuple("-30"))); x10_upper.add(factory.tuple("Craftman$0").product(factory.tuple("-29"))); x10_upper.add(factory.tuple("Craftman$0").product(factory.tuple("-28"))); x10_upper.add(factory.tuple("Craftman$0").product(factory.tuple("-27"))); x10_upper.add(factory.tuple("Craftman$0").product(factory.tuple("-26"))); x10_upper.add(factory.tuple("Craftman$0").product(factory.tuple("-25"))); x10_upper.add(factory.tuple("Craftman$0").product(factory.tuple("-24"))); x10_upper.add(factory.tuple("Craftman$0").product(factory.tuple("-23"))); x10_upper.add(factory.tuple("Craftman$0").product(factory.tuple("-22"))); x10_upper.add(factory.tuple("Craftman$0").product(factory.tuple("-21"))); x10_upper.add(factory.tuple("Craftman$0").product(factory.tuple("-20"))); x10_upper.add(factory.tuple("Craftman$0").product(factory.tuple("-19"))); x10_upper.add(factory.tuple("Craftman$0").product(factory.tuple("-18"))); x10_upper.add(factory.tuple("Craftman$0").product(factory.tuple("-17"))); x10_upper.add(factory.tuple("Craftman$0").product(factory.tuple("-16"))); x10_upper.add(factory.tuple("Craftman$0").product(factory.tuple("-15"))); x10_upper.add(factory.tuple("Craftman$0").product(factory.tuple("-14"))); x10_upper.add(factory.tuple("Craftman$0").product(factory.tuple("-13"))); x10_upper.add(factory.tuple("Craftman$0").product(factory.tuple("-12"))); x10_upper.add(factory.tuple("Craftman$0").product(factory.tuple("-11"))); x10_upper.add(factory.tuple("Craftman$0").product(factory.tuple("-10"))); x10_upper.add(factory.tuple("Craftman$0").product(factory.tuple("-9"))); x10_upper.add(factory.tuple("Craftman$0").product(factory.tuple("-8"))); x10_upper.add(factory.tuple("Craftman$0").product(factory.tuple("-7"))); x10_upper.add(factory.tuple("Craftman$0").product(factory.tuple("-6"))); x10_upper.add(factory.tuple("Craftman$0").product(factory.tuple("-5"))); x10_upper.add(factory.tuple("Craftman$0").product(factory.tuple("-4"))); x10_upper.add(factory.tuple("Craftman$0").product(factory.tuple("-3"))); x10_upper.add(factory.tuple("Craftman$0").product(factory.tuple("-2"))); x10_upper.add(factory.tuple("Craftman$0").product(factory.tuple("-1"))); x10_upper.add(factory.tuple("Craftman$0").product(factory.tuple("0"))); x10_upper.add(factory.tuple("Craftman$0").product(factory.tuple("1"))); x10_upper.add(factory.tuple("Craftman$0").product(factory.tuple("2"))); x10_upper.add(factory.tuple("Craftman$0").product(factory.tuple("3"))); x10_upper.add(factory.tuple("Craftman$0").product(factory.tuple("4"))); x10_upper.add(factory.tuple("Craftman$0").product(factory.tuple("5"))); x10_upper.add(factory.tuple("Craftman$0").product(factory.tuple("6"))); x10_upper.add(factory.tuple("Craftman$0").product(factory.tuple("7"))); x10_upper.add(factory.tuple("Craftman$0").product(factory.tuple("8"))); x10_upper.add(factory.tuple("Craftman$0").product(factory.tuple("9"))); x10_upper.add(factory.tuple("Craftman$0").product(factory.tuple("10"))); x10_upper.add(factory.tuple("Craftman$0").product(factory.tuple("11"))); x10_upper.add(factory.tuple("Craftman$0").product(factory.tuple("12"))); x10_upper.add(factory.tuple("Craftman$0").product(factory.tuple("13"))); x10_upper.add(factory.tuple("Craftman$0").product(factory.tuple("14"))); x10_upper.add(factory.tuple("Craftman$0").product(factory.tuple("15"))); x10_upper.add(factory.tuple("Craftman$0").product(factory.tuple("16"))); x10_upper.add(factory.tuple("Craftman$0").product(factory.tuple("17"))); x10_upper.add(factory.tuple("Craftman$0").product(factory.tuple("18"))); x10_upper.add(factory.tuple("Craftman$0").product(factory.tuple("19"))); x10_upper.add(factory.tuple("Craftman$0").product(factory.tuple("20"))); x10_upper.add(factory.tuple("Craftman$0").product(factory.tuple("21"))); x10_upper.add(factory.tuple("Craftman$0").product(factory.tuple("22"))); x10_upper.add(factory.tuple("Craftman$0").product(factory.tuple("23"))); x10_upper.add(factory.tuple("Craftman$0").product(factory.tuple("24"))); x10_upper.add(factory.tuple("Craftman$0").product(factory.tuple("25"))); x10_upper.add(factory.tuple("Craftman$0").product(factory.tuple("26"))); x10_upper.add(factory.tuple("Craftman$0").product(factory.tuple("27"))); x10_upper.add(factory.tuple("Craftman$0").product(factory.tuple("28"))); x10_upper.add(factory.tuple("Craftman$0").product(factory.tuple("29"))); x10_upper.add(factory.tuple("Craftman$0").product(factory.tuple("30"))); x10_upper.add(factory.tuple("Craftman$0").product(factory.tuple("31"))); x10_upper.add(factory.tuple("Craftman$1").product(factory.tuple("-32"))); x10_upper.add(factory.tuple("Craftman$1").product(factory.tuple("-31"))); x10_upper.add(factory.tuple("Craftman$1").product(factory.tuple("-30"))); x10_upper.add(factory.tuple("Craftman$1").product(factory.tuple("-29"))); x10_upper.add(factory.tuple("Craftman$1").product(factory.tuple("-28"))); x10_upper.add(factory.tuple("Craftman$1").product(factory.tuple("-27"))); x10_upper.add(factory.tuple("Craftman$1").product(factory.tuple("-26"))); x10_upper.add(factory.tuple("Craftman$1").product(factory.tuple("-25"))); x10_upper.add(factory.tuple("Craftman$1").product(factory.tuple("-24"))); x10_upper.add(factory.tuple("Craftman$1").product(factory.tuple("-23"))); x10_upper.add(factory.tuple("Craftman$1").product(factory.tuple("-22"))); x10_upper.add(factory.tuple("Craftman$1").product(factory.tuple("-21"))); x10_upper.add(factory.tuple("Craftman$1").product(factory.tuple("-20"))); x10_upper.add(factory.tuple("Craftman$1").product(factory.tuple("-19"))); x10_upper.add(factory.tuple("Craftman$1").product(factory.tuple("-18"))); x10_upper.add(factory.tuple("Craftman$1").product(factory.tuple("-17"))); x10_upper.add(factory.tuple("Craftman$1").product(factory.tuple("-16"))); x10_upper.add(factory.tuple("Craftman$1").product(factory.tuple("-15"))); x10_upper.add(factory.tuple("Craftman$1").product(factory.tuple("-14"))); x10_upper.add(factory.tuple("Craftman$1").product(factory.tuple("-13"))); x10_upper.add(factory.tuple("Craftman$1").product(factory.tuple("-12"))); x10_upper.add(factory.tuple("Craftman$1").product(factory.tuple("-11"))); x10_upper.add(factory.tuple("Craftman$1").product(factory.tuple("-10"))); x10_upper.add(factory.tuple("Craftman$1").product(factory.tuple("-9"))); x10_upper.add(factory.tuple("Craftman$1").product(factory.tuple("-8"))); x10_upper.add(factory.tuple("Craftman$1").product(factory.tuple("-7"))); x10_upper.add(factory.tuple("Craftman$1").product(factory.tuple("-6"))); x10_upper.add(factory.tuple("Craftman$1").product(factory.tuple("-5"))); x10_upper.add(factory.tuple("Craftman$1").product(factory.tuple("-4"))); x10_upper.add(factory.tuple("Craftman$1").product(factory.tuple("-3"))); x10_upper.add(factory.tuple("Craftman$1").product(factory.tuple("-2"))); x10_upper.add(factory.tuple("Craftman$1").product(factory.tuple("-1"))); x10_upper.add(factory.tuple("Craftman$1").product(factory.tuple("0"))); x10_upper.add(factory.tuple("Craftman$1").product(factory.tuple("1"))); x10_upper.add(factory.tuple("Craftman$1").product(factory.tuple("2"))); x10_upper.add(factory.tuple("Craftman$1").product(factory.tuple("3"))); x10_upper.add(factory.tuple("Craftman$1").product(factory.tuple("4"))); x10_upper.add(factory.tuple("Craftman$1").product(factory.tuple("5"))); x10_upper.add(factory.tuple("Craftman$1").product(factory.tuple("6"))); x10_upper.add(factory.tuple("Craftman$1").product(factory.tuple("7"))); x10_upper.add(factory.tuple("Craftman$1").product(factory.tuple("8"))); x10_upper.add(factory.tuple("Craftman$1").product(factory.tuple("9"))); x10_upper.add(factory.tuple("Craftman$1").product(factory.tuple("10"))); x10_upper.add(factory.tuple("Craftman$1").product(factory.tuple("11"))); x10_upper.add(factory.tuple("Craftman$1").product(factory.tuple("12"))); x10_upper.add(factory.tuple("Craftman$1").product(factory.tuple("13"))); x10_upper.add(factory.tuple("Craftman$1").product(factory.tuple("14"))); x10_upper.add(factory.tuple("Craftman$1").product(factory.tuple("15"))); x10_upper.add(factory.tuple("Craftman$1").product(factory.tuple("16"))); x10_upper.add(factory.tuple("Craftman$1").product(factory.tuple("17"))); x10_upper.add(factory.tuple("Craftman$1").product(factory.tuple("18"))); x10_upper.add(factory.tuple("Craftman$1").product(factory.tuple("19"))); x10_upper.add(factory.tuple("Craftman$1").product(factory.tuple("20"))); x10_upper.add(factory.tuple("Craftman$1").product(factory.tuple("21"))); x10_upper.add(factory.tuple("Craftman$1").product(factory.tuple("22"))); x10_upper.add(factory.tuple("Craftman$1").product(factory.tuple("23"))); x10_upper.add(factory.tuple("Craftman$1").product(factory.tuple("24"))); x10_upper.add(factory.tuple("Craftman$1").product(factory.tuple("25"))); x10_upper.add(factory.tuple("Craftman$1").product(factory.tuple("26"))); x10_upper.add(factory.tuple("Craftman$1").product(factory.tuple("27"))); x10_upper.add(factory.tuple("Craftman$1").product(factory.tuple("28"))); x10_upper.add(factory.tuple("Craftman$1").product(factory.tuple("29"))); x10_upper.add(factory.tuple("Craftman$1").product(factory.tuple("30"))); x10_upper.add(factory.tuple("Craftman$1").product(factory.tuple("31"))); bounds.bound(x10, x10_upper); TupleSet x11_upper = factory.noneOf(1); x11_upper.add(factory.tuple("unused0")); x11_upper.add(factory.tuple("unused1")); x11_upper.add(factory.tuple("Craftman$0")); x11_upper.add(factory.tuple("Craftman$1")); bounds.bound(x11, x11_upper); TupleSet x12_upper = factory.noneOf(1); x12_upper.add(factory.tuple("unused0")); x12_upper.add(factory.tuple("unused1")); x12_upper.add(factory.tuple("Craftman$0")); x12_upper.add(factory.tuple("Craftman$1")); bounds.bound(x12, x12_upper); TupleSet x13_upper = factory.noneOf(1); x13_upper.add(factory.tuple("-32")); x13_upper.add(factory.tuple("-31")); x13_upper.add(factory.tuple("-30")); x13_upper.add(factory.tuple("-29")); x13_upper.add(factory.tuple("-28")); x13_upper.add(factory.tuple("-27")); x13_upper.add(factory.tuple("-26")); x13_upper.add(factory.tuple("-25")); x13_upper.add(factory.tuple("-24")); x13_upper.add(factory.tuple("-23")); x13_upper.add(factory.tuple("-22")); x13_upper.add(factory.tuple("-21")); x13_upper.add(factory.tuple("-20")); x13_upper.add(factory.tuple("-19")); x13_upper.add(factory.tuple("-18")); x13_upper.add(factory.tuple("-17")); x13_upper.add(factory.tuple("-16")); x13_upper.add(factory.tuple("-15")); x13_upper.add(factory.tuple("-14")); x13_upper.add(factory.tuple("-13")); x13_upper.add(factory.tuple("-12")); x13_upper.add(factory.tuple("-11")); x13_upper.add(factory.tuple("-10")); x13_upper.add(factory.tuple("-9")); x13_upper.add(factory.tuple("-8")); x13_upper.add(factory.tuple("-7")); x13_upper.add(factory.tuple("-6")); x13_upper.add(factory.tuple("-5")); x13_upper.add(factory.tuple("-4")); x13_upper.add(factory.tuple("-3")); x13_upper.add(factory.tuple("-2")); x13_upper.add(factory.tuple("-1")); x13_upper.add(factory.tuple("0")); x13_upper.add(factory.tuple("1")); x13_upper.add(factory.tuple("2")); x13_upper.add(factory.tuple("3")); x13_upper.add(factory.tuple("4")); x13_upper.add(factory.tuple("5")); x13_upper.add(factory.tuple("6")); x13_upper.add(factory.tuple("7")); x13_upper.add(factory.tuple("8")); x13_upper.add(factory.tuple("9")); x13_upper.add(factory.tuple("10")); x13_upper.add(factory.tuple("11")); x13_upper.add(factory.tuple("12")); x13_upper.add(factory.tuple("13")); x13_upper.add(factory.tuple("14")); x13_upper.add(factory.tuple("15")); x13_upper.add(factory.tuple("16")); x13_upper.add(factory.tuple("17")); x13_upper.add(factory.tuple("18")); x13_upper.add(factory.tuple("19")); x13_upper.add(factory.tuple("20")); x13_upper.add(factory.tuple("21")); x13_upper.add(factory.tuple("22")); x13_upper.add(factory.tuple("23")); x13_upper.add(factory.tuple("24")); x13_upper.add(factory.tuple("25")); x13_upper.add(factory.tuple("26")); x13_upper.add(factory.tuple("27")); x13_upper.add(factory.tuple("28")); x13_upper.add(factory.tuple("29")); x13_upper.add(factory.tuple("30")); x13_upper.add(factory.tuple("31")); bounds.bound(x13, x13_upper); TupleSet x14_upper = factory.noneOf(1); x14_upper.add(factory.tuple("-32")); x14_upper.add(factory.tuple("-31")); x14_upper.add(factory.tuple("-30")); x14_upper.add(factory.tuple("-29")); x14_upper.add(factory.tuple("-28")); x14_upper.add(factory.tuple("-27")); x14_upper.add(factory.tuple("-26")); x14_upper.add(factory.tuple("-25")); x14_upper.add(factory.tuple("-24")); x14_upper.add(factory.tuple("-23")); x14_upper.add(factory.tuple("-22")); x14_upper.add(factory.tuple("-21")); x14_upper.add(factory.tuple("-20")); x14_upper.add(factory.tuple("-19")); x14_upper.add(factory.tuple("-18")); x14_upper.add(factory.tuple("-17")); x14_upper.add(factory.tuple("-16")); x14_upper.add(factory.tuple("-15")); x14_upper.add(factory.tuple("-14")); x14_upper.add(factory.tuple("-13")); x14_upper.add(factory.tuple("-12")); x14_upper.add(factory.tuple("-11")); x14_upper.add(factory.tuple("-10")); x14_upper.add(factory.tuple("-9")); x14_upper.add(factory.tuple("-8")); x14_upper.add(factory.tuple("-7")); x14_upper.add(factory.tuple("-6")); x14_upper.add(factory.tuple("-5")); x14_upper.add(factory.tuple("-4")); x14_upper.add(factory.tuple("-3")); x14_upper.add(factory.tuple("-2")); x14_upper.add(factory.tuple("-1")); x14_upper.add(factory.tuple("0")); x14_upper.add(factory.tuple("1")); x14_upper.add(factory.tuple("2")); x14_upper.add(factory.tuple("3")); x14_upper.add(factory.tuple("4")); x14_upper.add(factory.tuple("5")); x14_upper.add(factory.tuple("6")); x14_upper.add(factory.tuple("7")); x14_upper.add(factory.tuple("8")); x14_upper.add(factory.tuple("9")); x14_upper.add(factory.tuple("10")); x14_upper.add(factory.tuple("11")); x14_upper.add(factory.tuple("12")); x14_upper.add(factory.tuple("13")); x14_upper.add(factory.tuple("14")); x14_upper.add(factory.tuple("15")); x14_upper.add(factory.tuple("16")); x14_upper.add(factory.tuple("17")); x14_upper.add(factory.tuple("18")); x14_upper.add(factory.tuple("19")); x14_upper.add(factory.tuple("20")); x14_upper.add(factory.tuple("21")); x14_upper.add(factory.tuple("22")); x14_upper.add(factory.tuple("23")); x14_upper.add(factory.tuple("24")); x14_upper.add(factory.tuple("25")); x14_upper.add(factory.tuple("26")); x14_upper.add(factory.tuple("27")); x14_upper.add(factory.tuple("28")); x14_upper.add(factory.tuple("29")); x14_upper.add(factory.tuple("30")); x14_upper.add(factory.tuple("31")); bounds.bound(x14, x14_upper); TupleSet x15_upper = factory.noneOf(1); x15_upper.add(factory.tuple("-32")); x15_upper.add(factory.tuple("-31")); x15_upper.add(factory.tuple("-30")); x15_upper.add(factory.tuple("-29")); x15_upper.add(factory.tuple("-28")); x15_upper.add(factory.tuple("-27")); x15_upper.add(factory.tuple("-26")); x15_upper.add(factory.tuple("-25")); x15_upper.add(factory.tuple("-24")); x15_upper.add(factory.tuple("-23")); x15_upper.add(factory.tuple("-22")); x15_upper.add(factory.tuple("-21")); x15_upper.add(factory.tuple("-20")); x15_upper.add(factory.tuple("-19")); x15_upper.add(factory.tuple("-18")); x15_upper.add(factory.tuple("-17")); x15_upper.add(factory.tuple("-16")); x15_upper.add(factory.tuple("-15")); x15_upper.add(factory.tuple("-14")); x15_upper.add(factory.tuple("-13")); x15_upper.add(factory.tuple("-12")); x15_upper.add(factory.tuple("-11")); x15_upper.add(factory.tuple("-10")); x15_upper.add(factory.tuple("-9")); x15_upper.add(factory.tuple("-8")); x15_upper.add(factory.tuple("-7")); x15_upper.add(factory.tuple("-6")); x15_upper.add(factory.tuple("-5")); x15_upper.add(factory.tuple("-4")); x15_upper.add(factory.tuple("-3")); x15_upper.add(factory.tuple("-2")); x15_upper.add(factory.tuple("-1")); x15_upper.add(factory.tuple("0")); x15_upper.add(factory.tuple("1")); x15_upper.add(factory.tuple("2")); x15_upper.add(factory.tuple("3")); x15_upper.add(factory.tuple("4")); x15_upper.add(factory.tuple("5")); x15_upper.add(factory.tuple("6")); x15_upper.add(factory.tuple("7")); x15_upper.add(factory.tuple("8")); x15_upper.add(factory.tuple("9")); x15_upper.add(factory.tuple("10")); x15_upper.add(factory.tuple("11")); x15_upper.add(factory.tuple("12")); x15_upper.add(factory.tuple("13")); x15_upper.add(factory.tuple("14")); x15_upper.add(factory.tuple("15")); x15_upper.add(factory.tuple("16")); x15_upper.add(factory.tuple("17")); x15_upper.add(factory.tuple("18")); x15_upper.add(factory.tuple("19")); x15_upper.add(factory.tuple("20")); x15_upper.add(factory.tuple("21")); x15_upper.add(factory.tuple("22")); x15_upper.add(factory.tuple("23")); x15_upper.add(factory.tuple("24")); x15_upper.add(factory.tuple("25")); x15_upper.add(factory.tuple("26")); x15_upper.add(factory.tuple("27")); x15_upper.add(factory.tuple("28")); x15_upper.add(factory.tuple("29")); x15_upper.add(factory.tuple("30")); x15_upper.add(factory.tuple("31")); bounds.bound(x15, x15_upper); bounds.boundExactly(-32,factory.range(factory.tuple("-32"),factory.tuple("-32"))); bounds.boundExactly(-31,factory.range(factory.tuple("-31"),factory.tuple("-31"))); bounds.boundExactly(-30,factory.range(factory.tuple("-30"),factory.tuple("-30"))); bounds.boundExactly(-29,factory.range(factory.tuple("-29"),factory.tuple("-29"))); bounds.boundExactly(-28,factory.range(factory.tuple("-28"),factory.tuple("-28"))); bounds.boundExactly(-27,factory.range(factory.tuple("-27"),factory.tuple("-27"))); bounds.boundExactly(-26,factory.range(factory.tuple("-26"),factory.tuple("-26"))); bounds.boundExactly(-25,factory.range(factory.tuple("-25"),factory.tuple("-25"))); bounds.boundExactly(-24,factory.range(factory.tuple("-24"),factory.tuple("-24"))); bounds.boundExactly(-23,factory.range(factory.tuple("-23"),factory.tuple("-23"))); bounds.boundExactly(-22,factory.range(factory.tuple("-22"),factory.tuple("-22"))); bounds.boundExactly(-21,factory.range(factory.tuple("-21"),factory.tuple("-21"))); bounds.boundExactly(-20,factory.range(factory.tuple("-20"),factory.tuple("-20"))); bounds.boundExactly(-19,factory.range(factory.tuple("-19"),factory.tuple("-19"))); bounds.boundExactly(-18,factory.range(factory.tuple("-18"),factory.tuple("-18"))); bounds.boundExactly(-17,factory.range(factory.tuple("-17"),factory.tuple("-17"))); bounds.boundExactly(-16,factory.range(factory.tuple("-16"),factory.tuple("-16"))); bounds.boundExactly(-15,factory.range(factory.tuple("-15"),factory.tuple("-15"))); bounds.boundExactly(-14,factory.range(factory.tuple("-14"),factory.tuple("-14"))); bounds.boundExactly(-13,factory.range(factory.tuple("-13"),factory.tuple("-13"))); bounds.boundExactly(-12,factory.range(factory.tuple("-12"),factory.tuple("-12"))); bounds.boundExactly(-11,factory.range(factory.tuple("-11"),factory.tuple("-11"))); bounds.boundExactly(-10,factory.range(factory.tuple("-10"),factory.tuple("-10"))); bounds.boundExactly(-9,factory.range(factory.tuple("-9"),factory.tuple("-9"))); bounds.boundExactly(-8,factory.range(factory.tuple("-8"),factory.tuple("-8"))); bounds.boundExactly(-7,factory.range(factory.tuple("-7"),factory.tuple("-7"))); bounds.boundExactly(-6,factory.range(factory.tuple("-6"),factory.tuple("-6"))); bounds.boundExactly(-5,factory.range(factory.tuple("-5"),factory.tuple("-5"))); bounds.boundExactly(-4,factory.range(factory.tuple("-4"),factory.tuple("-4"))); bounds.boundExactly(-3,factory.range(factory.tuple("-3"),factory.tuple("-3"))); bounds.boundExactly(-2,factory.range(factory.tuple("-2"),factory.tuple("-2"))); bounds.boundExactly(-1,factory.range(factory.tuple("-1"),factory.tuple("-1"))); bounds.boundExactly(0,factory.range(factory.tuple("0"),factory.tuple("0"))); bounds.boundExactly(1,factory.range(factory.tuple("1"),factory.tuple("1"))); bounds.boundExactly(2,factory.range(factory.tuple("2"),factory.tuple("2"))); bounds.boundExactly(3,factory.range(factory.tuple("3"),factory.tuple("3"))); bounds.boundExactly(4,factory.range(factory.tuple("4"),factory.tuple("4"))); bounds.boundExactly(5,factory.range(factory.tuple("5"),factory.tuple("5"))); bounds.boundExactly(6,factory.range(factory.tuple("6"),factory.tuple("6"))); bounds.boundExactly(7,factory.range(factory.tuple("7"),factory.tuple("7"))); bounds.boundExactly(8,factory.range(factory.tuple("8"),factory.tuple("8"))); bounds.boundExactly(9,factory.range(factory.tuple("9"),factory.tuple("9"))); bounds.boundExactly(10,factory.range(factory.tuple("10"),factory.tuple("10"))); bounds.boundExactly(11,factory.range(factory.tuple("11"),factory.tuple("11"))); bounds.boundExactly(12,factory.range(factory.tuple("12"),factory.tuple("12"))); bounds.boundExactly(13,factory.range(factory.tuple("13"),factory.tuple("13"))); bounds.boundExactly(14,factory.range(factory.tuple("14"),factory.tuple("14"))); bounds.boundExactly(15,factory.range(factory.tuple("15"),factory.tuple("15"))); bounds.boundExactly(16,factory.range(factory.tuple("16"),factory.tuple("16"))); bounds.boundExactly(17,factory.range(factory.tuple("17"),factory.tuple("17"))); bounds.boundExactly(18,factory.range(factory.tuple("18"),factory.tuple("18"))); bounds.boundExactly(19,factory.range(factory.tuple("19"),factory.tuple("19"))); bounds.boundExactly(20,factory.range(factory.tuple("20"),factory.tuple("20"))); bounds.boundExactly(21,factory.range(factory.tuple("21"),factory.tuple("21"))); bounds.boundExactly(22,factory.range(factory.tuple("22"),factory.tuple("22"))); bounds.boundExactly(23,factory.range(factory.tuple("23"),factory.tuple("23"))); bounds.boundExactly(24,factory.range(factory.tuple("24"),factory.tuple("24"))); bounds.boundExactly(25,factory.range(factory.tuple("25"),factory.tuple("25"))); bounds.boundExactly(26,factory.range(factory.tuple("26"),factory.tuple("26"))); bounds.boundExactly(27,factory.range(factory.tuple("27"),factory.tuple("27"))); bounds.boundExactly(28,factory.range(factory.tuple("28"),factory.tuple("28"))); bounds.boundExactly(29,factory.range(factory.tuple("29"),factory.tuple("29"))); bounds.boundExactly(30,factory.range(factory.tuple("30"),factory.tuple("30"))); bounds.boundExactly(31,factory.range(factory.tuple("31"),factory.tuple("31"))); Variable x19=Variable.unary("this"); Decls x18=x19.oneOf(x6); Expression x22=x19.join(x10); Formula x21=x22.one(); Formula x23=x22.in(Expression.INTS); Formula x20=x21.and(x23); Formula x17=x20.forAll(x18); Expression x26=x10.join(Expression.UNIV); Formula x25=x26.in(x6); Expression x30=x7.product(x11); Expression x29=x7.join(x30); Formula x28=x29.in(x6); Expression x33=x8.product(x12); Expression x32=x8.join(x33); Formula x31=x32.in(x6); Expression x37=x9.product(x13); Expression x36=x9.join(x37); Formula x35=x36.one(); Formula x38=x36.in(Expression.INTS); Formula x34=x35.and(x38); Expression x42=x9.product(x14); Expression x41=x9.join(x42); Formula x40=x41.one(); Formula x43=x41.in(Expression.INTS); Formula x39=x40.and(x43); Expression x47=x9.product(x15); Expression x46=x9.join(x47); Formula x45=x46.one(); Formula x48=x46.in(Expression.INTS); Formula x44=x45.and(x48); IntExpression x53=IntConstant.constant(3); Expression x52=x53.toExpression(); Formula x51=x13.eq(x52); IntExpression x56=IntConstant.constant(14); Expression x55=x56.toExpression(); Formula x54=x14.eq(x55); Formula x50=x51.and(x54); IntExpression x59=IntConstant.constant(0); Expression x58=x59.toExpression(); Formula x57=x15.eq(x58); Formula x49=x50.and(x57); Variable x63=Variable.unary("c"); Decls x62=x63.oneOf(x6); Variable x65=Variable.unary("env"); Decls x64=x65.oneOf(x9); Decls x61=x62.and(x64); Expression x69=x63.join(x10); IntExpression x68=x69.sum(); Expression x71=x65.join(x47); IntExpression x70=x71.sum(); Formula x67=x68.gte(x70); Expression x74=x63.join(x10); IntExpression x73=x74.sum(); Expression x76=x65.join(x42); IntExpression x75=x76.sum(); Formula x72=x73.lte(x75); Formula x66=x67.and(x72); Formula x60=x66.forAll(x61); Variable x80=Variable.unary("c"); Decls x79=x80.oneOf(x6); Variable x82=Variable.unary("env"); Decls x81=x82.oneOf(x9); Variable x84=Variable.unary("rookie"); Decls x83=x84.oneOf(x7); Variable x86=Variable.unary("full_grown"); Decls x85=x86.oneOf(x8); Decls x78=x79.and(x81).and(x83).and(x85); Expression x92=x82.join(x42); IntExpression x91=x92.sum(); Expression x94=x80.join(x10); IntExpression x93=x94.sum(); IntExpression x90=x91.minus(x93); Expression x96=x82.join(x37); IntExpression x95=x96.sum(); Formula x89=x90.gt(x95); Expression x99=x86.join(x33); Formula x98=x80.in(x99); Expression x102=x84.join(x30); Formula x101=x80.in(x102); Formula x100=x101.not(); Formula x97=x98.and(x100); Formula x88=x89.implies(x97); Formula x104=x89.not(); Expression x107=x84.join(x30); Formula x106=x80.in(x107); Expression x110=x86.join(x33); Formula x109=x80.in(x110); Formula x108=x109.not(); Formula x105=x106.and(x108); Formula x103=x104.implies(x105); Formula x87=x88.and(x103); Formula x77=x87.forAll(x78); Formula x111=x0.eq(x0); Formula x112=x1.eq(x1); Formula x113=x2.eq(x2); Formula x114=x3.eq(x3); Formula x115=x4.eq(x4); Formula x116=x5.eq(x5); Formula x117=x6.eq(x6); Formula x118=x7.eq(x7); Formula x119=x8.eq(x8); Formula x120=x9.eq(x9); Formula x121=x10.eq(x10); Formula x122=x11.eq(x11); Formula x123=x12.eq(x12); Formula x124=x13.eq(x13); Formula x125=x14.eq(x14); Formula x126=x15.eq(x15); Formula x16=Formula.compose(FormulaOperator.AND, x17, x25, x28, x31, x34, x39, x44, x49, x60, x77, x111, x112, x113, x114, x115, x116, x117, x118, x119, x120, x121, x122, x123, x124, x125, x126); Solver solver = new Solver(); solver.options().setSolver(SATFactory.DefaultSAT4J); solver.options().setBitwidth(6); solver.options().setFlatten(false); solver.options().setIntEncoding(Options.IntEncoding.TWOSCOMPLEMENT); solver.options().setSymmetryBreaking(20); solver.options().setSkolemDepth(0); System.out.println("Solving..."); System.out.flush(); Solution sol = solver.solve(x16,bounds); System.out.println(sol.toString()); } }
とりあえず読み取れるのは、
「Int に対して 2の6乗のスコープを指定したら、
2の6乗ぶんのプレイスホルダーが設定されて、
さらにそれがなんらかの掛け算されていそう」
な気配、です。
というわけで、冒頭に挙げたアイデア、
テストデータの生成に、Alloy のモデル発見ロジックを使おうというアイデアは、現実的ではなかった。
いやまてよ、テストデータは、あくまで、Alloy によって生成された式の充足例に、
なんらかの具体値を当てはめればいいだけなんだから、
（※↑happy path 用のテストデータのみを考えた場合。negative path 用データはまた別に考察する。）
『Alloy のモデル発見ロジック』そのものにデータ生成処理を負担させる必要はないはずだよな。。。
テストデータ生成 = "Alloyの充足例に具体値を割り振る" という処理は、
モデル発見と同じ、制約充足問題（Constraint satisfaction problem）ではある（と思う）、が、
それは、Alloy のモデル発見プロセスとは別の工程として考えるべき、というのが今回の結論かな・・・？
Alloy Analyzer でOrphan Removal（を、もういちど。）
前回、写真共有サービスを想定して、@OneToMany(orphanRemoval=true) な
エンティティ群を定義してみました。その書き直し版です。
前回は、「状態をあらわすsig」を、書くと言っておきながら、
操作対象のインスタンス（=削除するUserとPhoto）のことだけを考えていました。
しかし、本来「状態」とは、操作対象でないインスタンスも含めて
（=RDBでいうと、関係するテーブルのレコードぜんぶ）表現していないと
いけないのでは思い直し、書き直しました。
module orphanRemoval /* 基本のエンティティ ======================================================= */ sig User { photos: set Photo } sig Photo { owner: one User } // 所有者のいないPhotoは無い fact { photos = ~owner } /* 状態管理用エンティティ =================================================== */ /* ■User削除前 */ one sig PhotoRel_RightS { u: set User, p: some Photo, rel: p -> u } { rel = p <: owner } fact { // ※このsigのフィールドはすべてのインスタンスを扱っていること all everyUser:User, everyPhoto:Photo, s:PhotoRel_RightS | (everyUser in s.u) && (everyPhoto in s.p) } /* ■UserのPhotoだけ削除完了 */ one sig PhotoRel_OrphanRemovedS { delUser: set User, u'': set User, p'': some Photo, rel'': p'' some -> (u'' - delUser) } { rel'' = p'' <: owner // ※Photoを限定：deluserのphotsは無い。 p'' = (u'' - delUser).photos } fact { all before:PhotoRel_RightS, process:PhotoRel_OrphanRemovedS, after:PhotoRel_AllRemovedS | // ※delUserを限定 process.delUser = before.u - after.u' && // ※Userを限定 (process.u'' = before.u) } /* ■User/Photo削除後 */ one sig PhotoRel_AllRemovedS { u': some User, p': some Photo, rel': p' -> u' } { rel' = p' <: owner // ※Photoを限定 p' = u'.photos } fact { // ※Userを限定：削除されたUserが必ず存在すること all before:PhotoRel_RightS, after:PhotoRel_AllRemovedS | (before.u - after.u') != none }
エンティティの sigと、状態を表す sig 、そして、それらにまつわる fact はこんな感じです。
状態を表す sig は、より厳密になったと思います。
そして、削除の振る舞いの表現は、以下のようにしました。
各状態が持つ、Photo -> User 型フィールド同士を比較すればいいはずです。
/* 振る舞いの表現 =========================================================== */ /* ▼各状態のrelを比較して判定。 */ pred deleteUser( rightS: PhotoRel_RightS, orphanRemovedS: PhotoRel_OrphanRemovedS, allRemovedS: PhotoRel_AllRemovedS, userDeleted: User ) { after_OrphanRemoved[rightS, orphanRemovedS] and after_AllRemoved[rightS, allRemovedS, userDeleted] } pred after_OrphanRemoved( rightS'': PhotoRel_RightS, orphanRemovedS'': PhotoRel_OrphanRemovedS ) { rightS''.rel - orphanRemovedS''.rel'' = orphanRemovedS''.delUser.photos <: owner } pred after_AllRemoved( rightS': PhotoRel_RightS, allRemovedS': PhotoRel_AllRemovedS, userDeleted': User ) { rightS'.rel - allRemovedS'.rel' = userDeleted'.photos <: owner } /* 振る舞いのcheck ========================================================== */ check deleteUser { all user: User, rightS: PhotoRel_RightS, orphanRemovedS: PhotoRel_OrphanRemovedS, allRemovedS: PhotoRel_AllRemovedS | // ※削除するUserを事後条件から特定 // TODO: これの else はどう表現するべきなのか？ user = rightS.u - allRemovedS.u implies deleteUser[rightS, orphanRemovedS, allRemovedS, user] }
事前状態 PhotoRel_RightS にも、事後状態 PhotoRel_AllRemovedS にも、
削除する（した）Userを特定する情報がありません。
それが正しいのかどうかわからないんですが、結果的にそうなりました。
この問題は、両者の差分（rightS.u - allRemovedS.u）をとることで、簡単に解決できるわけですが、
プログラマーの思考には、なんかしっくりこないやり方です。
事後の状態にあわせて引数を定義する・・・？
じゃあその定義外の引数については、どう考えたらいいんだろう？
あるいは、この定義に合わない「状態」（の組み合わせ）のほうを、除外していることになるんだろうか。
でもそれだったら、factで表現すべきだよな・・・？
そして前回同様、「状態をあらわすsig」の記述には手こずりました。
「状態」と、ひとくちに言っても、そこには、エンティティと/フィールドと/制約/
の三者が絡むという複雑さがあるので、alloyの要領に慣れないうちは、
このように手こずるんだと思います。ただ、正しく書ければ、それがビジュアルに
検証できるというありがたさがあるので、それを信じて今後も頑張る。
それにしても、たった一対のOneToMany（OneToOne）を表現するだけでもこの記述量とは・・・
とてもじゃありませんが、一般的なWEB＋RDBのシステム開発現場で、
普段づかい出来るような代物ではありません。
これらの一連の制約の記述、自動生成できないかな。DSL的に。
alloy言語そのものを拡張するか、あるいは、
alloy4eclipse のように、IDEのプラットフォームに乗っかって、
コードスニペットとして自動生成するツールを作るか、、、
面倒なものに手を出してしまった。。。
Alloy Analyzer でOrphan Removal
今回は、JPAでいう Orphan Removal のような、依存のある関連を扱ってみます。
Ruby on Rails でいうと
:dependent => :destroy とか、 :dependent => :delete_all といった、
アソシエーションのオプションを使って制御するアレですね。
JPA2でいうと、
@OneToMany(orphanRemoval=true) のようなアノテーション属性で制御するアレですね。
要は、親レコードが削除されたときに、親の無い子レコード（orphan）が発生しないようにするための策です。
ここでちょっと今までのやり方について再考しました。
今までにおぼえたやり方だと、
たとえば写真共有サービスを題材に考える場合
sig User { photos: set Photo } sig Photo { owner: one User } fact { // User <: photos = ~(Photo <: owner) // 相互な参照関係を↑いままでこう書いていたが、冗長だった。 // ↓このほうがスマート。id:kencoba さん、ご指摘ありがとうございます。 photos = ~owner }
このように、
- Photo の owner の限定子は、one にする
- 相互に参照しあう fact を書く
ことで
『Userに関係されていないPhotoは存在しない』
状態を定義できています。
しかしこれはあくまで静的な状態、つまり、エンティティ群のある状態を表現しているに過ぎないので、
『Userがサービスを退会したときにそのUserのphotosも削除されるかどうか』
というように、状態の遷移を伴う制約が成り立つかどうかは、定義できていません。
Orphan Removal の挙動を表現するにあたっては少なくとも、
- まず、User.photos を削除。そのあとに User を削除
というところも表現すべきかと。
Orphan Removal
今回のような、エンティティ = sig の追加削除を検査するには、どうも以下のような要領でやるのが基本のようです。
- 状態を表す sig を作り
- pred で、事前状態/事後状態 で結びこみ
- その pred の式を「成り立たせることができる」コンテキストを定義する
1.状態を表す sig を作る。
Tevfik Bultan 先生の資料では、事前状態・事後状態を、それぞれ sig で表現していたので、まずはそれに倣います。
この、状態を表す sig が、エンティティとしての sig を、フィールドに保持する形をとっています。
エンティティとしての sig を単独で持たせるだけでなく、そいつが持つ「関連」ごと保持するパターンが多いでしょうね、状態を管理する以上は。
でも状態を sig で表現するのはちょっとコツがいりますすね。
sig の定義に続けて書く {} （シグネチャファクト）内は、fact なので、どんな条件でも書けるんですが、
ここには、例えば、"User - u" のように、User エンティティ群全体を利用するような条件は
書かないのが正しいようです。書くと、そのあとの pred を構成する段になって、反例ばかり出てきて行き詰まりますし。
あくまでこの sig の中で完結するように条件を書くようにするのがよいようです。
2014/01/08 訂正
PhotoRel_RightState の各フィールドが、すべてのインスタンスを指し示していることを
意図して fact を書いていたんですが、そのようになっていなかったので、修正しました。
one sig PhotoRel_RightState { u: set User, p: some Photo, rel: Photo some -> User } fact { // PhotoRel_RightState の各フィールドは、すべてのインスタンスを指し示している、という状態を表現するfact all anyUser: User, anyPhoto: Photo, rs: PhotoRel_RightState | (anyUser in rs.u) && (anyPhoto in rs.p) && (rs.rel = rs.p <: owner) } /* User.photos の削除後の状態 */ lone sig PhotoRel_OrphanRemovedState { u': one User, p': some Photo, rel': Photo some -> User }{ #p' = 0 rel' = p' -> u' } /* そして User 削除後の状態 */ lone sig UserRemovedState { _u: lone User }{ #_u = 0 }こうしました。なお、削除まわりの状態を表す sig は、通常状態を表す sig の限定子が one なのに対して、lone です。
削除のときだけあらわれる、一時的な状態にはこういう対処でよい？2.pred で、事前状態/事後状態 で結びこみ
ここでの pred は、事前状態/事後状態/操作するエンティティ を引数にとり、
事前状態を事後状態を何らかのかたちでイコールで結びつけるのが基本の形みたいですね。
ここでは、子(Photo)エンティティの削除と親(User)エンティティの削除を、ふたつの pred に分けています。pred deleteUser(rightState: PhotoRel_RightState, orphanRemoved: PhotoRel_OrphanRemovedState, userRemoved: UserRemovedState, u: User) { // まず子を削除 ついで親を削除 after_PhotoRel_OrphanRemoved[ orphanRemoved, (u.photos - u.photos) -> u ] && after_UserRemoved[ // u.photos - u.photos がつまり削除をあらわしている。 userRemoved, u - u // u - u がつまり削除をあらわしている。 ] } pred after_PhotoRel_OrphanRemoved(orphanRemoval: PhotoRel_OrphanRemovedState, rel: Photo -> User) { orphanRemoval.rel' = rel } pred after_UserRemoved(userRemoved: UserRemovedState, u: User) { userRemoved._u = u }3.pred の式を「成り立たせることができる」コンテキストを定義する
それを check とするわけです。check { all u: User, rightState: PhotoRel_RightState, orphanRemoval: PhotoRel_OrphanRemoval, userRemoved: UserRemovedState | deleteUser[rightState, orphanRemoval, userRemoved, u] }ここは特にひねりはいらなかった。
以上です。
ところで、pred に引数を渡すときの要領は、これでいいのかな？
上の例でいうと、のところ。
after_PhotoRel_OrphanRemoved[orphanRemoved, (u.photos - u.photos) -> u]
after_UserRemoved[userRemoved, u - u]
photos の削除を表すのに u.photos - u.photos と書いたり、
User の削除を表すのに、u - u と書いたりしてますが、
この書き方が適切なのかどうかは、自信ないです。プログラム処理をAlloy で表現するときの基本は、
「状態を表す式=関数に、その式が真になるような引数を渡すこと」であるという原則は理解したんですが、
その「引数の渡し方」について学ぶ材料がもっと欲しいな。
WEBや書籍でみつかる Alloy のサンプルは、この、引数の渡し方の記述を示していない例が多くて、
なんでそんな文化になってんのかなー。まあ、この先学習を進めて、様々なケーススタディをこなす段階になったら、きっとまた理解が進むでしょう。
さて、Orphan Removal をやったからには、
Nullify = 外部キーがnull を許容するケースについても考えないといけないですね。
それは次回に。続々・Alloy Analyzer で「振る舞い」を表現するときの基本：繰り返し処理について
プログラムの処理をAlloyで表現する基本型は、
- 事後状態をあらわす式に引数を与えること
であるってことを前々回確認しました。
図を再掲しましょう。
今回はそこに、繰り返し処理を織り交ぜてみます。
この本の p.171-172 の内容です。
- 作者: 中島震
- 出版社/メーカー: オーム社
- 発売日: 2012/04/20
- メディア: 単行本（ソフトカバー）
- 購入: 1人 クリック: 11回
- この商品を含むブログ (4件) を見る
以下に書くのはもちろん僕自身の解釈を含めていますし、そもそも完全に理解ができているわけではないんで、
参考にする場合はご注意ください。このjavascriptを Alloy で表現してみます。
var x = 1; // 0 以上であること // 1) 代入処理 var y = 0; // 2) ループ while(x > y) { // 3) ループ内代入処理 y = y + 1; } { x = y }繰り返し処理のブロックは、
当然必要であるところの、最終的な事後条件 に加えて、
以下の4つの式を考える必要があるみたいです。
- ループ不変量
- 事後条件 = ループが終了する条件と、次に続く処理を表す
- 事前条件 = ループが継続する条件とブロック内処理を表す
- ループのブロック内処理
計 5 つ。では順にみていきましょう。
0. 最終的な事後条件
open util/integer sig Env { x,y: Int } pred fin(x,y: Int) { eq[x, y] }pred fin が最終的な事後条件です。当然こうなりますね。
1. ループ不変量
ループ不変量の正確な定義は実はよく理解していないんですが、
繰り返すブロックの中の処理が持つ性質を表現すればいいようです。
このjavascriptの例だと少なくとも{ x >= y }が、ループ不変量にあたるいえます。なのでこうだ。loopIdentity という名で表現しました。
pred loopIdentity(x,y: Int) { gte[x, y] }2. 事後条件 = ループが終了する条件と、次に続く処理を表す
このプログラムのループ部分の事後条件は、さきほど定義した pred fin を導くわけですから、以下のようになります。
さらに、この式には、ループ不変量も含まれてないといけないようです。pred loopBreak(x,y: Int) { (eq[x, y] and loopIdentity[x, y]) implies fin[x, y] }3. 事前条件 = ループが継続する条件とブロック内処理を表す
2. の、ループの収量を表す式と、3. の、ループの継続を表す式とを、別々に扱うんですね。
プログラマには無い習慣なんでいまいちピンと来ないですけど。pred loopGoOn(x,y: Int) { not(eq[x, y]) and loopIdentity[x, y] implies loopProc[x, y] }で、この loopProc は何かというと、
4. ループのブロック内処理
です。つまり
pred loopProc(x,y: Int) { loopIdentity[x, add[y, 1]] }loopIdentity をここでの事後条件と位置付けて、原則どおり、
事後条件のpredに引数を渡しています。そしてもうひとつ式が必要ですね。最初の代入文の表現です。
この文の事後条件 = 後に続く処理の事前条件 に、引数を渡すとなると・・・pred start(x: Int) { loopIdentity[x, 0] }こうなります。
「この文の事後条件 = 後に続く処理の事前条件 = 不変量の式」なんですね。
3. の式じゃないんだ。
1. の式は"不変"量っていうくらいだから、事前条件としてあつかってもいいってことですかね？これらを check するには、以下のように書きます。
check { all env: Env | gte[env.x, 0] => start[env.x] all env: Env | loopGoOn[env.x, env.y] all env: Env | loopBreak[env.x, env.y] }x は 0 以上であるという初期化処理を経て、pred start を検査すればいいわけです。
それに加えて別途、ループの事前条件、事後条件を検査をするんだそうです。以上の登場人物たちを図にまとめると
こんな感じかな。ループ不変量は重要っぽいですね。
ちなみにこの本のこの箇所、ページ数でいうとわずか2ページほどなんですが、
これだけ理解するのに何日もかかっちゃいました。
数学の素養のないプログラマーにはきつい本です。が、このループ処理の解説の箇所に限っていえば、
わかりにくい理由の大方は、関数名のネーミングだと思います。"pred ichi" とか、"pred ni" とかなんだもん。あと、本では、Env という sig は書かれていませんでした。裸の x, y という Int 型の変数をそのまま使って check 節が記述されていました。
しかしそれでは動きません。動かないっつーか、どんな式でもtrue になっちゃって、反例を返してくれなかった。
エラーにならないってことは、何か別の意味を成してしまっていたんでしょうね、x, y を裸で使った場合。
（ということは、前々回示したソースコードも sig Env {x,y: Int} を使う必要があったってことです。修正しました。）ところで数学の素養の無さといえば、僕は高校時代の数学のテストの点はいつも、0点とか4点とか0点でした。
しまいには、教科書の初っぱなに載ってる「例題1」すらわからなかった。
わからないならわからないでいいんですが、あのわからなさにも、このように、理由が実はあったんでしょうか。いずれにせよ、本2ページ読むのに何日もかかるようでは、Alloyのパワーを、あらゆるプログラマが日常的に利用する日は来ないでしょう。
なので今回扱ったようなところは、テンプレ化して何も考えずに使えるようにしたいものです。
この一連の Alloy のエントリはそこに至るための試行錯誤の過程の記録です。続・Alloy Analyzer で「振る舞い」を表現するときの基本【失敗】
(※追記あり) (※結論へ)
今回も引き続き、pred について調べます。
以下のような動きを Alloy で表現する方法を探りたいと思います。
- User エンティティが Instantiate される。
- User エンティティの id フィールドに、発番されたidが格納される。
テーブルをクラス としてマッピングしたときのエンティティを、
newして、それから永続化するときに、必ず出てくる動きですね。モデル定義は以下のようになります。
sig ID { value: disj one Int } sig User { id: disj lone ID }それから、
1. の前後の状態を判定するために、エンティティ群の状態を扱う sig も必要ですね。
こいつで事前条件事後条件を管理しましょう。(※)one sig DefaultContext { exists: User -> ID }{ exists = User <: id #(ID - User.exists) = 1 // User に保持されないID の数 #(User - exists.ID) = 1 // ID を保持しないUser の数 } one sig AfterContext extends DefaultContext { expected: User -> ID }{ expected = exists + (User - exists.ID) -> (ID - User.exists) }こんな感じでどうだろう。
User -> ID
という関係じたいを exists という名で保持し(2行目)、そしてそれは現存する「id を持つ User」に限ること(4行目)、
っていう意味ですこれは。
そして、新規追加しようとしている User エンティティと、そいつに割り振るための ID も、
各々ひとつづつ存在していることを義務づけました。
そして事後条件は、当然ですが事前条件を前提としているので、extends を利用して表現してみました。
事前条件の exists に加えて、IDの振られていない User -> ID を持たせて、これらの和集合を expected としています。実行すると、
お、ここまでのところ問題なさそう。では 1. の pred を書いてみましょうか。
とりあえずぜんぶの登場人物を引数で渡すことにするとしてcheck userAdd{ all new_user: User - (User <: id).ID | // idを保持していないUser all new_id: ID - User.id | // Userに保持されていないID addUser[DefaultContext, AfterContext, new_user, new_id] } pred addUser(ctx: DefaultContext, ctx': AfterContext, u: User, i: ID) { ctx'.expected = ctx.exists ++ (ctx.exists + u -> i) }Alloyから反例が提出されなかったんで、良いようです。
しかしほんとにこれでいいのかな。この式がtrueになるのは自明すぎるような気もするんですが・・・(※)
では続けて、
2.User エンティティの id フィールドに、発番されたidが格納される。
の pred を書いてみましょう。上記と同じ条件の引数を使うことになります。check setId { all new_user: User - (User <: id).ID | all new_id: ID - User.id | setId[new_user, new_id] } pred setId(u: User, i: ID) { i = u.id ++ i }これもAlloyから反例が提示されないんで、正しいと思われますが、正しくて当然ですよね、この式だと。
この式もあまりに自明すぎて、書く意味意味無いかな？まあ、フィールドに値を入れているだけなんで、当然の帰結ですが・・・(※)ここまで書いてみて、前回の内容を思い出してみました。前回の内容によると
「振る舞いの表現」=「事後条件を包括する何らかの式」
となるはずなんですが、どうも感じが違いますね。
これは書き直しの余地が大いにありそうです。
まずは、上記の、sig DefaultContext と、sig AfterContext は消します。
sig ID { value: disj one Int } sig User { id: disj lone ID } fun userNotPersist() : User { User - (User <: id).ID } fun idNotInvoked() : ID { ID - User.id }ついでに関数もふたつ作りました。
そしてあらためて、
「1.User エンティティが Instantiate される。」を表現するには？という問題。「振る舞いの表現」=「事後条件を包括する何らかの式」であるという原則からはずれないために、
"制約"と"それを成り立たせる文脈"をきっちりわけて考えていきます。
事後条件はこう。// u_i が事前のUser -> ID、u_i'が事後のUser -> ID です。 pred AfterCostraint(u_i,u_i': User -> ID, u: User, i: ID) { u_i' = u_i + u -> i }これが"制約"。で、これを成り立たせるための引数は、
check afterContext { AfterCostraint[ User <: id, User <: id + userNotPersist -> idNotInvoked, userNotPersist, idNotInvoked ] }・・・あれ、これ、check と pred を分割せずに書くと
check afterContext { User <: id + userNotPersist -> idNotInvoked = User <: id + userNotPersist -> idNotInvoked }になって、右辺に書いてる内容と左辺に書いてる内容がまったく同じ。つまり何も表現していないのと同じだ。
これは、自然言語で言い換えると、
表現しようとしている「振る舞い」が、そのまま事後条件になってしまっている。
ということですね。これか問題だったのか。つまり、やっぱり題材が悪かったんですかね。もうちょっと振る舞いらしい振る舞いを入れないと。
題材から考え直す必要がありそうです。
このエントリは失敗です。無かったことにします。
教訓は、「エンティティをいっこ、既存のエンティティ群に足しました。」みたいな、
単純すぎる振る舞いは、表現しないほうがいい
ということです。Alloy Analyzer で「振る舞い」を表現するときの基本：代入について
※ 2013/07/31 ソースコードを修正しました。ここまでは、Alloy Analyzer を使って、エンティティの関連を表現してきました。
しかし形式記述言語 Alloy には pred (=predicate 述語) というものがあります。ん、あれ？述語？
Alloy の記述の基本は式です。true or false しかない式だけで、どうやって「述語」を成り立たせるんだろう？
僕はここまでのところまだ pred をぜんぜん使ってないんですが、
この本を読んでいて、
- 作者: 中島震
- 出版社/メーカー: オーム社
- 発売日: 2012/04/20
- メディア: 単行本（ソフトカバー）
- 購入: 1人 クリック: 11回
- この商品を含むブログ (4件) を見る
p.170 からの、「7.1.2 プログラムの振る舞い解析の例」
を読んで、「お、そういうことか。」とちょっと思ったので、書き留めておこうと思います。サンプルプログラム
var a, x, y; // 1) 代入その一 a = x + 1; // 2) 分岐 if (a == 1) { y = 1; } else { y = a; } // 3) 代入その二 y = x + 1;このjavascript プログラムをAlloyで表現するにはどうするか。
逆から考えるんだ。
まずは、3) 代入その二 が、終わった後の状態を式として表現します。
これは、このプログラムが走り終わったあとの事後条件となります。open util/integer sig Env { x: Int } pred fin [x,y: Int] { eq[y, add[x,1]] }こうです。特に問題ないですね。そして次に、2) 分岐のところですが、
ここでやるべきことは、このプログラムの処理を、
後につづく条件Fin を成り立たせる式として表現すること、のようです。
わかりにくい日本語ですね。これはコード見てもらったほうが早い。pred proc_1 (x,a: Int) { ((eq[a,1] and fin[x,1]) or (not(eq[a,1]) and fin[x,a])) }こうです。
つまり、プログラムでいう「代入」は、ここでは「"事後"を表す式の変動要素=引数を満たす事」で表現してるんですね〜。
ということは、1) 代入その一はpred start (x: Int) { proc_1[x,add[x,1]] }こうだ。間違いない。
ちなみにこの仕様記述をキックするところは、こういう書き方なります。x の初期化をを忘れずにね、ってことです。run { all env: Env | start[env.x]} check { all env: Env | start[env.x]}そして、この pred start が、「事前条件」として成り立ちます。
さてこの構造を図に書いてみました。これでいいかな。
矢印は、プログラムでいう"処理"です。トランザクションスクリプトです。事前条件っていうのは事後条件を包括するものなわけですね、考えてみたら当たり前ですけど。
で、この包括関係を、順次、式で表現していくことで、Alloy で「振る舞い」が表現（評価）できるんですね。よしわかった。とりあえず原則だけは分かった。
利用例は、また後日のエントリでびしびし出てくると思います。
