Skip to content

Instantly share code, notes, and snippets.

@y-taka-23

y-taka-23/alloy_decimal.als

Created October 9, 2013 16:12
Show Gist options
  • Save y-taka-23/6903806 to your computer and use it in GitHub Desktop.
Save y-taka-23/6903806 to your computer and use it in GitHub Desktop.
Download ZIP
Alloy による十進位取り記数法のモデリング
Raw
alloy_decimal.als
// ************************************
// 十進法による符号なし整数演算のモデル
// ************************************
open util/ordering[Position]
// ------------------------------------
// 位取り記数法のモデリング
// ------------------------------------
// 位取りの位置
sig Position {
inverse : one Position // 桁の順番を逆転させたときの位置
}
// 桁の逆転に関する制約
fact inversePosition {
// 逆転は対称
inverse in ~ inverse
// 最初の桁と最後の桁は逆転させることで移り変わる
Position <: first -> Position <: last in inverse
// その他の桁に関する帰納的な定義
all p1 : Position - last, p2 : Position - first |
p1 -> p2 in inverse => p1.next -> p2.prev in inverse
}
// 各桁の数字
enum Digit { D0, D1, D2, D3, D4, D5, D6, D7, D8, D9 }
// 十進位取り記数法による符号なし整数
sig Decimal {
// すべての桁に数字が配置されていることに注意
// リトルエンディアン (Position が first 側が一の位) とする
notation : Position -> one Digit
}
// 十進表記が一致すれば整数として一致
fact uniqueNotation {
all n1, n2 : Decimal | n1.notation = n2.notation => n1 = n2
}
// ------------------------------------
// 加算の実装
// ------------------------------------
// 十進半加算器
// a, b は入力、s は (元の桁に残る) 和、c は上位桁への繰り上がり
pred halfAdd (a, b, s, c : Digit) {
(a = D0 && b = D0) => (s = D0 && c = D0)
(a = D0 && b = D1) => (s = D1 && c = D0)
(a = D0 && b = D2) => (s = D2 && c = D0)
(a = D0 && b = D3) => (s = D3 && c = D0)
(a = D0 && b = D4) => (s = D4 && c = D0)
(a = D0 && b = D5) => (s = D5 && c = D0)
(a = D0 && b = D6) => (s = D6 && c = D0)
(a = D0 && b = D7) => (s = D7 && c = D0)
(a = D0 && b = D8) => (s = D8 && c = D0)
(a = D0 && b = D9) => (s = D9 && c = D0)
(a = D1 && b = D0) => (s = D1 && c = D0)
(a = D1 && b = D1) => (s = D2 && c = D0)
(a = D1 && b = D2) => (s = D3 && c = D0)
(a = D1 && b = D3) => (s = D4 && c = D0)
(a = D1 && b = D4) => (s = D5 && c = D0)
(a = D1 && b = D5) => (s = D6 && c = D0)
(a = D1 && b = D6) => (s = D7 && c = D0)
(a = D1 && b = D7) => (s = D8 && c = D0)
(a = D1 && b = D8) => (s = D9 && c = D0)
(a = D1 && b = D9) => (s = D0 && c = D1)
(a = D2 && b = D0) => (s = D2 && c = D0)
(a = D2 && b = D1) => (s = D3 && c = D0)
(a = D2 && b = D2) => (s = D4 && c = D0)
(a = D2 && b = D3) => (s = D5 && c = D0)
(a = D2 && b = D4) => (s = D6 && c = D0)
(a = D2 && b = D5) => (s = D7 && c = D0)
(a = D2 && b = D6) => (s = D8 && c = D0)
(a = D2 && b = D7) => (s = D9 && c = D0)
(a = D2 && b = D8) => (s = D0 && c = D1)
(a = D2 && b = D9) => (s = D1 && c = D1)
(a = D3 && b = D0) => (s = D3 && c = D0)
(a = D3 && b = D1) => (s = D4 && c = D0)
(a = D3 && b = D2) => (s = D5 && c = D0)
(a = D3 && b = D3) => (s = D6 && c = D0)
(a = D3 && b = D4) => (s = D7 && c = D0)
(a = D3 && b = D5) => (s = D8 && c = D0)
(a = D3 && b = D6) => (s = D9 && c = D0)
(a = D3 && b = D7) => (s = D0 && c = D1)
(a = D3 && b = D8) => (s = D1 && c = D1)
(a = D3 && b = D9) => (s = D2 && c = D1)
(a = D4 && b = D0) => (s = D4 && c = D0)
(a = D4 && b = D1) => (s = D5 && c = D0)
(a = D4 && b = D2) => (s = D6 && c = D0)
(a = D4 && b = D3) => (s = D7 && c = D0)
(a = D4 && b = D4) => (s = D8 && c = D0)
(a = D4 && b = D5) => (s = D9 && c = D0)
(a = D4 && b = D6) => (s = D0 && c = D1)
(a = D4 && b = D7) => (s = D1 && c = D1)
(a = D4 && b = D8) => (s = D2 && c = D1)
(a = D4 && b = D9) => (s = D3 && c = D1)
(a = D5 && b = D0) => (s = D5 && c = D0)
(a = D5 && b = D1) => (s = D6 && c = D0)
(a = D5 && b = D2) => (s = D7 && c = D0)
(a = D5 && b = D3) => (s = D8 && c = D0)
(a = D5 && b = D4) => (s = D9 && c = D0)
(a = D5 && b = D5) => (s = D0 && c = D1)
(a = D5 && b = D6) => (s = D1 && c = D1)
(a = D5 && b = D7) => (s = D2 && c = D1)
(a = D5 && b = D8) => (s = D3 && c = D1)
(a = D5 && b = D9) => (s = D4 && c = D1)
(a = D6 && b = D0) => (s = D6 && c = D0)
(a = D6 && b = D1) => (s = D7 && c = D0)
(a = D6 && b = D2) => (s = D8 && c = D0)
(a = D6 && b = D3) => (s = D9 && c = D0)
(a = D6 && b = D4) => (s = D0 && c = D1)
(a = D6 && b = D5) => (s = D1 && c = D1)
(a = D6 && b = D6) => (s = D2 && c = D1)
(a = D6 && b = D7) => (s = D3 && c = D1)
(a = D6 && b = D8) => (s = D4 && c = D1)
(a = D6 && b = D9) => (s = D5 && c = D1)
(a = D7 && b = D0) => (s = D7 && c = D0)
(a = D7 && b = D1) => (s = D8 && c = D0)
(a = D7 && b = D2) => (s = D9 && c = D0)
(a = D7 && b = D3) => (s = D0 && c = D1)
(a = D7 && b = D4) => (s = D1 && c = D1)
(a = D7 && b = D5) => (s = D2 && c = D1)
(a = D7 && b = D6) => (s = D3 && c = D1)
(a = D7 && b = D7) => (s = D4 && c = D1)
(a = D7 && b = D8) => (s = D5 && c = D1)
(a = D7 && b = D9) => (s = D6 && c = D1)
(a = D8 && b = D0) => (s = D8 && c = D0)
(a = D8 && b = D1) => (s = D9 && c = D0)
(a = D8 && b = D2) => (s = D0 && c = D1)
(a = D8 && b = D3) => (s = D1 && c = D1)
(a = D8 && b = D4) => (s = D2 && c = D1)
(a = D8 && b = D5) => (s = D3 && c = D1)
(a = D8 && b = D6) => (s = D4 && c = D1)
(a = D8 && b = D7) => (s = D5 && c = D1)
(a = D8 && b = D8) => (s = D6 && c = D1)
(a = D8 && b = D9) => (s = D7 && c = D1)
(a = D9 && b = D0) => (s = D9 && c = D0)
(a = D9 && b = D1) => (s = D0 && c = D1)
(a = D9 && b = D2) => (s = D1 && c = D1)
(a = D9 && b = D3) => (s = D2 && c = D1)
(a = D9 && b = D4) => (s = D3 && c = D1)
(a = D9 && b = D5) => (s = D4 && c = D1)
(a = D9 && b = D6) => (s = D5 && c = D1)
(a = D9 && b = D7) => (s = D6 && c = D1)
(a = D9 && b = D8) => (s = D7 && c = D1)
(a = D9 && b = D9) => (s = D8 && c = D1)
}
// 十進全可算器
pred fullAdd (a, b, cIn, s, cOut : Digit) {
some s1, cOut1, cOut2 : Digit {
halfAdd[a, b, s1, cOut1]
halfAdd[s1, cIn, s, cOut2]
// 最後の半加算器では桁上がりは発生しない (c = D0) ことに注意
halfAdd[cOut1, cOut2, cOut, D0]
}
}
// 十進数同士の加算の関係 : n1 + n2 = answer
pred decPlus (n1, n2, answer : Decimal) {
// cOuts により各桁の繰り上がりをメモ化する
some cOuts : Decimal |
let n1n = n1.notation, n2n = n2.notation,
ansn = answer.notation, cosn = cOuts.notation {
halfAdd[n1n[first], n2n[first], ansn[first], cosn[first]]
all p : Position - first |
fullAdd[n1n[p], n2n[p], cosn[p.prev], ansn[p], cosn[p]]
}
}
// 例 : 794 + 1192 = 1986
pred example794Plus1192 {
some n1, n2, answer : Decimal |
let n1n = n1.notation, n2n = n2.notation {
// n1 = 794
n1n[first] = D4
n1n[first.next] = D9
n1n[first.next.next] = D7
all p : Position |
p in nexts[first.next.next] => n1n[p] = D0
// n2 = 1192
n2n[first] = D2
n2n[first.next] = D9
n2n[first.next.next] = D1
n2n[first.next.next.next] = D1
all p : Position |
p in nexts[first.next.next.next] => n2n[p] = D0
// n1 + n2 = answer
decPlus[n1, n2, answer]
}
}
run example794Plus1192 for 4 Position, 4 Decimal, 0 DecArray
// ------------------------------------
// 乗算の実装
// ------------------------------------
// 十進乗算器ユニット
// a, b は入力、結果は十進表示整数で返す
pred digitProd (a, b : Digit, answer : Decimal) {
let ansn = answer.notation {
(a = D0 && b = D0) => (ansn[first] = D0 && ansn[first.next] = D0)
(a = D0 && b = D1) => (ansn[first] = D0 && ansn[first.next] = D0)
(a = D0 && b = D2) => (ansn[first] = D0 && ansn[first.next] = D0)
(a = D0 && b = D3) => (ansn[first] = D0 && ansn[first.next] = D0)
(a = D0 && b = D4) => (ansn[first] = D0 && ansn[first.next] = D0)
(a = D0 && b = D5) => (ansn[first] = D0 && ansn[first.next] = D0)
(a = D0 && b = D6) => (ansn[first] = D0 && ansn[first.next] = D0)
(a = D0 && b = D7) => (ansn[first] = D0 && ansn[first.next] = D0)
(a = D0 && b = D8) => (ansn[first] = D0 && ansn[first.next] = D0)
(a = D0 && b = D9) => (ansn[first] = D0 && ansn[first.next] = D0)
(a = D1 && b = D0) => (ansn[first] = D0 && ansn[first.next] = D0)
(a = D1 && b = D1) => (ansn[first] = D1 && ansn[first.next] = D0)
(a = D1 && b = D2) => (ansn[first] = D2 && ansn[first.next] = D0)
(a = D1 && b = D3) => (ansn[first] = D3 && ansn[first.next] = D0)
(a = D1 && b = D4) => (ansn[first] = D4 && ansn[first.next] = D0)
(a = D1 && b = D5) => (ansn[first] = D5 && ansn[first.next] = D0)
(a = D1 && b = D6) => (ansn[first] = D6 && ansn[first.next] = D0)
(a = D1 && b = D7) => (ansn[first] = D7 && ansn[first.next] = D0)
(a = D1 && b = D8) => (ansn[first] = D8 && ansn[first.next] = D0)
(a = D1 && b = D9) => (ansn[first] = D9 && ansn[first.next] = D0)
(a = D2 && b = D0) => (ansn[first] = D0 && ansn[first.next] = D0)
(a = D2 && b = D1) => (ansn[first] = D2 && ansn[first.next] = D0)
(a = D2 && b = D2) => (ansn[first] = D4 && ansn[first.next] = D0)
(a = D2 && b = D3) => (ansn[first] = D6 && ansn[first.next] = D0)
(a = D2 && b = D4) => (ansn[first] = D8 && ansn[first.next] = D0)
(a = D2 && b = D5) => (ansn[first] = D0 && ansn[first.next] = D1)
(a = D2 && b = D6) => (ansn[first] = D2 && ansn[first.next] = D1)
(a = D2 && b = D7) => (ansn[first] = D4 && ansn[first.next] = D1)
(a = D2 && b = D8) => (ansn[first] = D6 && ansn[first.next] = D1)
(a = D2 && b = D9) => (ansn[first] = D8 && ansn[first.next] = D1)
(a = D3 && b = D0) => (ansn[first] = D0 && ansn[first.next] = D0)
(a = D3 && b = D1) => (ansn[first] = D3 && ansn[first.next] = D0)
(a = D3 && b = D2) => (ansn[first] = D6 && ansn[first.next] = D0)
(a = D3 && b = D3) => (ansn[first] = D9 && ansn[first.next] = D0)
(a = D3 && b = D4) => (ansn[first] = D2 && ansn[first.next] = D1)
(a = D3 && b = D5) => (ansn[first] = D5 && ansn[first.next] = D1)
(a = D3 && b = D6) => (ansn[first] = D8 && ansn[first.next] = D1)
(a = D3 && b = D7) => (ansn[first] = D1 && ansn[first.next] = D2)
(a = D3 && b = D8) => (ansn[first] = D4 && ansn[first.next] = D2)
(a = D3 && b = D9) => (ansn[first] = D7 && ansn[first.next] = D2)
(a = D4 && b = D0) => (ansn[first] = D0 && ansn[first.next] = D0)
(a = D4 && b = D1) => (ansn[first] = D4 && ansn[first.next] = D0)
(a = D4 && b = D2) => (ansn[first] = D8 && ansn[first.next] = D0)
(a = D4 && b = D3) => (ansn[first] = D2 && ansn[first.next] = D1)
(a = D4 && b = D4) => (ansn[first] = D6 && ansn[first.next] = D1)
(a = D4 && b = D5) => (ansn[first] = D0 && ansn[first.next] = D2)
(a = D4 && b = D6) => (ansn[first] = D4 && ansn[first.next] = D2)
(a = D4 && b = D7) => (ansn[first] = D8 && ansn[first.next] = D2)
(a = D4 && b = D8) => (ansn[first] = D2 && ansn[first.next] = D3)
(a = D4 && b = D9) => (ansn[first] = D6 && ansn[first.next] = D3)
(a = D5 && b = D0) => (ansn[first] = D0 && ansn[first.next] = D0)
(a = D5 && b = D1) => (ansn[first] = D5 && ansn[first.next] = D0)
(a = D5 && b = D2) => (ansn[first] = D0 && ansn[first.next] = D1)
(a = D5 && b = D3) => (ansn[first] = D5 && ansn[first.next] = D1)
(a = D5 && b = D4) => (ansn[first] = D0 && ansn[first.next] = D2)
(a = D5 && b = D5) => (ansn[first] = D5 && ansn[first.next] = D2)
(a = D5 && b = D6) => (ansn[first] = D0 && ansn[first.next] = D3)
(a = D5 && b = D7) => (ansn[first] = D5 && ansn[first.next] = D3)
(a = D5 && b = D8) => (ansn[first] = D0 && ansn[first.next] = D4)
(a = D5 && b = D9) => (ansn[first] = D5 && ansn[first.next] = D4)
(a = D6 && b = D0) => (ansn[first] = D0 && ansn[first.next] = D0)
(a = D6 && b = D1) => (ansn[first] = D6 && ansn[first.next] = D0)
(a = D6 && b = D2) => (ansn[first] = D2 && ansn[first.next] = D1)
(a = D6 && b = D3) => (ansn[first] = D8 && ansn[first.next] = D1)
(a = D6 && b = D4) => (ansn[first] = D4 && ansn[first.next] = D2)
(a = D6 && b = D5) => (ansn[first] = D0 && ansn[first.next] = D3)
(a = D6 && b = D6) => (ansn[first] = D6 && ansn[first.next] = D3)
(a = D6 && b = D7) => (ansn[first] = D2 && ansn[first.next] = D4)
(a = D6 && b = D8) => (ansn[first] = D8 && ansn[first.next] = D4)
(a = D6 && b = D9) => (ansn[first] = D4 && ansn[first.next] = D5)
(a = D7 && b = D0) => (ansn[first] = D0 && ansn[first.next] = D0)
(a = D7 && b = D1) => (ansn[first] = D7 && ansn[first.next] = D0)
(a = D7 && b = D2) => (ansn[first] = D4 && ansn[first.next] = D1)
(a = D7 && b = D3) => (ansn[first] = D1 && ansn[first.next] = D2)
(a = D7 && b = D4) => (ansn[first] = D8 && ansn[first.next] = D2)
(a = D7 && b = D5) => (ansn[first] = D5 && ansn[first.next] = D3)
(a = D7 && b = D6) => (ansn[first] = D2 && ansn[first.next] = D4)
(a = D7 && b = D7) => (ansn[first] = D9 && ansn[first.next] = D4)
(a = D7 && b = D8) => (ansn[first] = D6 && ansn[first.next] = D5)
(a = D7 && b = D9) => (ansn[first] = D3 && ansn[first.next] = D6)
(a = D8 && b = D0) => (ansn[first] = D0 && ansn[first.next] = D0)
(a = D8 && b = D1) => (ansn[first] = D8 && ansn[first.next] = D0)
(a = D8 && b = D2) => (ansn[first] = D6 && ansn[first.next] = D1)
(a = D8 && b = D3) => (ansn[first] = D4 && ansn[first.next] = D2)
(a = D8 && b = D4) => (ansn[first] = D2 && ansn[first.next] = D3)
(a = D8 && b = D5) => (ansn[first] = D0 && ansn[first.next] = D4)
(a = D8 && b = D6) => (ansn[first] = D8 && ansn[first.next] = D4)
(a = D8 && b = D7) => (ansn[first] = D6 && ansn[first.next] = D5)
(a = D8 && b = D8) => (ansn[first] = D4 && ansn[first.next] = D6)
(a = D8 && b = D9) => (ansn[first] = D2 && ansn[first.next] = D7)
(a = D9 && b = D0) => (ansn[first] = D0 && ansn[first.next] = D0)
(a = D9 && b = D1) => (ansn[first] = D9 && ansn[first.next] = D0)
(a = D9 && b = D2) => (ansn[first] = D8 && ansn[first.next] = D1)
(a = D9 && b = D3) => (ansn[first] = D7 && ansn[first.next] = D2)
(a = D9 && b = D4) => (ansn[first] = D6 && ansn[first.next] = D3)
(a = D9 && b = D5) => (ansn[first] = D5 && ansn[first.next] = D4)
(a = D9 && b = D6) => (ansn[first] = D4 && ansn[first.next] = D5)
(a = D9 && b = D7) => (ansn[first] = D3 && ansn[first.next] = D6)
(a = D9 && b = D8) => (ansn[first] = D2 && ansn[first.next] = D7)
(a = D9 && b = D9) => (ansn[first] = D1 && ansn[first.next] = D8)
all p : Position - (first + first.next) | ansn[p] = D0
}
}
// 上位桁側への論理シフト
pred upperShift (n, shifted : Decimal) {
let nn = n.notation, sftn = shifted.notation {
sftn[first] = D0
all p : Position - first | sftn[p] = nn[p.prev]
}
}
// シフトと加算の組合せ : n1 + n2 * 10 = answer
pred shiftingPlus (n1, n2, answer : Decimal) {
some shifted : Decimal {
upperShift[n2, shifted]
decPlus[n1, shifted, answer]
}
}
// メモ化用の配列
sig DecArray {
// 十進表示の桁数と同じ長さを持ち、null 値は不可
get : Position -> one Decimal
}
// 一桁ずつシフトしながら加算
pred foldShiftingPlus (ns : DecArray, answer : Decimal) {
// acc により畳み込みの途中経過をメモ化
some acc : DecArray {
// ns に対して逆順に畳み込みを行う
acc.get[first] = ns.get[last]
all p : Position - first |
shiftingPlus[ns.get[p.inverse], acc.get[p.prev], acc.get[p]]
acc.get[last] = answer
}
}
// 十進数同士の乗算の関係 : n1 * n2 = answer
pred decMul (n1, n2, answer : Decimal) {
// pProds により部分積をメモ化
// pProds.get[i] は n1 全体と、n2 の i 桁目との部分積
some pProds : DecArray | let n1n = n1.notation, n2n = n2.notation {
all i : Position | some dProds : DecArray {
// n1 の j 桁目と n2 の i 桁目との積を計算して
// j に関してシフトしつつ和を取ると部分積が得られる
all j : Position | digitProd[n1n[j], n2n[i], dProds.get[j]]
foldShiftingPlus[dProds, pProds.get[i]]
}
// さらに i に対してシフトしつつ和を取ると最終的な積が得られる
foldShiftingPlus[pProds, answer]
}
}
// 例 : 13 * 57 = 741
// Skolem depth >= 2 推奨
pred example13Times57 {
some n1, n2, answer : Decimal |
let n1n = n1.notation, n2n = n2.notation {
// n1 = 13
n1n[first] = D3
n1n[first.next] = D1
all p : Position | p in nexts[first.next] => n1n[p] = D0
// n2 = 57
n2n[first] = D7
n2n[first.next] = D5
all p : Position | p in nexts[first.next] => n2n[p] = D0
// n1 * n2 = answer
decMul[n1, n2, answer]
}
}
run example13Times57 for 3 Position, 14 Decimal, 7 DecArray
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment