Alloyで人生モデリングその2：時間軸を設定する - 檜山正幸のキマイラ飼育記 (はてなBlog)

「少しずつダラダラふらりふらり」とは言いましたが、それにしてもあいだが空いたので、少しはなんか書いておこうかな、っと。

人生モデリングの目的は、時間概念の扱い方を練習することです

人間のあいだの関係は、時間とともに変化するし、「母のかつての夫」とか「未来の妻」とか時間を含む概念もあります。そこで、次は時間を扱ってみたいと思います。

というわけで、とりあえず時間軸を設定する話をします。

Alloyアナライザーにモデル記述ファイルの置き場所を教える

本論に入る前に、Alloyアナライザーの使い方についての小ネタを：モデル記述ファイルの置き場所をAlloyアナライザーに教える方法です。http://groups.google.com/group/alloy-jp に、僕の質問やid:bonotakeさんのお答えとかアーカイブされてます。要するに、Javaのプロパティ user.home にモデル記述ファイルを入れているディレクトリを指定しておくと便利だよ、ってことです。

「Windowsのcmd.exeとbashのどちらでも実行できるバッチファイルの書き方」で紹介した方法でバッチファイルにすると次のようです。

: <<EOF
@echo off
goto Windows
EOF
exec cmd //c $0 $*
:Windows
rem invoke Alloy Analyzer 4
setlocal

if "%HOME%"=="" goto ConstructHome
set _HOME=%HOME%
goto ModelDir

:ConstructHome
set _HOME=%HOMEDRIVE%%HOMEPATH%
goto ModelDir

:ModelDir
if "%ALLOY_MODELS%"=="" goto DefaultModelDir
set _ALLOY_MODELS=%ALLOY_MODELS%
goto Invoke

:DefaultModelDir
set _ALLOY_MODELS=%_HOME%/Alloy/models
goto Invoke

:Invoke
echo javaw -Duser.home=%_ALLOY_MODELS% -jar %_HOME%/Alloy/alloy4.2-rc.jar
start javaw -Duser.home=%_ALLOY_MODELS% -jar %_HOME%/Alloy/alloy4.2-rc.jar

util/orderingライブラリモジュールを使ってみる

時間は全順序（線形順序）を持つので、時間軸を表す集合には全順序を導入する必要があります。「自然数の区間をAlloyで書いてみる」では、自前で全順序を定義しましたが、今回はライブラリを使いましょう。

util/orderingを使えば、全順序を定義できます。次のようにします。

-- 時間の練習 1
module time_ex1

-- orderingライブラリを使う
open util/ordering[time]

sig time {}

run {} for 5 time

util/orderingモジュールにパラメータ [time] を付けてopenします。これによって、自分で定義したシグニチャtimeの台集合に全順序が入ります。しかし、util/orderingによって導入された関係は可視化されません。時間の順序が見えてないと事情がわからない場合もあるので、全順序を可視化しましょう。

とはいっても、util/orderingが何をしているか分からないと、可視化の手段も見当が付かないのでソースを眺めてみました。Alloyの配布アーカイブ（兼実行可能ファイル）であるjarを展開すると、modeles/ディレクトリの下にutil/ordering.alsが入っています。

util/ordering.alsのコメントを読むと、パラメータに入れたシグニチャ（今の場合はtim）の集合は、常にその最大数の要素（アトム）を持つことになって、その上に全順序が定義される、と。内部的には、time上に First, Next というフィールドが定義されるようですが、privateになっているので、First, Nextは見えません。代わりに、first, nextという関数がパブリックに定義されます。この関数を使いましょう。

-- 時間の練習 1
module time_ex1

-- orderingライブラリを使う
open util/ordering[time]

sig time {
 nextTime: lone time
}

fact {
 all t: time |
   t.nextTime = next[t]
}

run {} for 5 time

次のように可視化されます。

timeにnextTimeというフィールドを設けました。フィールドってのは、まーだいたいはメソッドみたいなものです。t∈time に対して t.nextTime が定義されます。 nextTime: lone time という宣言から、nextTime はほぼ部分関数（partial function）と言えます。この部分関数を、前もって定義されている大域関数 next と同じにしたのです。

ちょっとややこしいのは、「nextTimeは部分関数」といったときの関数と、「nextという関数」といったときの関数の意味が違うことです。nextのように、funで定義される“関数”は関係を値に持つ式に名前を付けたものです。

生きている時

とりあえず人を1人、モデル内に導入して、その人の生きている時間を表すつもりの live というフィールドを定義してみます。

-- 時間の練習 1
module time_ex1

-- orderingライブラリを使う
open util/ordering[time]

sig time {
 nextTime: lone time
}

fact {
 all t: time |
   t.nextTime = next[t]
}

sig person {
 live: set time
}

run {} for exactly 1 person, 5 time

Alloyアナライザーは次のような例を探してきます。

時点0と時点2で人は生きてますが、時点1では生きてません。一度死んで生き返った形になっているんで具合悪いです。ここらはなんらかの方法で制約を付ける必要がありますね。

時間軸が設定できて、課題が持ち上がりました。と、今日はこのへんにしておきます。