2014-02-02

“石の上にも三年” という格言を Alloy でモデリングします。

まあ、格言は実はどうでもよくて、Alloyにおける、数値（Integer）の扱いについて確認したかったんです。

Alloy 教科書の131ページには

整数の演算が必要に思えるなら、考え直したほうがいい。
より抽象的に記述したほうが、より問題に適合する記述にできることが多い。
〜（中略）〜
もちろん、数値演算への依存が大きいような問題を扱うのなら整数（あるいはもっと別の数値）
が必要になるだろうが、おそらくその問題は Alloy には向いていない。

と、書いてあります。

抽象によるソフトウェア設計−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 で、あの格言をモデリングする