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

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

レイトン教授と奇跡の仮面(特典なし) - 3DS

その中の『ウサギ』シリーズの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ビューだと幾分か見やすいと思う。暇だったら専用ビューワを書くかもしれない。

『抽象によるソフトウェア設計』（Alloy本）発売しています

もうすっかり放置してしまっているはてなですが、さすがにこの記事を書かないまま放置するのはまずい。ので一言だけ書いておきます。

"Software Abstractions"（通称Alloy本）の邦訳しました。現在、全国各書店で発売中です。

抽象によるソフトウェア設計−Alloyではじめる形式手法−

自分が思った以上に反響があって、うれしい驚きです。
特に「熱い」「技術書である前に、読み物として面白い」という感想をチラホラ頂いていて、訳者冥利に尽きるなぁと思う次第。やってよかったなぁと思っています。

形式手法、形式仕様記述と呼ばれるものの中でAlloyの位置づけは非常に独特です。こんなに気軽に形式仕様を書けるのは、僕の知る限り、メジャーなものではまだAlloyしかありません。

でも本当は、もっと同じような手法が広まるべきだし、今後Alloyを超えていく言語・手法があってしかるべきだと思っています。Alloyが起こした小さなさざ波を、太平洋をまたいだ日本にも伝えられれば本望です。

Alloy本翻訳レビュー始まります＆Alloy 4.2 RCリリース

以前、"Software Abstractions"翻訳のレビュワーを募集しましたが（"Software Abstractions"翻訳本のレビュアーを募集します - たけをの日記＠天竺から帰ってきたよ）、予想よりたくさんのご応募いただきました。

元々は片手で数える程度の方にお願いするつもりだったところを倍に増やしても枠が全然足りず、「なるべくレビュワーの属性をバラす」という方針のもと、勝手にこちらで選定させていただきました。
選定した方には既に内々に打診しています。明日以降に正式にお願いして、作業に入ってもらうことになると思います。選に漏れた方、ゴメンなさい。

あ、募集時には3月の作業、となってましたが、1ヶ月スケジュールが押しました（テヘペロ）

それから、久々にAlloy Analyzerがバージョンアップしまして（といっても、まだRelease Candidateですが）、4.2 RCがリリースされました。

• http://alloy.mit.edu/alloy4/

今回、整数周りの仕様が変更されてます。今まで整数のプリミティブ型だったintと整数のシグネチャ（集合）としてのIntが両方存在していたのですが、前者がなくなり、後者にすべて統一されました。

この新バージョンの仕様は、我々が翻訳を進めながら原著者と進めた議論がきっかけになってできたものです…が、かなりできたてホヤホヤで、実はまだ、自分もまだ全貌を把握できていなかったり。

自分も今いろいろ動かして試してるんですが、とりあえずレビューして頂く方も頂けない方も、ぜひ積極的に使って、人柱になってください(^^;
何かおかしいぞ？というのを見つけた方は、Alloyのコミュニティサイト（英語）に投げてもらうか、日本語がよければここのコメント欄にでも。

かけっこのパズル revisited

Alloy本翻訳のレビュワー募集記事で、過去に自分が「かけっこのパズル」をAlloyで解いた記事を参照したのですが…
参考）

• 駆けっこのパズルをAlloyで解く （Alloyチュートリアル風） - たけをの日記＠天竺から帰ってきたよ
• 長男に教わったパズル - 檜山正幸のキマイラ飼育記

今見直すと、なんかイマイチ。
特に、3人の嘘を見抜くのに、いちいち3回コマンド走らせないといけないのがダサい。

ということで、書き直してみました。
内容の詳細はコメント見てください。

-- かけっこ
one sig FootRace {
  -- 順位の配列
  runner: seq Person
}
{
  -- すべての人に順位が決まる
  runner in Int one -> Person
}

-- 一郎、二郎、三郎の宣言
enum Person { Ichiro, Jiro, Saburo }
-- うそつきが一人
one sig Liar in Person {}

-- 順位
fun rank (p: Person): Int {
  FootRace.runner.idxOf[p]
}

-- 「僕は一番じゃない」
pred word1(p: Person) {
  not p in Liar iff p.rank != 0 
}

-- 「僕は一番だ」
pred word2(p: Person) {
  not p in Liar iff p.rank = 0
}

--「僕は二番だ」
pred word3(p: Person) {
  not p in Liar iff p.rank = 1
}

-- 誰が嘘をついた？
pred whoIsLiar {
  -- 一郎が word1 を発言
  Ichiro.word1
  -- 二郎が word2 を発言
  Jiro.word2
  -- 三郎が word3 を発言
  Saburo.word3
}

run whoIsLiar

うう、Alloyのキーワード色づけされる日が来ないかな…

てな感じで、実行結果のスクリーンショット。

"Software Abstractions"翻訳本のレビュアーを募集します

注：既に募集は終了しました。参考：こちら

twitterではぼそぼそとつぶやいていましたが、現在下記の本の翻訳を進めています。

Software Abstractions: Logic, Language, and Analysis

これは、形式仕様記述言語Alloyを使ったソフトウェア設計の解説書です。
Alloyは"lightweight formal method"を謳っていて、お手軽なのがウリ。
もうちょびっと詳しく知りたい方は、過去の日記（駆けっこのパズルをAlloyで解く （Alloyチュートリアル風） - たけをの日記＠天竺から帰ってきたよ）なんかを参考にしてください。

で、その翻訳のレビューをお願いできる方を募集します。

• 募集人員：若干名
• 期間：3月初旬から3月いっぱいまで（予定）
• 応募方法： takeo.bono at gmail.com にメール または twitterで @bonotake にmentionしてください。
  • ※ twitter経由の場合リプライはさせて頂いておりませんが、こちらでちゃんと把握してますのでご了承ください。

手を挙げていただいた方のうち何名かを選抜して、2/22以降にこちらから声をかけさせていただきます。（応募頂いても、残念ながらお願いしない場合がありますので、悪しからずご了承下さい）
Alloyの知識あるなしは問いません。ユーザー、あるいは入門者の視点で読んでくださる方歓迎です。

なお、原著の方は現在、現バージョンのAlloy4に合わせた改訂を進めており、翻訳はその改訂版を反映させたものになります。

ということで、ご興味ある方は、よろしくお願いします。

うみねこの話：なぜ「一なる真実」は明らかにされないのか

うみねこのなく頃にep8感想、続き。あの後ぼんやりと考えていたことを記す。

謹賀新年＆うみねこのなく頃に ep8やりました

前回のエントリーがep7感想ってどうなんよ俺。半年全然書かんかったと言うことか。ひどいな。
ええと、今年もよろしくお願いします。

とりあえず、「うみねこのなく頃に」ep8やったよ、という一言だけ書きたかったのです。
以下、さらっと思いつくままに。深い考察などは一切ありません。感想のみ。
本当はもっと考察まとめてからゆっくり書きたいんだけど、ちょっと忙しくて今書かないと忘れちゃいそうなので。
ただし、ネタバレは気にせず書いてますので、ご注意。