msakai · January 13, 2011 00:29 · Jan 14, 2011 · Jan 13, 2011 · Jan 13, 2011
diff --git a/fakecoin3.als b/fakecoin3.als
@@ -0,0 +1,31 @@
+sig Coin {}
+
+sig State {
+  disj left, right : set Coin, 
+  eq, lt, gt : lone State,
+  candidates : set Coin,
+} {
+  not this in this.^(@eq+@lt+@gt)
+  not lone candidates => {
+    #left = #right
+    eq.@candidates = candidates - left - right
+    lt.@candidates = candidates & left
+    gt.@candidates = candidates & right
+
+    -- optimization
+    one eq
+    one lt
+    one gt
+    some left
+    left in candidates or right in candidates
+  }
+}
+
+pred solve {
+  one root : State {
+    root.candidates = Coin
+    no root.(eq+lt+gt).(eq+lt+gt).(eq+lt+gt) -- optimization
+  }
+}
+
+run solve for 1 int, 13 State, exactly 9 Coin
diff --git a/fakecoin.als b/fakecoin.als
@@ -1,3 +1,4 @@
+// 失敗版
 sig Coin {}
 
 abstract sig State {

diff --git a/fakecoin2.als b/fakecoin2.als
@@ -0,0 +1,35 @@
+sig Coin {}
+
+pred test[s, left, right, eq, lt, gt : set Coin] {
+  no left & right
+  #left = #right
+  eq = s - (left + right)
+  lt = s & left
+  gt = s & right
+}
+
+pred final[s : set Coin] { lone s }
+
+pred solve {
+  some l, r, eq, lt, gt,
+       eq_l, eq_r, eq_eq, eq_lt, eq_gt,
+       lt_l, lt_r, lt_eq, lt_lt, lt_gt,
+       gt_l, gt_r, gt_eq, gt_lt, gt_gt
+       : set Coin {
+    test[Coin, l, r, eq, lt, gt]
+    test[eq, eq_l, eq_r,  eq_eq, eq_lt, eq_gt]
+    test[lt, lt_l, lt_r,  lt_eq, lt_lt, lt_gt]
+    test[gt, gt_l, gt_r,  gt_eq, gt_lt, gt_gt]
+    final[eq_eq]
+    final[eq_lt]
+    final[eq_gt]
+    final[lt_eq]
+    final[lt_lt]
+    final[lt_gt]
+    final[gt_eq]
+    final[gt_lt]
+    final[gt_gt]
+  }
+}
+
+run solve for 5 int, exactly 8 Coin
diff --git a/gistfile2.txt b/gistfile2.txt
diff --git a/fakecoin.als b/fakecoin.als
@@ -0,0 +1,31 @@
+sig Coin {}
+
+abstract sig State {
+  candidates : set Coin,
+}
+
+sig Branch extends State {
+  left, right : set Coin, 
+  eq, lt, gt : State
+}
+fact {
+  all b : Branch {
+    not b in b.^(eq+lt+gt)
+    no b.left & b.right
+    #b.left = #b.right
+    b.eq.candidates = b.candidates - (b.left + b.right)
+    b.lt.candidates = b.candidates & b.left
+    b.gt.candidates = b.candidates & b.right
+  }
+}
+
+sig Leaf extends State { }
+{ lone candidates }
+
+pred solve {
+  one root : State {
+    root.candidates = Coin
+    State in root.*(eq+lt+gt)
+  } 
+}
+run solve for 5 int, 4 Branch, 9 Leaf,  exactly 8 Coin
diff --git a/gistfile2.txt b/gistfile2.txt