ボイラープレート - TLA+メモ@ウィキ

ボイラープレートとはいわゆるテンプレートのこと。

ボイラープレート

TLA+は一見ではプログラミング言語のように見える。しかし、プログラムは実行される処理を表しているのに対してTLA+は仕様そのものを記述する。

------------------------------- MODULE sample-------------------------------
 
EXTENDS Integers
 
(*--algorithm sample {
\* ここにPlusCalのコードを記述する。
 (* グローバル変数宣言 *)
 (* define(演算子)定義 *)
 (* マクロ定義 *)
 (* プロシジャ *)
 (* アルゴリズム本体、もしくはプロセス宣言 *)
}*)
\* BEGIN TRANSLATION
\* PlusCalからTLAに翻訳されたコードは以下に出力される。
 
Next == Lbl_1 \/ Terminating
 
Spec == Init /\ [][Next]_vars
 
Termination == <>(pc = "Done")
\* END TRANSLATION 
=============================================================================
 

モジュール (MODULE)

TLA+ にはモジュールという大きな単位があり、モジュールは、他のモジュールから再利用可能なコードの塊を定義する。
“---- MODULE モジュール名 ----" で始まり “====” で終了する。またモジュール中の “----" は可読性のための罫線として使用することができる。
これらは 4 文字以上連続する - または = であれば良い。
ファイル名の [モジュール名].tla と TLA+ 構文の MODULE [モジュール名] でモジュール名を同じにしなければならない。
ただし、 PlusCal構文の algorithm [アルゴリズム名] はモジュール名とは異なる名前にしても良い。

EXTENDS

EXTENDS はモジュールをインポートする。EXTENDS はモジュールの先頭に定義する必要がある。EXTENDS 文は複数あってはならない。複数のモジュールをインポートする場合は、連続して記述する。

EXTENDS ModuleA, ModuleB, ModuleC

以下は正しくない。

EXTENDS ModuleA
EXTENDS ModuleB

EXTENDSでインポートされたモジュールの演算子等はグローバルなものとして扱われる。

INSTANCE

EXTENDS同様にモジュールをインポートする。似ているが異なる点がいくつかある。INSTANCE文は複数のモジュールを一度にインポートすることができない。複数のモジュールをインポートする場合は、複数回定義する。EXTENDSと異なる点に注意。

INSTANCE SequencesA
INSTANCE SequencesB

演算子に代入することでネームスペースとして使用できる。

Foo == SequencesA
 
Foo!Append(x,y)

FooやBarはネームスペースとして扱われ、呼び出す際に頭にネームスペースに続き、’!’をつける。
INSTANCE の前にLOCALをつけることでそのモジュールのローカルインスタンスとすることができる。

LOCAL INSTANCE SequencesA

LET文と組み合わせてローカルにインポートすることができる。（範囲を限定できる）

LET Foo == INSTANCE Sequences
IN Foo!Append(seq, 1)

標準モジュールについて

TLA+の標準モジュールには以下のようなモジュールがある。

MODULE名	機能
FiniteSets (有限集合)	集合とその操作に関する定義を提供しています。
Sequences (シーケンス)	シーケンス（順序付けられた要素の集合）の操作と関数を提供する。
Bags (バッグ)	重複を許す集合（マルチセット）とその操作を提供する。
Naturals	このモジュールは、自然数とその演算に関する定義を提供する。
Integers	整数を定義する。
Reals	実数と除算と無限大を定義する。
RealTime	リアルタイムシステムのモデリングに必要な時刻とその操作を提供する。
TLC	アサートやプリントなどのユーティリティ関数を提供する。

定数宣言 (CONSTANTS)

CONSTANTSキーワードを使用して、定数を宣言することができる。例えば以下は名前が"MaxValue"の定数を宣言することを示す。

CONSTANTS MaxValue

変数宣言 (VARIABLES)

“VARIABLES” (“VARIABLE”でも可)に続き変数を定義する。TLA+の変数、演算子に日本語は使用できない。
変数の宣言は以下のように行う。

VARIABLES x, y

コメント

TLA+では1行コメントは ”\*”、ブロックコメントは ”(*” で始まり、“*)”で終わる。
コメントには日本語を使用することもできる。PlusCalの構文はコメント内に配置される。

\* This is a single-line comment
 
(*
  This is a
  multi-line comment
*)
 

セミコロン

TLA+は文末にセミコロンを必要としない。PlusCalは文末にセミコロンを必要とする。