memoryless sources

無記憶情報源。

0リアクション &

仕事でアプリケーションの設計に Alloy を使いたいと思っていたけど、なかなかマスターできないまま年月が過ぎてしまった。ので、再挑戦。狼とヤギとキャベツの問題を解いてみた。

open util/ordering[Time]

sig Time {}
abstract sig Position {pos: set Actor -> Time}
one sig Left, Right extends Position {}

abstract sig Actor {}

one sig Goat, Wolf, Cabbege, Man extends Actor {}

pred init (t: Time) {
    pos[Left].t = Actor
    no pos[Right].t
}

fact Traces {
    first.init
    all t: Time - last |
        (one obj: Actor - Man, p: Position | deliver [t, obj, p])
        or (one p: Position | justMove [t, p])
}

pred deliver (t: Time, obj: Actor - Man, p: Position) {
    let t' = t.next, p' = Position - p |
        (Man + obj) in pos[p].t
        and pos[p].t' = pos[p].t - (Man + obj)
        and pos[p'].t' = pos[p'].t + Man + obj
}

pred justMove (t: Time, p: Position) {
    let t' = t.next, p' = Position - p |
        Man in pos[p].t
        and pos[p].t' = pos[p].t - Man
        and pos[p'].t' = pos[p'].t + Man
}

pred doNotEat {
    no t: Time |
        (pos.t.Wolf = pos.t.Goat
        and pos.t.Goat != pos.t.Man)
        or (pos.t.Cabbege = pos.t.Goat
        and pos.t.Goat != pos.t.Man)
}

pred finish (t: Time) {
    pos[Right].t = Actor
    no pos[Left].t
}

pred doNotRepeat {
    no disj t, t': Time | pos.t = pos.t'
}

pred alldone {
    doNotEat
    doNotRepeat
    last.finish
}

run alldone for 8

最後に 8 をスコープに設定しているのはそうしないと解が存在しないからなんですが、最小の手数を見つけたいときとかはどうすればいいのかな。

GitHub は Alloy のコードもちゃんと色付けしてくれてすごい。 https://github.com/torus/alloy-renshu/blob/master/river.als

登録カテゴリ: programming alloy

0リアクション &

Using Ack-and-a-half on Emacs 24 on Windows

  • Install ack-and-a-half with M-x package-list-packages
  • Add following lines to your .emacs file:

    (require 'ack-and-a-half)
    (defalias 'ack 'ack-and-a-half)
    (defalias 'ack-same 'ack-and-a-half-same)
    (defalias 'ack-find-file 'ack-and-a-half-find-file)
    (defalias 'ack-find-file-same 'ack-and-a-half-find-file-same)
    
  • Install ack using Chocolatey. http://chocolatey.org/packages/ack

  • Set the ack-and-a-half-executable variable using M-x customize-group ack-and-a-half. The value should be like this:

    "C:\\ProgramData\\chocolatey\\bin\\ack.cmd"
    

    (Note that each \ is replaced with \\)

  • Try M-x ack and enjoy.

登録カテゴリ: emacs ack ack-and-a-half windows

0リアクション &

iCloud のディスクは値下げしたってことか?

こんなメールがいま届いた:

Your plan has been upgraded from 15 GB of total storage at ¥2,000 a year to 20 GB at just ¥1,200 a year. You will receive a prorated refund of ¥30, which is based on the price reduction and the remaining months on your subscription. On October 1, 2014 this 20 GB plan will automatically renew and you will be charged ¥1,200.

登録カテゴリ: icloud

0リアクション &

ロジバン - Wikipedia

人工言語というのは究極の車輪の再発明のように思えるけど、エスペラント以降にも研究が進んでいて、「実用段階に入った」っていうのが面白い。

ロゴといい語根の選び方といい、クトゥルーもびっくりの中二病加減だ。