文法 (Syntax) - TLA+メモ@ウィキ

文法 (Syntax)

TLA+の文法について

=と==の違い

TLA＋ではxを初期化した場合は”x = 1”と記述する。xが初期化されていて、2を割り当てたい場合は、”x’ = 2”(xに” ’ ”をつける)と記述する。xと1を比較したい場合は“x = 1”と記述する。
つまり、初めて変数を使用する際には”=”は初期化として使用され、以降は等号として扱われる。また、”==”は比較ではなく演算子を定義するために使用する。

論理演算子

以下の論理演算子が定義されている。

演算子	意味	例	結果
a = b	equal	1 = 1	TRUE
a /= b a # b	not equal	1 /= 2	TRUE
a < b	less than	1 < 2	TRUE
a <= b	less than or equal	1 <= 2	TRUE
a > b	greater than	1 > 2	FALSE
a >= b	greater than or equal	2 >= 2	TRUE
a /\ b	AND	TRUE /\ FALSE	FALSE
a \/ b	OR	TRUE \/ FALSE	TRUE
~a	ノット	~TRUE	FALSE

述語論理

量化記号

記号	意味	例
\A	集合に含まれるすべての要素	AllLessThan(set,max) == \A num \in set : num < max
\E	集合に含まれるある要素	SeqOverLapSet(seq, set) == \E x \in 1..Len(seq): seq[x] \in set
~\A	集合のどの要素でもない
~\E	集合内に要素が存在しない。

\Aの集合に空集合を渡した場合、常にTRUEとなる。\Eの集合に空集合を渡した場合、常にFALSEとなる。

命題記号

記号	意味	例
a => b	含意 (aならばb) aがfalseである場合はbがtrue, falseどちらでもこの式はtrueとなる	宿題やった＝＞おやつ食べていい (宿題をやらなかった場合にはふれていないため、宿題をやらなかった場合はおやつを食べても食べなくてもよい)
a <=> b	同値 (aとbは同値である)	宿題やった＜＝＞おやつ食べていい。 (おやつ食べていいのは宿題やったとき)

式 (Expression)

IF-THEN-ELSE

IF-THENは条件式であり、一致した場合、値を返す。以下のような定義ができる。

x := IF p THEN x + 1 ELSE x – 1 

値を返すことのない以下のような式は定義できない。

IF p THEN x := x + 1 ELSE x := x – 1 

IF文に対するELSE文が必ず必要である。また、通常のプログラム言語にあるようなELSE IFにあたる表現はない (入れ子にすることでELSE IFを表現することは可能)。C言語の3項演算子に近い。

• IF-THEN(TLA+)とif then(PlusCal)の違い

TLA+のIF-THEN が式 (expression)であるのに対して、PlusCalのif-thenは構文(statement)であり値を返さない。

CASE-OTHER

IF-THEN-ELSEと異なる点は条件式が複数となる。expressionとなる式を評価する。2つ目以降ケースは[ ]を記述する。CASE-OTHERもIF-THEN-ELSEと同様に値を返す式である。

CASE x = 1 -> expression1
  [] x = 2 -> expression2
  [] x = 3 -> expression3
  [] OTHER -> expression
 

OTHERはデフォルトである。条件に一致するケースがない場合が該当する。一致するケースがなく、OTHERもない場合、TLCはエラーとして扱う。複数のケース式に一致した場合の振る舞いは未定義（最初に見つかったものが選ばれる?）。各ケース式が相互排他となるようにする必要がある。

CHOOSE

CHOOSEの定義は以下。

CHOOSE x \in S : P(x)
 

式の意味は「集合SからP(x)がTRUEとなるようなxを選択する」。複数のxと一致する場合、TLCは任意のxを選択する (実装としては最初に見つかったx ?) 。どのxとも一致しない場合はエラーとなる。

以下の例はCHOOSEと述語論理を組み合わせて集合Setからすべての要素(y)に対して等しいまたは大きいxを返す。つまり、setから最大値を選択する。

Max(Set) == CHOOSE x \in Set : \A y \in Set : x >= y
 

LET-IN

LET-INを使ってその式だけのローカル演算子やローカル定義を追加できる。

LET <definition1>
    <definition2>
    ...
IN <exprssion>
 

以下の例ではLET-IN構文を使用して x と y という2つのローカル変数を導入し、それらを使用して sum を計算する。 foo と bar は sum を計算するために使用する。

(* Define two variables and calculate their sum *)
foo == 2
bar == 3
sum == LET x == foo + 1
           y == bar * 2
       IN x + y
 

TLA+でLET-INを使用する際には、ローカル変数が重複せず唯一である必要がある。また、ローカル変数は、そのLET-IN構文の外側の式からはアクセスできない。

演算子 (Operator)

TLA+において演算子は通常のプログラミングの関数に相当する。以下のようにして演算子を定義することができる。

Op(arg1, arg2, …, argn) == Expr
 

演算子を定義する際は、等号は2つ(==)となる。引数がない場合は、”Op == Expr”となる。
演算子ではすべての変数の値を明示的に定義する必要がある。定義しない場合、未定義となる。

補足：状態遷移をTLA+で表現する場合、演算子を状態遷移のイベントとして扱う場合が多い。

有意なスペース

TLA＋においてインデントが意味を持つ箇所がある。１つの演算子に複数の句を連続して定義することができる。

Foo == /\ x
       /\ y
         \/ z
 

上記は x and ( y or z )と解釈される。

LAMBDA

LAMBDA式を使って無名の演算子を定義することができる。無名演算子の用途は他の演算子に対する引数に限られていて、独立した演算子として使うことはできない。

LAMBDA param1, param2, …, paramN: body
 

PrintT

標準モジュールのTLCをインポートすることでPrinT演算子を使用することができる。モデルの状態や変数の値を表示することができ、デバッグやモデルの検証に役に立つ。

PrintT(var) 

未分類

UNCHANGED構文

UNCHANGED構文は、式の評価前と後で、指定された変数や式が変化しないことを表す。UNCHANGED構文は、以下のような形式を持ちます。

UNCHANGED <<variable1, variable2, ..., variableN>>
 

この式は、variable1、variable2、...、variableNのいずれかが変化しないことを表す。変数のリストは、カンマで区切られて、<<と>>で囲まれる。また、UNCHANGED構文は、以下のように、算術式や真偽値式などの式でも使用できる。

UNCHANGED <<expr1, expr2, ..., exprN>> 
 

この式は、expr1、expr2、...、exprNのいずれかが変化しないことを表す。TLA+では、UNCHANGED構文は不変条件を表現するためによく使用される。例えば、”UNCHANGED x”は、xの値が変わらないことを表し、システムの不変条件の一部として使用される。また、UNCHANGED構文は、Nextステップ関数内で不変条件を維持するために使用されることがある。

EXCEPT構文を使った更新

PlusCalをTLA+に変換した際、つぎのような表現を見ることがある。

pc' = [pc EXCEPT !["writer"] = "Write"]

式の右側は、pcレコードの"writer"フィールドを"Write"に更新するという意味でEXCEPT演算子は、レコードの特定のフィールドを更新するために使用される。!["writer"]は、pcレコードの"writer"フィールドを指定し、=演算子は新しい値を割り当てる。他のフィールドの値はコピーされる(元の値のままとなる)。
EXCEPT構文は、レコードの不変条件を保持しながら、特定のフィールドを変更することができるため、TLA+でよく使用される。また、EXCEPT構文は、レコードのコピーを作成するため、元のレコードは変更されない。
以下のように連続して記述することで複数のレコードを更新することができる。

record EXCEPT ![field1] = value1, ![field2] = value2, ... , ![fieldn] = valuen
 

ボックス演算子

“[P]_x” という特殊な表現がある。これは以下の意味を持つ。

P \/ UNCHANGED x