Zenn
⏱

Alloy 6 の新機能 Mutable Field と線形時相論理

2021/12/08に公開
形式手法
モデル検査
alloy
tech

こんにちは、チェシャ猫です。

Alloy は関係論理を用いた形式手法ツールの一種です。本記事では、2021 年 11 月にリリースされた Alloy 6 の新機能、Mutable Field を用いた検査について解説します。この機能を使用することで、時間発展するタイプのシステムをよりシンプルに記述できるようになりました。

なお、本記事は従来の v5 以前の Alloy に触ったことがある読者を想定しています。したがって Alloy のツールとしての位置付けや基本的な文法・機能については説明しません。興味のある読者には『抽象によるソフトウェア設計ーAlloy ではじめる形式手法』（以下 Jackson 本）をお勧めします。

それでは早速、Alloy 6 をダウンロードして始めましょう。

TL;DR

  • Mutable Field が導入され、時刻に従って変化するような関係が記述可能になった
  • それに伴い、Visualizer の UI が刷新された
  • 検査に用いる条件式として、線形時相論理式が使用可能になった
  • 基本的に後方互換ではあるが、予約語の衝突により従来の記述はエラーになる可能性がある

シンプルな例：故障するランプ

このセクションでは、ごく単純なサンプルプログラムを用いて、Alloy 6 の Mutable Field や時相論理がどのように使用されるのかを解説します。

ランプの動作

  • ランプが 1 つだけ存在し、点灯・消灯・故障のいずれかの状態を取る
  • 初期状態は消灯。スイッチを押すたびに消灯状態と点灯状態が切り替わる
  • 点灯状態から故障状態になることがある。消灯状態から直接故障することはない
  • 一度、故障状態になった場合、二度とそれ以外の状態には戻らない

Alloy 5 以前の記述

最初に、比較のため Alloy 5 までの従来機能を用いてこのランプを記述してみましょう。

まずはランプの定義です。ランプが取り得る状態を enum で表現しておきます。

module lamp

one sig Lamp {
  state: State
}

enum State { On, Off, Broken }


ランプとその状態

続いて状態の遷移を記述します。従来、Alloy で時間発展するシステムを記述する場合には、以下の方法が定石でした。

  • 新しく Time のようなシグネチャを導入する
  • Alloy 標準の util/ordering モジュールを用いて、Time に全順序を定義する
  • 時間に依存する関係には Time を含めるようにする

今回のランプの例にこれを適用すると、以下のような記述になります。

module lamp
+ open util/ordering[Time]

+ sig Time {}

one sig Lamp {
-   state: State
+   state: State one -> Time
}

enum State { On, Off, Broken }

新しく時間依存性が導入された state を用いて、考えられる状態遷移を定義しましょう。1 つの述語にまとめてしまうこともできますが、今回は「スイッチを On にする」「スイッチを Off にする」「故障する」「すでに故障しているので何も起こらない」をそれぞれ別々に述語として定義します。

pred turnOn[t, t": Time] {
  Lamp.state.t = Off && Lamp.state.t" = On
}

pred turnOff[t, t": Time] {
  Lamp.state.t = On && Lamp.state.t" = Off
}

pred break[t, t": Time] {
  Lamp.state.t = On && Lamp.state.t" = Broken
}

pred stayBroken[t, t": Time] {
  Lamp.state.t = Broken && Lamp.state.t" = Broken
}

通例使用される t' ではなく t" を使用しています。これは Alloy 6 の新機能導入によって「' を付けた変数」が特殊な意味を持つようになったことによるエラーを避けるためです。後で詳しく説明します。

最後に、初期状態を定義し、さらに定義した以外の状態遷移が起こらないことを強制します。

pred init[t: Time] {
  Lamp.state.t = Off
}

fact trace {
  init[first]
  all t: Time - last, t": t.next {
    turnOn[t, t"] || turnOff[t, t"] || break[t, t"] || stayBroken[t, t"]
  }
}

それでは、このランプの性質について検査を行なってみましょう。以下の記述は、「ずっと故障が発生しない」および「いつか故障が発生する」という条件について、具体例を Alloy に探索させています。

pred alwaysNotBroken {
  all t: Time | Lamp.state.t != Broken
}
run alwaysNotBroken

pred eventuallyBroken {
  some t: Time | Lamp.state.t = Broken
}
run eventuallyBroken

Mutable Field を用いた記述

ここまで見てきたように、従来の Alloy では時間発展するシステムを記述する際には Time のような追加のシグネチャを導入する必要がありました。しかし Alloy 6 で導入された新機能 Mutable Field を用いた場合、余分なシグネチャを導入する必要がありません。さらに Visualizer の表示もより状態遷移を扱いやすいものに変わります。

全面的な書き直しになるので、サンプルコードは最初の Lamp と State を定義した直後から再度始めます。最初にやるべきことは、時間依存の関係 state に Alloy 6 から導入された新しい予約語 var を付けることです。

module lamp

one sig Lamp {
-  state: State
+  var state: State
}

enum State { On, Off, Broken }

この状態で一度実行してみましょう。Visualizer の表示が今までとは変化しているはずです。


Mutable Field を持つランプ

まず目に付く変化として、今まで 1 つだった表示が二分割されています。表示の左右は上部にある状態遷移図のフォーカスされた部分に対応しており、「←」「→」ボタンで状態を進めたり戻したりできます。

また、今まで「New」のみだった新しいインスタンスを探索させるためのボタンが増えています。ただ、ここまでの記述の範囲ではそれぞれのボタンの効果が分かりづらいため、制約を追加した後であらためて解説します。

次に、この記述に状態遷移を表す述語を追加していきます。しかし Alloy 5 の記述とは異なり今回は Time に相当するシグネチャがないため、述語の引数として時間を取ることができません。Alloy 6 では状態遷移は以下のような書き方をします。

pred turnOn {
  Lamp.state = Off && Lamp.state' = On
}

pred turnOff {
  Lamp.state = On && Lamp.state' = Off
}

pred break {
  Lamp.state = On && Lamp.state' = Broken
}

pred stayBroken {
  Lamp.state = Broken && Lamp.state' = Broken
}

述語の名前は Alloy 5 による先ほど挙げた Alloy 5 と合わせてあります。引数が無くなり、かつ今までどこでも定義されていないはずの state' が使用されていることに注意してください。

Mutable Field を含む述語は従来の述語とは異なり、 時間発展する状態列の中の、どこか 1 つの状態を「基準点」とする ことにより真偽が定まります。暗黙のうちに状態を引数に取っていると考えても構いません。

そして var が付与された関係については、' が付かないものはその基準点での値、' が付くものは基準点の直後の値 であると解釈されます。すなわち Alloy 5 の記述で t と表現されていた状態が今回は暗黙の引数となり、state.t と state.t" はそれぞれ state と state' に対応します。ただし、従来の述語では t と t" は単に「2 つの状態を引数に取る」以上の意味はなく、状態遷移の事前・事後状態であることはあくまでもファクト trace によって制約されていました。一方で今回の state と state' は他に何も言わなくとも連続した状態を指すものとみなされます。

なお、Alloy 5 による記述の際に t' ではなく t" を使用したのは、Alloy が ' をこの新しい記述方法と解釈することによるエラーを避けるためです。同じ理由から、Jackson 本に掲載されているサンプルコードの大部分は Alloy 6 では構文エラーになります。

最後に、Alloy 5 の場合と同じく、意図した以外の状態遷移が発生しないという制約を加えます。

pred init {
  Lamp.state = Off
}

fact trace {
  init
  always (turnOn || turnOff || break || stayBroken)
}

init については他の状態遷移の述語と考え方は同じで、引数が暗黙化されて無くなっています。「次の状態」については特に条件が必要ないため、ここでは state' は使用されていません。

注目すべきは trace で使用されている always です。今までに登場した述語は、状態の列を与えたとき「基準点となる状態」と「その次の状態」のみに対して真偽が定まるタイプのものでした。一方で always が付加された条件は、「基準点から後の任意の状態」 においてその条件が成立することを要求します。

そして、トップレベルに現れる条件は、状態列の先頭を基準点としたとき成立することを意味します。つまり、trace は以下のような制約を表現していることになります。

  • 初期状態で init が成立する
  • 時間発展する状態列のどの瞬間にフォーカスしても、その状態と次の状態では turnOn、turnOff、break および stayBroken のいずれかが成立する

したがって結果的に、Alloy 5 の場合と同じく、このファクト trace によって意図したランプの動作のみを Alloy に探索させることができます。

さて、制約を記述し終わったので、先ほど棚上げにしていたボタンについて解説します。記述が Mutable State を含む場合、従来の「New」ボタンに代わって「New Config」「New Trace」「New Init」および「New Fork」の各ボタンが現れます。


新しくなったツールバー

New Config ボタン は、時間に依存しない構造について他の例があるかどうかを探索します。いわば従来の New ボタンに相当しますが、今回の例の記述はこのような構造を含まないため、押しても画面は変化しません。

逆に New Trace ボタン は、現在表示しているものとは別の時間発展の例を探索します。今回で言えば、ボタンを押すたびに「全く故障しない系列」「1 回目の点灯で故障する系列」「2 回目の点灯で故障する系列」のように切り替わるはずです。

New Init ボタン は、別の初期状態の例を探索します。今回の記述では init によって初期状態は一通りに確定しているため、New Init ボタンを押すと即座に探索が終了します。

New Fork ボタン は、現在表示している状態から、それ以外の遷移先があるかどうかを探索します。画面の右側を別のものに入れ替えようとする、と言ってもよいでしょう。今回の記述で言えば、左側が Off になっているときに New Fork ボタンを押すと即座に探索が終了します。また左側が On になっているときに押すと右側に表示された遷移先が Off から Broken に（あるいはその逆に）変わるのが分かります。

それでは仕上げとして、先ほど Alloy 5 で例として挙げた検査条件が Alloy 6 ではどう記述されるかを見てみましょう。

pred alwaysNotBroken {
  always Lamp.state != Broken
}
run alwaysNotBroken

pred eventuallyBroken {
  eventually Lamp.state = Broken
}
run eventuallyBroken

1 つ目の alwaysNotBroken については trace と同じく always が使用されています。直接 run に渡された述語はトップレベル扱いになるため、この always は初期状態に続く任意の状態、要するに全ての状態で故障状態にならないことを要求します。

2 つ目の eventuallyBroken で使用されている eventully は always と同じく、Alloy 6 で導入された新しい機能です。always が「基準点以降の任意の状態」での成立を要求するのに対し、eventually は 「基準点以降、最低でも 1 つの状態」 での成立を要求します。ここではやはり run に対してトップレベルで出現しているため基準点は初期状態とみなされ、どこかのタイミングで一度でも故障状態になる例が探索の対象となります。


相異なる 7 つの状態を取り、3 回目の点灯で故障する例

線形時相論理の演算子

ここまでに登場した always と eventually は時相演算子と呼ばれます。Alloy 6 ではこれ以外にもいくつかの演算子が用意されており、それぞれ 線形時相論理 (Linear Temporal Logic, LTL) に基づいた意味が与えられています。このセクションではこれらの演算子について図解します。

always

すでに解説したとおり、述語 P に対して always P は「その状態以降の任意の状態で P が成り立つ」ことを意味します。以下の図は always P が成立する状態を太い枠線で示したものです。

eventually

こちらもすでに解説したとおり、述語 P に対して eventually P は「その状態以降の少なくとも 1 つの状態で P が成り立つ」ことを意味します。以下の図は eventually P が成立する状態を太い枠線で示したものです。

after

ここからはまだ本記事に登場していない演算子です。述語 P に対して after P は「その状態のすぐ次の状態で P が成り立つ」ことを意味します。以下の図は after P が成立する状態を太い枠線で示したものです。

until

ここまでの演算子は単項演算子でしたが、二項演算子も使用可能です。述語 P と Q に対して P until Q は「その状態以降の少なくとも 1 つの状態で Q が成り立ち、かつそこまでの間ずっと P が成り立つ」ことを意味します。

仮に Q が成り立たない場合、P until Q も成り立たないことに注意しましょう。以下の図は P until Q が成立する状態を太い枠線で示したものです。

releases

述語 P と Q に対して P releases Q は以下の 2 つの条件の両方が成り立つことを意味します。

  • その状態以降の少なくとも 1 つの状態で P が成り立つならば、そこまでの間は Q が成り立つ
  • その状態以降の任意の状態で P が成り立たないならば、以降ずっと Q が成り立つ

until との違いに注意しましょう。P releases Q は P と Q の役割が逆になっており、さらに P が成り立たないときであっても Q さえ継続していれば P releases Q は成り立ちます。下の図は P releases Q が成立する状態を太い枠線で示したものです。

;

述語 P と Q に対して P ; Q は「その状態で P が成り立ち、かつすぐ次の状態で Q が成り立つ」ことを意味します。下の図は P ; Q が成立する状態を太い枠線で示したものです。

過去演算子

ここまでに登場した演算子はすべて、基準点から見て「その状態以降の状態」に対する条件を要求するものでした。このような演算子を未来演算子 (feature-time operator) と呼びます。

一方で、基準点から見て「その状態以前の状態」に対して条件を要求する演算子も存在し、これを過去演算子 (past-time operator) と呼びます。; 以外の演算子には対応する過去演算子が存在し、例えば always P と対となる historically P であれば「その状態以前の任意の状態において P が成り立つ」といった意味になります。以下は Alloy 6 における未来演算子と過去演算子の対応表です。

未来演算子 過去演算子
always historically
eventually once
after before
until since
released triggered

もう少し複雑な例：リーダー選出

このセクションでは、もう少し複雑な例としてリングトポロジ上のリーダー選出アルゴリズムの検証を取り上げます。Jackson 本でも解説されている例ですが、今回はこれを Alloy 6 の機能を用いて書き直してみます。

システムの特徴

  • 複数のプロセスがリング状に配置されている
  • 各プロセスは隣のプロセスとしか通信できず、リング全体のサイズも確認できない
  • 各プロセスには一意かつ比較可能な識別子が振られている
  • 最大の識別子を持つプロセスをリーダーとして選出したい
  • 初期状態で各プロセスが知っているのは自分の識別子のみである
  • 通信路は到着順序を保証しないが、通信内容の破損や消失は発生しない

記述したいアルゴリズム

  • プロセスの識別子と対応するトークンを用意する
  • 初期状態で各プロセスは自分の識別子と同じトークンのみを持つ
  • 各プロセスは自分の持つトークンを隣のプロセスに渡す
  • 自分自身より小さい識別子のトークンを受信した場合、次に回さずに破棄する
  • もし自分のトークンが一周して戻ってきたら、自分がリーダーであるとみなす

リングトポロジの定義

まず時間発展に関わらない部分、すなわちプロセスがリング状に並んでいるという制約を記述します。この部分は元となった Jackson 本の記述と同じです。

module leader

sig Process {
  succ: Process,
}

fact ring {
  all p: Process | Process in p.^succ
}

トポロジ上で「自分の次」に当たるプロセスがただ 1 つ存在するため、それを succ で表現しています。またファクト ring から、どのプロセスをスタート地点にしても succ を 1 回以上辿ることで自分自信を含む任意のプロセスに到達できる必要があります。結果として、全体が 1 つのリング状に接続されていることが保証できます。

通信の定義

さて次に、時間発展する要素として、各プロセスが保持しているトークンを表現しましょう。

module leader
+ open util/ordering[Process]

sig Process {
  succ: Process,
+  var toSend: set Process
}

fact ring {
  all p: Process | Process in p.^succ
}

アルゴリズム中には「プロセスの識別子と対応するトークン」が登場します。識別子を表すために Id のようなシグネチャを別途用意する方法もありますが、今回は Process 自体に util/ordering で全順序を入れ、プロセスとトークンとを同一視することにします。

各プロセスに対して、toSend はそのプロセスが各状態で保持しているトークンの集合を表現しています。toSend には var が付加されており、ここまでに説明してきたようにこれは時間に依存した構造です。

プロセス p が自身の保持するトークンを次のプロセスに渡す遷移は、次のように表現できます。

pred step[p: Process] {
  some id: p.toSend {
    p.toSend' = p.toSend - id
    p.succ.toSend' = p.succ.toSend + (id - p.succ.prevs)
  }
}

すなわち、事前状態で p が保持していたトークンの集合 p.toSend の中から id を選択し、p の次のプロセスである p.succ の toSend に移動させます。事後状態としては p.toSend' からは id が取り除かれ、その代わり p.succ.toSend' に id が追加されます。

p.toSend の中からどの id を選択するかは制約としては与えられていません。これはもともとのシステム仕様にあった「通信の順序が保証されない」という条件に対応します。今回は通信路を明示的に実装してはいません。しかし toSend に「送信したがまだ受信されていないトークン」まで含まれていると考えることで、通信路上での追い越しを擬似的に表現しています。

また、次のプロセスに対する事後条件 p.succ.toSend' には id を追加したうえで p.succ.prevs を除外しています。これは「自分の識別子より小さいトークンは破棄する」という条件に対応します。今 Process には util/ordering による全順序が導入されているため、p.succ.prevs によって「p.succ より小さいすべての Process」を表現できます。

ランプの場合と異なり、今回のリーダー選出では動作の主体となるプロセスが複数あります。あるプロセスとその隣のプロセスがトークンを送受信している間、他のプロセスの状態が変化しないことを表現するための述語も用意しておきましょう。

pred skip[p: Process] {
  p.toSend' = p.toSend
}

初期状態と時間発展の定義

これで「トークンを受け渡す」という状態遷移は述語として定義できました。ランプの時と同じく、この述語を用いてそれ以外の遷移が発生しないという制約を加えます。

pred init {
  all p: Process | p.toSend = p
}

fact trace {
  init
  always all p: Process | step[p] || step[succ.p] || skip[p]
}

まず初期状態を init で制約します。初期状態において全てのプロセスは自分のトークンのみを持っています。繰り返しになりますが、トップレベルに現れた述語の基準点は初期状態であることを思い出しましょう。さらにそこから続くすべての遷移を always で制約します。

すべてのプロセスは「送信側になる」「受信側になる」「それ以外なので保持トークンが変化しない」のいずれかですが、step[succ.p] はややトリッキーです。受信側になったプロセスは保持トークンが増えるので、skip には該当しません。また、先に定義したとおり step[p] は「p が送信する」なので、受信側のプロセスはこちらにも該当しません。しかし step は受信側のトークンの変化まで定義に含んでいるため、p の 1 つ前のプロセスである succ.p が送信側であることをもって p は受信側であることが表現できます。

アルゴリズムの正当性の検査

それでは、目標だったアルゴリズムの正当性の検査に入っていきましょう。プロセスがリーダーとして選出されるには、自身のトークンが途中で破棄されずに一周して戻ってくることが必要でした。

pred elected[p: Process] {
  p in p.toSend' - p.toSend
}

ここでは「遷移の事前状態には自身のトークンを保持していなかったが、事後状態では保持している」という形で選出を表現しました。単純に「自身のトークンを保持している」としていないのは、初期状態を選出とみなしてしまうことを避けるためです。

まずアルゴリズムが最低限機能していることを確認するために、選出が発生する具体例を探索してみましょう。

pred successfullyElected {
  eventually some p: Process | elected[p]
}
run successfullyElected

実行してみると、実際にリーダーとして選出されるシーケンスが見つかります。なお以下のスクリーンショットでは、toSend の表示方法の「Show as arcs」を「Show as attribute」に切り替えて見やすくしてあります。この設定は Visualizer の Theme から可能です。


Process2 のトークンが一周することでリーダーに選出される例

今回のアルゴリズムに要求したい仕様として、以下の 2 つを考えます。

  • あるプロセスがリーダーに選出される場合、それ以外のプロセスはリーダーに選出されない
  • 少なくとも 1 つのプロセスがいつかはリーダーに選出される

1 つ目の仕様が「同時に 2 つのプロセスがリーダーに選出されない」では ない という点に注意しましょう。今回の記述では p が選出されたとみなされる、すなわち elected[p] が成立するのは状態遷移の 直後 のみなので、2 つのプロセスが別のタイミングで選出される可能性が残っています。実際には識別子が最大のプロセスがリーダーになるので、たとえタイミングがずれていても 2 つのプロセスが別々に選出されることはないはずです。

assert atMostOneElected {
  all disj p1, p2: Process {
    eventually elected[p1] => always !elected[p2]
  }
}
check atMostOneElected

条件を読み下すと「もし初期状態から続く状態列のどこかで p1 が選出されるならば、p2 は常に選出されていない状態が続く」となります。check を実行して反例が見つからないことを確認しましょう。

続いて 2 つ目の仕様です。条件に「いつかは」とあるので、一見 eventually を用いてそのまま記述できる気がするかもしれません。

assert atLeastOneElected {
  eventually some p: Process | elected[p]
}
check atLeastOneElected

しかし、予想に反してこの条件で実行すると反例が発見されるはずです。表示された状態遷移をみるとすぐ分かるとおり、この反例はすべてのプロセスが skip し続けるというものです。


どのプロセスも動かず、選出が行われない反例

そこで、この反例の可能性を除外するために「常に少なくとも 1 つ skip でないプロセスが存在する」という制約 progress を加えます。検査の前提として常に progress が成り立つことを条件としましょう。

+pred progress {
+  some p: Process | !skip[p]
+}

pred successfullyElected {
-  eventually some p: Process | elected[p]
+  always progress && eventually (some p: Process | elected[p])
}
run successfullyElected

assert atLeastOneElected {
-  eventually some p: Process | elected[p]
+  always progress => eventually some p: Process | elected[p]
}
check atLeastOneElected

この状態で check を実行すると、反例は無事に消えることが分かります。

ここで atLeastOneElected だけでなく successfullyElected にも progress を追加していることに注意してください。これは実用上重要で、仮に progress が制約として強過ぎてどうやっても成り立たない場合、前提が偽になることで atLeastOneElected は選出の可否に関係なく真になってしまいます。successfullyElected で具体例を検出することによって初めて、progress は実際に実現しうる条件であることが確認できます。

まとめ

本記事では、2021 年 11 月にリリースされた Alloy 6 の新機能、Mutable Field を用いた検査について解説しました。

  • Mutable Field が導入され、時刻に従って変化するような関係が記述可能になった
  • それに伴い、Visualizer の UI が刷新された
  • 検査に用いる条件式として、線形時相論理式が使用可能になった
  • 基本的に後方互換ではあるが、予約語の衝突により従来の記述はエラーになる可能性がある

Mutable Field と時相論理による検査機能を使用することで、時間発展するタイプのシステムを従来よりもシンプルに記述できるようになります。是非、新しい Alloy をダウンロードして体験してみてください。

参考文献

Discussion