表达式

到目前为止，我们一直在隐式地使用表达式；我们只是没说清楚。对于我们的目的，表达式是任何跟在==，=，:=或\in后面的东西。在本节中，我们将介绍一些通用表达式修饰符。

逻辑联结词

我们已经使用了逻辑联结词有一段时间：/\ (且)，\/( 或)。我们可以把表达式和它们连接起来。一个微妙之处是，这是TLA+对空格敏感的唯一情况。如果你对某一行进行缩进，TLA+将认为这是子句的开始。例如:

  1. /\ TRUE
  2.   \/ TRUE
  3. /\ FALSE \* (T \/ T) /\ F
  5. /\ TRUE
  6.   \/ TRUE
  7.   \/ FALSE \* (T \/ T \/ F)
  9. \/ TRUE
  10. \/ TRUE
  11.   /\ FALSE \* T \/ (T /\ F)

这有几点经验:

  • 如果两个逻辑运算符位于相同的缩进级别，那么它们属于相同的表达式级别。
  • 如果逻辑运算符位于缩进的更高级别，则它是前面运算符语句的一部分。
  • 每个缩进级别只使用一种类型的运算符。

LET-IN

任何表达式都可以使用LET-IN将局部运算符和定义单独添加到该表达式中：

  1. LET IsEven(x) == x % 2 = 0
  2. IN  IsEven(5)
  4. LET IsEven(x) == x % 2 = 0
  5.     Five == 5
  6. IN  IsEven(Five)
  8. LET IsEven(x) == LET Two == 2
  9.                      Zero == 0
  10.                  IN x % Two = Zero
  11.     Five == 5
  12. IN  IsEven(Five)

这里的空格并不重要：我们可以LET IsEven(x) == x % 2 = 0 Five == 5 IN IsEven(Five)，它将正确解析为LET-IN中的两个独立操作符。但是为了易读性，你还是应该使用换行符。

IF-THEN-ELSE

正如你所期望的：

  1. IsEven(x) == IF x % 2 = 0 
  2.              THEN TRUE
  3.              ELSE FALSE

和之前一样，是否对齐并不重要，但是你应该对齐它们，除非你真的讨厌你的同事。

CASE

大多数情况下，情况都是你所期望的一样，但有一个细微的不同：

  1. CASE x = 1 -> TRUE
  2.   [] x = 2 -> TRUE
  3.   [] x = 3 -> 7
  4.   [] OTHER -> FALSE

OTHER的是默认的。如果没有一种情况匹配，而你遗漏了另一种情况，TLC认为这是一个错误。如果有多个匹配项，TLC将为你选择一个，而不是分支。换句话说，就是下面的代码:

  1. CASE TRUE -> FALSE
  2.   [] TRUE -> TRUE

Nesting(嵌套)

表达式的所有部分都是表达式或标识符，因此可以将表达式放在其他表达式中。此外，所有表达式都可以在PlusCal代码中使用。