TLA+に再挑戦(2022.5)

development tlaplus

英語のドキュメント を読んだけどあまり理解できてなかったので 日本語 で再挑戦する会。

進捗

8.1 リンクリスト

  • ユースケース
    • 循環を持つリンクリストをアルゴリズムが生成しないようにする。
      • 検証したいのはアルゴリズムで、リンクリストを部品として使用するっぽい
    • 循環を見つけ出すアルゴリズムを記述する。
      • リンクリスト自体を検証したいっぽい
    • 循環を持つリンクリストが与えられてもシステムが正しく動作するようにする。
      • 検証したいのはシステムで、リンクリストを部品として使用するっぽい

まず、ノード間で考えられるマッピングをすべて定義する
次に、「最後のノード」の概念が必要である

これだけで全ての要素の全ての組み合わせを定義したことになる。便利だ。

CONSTANT NULL
PointerMaps(Nodes) == [Nodes -> Nodes \union {NULL}]

PointerMapsは考えられるメモリマッピングの集合だが、それらのマッピングが全てリンクリストであるとは限らない

実は先に「8.2検証」まで読んでから戻ってきたのだけど、ようやく説明してることがわかってきた。
全ての要素の全ての組み合わせを定義してる から それらのマッピングが全てリンクリストであるとは限らない のか。
そこで次のようなアルゴリズムを導入しようとしている。

リンクリストのノードを「たどっていく」とシーケンスになることに着目するのである。
そうすると、与えられたPointerMapが単一のリンクリストである場合は、それ以降のすべての要素が
その手前の要素の次のノードであるというノードのシーケンスが得られる。たとえば、
リンクリストが[a |-> b, b |-> NULL, c |-> a] であるとすれば、シーケンスは<<c, a, b>>になる。

こういう解釈であってるのかな。

  • 「それ以降の全ての要素」とは
    • a |-> b b |-> NULL c |-> a のこと
  • 「その手前の要素の次のノードであるというノード」とは
    • a |-> b について
      • 「次のノード」が a になるのは c |-> a だから c
    • b |-> NULL について
      • 「次のノード」が b になるのは a |-> b だから a
    • c |-> a について
      • 「次のノード」が c になるノードはない、つまり NULL だから b
  • したがって、シーケンスは <<c, a, b>> になる

(1周目)以降の説明や実装がよくわからなかったので、「8.2検証」を読んだら戻ってくることにする。

---------------------------- MODULE LinkedLists ----------------------------
CONSTANT NULL

LOCAL INSTANCE FiniteSets \* Cardinality
LOCAL INSTANCE Sequences \* Len
LOCAL INSTANCE TLC \* Assert

\* 考えられるメモリマッピングの集合
\* まだこの演算子の役割がわからない
LOCAL PointerMaps(Nodes) == [Nodes -> Nodes \union {NULL}]

\* シーケンスをセットに変換する
LOCAL Range(f) == {f[x]: x \in DOMAIN f}

\* PointerMapはPointerMapsの要素
\* 与えられたPointerMapが単一のリンクリストになっていることをチェックする
\* PointerMapが[a |-> b, b |-> NULL, c |-> a]なら <<c, a, b>> になっていることをチェックする
LOCAL isLinkedList(PointerMap) ==
    LET
        nodes == DOMAIN PointerMap
        \* 1..Cardinality(nodes) は 1..len(nodes) の範囲になる
        \* つまりnodesの全ての要素について、重複を許す全ての組み合わせのシーケンスのセットになる
        \* [1..3 -> {4,5,6}] なら {<<4,4,4>>,...,<<6,6,6>>} になる
        all_seqs == [1..Cardinality(nodes) -> nodes]
    \* PointerMapに含まれる全てのノードの全ての並び順を網羅したシーケンスから、
    \* リンクリストの構成要件を満たすシーケンスが見つかれば、それはリンクリストだと判断できる
    IN \E ordering \in all_seqs:
        \* ordering[i]=a |-> bならPointerMap[ordering[i]]=c |-> aになる
        \* だからordering[i+1]=c |-> aになっていて欲しい
        /\ \A i \in 1..Len(ordering)-1:
            PointerMap[ordering[i]] = ordering[i+1]
\*        /\ \A n \in nodes:
\*            \E i \in 1..Len(ordering):
\*                ordering[i] = n
        \* マッピングのすべてのノードは ordering に含まれる
        \* Rangeはシーケンスのorderingをセットに変換する
        \* orderingはnodesの要素から生成した全ての組み合わせのシーケンスなので、
        \* 一部の要素だけ選択した場合nodesが部分集合にならない場合がある
        /\ nodes \subseteq Range(ordering)

\* リンクリスト演算子
LinkedLists(Nodes) ==
    IF NULL \in Nodes THEN
        Assert(FALSE, "NULL cannot be in Nodes")
    ELSE
        {pm \in PointerMaps(Nodes): isLinkedList(pm)}

この時点で main モジュールから LinkedList モジュールを読み込んで、実行できるようになる。
そうすると Evaluate Constant Expression でどういう結果になるのか観測できるようになる。
1度実行しないと Model Checking Results は出てこない。

-------------------------- MODULE main --------------------------
CONSTANTS NULL
INSTANCE LinkedLists WITH NULL <- NULL
  • Model Overview
    • What is the behavior spec?: No behavior spec
    • What is the model?
      • NULL <- [model value]

Model Checking Results でこういう結果を観測できる。

Expression:
LinkedLists({"a", "b"})

Value:
{ [a |-> NULL, b |-> "a"],
     [a |-> "a", b |-> "a"],
     [a |-> "b", b |-> NULL],
     [a |-> "b", b |-> "a"],
     [a |-> "b", b |-> "b"] }

これが

しかし、LinkedLists(Nodes) を呼び出してみると、長さが Cardinality(Nodes) のリンクリストが得られるだけである

ということなのかな。
NULL で終端できてないことや、循環してることは問題ないんだろうか。
それらは後で記述されているから、ここではリストの長さが等しくなってしまう、つまり機能不足であることを問題視しているんだな。

考えられるノードのサブセットをすべて生成し、サブセットごとにポインタマップをすべて定義し、生成されたポインタマップのすべてで isLinkedList を呼び出せばよい

すると次のように変化した。なるほどバリエーションが出てきてよさそう。

Expression:
LinkedLists({"a", "b"})

Value:
{ [a |-> NULL],
     [a |-> "a"],
     [b |-> NULL],
     [b |-> "b"],
     [a |-> NULL, b |-> "a"],
     [a |-> "a", b |-> "a"],
     [a |-> "b", b |-> NULL],
     [a |-> "b", b |-> "a"],
     [a |-> "b", b |-> "b"] }

開始点や循環リストの話は次回にする。

参考リンク