TLA+ 算子和值

算子

在 TLA+ 中, 算子 (operator) 就是编程语言中的函数。它们接受参数并求值为表达式。

EXTENDS Integers

MinutesToSeconds(m) == m * 60

算子可以接收任意数量的参数. 没有默认值, 重载或者是可选参数. 如果一个算子接收两个参数, 那么就必须传递两个参数. 如果一个算子不接受参数, 那么可以写成没有参数的形式. 在这种情况下, 它就像一个常量

SecondsPerMinute == 60

算子的右半部分称之为表达式.

IF-THEN-ELSE

在 TLA+ 中有三个结构化表达式的关键字, 分别是 let 语句, case 语句以及条件语句.

条件语句如下

Abs(x) == IF x < 0 THEN -x ELSE x

语句意义和常用编程语言中的三元表达式是相同的.

表达式总是会等于一个值, 因此 ELSE 是必须存在的.

值

TLA+ 是一个起源于数学的语言, 因此其中的值是无类型的. 在实际使用时, 模型检查器可以识别四种基本类型和四种复杂类型.

• 基本类型: strings, booleans, integers 以及 models value.

• 复杂类型: sets, sequences, structures 以及 functions.

在 TLA+ 中的每种类型都有着各自的算子, 不能被重载, 重写. 例外的算子是 “=” 和 “#”, 表示相等和不相等.

不同类型的值是不能进行比较的, 对不同类型的值进行比较会返回错误.

显而易见

Integers 和 strings 要使用基本的加法运算符，需要 EXTENDS Integers。字符串必须使用 “双引号”，不能使用单引号。除了 = 和 # 之外，字符串没有运算符。实际上，字符串被用作不透明的标识符，类似于某些语言的 :symbol 类型。如果您的系统需要操作字符串，我们可以将其存储在序列中。

需要注意的是, 在 TLA+ 中没有 float 类型。浮点数具有复杂的语义，极难表示。通常情况下，可以将其抽象出来. 但如果您绝对需要浮点数，那么 TLA+ 就是一个错误的工具。

Booleans

布尔类型的值是 TRUE 和 FALSE

boolean 的算子在 TLA+ 中更像是数学中的符号, 而不是编程语言中的符号。

逻辑	TLA+ 符号	数学符号
且(and)	/\	⋀
或(or)	/	⋁
非(not)	~	¬

我们可以使用基础算子来构建新的算子, 如异或(xor)

Xor(A, B) == A = ~B

初次之外, boolean 还有一个算子 =>, 表示蕴含. A => B 表示 “A 至少和 B 一样为真”。A => B = FALSE 当 A 为真且 B 为假时为假，否则为真。B 为真或 A 为假（或两者皆假）。这在编程中并不常见，因为它对控制流毫无用处。但它对任何规范工作都极为重要。

另外, 在 TLA+ 中, 布尔运算还有着 “bullet point notation” . 当有一个表达式像 A /\ (B \/ C) /\ (D \/ (E /\ F)) 这样, 就会难以阅读, 因此可以将其改写为:

/\ A
/\ \/ B
   \/ C
/\ \/ D
   \/ /\ E
      /\ F

这样看起来就变得极为清晰了. 在 A 前面有一个额外的 /\, 这不是必须的, 但是它让整个结构看起来更为舒适. 这也是语言中唯一需要留白的地方。假设我写的是

/\ A
/\ \/ B
   \/ C
/\ \/ D
   \/ /\ E
/\ F

那么所有的逻辑都将变化了, 现在表达式等于 A /\ (B \/ C) /\ (D \/ E) /\ F.

Sequences

sequences 就像其它语言中的 list. 一个 sequence 可以被写成 <<a, b, c>>, 它的值可以是任何类型的(包括 sequence). 和其它大多数语言一样, 我们通过 seq[n] 的语句来获取指定位置的值, 只不过在 TLA+ 中, 列表的索引是从 1, (1..Len(seq) )开始的, 而不是从 0 开始.

在 TLA+ 中通用也有着 Sequence 模块, 如果使用了EXTENDS Sequences, 并且定义了 S == <<"a">>

表达式	结果
Append(S, "b")	<<"a", "b">>
S \o <<"b", "c">>	<<"a", "b", "c">>
Head(S)	"a"
Tail(<<1, 2, 3>>)	<<2, 3>>
Len(S)	1
SubSeq(<<1, 3, 5>>, 1, 2)	<<1, 3>>

在 TLA+ 中只支持一行 EXTENDS, 如果有多个模块需要导入, 那么就使用逗号分隔开.

通过 sequences, 我们可以使用 <<hour, minute, second>> 的形式来表达一个 24 小时制的时钟

EXTENDS Integers, Sequences

ToSeconds(time) == time[1]*3600 + time[2]*60 + time[3]
Earlier(t1, t2) == ToSeconds(t1) < ToSeconds(t2)

Sets

一个 set 就是一个无序, 不同值的集合. 可以写成 {1, 2, 3}, 或者 {<<"a">>, <<"b", "c">>}, 一个 set 甚至可以包含其它 set {{1}, {2}, {3}}.

set 不可以包含不同类型的值, {1, "a"} 是无效的.

set 算子

为了检查 x 是 set 中的元素, 我们可以写 x \in set. \in 也可以在其它的一些场景使用, 而不仅做为一个算子. 当然也有反向的算子\notin. set1 \subseteq set2 测试 set1 中的每个元素是否都在 set2 中.

其它的一些算子

• set1 \union set2: 表示 set1 和 set2 的并集
• set1 \intersect set2: 表示 set1 和 set2 的交集
• set1 \ set : 表示 set1 和 set2 的差集, 即仅存在与 set1 中的元素

>>> {1, 3} \union {1, 5}

{1, 3, 5}

>>> {1, 3} \intersect {1, 5}

{1}

>>> {1, 3} \ {1, 5}

{3}

如果你导入了 FinitesSets 模块, EXTEND FiniteSets, 那么就可以使用 Cardinality(set)算子来获取 set 中的元素数量.

Sets of Values

假设我们正在写一个 spec, 使用 clock 的值, 并且我们想要一个算子来快速计算并返回相加后的时间. 可能将它写为下面的形式

AddTimes(t1, t2) == <<t1[1] + t2[1], t1[2] + t2[2], t1[3] + t2[3]>>

然后使用 AddTimes(<<2, 0, 1>>, <<1, 2, 3>>) = <<3, 2, 4>>, 和 AddTimes(<<2, 0, 1>>,<<1, 2, 80>>) = <<3, 2, 81>>.

这时我们发现不对了, 我们的时钟显示了 81 秒, 正确的答案应该是 <<3, 3, 21>>. 一个有效的时钟值集合应该是从 <<0, 0, 0>> 到 <<23, 23, 59>> 的, 并且 AddTime 返回的结果也是其中的值.

我们可以在 TLA+ 中强制这样, 但是首先我们需要一种从数值生成数值集的方法. 幸运的是, TLA+ 中的每种类型的值都是可以生成值的集合的.

首先从最简单的 boolean 类型的值开始, 需要获取所有布尔类型的值的集合, 直接写 BOOLEAN , 它代表 {TRUE, FALSE}. 对 Intergers 的来说, a..b 是集合 {a, a+1, a+2, …, b}. 需要 EXTENDSIntegers 来使它生效.

接下来是 Sequence, 两个集合 S 和 T 的笛卡儿乘积是所有序列的集合，其中第一个元素在 S 中，第二个元素在 T 中。例如，LoginAttempt 包含登录者、尝试登录的时间以及登录是否成功。我可以将所有可能值的集合表示为 LoginAttempt == Person \X Time \X BOOLEAN.

\X 不是相关联的.

S == 1..3

>> <<1, 2, 3>> \in S \X S \X S
TRUE

>> <<1, 2, 3>> \in (S \X S) \X S
FALSE

>> <<<<1, 2>>, 3>> \in (S \X S) \X S
TRUE

对于时钟类型来说, 我们可以使用 \X 和 .. 来得到我们需要的类型.

ClockType == (0..23) \X (0..59) \X (0..59)

你会发现它有 86400 个元素。现在我们离 AddTimes 的属性又近了一步：我们希望 AddTimes 的结果总是返回 ClockType 的值。

Map Filter

Set 可以被 map 以及 filter

\* Map
Squares == {x*x: x \in 1..4}

\* Filter
Evens == {x \in 1..4: x % 2 = 0 }

CHOOSE

从时钟值中获取午夜过后的秒数非常简单。但反过来呢？如果我们有一个以秒为单位的时间，我们可以通过以下方法得到时钟时间

1. Floor 除以 3600，得到总小时数。

2. 再用余数除以 60，得到总的分钟数。

3. 将第二次除法的余数作为秒。

这样就能从总秒数中构建出时钟值。这就是我们在编程语言中实现算法的方法。但这也容易出错。如果我输入 90,000 会怎样？这样就会得到 <<25, 0, 0>> - 一个不属于 ClockType 的值。

我们还可以这样做：

1. 获取所有可能的时钟值集合。

2. 在集合中选择一个元素，将其转换为秒后，我们就得到了这个值。

我们不会这样做，因为 “所有可能的时钟值集合 “长度超过 80,000 个元素，在 80,000 个元素的列表中进行查找会浪费资源。但这样做更符合转换的定义，使其对规范更有用。在 TLA+ 中，我们可以这样编写选择：

ToClock(seconds) == CHOOSE x \in ClockType: ToSeconds(x) = seconds

CHOOSE x \in set: P(x) 是通用的 “选择 “语法.

当我们需要从一个集合中提取一个值时，CHOOSE 就会派上用场。

如果我们写 ToClock(86401) 会怎样？没有任何时钟时间有 86,401 秒。如果尝试这样做，TLC 将引发错误。这与实现方案截然不同，后者会给出一个无意义的值。99% 的情况下，如果找不到对应的集合元素，那就是规范中的错误，是你没有考虑到的边缘情况。最好是强化算子:

ToClock(seconds) == CHOOSE x \in ClockType: ToSeconds(x) = seconds % 86400

LET

现在, 你可以想象到 TLA+ 的算子可以非常负责. 为了简化他们, 我们可以通过 LET 来将他们划分为不同的子算子

ToClock(seconds) ==
  LET seconds_per_day == 86400
  IN CHOOSE x \in ClockType: ToSeconds(x) = seconds % seconds_per_day

LET 给我们提供了一个新定义，本地作用域为 ToClock。seconds_per_day 是一个操作符，只存在于这个定义中。

我们也可以在 LET 中添加参数化操作符！

ThreeMax(a, b, c) ==
   LET
     Max(x, y) == IF x > y THEN x ELSE y
   IN
     Max(Max(a, b), c)

你可以定义多个算子在一个 LET 中:

ThreeMax(a, b, c) ==
   LET
     Max(x, y) == IF x > y THEN x ELSE y
     maxab == Max(a, b)
   IN
     Max(maxab, c)

LET 中的每个运算符都可以引用该范围内先前定义的运算符。这样，我们就可以逐步构建解决方案。

ToClock2(seconds) ==
  LET
    h == seconds \div 3600
    h_left == seconds % 3600
    m == h_left \div 60
    m_left == h_left % 60
    s == m_left
  IN
    <<h, m, s>>