PT模块代码

This is the PT module, which contains useful support operators to help people reading Practical TLA+.
Normally we would break the operators up by domain, but we lump them all here to make it easier on beginners.
All operators have a description of how they work.

---- MODULE PT ----

\* LOCAL means it doesn't get included when you instantiate the module itself.
LOCAL INSTANCE FiniteSets
LOCAL INSTANCE Sequences
LOCAL INSTANCE Integers

Max(x, y) == IF x > y THEN x ELSE y
Min(x, y) == IF x < y THEN x ELSE y

(* SET STUFF *)

(* Fairly simple one, uses a set comprehension to filter subsets by their cardinality (number of elements) *)
SubsetsOfSize(set, n) == { set1 \in SUBSET set : Cardinality(set1) = n} 

(*
TLA+ forbids recursive higher-order operators, but it is fine with recursive functions.
ReduceSet generates a recursive function over the subsets of a set, which can be used to
recursively run a defined operator. This can then be used to define other recursive operators.
*)
ReduceSet(op(_, _), set, acc) ==
  LET f[s \in SUBSET set] == \* here's where the magic is
    IF s = {} THEN acc
    ELSE LET x == CHOOSE x \in s: TRUE
         IN op(x, f[s \ {x}])
  IN f[set]


(* FUNCTION STUFF *)

(* 
Gets the set of all possible values that f maps to.
essential the "opposite" of DOMAIN. Uses a set comprehension-map.
*)
Range(f) == { f[x] : x \in DOMAIN f }

(*
Places an ARBITRARY ordering on the set. Which ordering you get is implementation-dependent
but you are guaranteed to always receive the same ordering.
*)
OrderSet(set) == CHOOSE seq \in [1..Cardinality(set) -> set]: Range(seq) = set

\* Get all inputs to a function that map to a given output
Matching(f, val) == {x \in DOMAIN f: f[x] = val}

(* SEQUENCE STUFF *)
\* TupleOf(s, 3) = s \X s \X s
TupleOf(set, n) == [1..n -> set]

\* All sequences up to length n with all elements in set.
\* Equivalent to TupleOf(set, 0) \union TupleOf(set, 1) \union ...
\* Includes empty sequence
SeqOf(set, n) == UNION {TupleOf(set, m) : m \in 0..n}

ReduceSeq(op(_, _), seq, acc) == 
  ReduceSet(LAMBDA i, a: op(seq[i], a), DOMAIN seq, acc)

(*
  SelectSeq lets you filter a sequence based on a test operator. It acts on the values.
  SelectSeqByIndex does the exact same, except the operator tests the indices.
  This is useful if you need to round-robin a thing.
*)
SelectSeqByIndex(seq, T(_)) ==
  ReduceSet(LAMBDA i, selected: 
              IF T(i) THEN Append(selected, seq[i]) 
              ELSE selected, 
            DOMAIN seq, <<>>)

\* Pulls an indice of the sequence for elem.
Index(seq, elem) == CHOOSE i \in 1..Len(seq): seq[i] = elem

(*
  % is 0-based, but sequences are 1-based. This means S[x % Len(S)] might be an error,
  as it could evaluate to S[0], which is not an element of the sequence.
  This is a binary operator. See [cheat sheet] to see the defineable boolean operators.
*)
LOCAL a %% b == IF a % b = 0 THEN b ELSE a % b
SeqMod(a, b) == a %% b

=====

对代码进行解释

这是 PT（Practical TLA+） 模块，其中包含一些实用的支持运算符，帮助初学者更容易理解。这些运算符按照领域分成不同的部分，但在此模块中将它们整合在一起。

---- MODULE PT ----

(* LOCAL 表示这些运算符不会在实例化模块时被包含进来。*)
LOCAL INSTANCE FiniteSets
LOCAL INSTANCE Sequences
LOCAL INSTANCE Integers

Max(x, y) == IF x > y THEN x ELSE y
Min(x, y) == IF x < y THEN x ELSE y

Max(x, y)：返回 x 和 y 中较大的值。
Min(x, y)：返回 x 和 y 中较小的值。

(* SET STUFF *)

SubsetsOfSize(set, n) == { set1 \in SUBSET set : Cardinality(set1) = n}

SubsetsOfSize(set, n)：返回集合 set 中元素个数为 n 的子集。

ReduceSet(op(_, _), set, acc) ==
  LET f[s \in SUBSET set] == 
    IF s = {} THEN acc
    ELSE LET x == CHOOSE x \in s: TRUE
         IN op(x, f[s \ {x}])
  IN f[set]

ReduceSet(op(_, _), set, acc)：定义了一个递归函数，用于对集合的子集进行递归运算。这可以用于定义其他递归运算符。

(* FUNCTION STUFF *)

Range(f) == { f[x] : x \in DOMAIN f }

Range(f)：返回函数 f 映射到的所有可能值的集合。

OrderSet(set) == CHOOSE seq \in [1..Cardinality(set) -> set]: Range(seq) = set

OrderSet(set)：对集合进行排序，返回一个具有特定排序顺序的序列。具体的排序顺序是实现相关的，但保证始终得到相同的排序顺序。

Matching(f, val) == {x \in DOMAIN f: f[x] = val}

Matching(f, val)：返回函数 f 中映射到给定输出值 val 的所有输入值的集合。

(* SEQUENCE STUFF *)

TupleOf(set, n) == [1..n -> set]

TupleOf(set, n)：返回集合 set 的所有长度为 n 的元组。

SeqOf(set, n) == UNION {TupleOf(set, m) : m \in 0..n}

SeqOf(set, n)：返回集合 set 中所有元素都来自 set，长度不超过 n 的所有序列的并集。包括空序列。

ReduceSeq(op(_, _), seq, acc) == 
  ReduceSet(LAMBDA i, a: op(seq[i], a), DOMAIN seq, acc)

ReduceSeq(op(_, _), seq, acc)：对序列中的元素进行递归运算，返回累积结果。

SelectSeqByIndex(seq, T(_)) ==
  ReduceSet(LAMBDA i, selected: 
              IF T(i) THEN Append(selected, seq[i]) 
              ELSE selected, 
            DOMAIN seq, <<>>)

SelectSeqByIndex(seq, T(_))：根据索引条件过滤序列中的元素，并返回符合条件的子序列。

Index(seq, elem) == CHOOSE i \in 1..Len(seq): seq[i] = elem

Index(seq, elem)：返回序列 seq 中元素 elem 的索引。

LOCAL a %% b == IF a % b = 0 THEN b ELSE a % b
SeqMod(a, b) == a %% b

a %% b 和 SeqMod(a, b)：这是一个二元运算符，用于处理序列的索引。注意，TLA+ 中的序列索引是从 1 开始的，而取模运算符 % 是从 0 开始的。这两个运算符用于在序列索中获取正确的索引值，避免出现索引超出范围的错误。

以上是 PT（Practical TLA+）模块中的一些运算符及其功能的简要说明。这些运算符提供了在 TLA+ 中进行常见操作的实用工具函数，并帮助简化代码的编写。