たけをの日記＠天竺から帰ってきたよ

シグネチャのフィールドにある関係の多重度 続き

Alloy | 07:53 |

昨日の日記 の続き。 id:koji8y さんから、トラックバックで

じゃあ，昨日のスタート Alloy の演習中に僕らが表現したかったこと，

sig A {
	r: B -> C
}

で，各 A の各 r が one to one の関係 (functional かつ injective な関係) となること*1を表現するにはどう記述したらいいでしょうね?

（略）

sig A {
	r: B -> C
}{
	// functional (left-unique)
	all b: B, c1, c2: C {
		(b->c1 in r and b->c2 in r) => c1 = c2
	}
	// injective (right-unique)
	all b1, b2: B, c: C {
		(b1->c in r and b2->c in r) => b1 = b2
	}
}

とすると，表示したインスタンスは求めている形になっていそう．

でももっと簡単に記述できるるのではないかと...

と追加質問いただいたんですが…これって

  sig A {
    r: B lone -> lone C
  }

では？シグネチャファクト中の

  all b: B, c1, c2: C {
    (b->c1 in r and b->c2 in r) => c1 = c2
  }

って制約は

  all b: B {
    lone b.r
  }

と同じ意味に読めます。

実際、下記のように書いたアサーションで反例は（スコープをいくつにしても）出ないです。

（アサーションを記述するため、シグネチャファクトや宣言制約を述語内に書き下しています）

sig A {
	r: B -> C
}
sig B, C {}

pred p1 {
  all a: A {
	// functional (left-unique)
	all b: B, c1, c2: C {
		(b->c1 in a.r and b->c2 in a.r) => c1 = c2
	}
	// injective (right-unique)
	all b1, b2: B, c: C {
		(b1->c in a.r and b2->c in a.r) => b1 = b2
	}
  }
}

pred p2 {
  all a: A | a.r in B lone -> lone C
}

assert equivalence {
  p1 <=> p2
} 

check equivalence for 6

スタートAlloyやりました

Alloy | 21:53 |

cf. http://atnd.org/events/27160

ヒジョーに適当な準備だけで（テキトーな資料でホントすいません）、しかも「習うより慣れろ」と吹いてAlloy言語のレクチャーほとんどなしに演習やってもらうという無謀な試みにも関わらず、（Alloy初心者の方々も含め）全体的に皆さん大健闘されまして、僕としてはうれしい誤算でした。

というか、やってみるもんだなぁ。僕もいろいろ勉強になりました。

当日の演習課題について

課題にしたのは「バージョン管理システムのモデリング」。

1. 1人だけで使う状況を考える
   • コミット と 更新 ができる
   • ヒント：シグネチャ「リポジトリ」「ローカル」「ファイル」
2. 複数人で使う状況を考える
   • 1つのリポジトリを複数の開発者で共有する
     1. コンフリクトが起こる状況をモデル化する
     2. コンフリクト解消の機能をモデル化し、それで正しく動作することを確かめる
3. 発展的課題
   • 既存のバージョン管理システムが持つ他の機能をモデル化する
     • ブランチ作成、マージ
     • リポジトリが複数ある状況（分散バージョン管理）
   • 既存のバージョン管理システムの気になるところを検証してみる
   • 最強のオレオレバージョン管理ツールを考える（自由課題）

…と、3問用意していたのですが、実は1. だけでも半日〜数日は余裕で遊べる、ヒジョーに難しい課題でした*1。

何が難しいかというとですね。

普通のOS上のファイルシステムなら、同一フォルダ内で同じファイルかどうか、というのは、同じファイル名かどうかで単純に区別がつきます。

ところが、バージョン管理システムでは、それ以外に

• リポジトリ内とローカルファイルとで別々に存在するファイルが同一のものか否か
• 同じリポジトリ内で、リビジョン違いの同一ファイルか否か

があり、「ファイル」という概念に3種類の同一性を導入しないといけないのです。

ということで、かなりハードだったはずです。でも皆さん、その全てではないにしても、問題の本質に気づいてそれなりにモデリングをこなされていたので、すばらしかったです。

AlloyモデリングのTips

で、今回皆さんのさまざまな反応を見て思った、Alloyでのモデリングのコツ。自分のためにも残しておきます。

とにかくシンプルに、シンプルに。

設計対象の本質（「抽象」）だけをモデル化していくべし。

言い換えると、「それがなかったら、このシステムは実現不可能」な概念だけを導入してください。

たとえば、バージョン管理システムに「ファイルの差分」という概念は、必ずしも必要ではないですよね。

自分の中の「仕様」を疑え。

プログラミングとAlloyを使ったモデリングは、似ているようで、決定的に違うところがあります。

それは、Alloyの出力結果が正しくて、自分の頭の中の仕様が間違ってるケースが多々あるということです。そもそも、元々ぼんやりとした要求しかないところから、仕様を考える作業をしているのだから、当たり前です。

だから、Alloyが変なインスタンスを出してきたからといって、すぐにバグ扱いしないでください。それ以前にまず、それをバグだとする判断が自分の思い込みではないのかを疑ってください。

想像力を働かせて、現実にそういう状況が起こりうるのか、起こっても大丈夫かが確認できたら、それはスルーして大丈夫なのです。むしろ積極的に、そういう状況を受け入れ可能なように、自分の脳内イメージを改めてください。

制約を緩めることも大事。

（上記を踏まえた上で）どう考えてもあってはならないインスタンスが出力されたら、それはモデルに制約を追加するときです。

一方、意図したようなインスタンスが出力されなかったら、それは十中八九モデル中の制約が強すぎるときです。なので、このときは逆に、制約を緩めないといけません。ここで更に制約を追加すると、おかしなことになります。

そして、注意すべきは、制約が少なければ少ないほど、システムは堅牢になるということです。制約とはシステムが正常動作する前提条件です。余計な前提条件があればあるほど、脆いシステムになってしまいます。

シグネチャのフィールドにある関係の多重度

Alloy | 22:33 |

さて、スタートAlloy中、頂いたテクニカルな質問のうち1つに、当日うまく答えられませんでした（すいません… orz）。

ちゃんと考え直したので(^^; ここに書いておきます。（thx to @masahiro_sakaiさん）

質問

以下のようなシグネチャ宣言があったとする。

sig A {
  r: B one -> one C
}

ここで、Bのスコープを1にすると、任意の a: A から得られる a.r が全部同じになってしまう。

たとえば、以下のようなコマンドで反例が出ない。

check {
  all disj a1, a2: A | a1.r = a2.r
} for 3 but 1 B

たとえば a1.r は空で、a2.r は空でないような可能性があるように思うが、なぜないのか？

回答

まず、シグネチャのフィールドにある関係は、次のように解釈されます。（Alloy本 p.261）

…したがって、例えば

sig S {f: e}

という宣言によって導入される制約は、（fを通常の変数とした場合の）fが式eの部分集合であるという制約ではなく、以下のような制約になる。

all this: S | this.f in e

よって、先ほどのシグネチャA内のフィールドrの宣言は、

all a: A | a.r in B one -> one C

という制約だと解釈されます。（thisはaに置き換えました）

更に、関係の中の多重度についてですが、（Alloy本 p. 76）

多重度は単なる省略記法であり、標準的な制約に置き換えることができる。以下の多重度制約は、

r: A m -> n B

以下のように書き換えることができる。

all a: A | n a.r
all b: B | m r.b

とあります。コロンは in と読み替えても意味的には同じです。

ということで、先ほどの制約式を、更に展開すると

all a: A | all b: B | one b.(a.r)
all a: A | all c: C | one (a.r).c

となります。

なので、Bのスコープが1だと、B、C ともに空で a.r が常に空になるか、B、C ともにサイズ1で、aによらず a.r が存在して一意に定まるか、いずれかになります。

追記

続きを書きました → シグネチャのフィールドにある関係の多重度 続き - たけをの日記＠天竺から帰ってきたよ

イラストロジックをAlloyで解く

Alloy | 15:59 |

「イラストロジックはAlloyに向かない」 って書いておくと id:bonotake さんが解決してくれないかな(チラッ) Alloyでイラストロジックを解く−西尾泰和のはてなダイアリー

ちょｗｗｗ

いやいや、そういうムチャぶりはやめてください（^^;

というか実際のところ、自信ありません(^^;;;

イラストロジックがAlloyに向くか向かないかは微妙なところがあります。数独なんかもそうですが、この手のニコリ系パズルは書き方間違えると簡単に計算が爆発しちゃうんですよ。

うーんでも、話を振られた以上は、やってみないとダメかなぁ、でも最近時間ないしなぁ…と思っていたのですが、うまい具合に今日奥様からインフルエンザをもらって仕事ができなくなり（ぇ 予定外の時間ができたのでちょっとやってみました。

なお、id:nishiohirokazuさんの記事と同様、イラストロジックの定義と例題はこちらからお借りしました。

とりあえず、僕の書いたイラストロジックのモデル（空行とか含めて約90行＋問題の定義約20行）。Gistにも貼ってます。

見てもらうとわかりますが、ほぼ同様の記述が行と列で別々に書き分けてあって、コードクローンが発生しております。なので、まとめたらもっと短く書けると思います。

open util/ordering[Col] as cols
open util/ordering[Row] as rows

abstract sig Region {}
sig Col extends Region {
  cell: Row -> Cell
}
sig Row extends Region {}
enum Cell { Black, White }

fact {
  all c: Col, r: Row | one cell [c, r]
}

-- about rows
pred blackHeadInRow (c: Col, r: Row) {
  c in first or cell[c.prev, r] in White
  cell[c, r] in Black
}

fun headsInRow (r: Row): set Col {
  { c: Col | blackHeadInRow[c, r] }
}

fact noOtherHeadsInRow {
  no c: Col, r: Row | c not in headsInRow[r] and blackHeadInRow[c, r]
}

pred headsSeqInRow (r: Row, s: seq Col) {
  s.elems = headsInRow[r]
  all i: s.butlast.inds | lt [s[i], s[plus[i, 1]]]
}

fun Int2Row (i: Int): Row {
  {r: Row | #(r.prevs) = i}
}

fun Row2Int (r: Row): Int {
  #(r.prevs)
}

pred rowHint (j: Int, sizes: seq Int) {
  let r = Int2Row[j] | some cs: seq Col {
    #sizes = #cs
    headsSeqInRow [r, cs]
    all i: sizes.inds | 
      let start = cs [i], end = Int2Col [plus [Col2Int [start], minus[sizes [i], 1] ]] {
       some end
       all c: start.*cols/next - end.^cols/next | cell [c, r] in Black
       no end.next or cell [end.next, r] in White
     }
  }
}

-- about cols
pred blackHeadInCol (c: Col, r: Row) {
  r in first or cell[c, r.prev] in White
  cell[c, r] in Black
}

fun headsInCol (c: Col): set Row {
  { r: Row | blackHeadInCol[c, r] }
}

fact noOtherHeadsInCol {
  no c: Col, r: Row | r not in headsInCol[c] and blackHeadInCol[c, r]
}

pred headsSeqInCol (c: Col, s: seq Row) {
  s.elems = headsInCol[c]
  all i: s.butlast.inds | lt [s[i], s[plus[i, 1]]]
}

fun Int2Col (i: Int): Col {
  {c: Col | #(c.prevs) = i}
}

fun Col2Int (c: Col): Int {
  #(c.prevs)
}

pred colHint (j: Int, sizes: seq Int) {
  let c = Int2Col[j] | some rs: seq Row {
    #sizes = #rs
    headsSeqInCol [c, rs]
    all i: sizes.inds | 
      let start = rs [i], end = Int2Row [plus [Row2Int [start], minus[sizes [i], 1] ]] {
       some end
       all r: start.*rows/next - end.^rows/next | cell [c, r] in Black
       no end.next or cell [c, end.next] in White
     }
  }
}

-- riddle from http://homepage1.nifty.com/sabo10/rulelog/illust.html
solve: run {
  rowHint [0, 0 -> 3]
  rowHint [1, 0 -> 2 + 1 -> 2]
  rowHint [2, 0 -> 1 + 1 -> 1 + 2 -> 1]
  rowHint [3, 0 -> 3 + 1 -> 3]
  rowHint [4, 0 -> 5]
  rowHint [5, 0 -> 7]
  rowHint [6, 0 -> 7]
  rowHint [7, 0 -> 7]
  rowHint [8, 0 -> 7]
  rowHint [9, 0 -> 5]

  colHint [0, 0 -> 4]
  colHint [1, 0 -> 6]
  colHint [2, 0 -> 7]
  colHint [3, 0 -> 9]
  colHint [4, 0 -> 2 + 1 -> 7]
  colHint [5, 0 -> 1 + 1 -> 6]
  colHint [6, 0 -> 2 + 1 -> 4]
  colHint [7, 0 -> 3]
  colHint [8, 0 -> 1]
  colHint [9, 0 -> 2]
} for 10 but 5 Int

で、動かしてみると、こんな感じ。約2.5秒。予想外に(^^; 結構さっくり解けました。

5年前のサブノートPCでこれくらいなので、最近のPCならもっと速いでしょう。

結果は元サイトのと同じになるので、動かしてみてください。見づらいですが（誰かの書いたビューワ使い回せないだろうか…みんな同じようなパズルAlloyで解いて、その度にビューワ書いてる気がする。）

あ、そうそう。最近時間なくて反応できてませんが、id:nishiohirokazuさんの最近のAlloy関連記事、面白いですよ。皆さんもぜひご一読ください。Alloyガールの続きまだかなー （・∀・ ）っ/凵⌒☆ﾁﾝﾁﾝ

cf. Alloyまとめ - 西尾泰和のはてなダイアリー

追記: モデルの中にコメントも何も書いてなかったので、そのへんぼちぼち追加しながら説明を書き足そうかな、と思っていたら、id:nishiohirokazuさんがさっさと解読・解説する記事をAlloyガールで書いてくれました。うはー。

• Alloyガール番外編「イラストロジック」 - 西尾泰和のはてなダイアリー

カロタンパズルをAlloyで解く

Alloy | 17:04 |

今日、twitterで @mr_konn さんがこのような発言をなされました。

……

ほほぅ……

……

というのはウソですが、これくらいの論理パズルが向かないってことはないだろー。

と思い、解いてみました。

ちなみに、カロタンパズルはこんなの（こちらから引用）。

カロタンは奇妙な癖のある種族です。男は常に真実を語り、女はいちどきに 2 つの真実は言わない、あるいは、いちどきに 2 つの嘘は言わないというものです。

ある人類学者(彼をウォルフと呼びましょう)が彼らの研究を始めました。ウォル フはまだ、カロタンの言葉を知りません。ある日、カロタンのカップル(異性)と その子どものキビと出会いました。ウォルフはキビに「きみは男の子？」とたず ねました。キビはカロタン語で答えたので、ウォルフには分りませんでした。

ウォルフは両親(英語を知っている)に説明を求めました。ひとりが、「キビは、 自分は男の子だといっている」と言いもうひとりが、「キビは女の子。キビは嘘 をついた」と付け加えました。

この両親の性別とキビの性別をあててください。

で、Alloyのモデル。（Gistにも貼ってあります。）

abstract sig カロタン {
  性別: 男か女か,
  発言1: Prop,
  発言2: lone Prop
}
{
  // 男なら常に真実を語る
  性別 in 男性 => 発言1.真偽 in ホント and (some 発言2 =>発言2.真偽 in ホント)
  // 女はどっちかホントでどっちかがウソ
  else some 発言2 => 発言1.真偽 != 発言2.真偽
}
enum 男か女か { 男性, 女性 }

one sig キビ extends カロタン {}
{
  // 自分を男といったか、女といったかのどちらか
  発言1 in キビは男の子 + キビは女の子
  no 発言2
}
one sig 親A extends カロタン {}
{
  発言1 in キビは男の子と言っている
  no 発言2
}
one sig 親B extends カロタン {}
{
  発言1 in キビは女の子
  some 発言2
  発言2 in キビはウソをついている
}

fact 親の性別はたぶん別々 {
  親A.性別 != 親B.性別
}

/** 皆さんの発言（命題）*/
abstract sig Prop {
  真偽: ホントかウソか
}
enum ホントかウソか { ウソ, ホント }

one sig キビは男の子 extends Prop {}
{
  真偽 in ホント <=> キビ.性別 in 男性
}
one sig キビは女の子 extends Prop {}
{
 真偽 in ホント <=> キビ.性別 in 女性
}
one sig キビは男の子と言っている extends Prop {}
{
  真偽 in ホント <=> キビ.発言1 in キビは男の子
}
one sig キビはウソをついている extends Prop {}
{
  真偽 in ホント <=> キビ.発言1.@真偽 in ウソ
}

run {  } 

出てきた解のスナップショット。

[追記] ミソは、カロタン親子の発言をどうモデル化するかです。

特に、「キビが男の子である」という事実と、「キビは（自分を）男の子と（あるいは女の子と）言った」という事実と、更にそれを言明する親の発言とを、ナイーブにAlloyの制約式にしてしまうと同列にモデル化できないわけです。

得てして高階論理で書きたくなるかもしれませんが、Alloyは一階論理しか扱えません（mr_konnさんが「向かない」と思ったのも、たぶんこの辺り）。

その解決策として、ここでは各発言（命題）を述語やファクトでなく、シグネチャでモデル化してます。こうすることで、各発言やその真偽みたいなものを、Alloyのモデル上で統一的に扱えるようにしているのです。[/追記]

レイトン教授ナゾ配信『ウサギ』ソルバをAlloyで書いた

Alloy, その他 | 06:40 |

『レイトン教授 奇跡の仮面』では毎日パズルを配信してくれるんだけど、

その中の『ウサギ』シリーズの1つがどうしても解けなくて、ついAlloyでソルバを書いてしまった。

ムシャクシャしてやった。反省はしていない。

『ウサギ』シリーズの説明はコチラが詳しそう。動画も拝借してみる。

ということで、ソルバを公開してみたりする。

みんなこんなのに頼っちゃダメだよ（はあと）

open util/ordering [Rabbit] as rab

abstract sig Carrot {
  x: Int, y: Int
}
{
  x >= 0
  y >= 0
}

one sig C0_0 extends Carrot { } { x = 0 y = 0 }
one sig C1_0 extends Carrot { } { x = 1 y = 0 }
one sig C2_0 extends Carrot { } { x = 2 y = 0 }
one sig C3_0 extends Carrot { } { x = 3 y = 0 }
one sig C0_1 extends Carrot { } { x = 0 y = 1 }
one sig C2_1 extends Carrot { } { x = 2 y = 1 }
one sig C0_2 extends Carrot { } { x = 0 y = 2 }
one sig C1_2 extends Carrot { } { x = 1 y = 2 }
one sig C3_2 extends Carrot { } { x = 3 y = 2 }
one sig C0_3 extends Carrot { } { x = 0 y = 3 }
one sig C2_3 extends Carrot { } { x = 2 y = 3 }
one sig C4_3 extends Carrot { } { x = 4 y = 3 }
one sig C3_4 extends Carrot { } { x = 3 y = 4 }

run { } for exactly 13 Rabbit

sig Rabbit {
  at: disj Carrot,
  go: Direction 
}
{
  this != last => {
    move [this, this.next]
    go in DOWN => this.next.@go not in UP
    go in UP => this.next.@go not in DOWN
    go in RIGHT=> this.next.@go not in LEFT
    go in LEFT=> this.next.@go not in RIGHT
  }
}

enum Direction { UP, RIGHT, DOWN, LEFT }

pred move (r, r': Rabbit) {
  r.go in UP =>  goUp [r, r']
  r.go in DOWN =>  goDown [r, r']
  r.go in RIGHT =>  goRight [r, r']
  r.go in LEFT =>  goLeft [r, r']
}

pred goUp (r, r': Rabbit) {
  r'.at not in  (r + r.prevs).at
  upper[r'.at, r.at]
  all c: Carrot | upper [c, r.at] => c in r'.at or c in r.prevs.at or upper[c, r'.at]
}
pred goDown (r, r': Rabbit) {
  r'.at not in (r + r.prevs).at
  downer[r'.at, r.at]
  all c: Carrot | downer [c, r.at] => c in r'.at or c in r.prevs.at or downer[c, r'.at]
}
pred goRight (r, r': Rabbit) {
  r'.at not in (r + r.prevs).at
  righter[r'.at, r.at]
  all c: Carrot | righter [c, r.at] => c in r'.at or c in r.prevs.at or righter[c, r'.at]
}
pred goLeft (r, r': Rabbit) {
  r'.at not in (r + r.prevs).at
  lefter[r'.at, r.at]
  all c: Carrot | lefter [c, r.at] => c in r'.at or c in r.prevs.at or lefter[c, r'.at]
}
pred upper (c1, c2: Carrot) {
  c1.x = c2.x
  c1.y < c2.y
}
pred downer (c1, c2: Carrot) {
  c1.x = c2.x
  c1.y > c2.y
}
pred righter (c1, c2: Carrot) {
  c1.x > c2.x
  c1.y = c2.y
}
pred lefter (c1, c2: Carrot) {
  c1.x < c2.x
  c1.y = c2.y
}

Carrotでニンジンの座標を1つ1つ定義して、あと run {} for exactly XX Rabbit の XX にニンジンの数（＝ウサギの動くステップ数）を入れる。

出力はTreeビューだと幾分か見やすいと思う。暇だったら専用ビューワを書くかもしれない。