通常の論理で記述する命題は、ある一つの状態で成り立つかどうかを表す。 しかし、状態が変化するシステムでは、「要求を受けたら、いつか応答する」や「認証されるまでは管理画面を表示しない」のように、複数の状態にまたがる性質も扱いたい。 時相論理は、状態を時間順に並べた列に対して、このような性質を記述する論理である。
時相論理の演算子は、命題が列のどこで成り立つかを表す。 たとえば always P は現在以降のすべての状態で P が成り立つこと、eventually P は現在以降のどこかの状態で P が成り立つこと、after P は次の状態で P が成り立つことを意味する。 これにより、「悪い状態へ到達しない」という安全性と、「望ましい状態へいつか到達する」という活性を区別して記述できる。
処理要求が完了するまで
処理要求を受け付けるシステムを考える。 要求 r は、受け付けられると処理待ちの集合 Pending に入り、処理されると完了済みの集合 Done へ移る。 正常に進んだ実行は、次の状態列になる。
状態0: Pending = none, Done = none
状態1: Pending = r, Done = none
状態2: Pending = none, Done = r一つの状態だけを見れば、「同じ要求が処理待ちと完了済みに同時に含まれない」と検査できる。 しかし、「処理待ちになった要求はいつか完了する」を検査するには、状態1より後の状態も見る必要がある。
Alloy 6 では、var を付けたシグネチャや関係が状態ごとに変化する。 次の状態の値はプライム演算子で表し、時相演算子を使って状態の列全体を制約する。
sig Request {}
var sig Pending, Done in Request {}
pred complete[r: Request] {
r in Pending
Pending' = Pending - r
Done' = Done + r
}
assert NeverPendingAndDone {
always no Pending & Done
}
assert PendingEventuallyCompletes {
always all r: Request |
r in Pending implies eventually r in Done
}NeverPendingAndDone は、すべての状態で Pending と Done が交わらないことを要求する安全性である。 PendingEventuallyCompletes は、どの状態で要求が Pending に入っても、その状態以降のどこかで Done に入ることを要求する活性である。
complete という遷移を定義しただけでは、システムがその遷移を実行するとは限らない。 何もせず Pending に要求を残し続ける状態列も許していれば、Alloy Analyzer は PendingEventuallyCompletes の反例としてその列を示す。 この反例によって、個々の遷移が正しいことと、システム全体がいつか処理を進めることは別の性質だと分かる。
通常の Alloy が「あり得る構造」を調べるのに対し、時相論理を使う Alloy は「あり得る変化」を調べると捉えられる。