• 2 Introduction to TLA+
  • 2.1 A Simple Math
    • 2.1.1 Propositional Logic
      • 2.1.1.1 Definition
      • 2.1.1.2 Formula of Propositional Logic
      • 2.1.1.3 Tautology
    • 2.1.2 Sets
      • 2.1.2.1 Concepts
      • 2.1.2.2 Operations on Set
    • 2.1.3 Predicate Logic
    • 2.1.4 Tautologies
    • 2.1.5 Set Constructor
    • 2.1.6 The Mathematical Definition of GCD
    • 2.1.7 Review
  • 2.2 TLA+ Syntax
    • 2.2.1 ASCII Representation
    • 2.2.2 CHOOSE
      • 2.2.2.1 Definition
      • 2.2.2.2 Application
    • 2.2.3 Integers
    • 2.2.4 TLA+ Toolbox
      • 2.2.4.1 New Spec
      • 2.2.4.2 Typical Spec
      • 2.2.4.3 TLC
    • 2.2.5 Simple Operators
    • 2.2.6 Exercise 1
    • 2.2.7 Higher-order Operators
    • 2.2.8 IF/THEN/ELSE
    • 2.2.9 CASE
    • 2.2.10 LET-IN
    • 2.2.11 Exercise 2
    • 2.2.12 Tuples
    • 2.2.13 Sequences
    • 2.2.14 Exercise 3
    • 2.2.15 Sets of Tuples
    • 2.2.16 Structures/Records
    • 2.2.17 Sets - Filtering
    • 2.2.18 Sets - Mapping
    • 2.2.19 Exercise 4
    • 2.2.20 Set Operators 1
    • 2.2.21 Exercise 5
    • 2.2.22 Set Operators 2
    • 2.2.23 Exercise 6
    • 2.2.24 FiniteSets
    • 2.2.25 Exercise 7
    • 2.2.26 Logic 1
    • 2.2.27 Exercise 8
    • 2.2.28 Logic 2
    • 2.2.29 Exercise 9
    • 2.2.30 CHOOSE Again
    • 2.2.31 Functions
    • 2.2.32 Exercise 10
    • 2.2.33 Function Set
    • 2.2.34 Exercise 11
    • 2.2.35 Exercise 12
    • 2.2.36 Exercise 13
    • 2.2.37 Why Don't Computer Scientists Learn Math?
    • 2.2.38 Exercise 14
    • 2.2.39 Exercise 15
    • 2.2.40 Summary
    • 2.2.41 Function Definitions
    • 2.2.42 Examples
    • 2.2.43 Paper: How to Write a Long Formula
    • 2.2.44 EXCEPT
    • 2.2.45 GCD
    • 2.2.46 CarTalkPuzzle

在前面的内容中，用Init和Next描述一个序列，对于简单的系统这样描述没有问题，对于复杂的系统是远远不够的，Init和Next里并没有时序逻辑，只是简单的序列公式。TLA是对Init和Next再做一个提升，更加优雅，能够以简单的方式去描述更复杂的系统。TLA只关心序列、序列的形态，但不关心一个Si里有哪些状态、这些状态如何描述，"+ (Plus)"就是解决这个问题的。TLA+一方面关注整个行为的描述，一方面关注一个Si里的状态如何定义，静态的，如何表达堆栈、如何表达复杂的业务数据结构等。其中"+ (Plus)"选用一阶逻辑、集合论、函数这样一些简单的概念，基于这些概念可以表达任意复杂的业务上所需要的数据结构。

这一部分主要讲"+ (Plus)"，Data Logic和Data Operation。

Writing is nature's way of letting you know how sloppy your thinking is.
                                                            Dick Guindon

Mathematics is nature's way of letting you know how sloppy your writing is.

... Formal mathematics is nature's way of letting you know how sloppy your mathematics is.
                                                       Leslie Lamport, Specifying Systems

Dick Guindon是一个漫画家，但Lamport很推崇他说的这句话。《Specifying Systems》是Lamport写的一本好书，看前80页就够了。

如果不写你不知道你自己想得有多糟糕。 如果不学数学你不知道你自己写得有多糟糕。 如果不用形式化的数学你不知道你的数学有多糟糕。

用自然语言加公式描述其实也不清晰，只有形式化地写出来才真正的清楚了。

首先要写，其次要用数学写，还要用formal形式化地写，这才是清晰的思维，思考的程度越来越高。

TLA+是规格说明的语言，它是一种堂吉诃德式的尝试，帮助工程师克服对数学的恐惧和厌恶。把长期以来根深蒂固的情绪化的反应能够稍微压制一下。TLA+本身确实非常优美、简单、易于理解，而且确实能解决实际问题。

数学也可以运行起来，而且可以验证一些更深入的东西。大家可以体会一下用数学解决问题跟用编程语言解决问题的区别。

下面把一阶逻辑和集合论的知识快速地过一遍。

一阶命题逻辑。初等代数里有数和数的操作。一阶命题逻辑也是一门数学，有值和值的操作，值比代数简单，只有TRUE和FALSE两个。操作符有5个，如上图所示。初等代数和一阶命题逻辑可以做一个同构映射。

F和G是一阶逻辑表达式，TRUE、FALSE也是表达式，是原子表达式，表达式可以组合。and、or、not、is equivalent to的语义很简单。重点看一下implies(蕴含)。

F=>G，F为假或者G为真(包括F和G均为真)。implies(蕴含)的真值表如下图所示：

【Faye】我在网上搜索了一下资料，有些说法可以帮助理解记忆。

• 只有在F为真、G为假时，F=>G才为假；或者，(要想F=>G为真，那么)F为真时，G必须也为真。
• 如果F=>G，当F为真，G一定为真；当F为假，G可能为真也可能为假；当G为真，F可能为真也可能为假；当G为假，F一定为假。

举个例子，如果整数x大于4，那么x一定大于2，即(x > 4) => (x > 2)这句话永远是对的。如果x=5，因为x大于4，那么x一定大于2。如果x=3，因为x小于4，那么x可能大于2可能小于2，这里x大于2。

【Faye】我根据implies的真值表计算如下：

F: x > 4  G: x > 2  F => G: (x > 4) => (x > 2)

        x > 4   x > 2   (x > 4) => (x > 2)
x = 5    TRUE    TRUE          TRUE
x = 3   FALSE    TRUE          TRUE
x = 1   FALSE   FALSE          TRUE
         TRUE   FALSE (IM)    FALSE

IM: Impossible

【Faye】再举个例子，如果他去过法国，他就一定去过欧洲。如果他没去过法国，他有可能去过欧洲，也有可能没去过。我根据implies的真值表计算如下：

F：France  G: Europe  F => G: France => Europe

         France   Europe   France => Europe
France    TRUE     TRUE          TRUE
England  FALSE     TRUE          TRUE
China    FALSE    FALSE          TRUE
          TRUE    FALSE (IM)    FALSE

IM: Impossible

跟代数一样，也可以用标识符来表示一个值，例如x。

永真式(重言式)。

(x = 2) => (x + 1 = 3) 这句话对吗？ 逻辑的表达式只是语法，它没有任何意义，只要是满足语法的合法表示即可，它的意义是靠我解释的。跟编程语言一样，用编程语言写的程序本来没有任何意义，它的意义是为Compiler服务的，如果换另外一个Compiler，意义可能就变了。所以我们在谈一个公式的真假时一般会蕴含一个上下文。上面这个例子中的x如果是整数，按这样解释，这个表达式为真。但如果换一种解释，定义另外一个整数系统，x + 1 = 5，这个表达式就为假。不同的解释下表达式的值不一样。

【Faye】在整数系统的上下文里，我根据implies的真值表计算如下：

F: x = 2  G: x + 1 = 3  F => G: (x = 2) => (x + 1 = 3)

         x = 2    x + 1 = 3    (x = 2) => (x + 1 = 3)
x = 2     TRUE      TRUE              TRUE
x = 2     TRUE     FALSE (IM)        FALSE
x ≠ 2    FALSE     FALSE              TRUE
x ≠ 2    FALSE      TRUE (IM)         TRUE

IM: Impossible

去掉两种不可能的情况，在整数系统里，(x = 2) => (x + 1 = 3)为真。

再来看(x = 2) => (x = 2) / (y > 7)，这个表达式无论怎么解释都为真。 在某种解释下，x = 2要么真要么假，如果x = 2为假，(x = 2) / (y > 7)可能为真也可能为假，表达式为真；如果x = 2为真，(x = 2) / (y > 7)肯定为真，表达式为真。

【Faye】以整数系统的上下文为例，我根据implies的真值表计算如下：

F：x = 2  G: (x = 2) \/ (y > 7)  F => G: (x = 2) => (x = 2) \/ (y > 7)

                x = 2    (x = 2) \/ (y > 7)    (x = 2) => (x = 2) \/ (y > 7)
x = 2 y = any    TRUE           TRUE                  TRUE
x = 2 y = any    TRUE          FALSE (IM)            FALSE
x ≠ 2 y = 6     FALSE          FALSE                  TRUE
x ≠ 2 y = 8     FALSE          TRUE                   TRUE

去掉一种不可能的情况，无论怎么解释，(x = 2) => (x = 2) / (y > 7)永远为真。

这种在任何情况下都为真的表达式，称为Tautology(永真式)。

这个式子很有用。

【Faye】可以对应到前面的解释：F=>G，F为假或者G为真(包括F和G均为真)；或者，只有在F为真、G为假时，F=>G才为假。

1. 集合(set)

"集合(set)"这个概念不能讲，一讲就会动摇基础。我们就认为"集合(set)"是一个非常基础的、已经定义好的概念。但我们要知道有些东西不是集合。如果一个东西太大，肯定不是集合。什么是太大？后面会讲到。

2. 属于(∈) "属于(∈)"是一个relation。如果x∈S，那么x与S之间有数学关系，代表x是S中的一个元素，通常称为"x in S"。

3. 集合可以有有限或无限个元素。 所有自然数集合的元素是无限的，所有小于3的自然数集合的元素是有限的，即{0, 1, 2}。

4. 一个集合完全由它的元素决定。 元素唯一且顺序无关。两个集合相等当且仅当它们拥有相同的元素，不用考虑顺序。{1, 2, 3}和{2, 1, 3}相等。

• ∩：intersection，交集
• ∪：union，并集
• ⊆：subset，子集
• \：set difference，差集

在命题逻辑的基础上增加了两个修饰符(量词)就变成了谓词逻辑。

• ∀：for all，全称量词，任给，对于集合中的所有元素，后面的命题逻辑为真
• ∃：there exists，存在量词，存在，集合中至少存在一个元素，后面的命题逻辑为真

因为是定义在一阶逻辑上，所以任给和存在只能修饰值(value)，任给和存在里面不能再出现谓词。只能说，存在一个值；不能说，存在一个谓词P。

• ∀x∈S : F：F是命题逻辑的公式。对于S中的每一个元素，用这个元素替换F中的x，F都为真。

  • F是x > 2，S是{1, 2, 3}，那么"任给x属于S、F为真"这句话为假。
  • ∀n∈Nat : n+1>n，"任给n属于自然数(Nat)，n+1>n"这句话为真。

• ∃x∈{} : F："存在x属于空集，F(不管F是什么)"为假。因为空集合没有任何元素。

• ∀x∈{} : F："任给x属于空集，F(不管F是什么)"为真。因为空集合没有任何元素，找不到元素，找不出来反例，肯定是任意的、所有的。

永真式(重言式)。我们写的大部分Spec都没有这么复杂，只是给大家介绍一下，不用害怕，根本在于我们对于系统的理解。

• (∀x∈S : F) ≡ (∀x : (x∈S) => F)：任意x属于S、F为真 等价于 任意x，x属于S蕴含F
• (∃x∈S : F) ≡ (∃x : (x∈S) ∧ F)：存在x属于S、F为真 等价于 存在x，x属于S合取F
• (∃x : F) ≡ ┐(∀x : ┐F)：存在x、F为真(肯定有个x使得F为真) 等价于 "任给x，F都为假"为假。再理解一下，存在x使得F为真，任意x使得F为假是不对的，所以再"not"一下。

"存在"和"任给"、"与"和"或"等称之为"对偶"关系。"对偶"是一种非常有趣、优美的结构，它将两个看似无关的东西通过一个触发器(比如第三个式子里的not)关联起来，，用"任给"定义"存在"。

【Faye】试着从直觉上理解一下第一个和第二个式子。 第一个式子左边的含义是"任给x属于S，使得F都为真"，式子右边的含义是"任给x，x属于S蕴含了F为真"。implies的真值表如下：

任给x   x ∈ S  F为真   x ∈ S => F为真
        TRUE   TRUE           TRUE
        TRUE  FALSE          FALSE
       FALSE   TRUE           TRUE
       FALSE  FALSE           TRUE

上面两行好理解。下面两行稍微解释一下，"任给x，x属于S"为FALSE的含义是"存在x，x不属于S"，这种情况下F可能为真也可能为假，蕴含关系始终为真。

第二个式子左边的含义是"存在x属于S，使得F为真"，式子右边的含义是"存在x，使得x属于S和F同时为真"。

以上是两个例子。这两个公式要了解一下，后面会用到。这样可以把一个很长的"与"或者"或"表达式，用"任给"或者"存在"就搞定了。

如何构造一个集合。

都很简单，缺的只是我们如何把它们用好，用来解决实际问题。

• {}是空集合，{1,2,3}是字面值作为元素。
• {x∈S : P}是过滤(filter)，对于S中的每一个x，如果P为真，就把x返回回来。
  • {n∈Nat : n%2 = 1}是所有奇数的集合。
• {E : x∈S}是真正的List Comprehension，List Comprehension来自于集合论。E是一个表达式，对于S中的任意x，用x的值代替E中的x得到新值，就是Map。
  • {2*n+1 : n∈Nat}也是所有奇数的集合。

做一个练习，由简单到复杂，否则把学习过程和问题本身搅在一起会造成障碍。

最大公约数(GCD)的数学定义。欧几里得(Euclid)很早之前就发明了、现在一直在用的一个很著名的算法。

在数学层面上，两个或多个都不等于0的整数，这些整数的所有因子里最大的，就是它们的最大公约数。

能不能用数学语言把这个定义表达出来？注意这不是算法，是数学定义。这是一种很重要的训练。

GCD的数学定义的思考过程：

1. 什么叫整除(divide)？ N和P两个数，N是P的一个因子，即P除以N是一个整数，如何定义？存在另外一个整数，乘以N，等于P。

2. 什么叫一个整数的所有因子？ 这是一个集合，filter，一个一个看，所有整数都过一遍，是整数的因子就过滤出来。这样可以得到两个整数各自所有因子的集合。

3. 什么叫两个数的共同因子？ 两个整数各自所有因子的集合的交集。

4. 什么叫共同因子里的最大值？ 假设集合S，找到一个数x属于S，任给y属于S，y都小于等于x。

这不是算法，是数学定义。为什么会有算法呢？因为算法效率、性能更高。数学定义是不管性能的，对于某些大规模M、N，实用性会打折扣，但肯定是对的。

Writing is nature's way of letting you know how sloppy your thinking is.
                                                            Dick Guindon

Mathematics is nature's way of letting you know how sloppy your writing is.

... Formal mathematics is nature's way of letting you know how sloppy your mathematics is.
                                                       Leslie Lamport, Specifying Systems

再来回顾一下这几句话，我们写出来的到底是什么意思呢？不用数学表达出来不见得真地想清楚了，能用数学表达出来说明真地想清楚了。先不用考虑性能，先保证正确性才能谈性能。

TLA+就是数学，不是编程语言，它就是数学概念。

数学符号的ASCII表示法。

• == 是definition。
• \div 是整数除。
• -> Function Set会提到。

CHOOSE x∈S : P(x)：假设一个集合S，CHOOSE一个x属于S，然后P(x)，很像"存在"。CHOOSE的意思是，如果集合里有一个或多个值，能够让P为真，就选一个出来。

CHOOSE x∈{1, 2, 3} : x > 1：2和3都可以，选哪一个呢？CHOOSE会选2或3，但它是一个确定性的，永远选2或者永远选3，不会一会儿选2、一会儿选3。

CHOOSE名字起得不好，可以认为CHOOSE是一个sum，有一个拿出来就行。

用CHOOSE实现求解GCD问题中的max，假设一个集合S：

CHOOSE x∈S : ∀y∈S : y <= x

这样CHOOSE会返回一个值。"存在"是一个布尔判断，CHOOSE是得到一个值，注意区分。

Choose Axiom(公理)：

"存在x属于S，P(x)为真" 蕴含着
    "CHOOSE x属于S，P(x)为真，返回一个值，值属于S"
 且 "CHOOSE x属于S，P(x)为真，返回一个值，值是满足P的"。

两个恒等式：

• 第一个恒等式好理解。
• 第二个恒等式的意思是CHOOSE永远选一样的值。这里体现了Right Uniqueness(右向唯一性)，就是说，CHOOSE不是一个非确定性的，是确定性的，可能有多个值，CHOOSE永远返回同样一个值。

CHOOSE是TLA里的一个Operator，是找值的，用来从集合里选出一个值。

1. ChooseOne(S, P(_))是一个Definition，定义了一个Operator。有两个参数，一个是集合S，一个是谓词P。"CHOOSE一个x属于S，P(x)为真"并且"任给y属于S，P(y)为真"蕴含"y = x"。ChooseOne表示从S中选出唯一一个满足P为真的元素。

举例：

• S: {2, 3, 5} P: 选出集合里唯一的偶数，ChooseOne(S, P)返回2。
• S: {2, 3, 4, 5} P: 选出集合里唯一的偶数，y = x是FALSE，"蕴含"的状态是"如果是TRUE，但是是FALSE"的意思是FALSE，可以写为CHOOSE x∈S : FALSE，或者写为CHOOSE x∈{}，ChooseOne(S, P)返回Undefined，什么都不是。

可以用这个技巧来定义不属于某个集合的值。

2. AnyOf(S) 能选出一个确定的值，不用关心值具体是什么。具体选出哪一个值依赖于实现，但保证是确定的。

3. NotAnS 会选出一个值，但这个值肯定不属于S，不用关心值具体是什么。

4. Error 其实不是Error。找到一个不是Int的值。

这都是一些技巧，在建模的时候定义一些特殊的值来表示概念。

在TLA里，1、2、3这些数都是有定义的。其实深挖一下，我们认为1、2、3是value，其实都是set，任何值都是set，这里不深究，我们认为它们都是值就行了。

如果我们想用1、2、3这些值，并且用+、-、*、÷这些操作符的话，TLA里自带了Integers module，用"EXTENDS"引进来才能用。

• Int是所有整数的集合。
• Nat是所有自然数的集合。
• ..是set的快捷构造器，m..n是指大于等于m、小于等于n的整数的集合。
• ÷是整数除，返回还是整数，用"\div"表示。
• %是模。

前面的求解GCD问题需要EXTENDS Integers。

打开TLA+ Toolbox，点击"File->OpenSpec->Add New Spec..."菜单项，找个目录，起个名字"Exam"，点击"Finish"后，如下图所示：

图中的"-"和"="都是4个就够了，要求至少4个，写这么长是为了好看。MODULE是关键字，后面是Module的名字，名字必须跟文件名一样。目前是一个空的spec。

一个典型的Spec由以下几部分组成：

• EXTENDS：引入一些Module，例如Integers、TLA工具库或者自己定义的模块。
• CONSTANTS：对于序列来说，序列不允许变化，就是CONSTANTS。
• VARIABLE：地球围着太阳转，一个position这样的量，在不同的时刻有不同的值。
• ASSUME：假设，帮助我们做一些TLA的Check。如果定义了CONSTANTS C1，可以ASSUME C1是整数、C1是自然数或者C1属于某个集合。不写不影响，写了更清楚，可以知道这些常量有什么要求。
• TLA里没有类型：这里也是有争议的，很多人认为写规格说明的语言没有类型是不可接受的，但Lamport觉得有类型完全搞复杂了。类型有好处，但对于Spec来说，首先整个Spec不会很大，其次增加类型后会影响表达力，要通过增加复杂性来提升表达力，很别扭，得不偿失。Lamport认为类型其实也是Invariant。举个例子，我们说x1是整数，就是说可以定义一个Invariant：x1∈Int，可以Check"x1永远属于Int"。可以用这种方式解决类型的问题。
• Definition：可以认为就是简便写法。可以有参数，可以没参数。也叫Operator，但Operator感觉更面向编程。在任何地方，"=="左边的都用右边的替换，而且替换是发生在Spec运行之前，可以大概认为是"宏"。而且Operator支持递归。
• Function：可以认为是完全数学意义上的Function，不是编程语言里的Function，完全不是一个概念。f[]中的S是函数的定义域(Domain)。函数有定义域(Domain)和值域(Range或Image)。两个集合S1、S2，f是从S1到S2映射，对f来说，S1就是定义域，S2就是值域。f有很多种：单射、满射、双射。例如：f[x \in {1, 2, 3}] == x + 2就是一个函数，其实是一种关系，1跟3有关、2跟4有关，3跟5有关。定义域里的值跟值域里的值是一个pair。
• \*是单行注释，(...)是块注释。
• TLA+的所有关键字或保留字都是全大写的。

TLA+ toolbox里包含了TLC，TLC是TLA+的Model Checker工具。可以不用写任何Spec，点击"TLC Model Checker->New Model..."菜单项，输入Model名字(名字随意，缺省Model_1)，新建一个Model。

会产生一个Model_1的Tab页。选择"Model_1"的第一个子Tab页"Model Overview"：

"Model Overview"中的Init、Next看着很熟悉，勾上"No Behavior Spec"(缺省就是勾上的)，不需要任何Spec。

再选择"Model Checking Results"Tab页，找到"Evaluate Constant Expression"，在"Expression:"中可以写TLA+表达式，例如"2+2"，点击"Run"按钮，就会在"Value:"中显示运行结果。像一个Shell。需要注意的是，由于"+"属于Integers，需要在Spec里写"EXTENDS integers"，否则会报错。

还可以再试几个表达式：

Expression                  Value
\A x \in {1,2,3} : x > 2    FALSE
\E x \in {1,2,3} : x > 2    TRUE

就是前面讲过的Definition。

id ≜ a + b
Op(a) ≜ b * a + c
F(x) ≜ ∃i∈S : x + 1 > i

1. 没有参数，算术表达式
2. 一个参数a，算术表达式
3. 逻辑表达式。

Write an operator that tests if two numbers are not equal.

写一个Operator测试两个值是否相等。

not_eq(a, b) == a /= b
not_eq_2(a, b) == ~ (a = b)

这里的"="就真的是数学的等号，不是赋值。

现在还没有behavior spec，只有mathematic definition。

用TLC测试：

Expression      Value
not_eq(1, 2)    TRUE
not_eq(2, 2)    FALSE

在定义Operator的时候，它接受的参数还可以是一个Operator，但一定要写上Operator接受几个参数。

Operator支持递归。SetReduce是对集合进行reduce操作。首先要用"RECURSIVE"声明一下。因为是对集合的元素进行操作，所以SetReduce()的第一个参数是一个Operator，第二个参数是集合，第三个参数是初始值/累积值。如果集合已经是空集合了，就是value。如果集合不为空，...。

先介绍一下LET...IN操作。Sum和Do这种Operator有点类似于全局性的、Global的Operator，但有些Operator只是针对一些局部的运算，避免写重复代码，这时就会引入LET...IN，用LET定义在IN后面的Fomula中要用到的一些局部的操作符。图中的LET...IN的意思是，从集合S中选出一个元素s，谓词逻辑是TRUE，就是从集合中选出一个，CHOOSE是一个确定性的操作，就是说只要是同样的集合，返回的都是同一个元素。S \ {s}是利用集合相减从集合S中去除元素s，Op(s, value)是在累积值value上做Op操作。

需要注意的是，LET...IN的LET中是定义局部操作符，所以是两个等号"=="。

这里的"="就是真的等号，含义是相等，不是赋值。

Operator的名字无所谓大小写，但大小写不一样。

OTHER是缺省分支。中括号一定要加，是否对齐没关系。

前面High-order Operators已经讲过了，LET-IN定义局部Operator，可以定义多个，还可以嵌套。

IsCommutative(f(_,_), a, b) == f(a, b) = f(b, a)

IsCommutative是High-order Operator，注意占位符。

用TLC测试时，注意用可以交换的测试一下，再用不能交换的测试一下。

Operator一定要定义在Module中，不能定义在Constants Expression中，但运行时可以在Constants Expression中调用Operator。

• Tuple可以认为是一个顺序的列表，只不过长度是固定的，元素允许重复。前面讲的Set是没有顺序的、且元素不能重复。
• 访问元素下标从1开始，不是从0开始。
• 支持DOMAIN(定义域)操作符，返回Tuple的下标集合，即1..Tuple Length的Set。
• Tuple可以认为是语法糖，它其实是函数，Tuple的定义域是1..Tuple Length的Set，值域是Tuple中的值。DOMAIN是一个Operator，接受一个f，返回这个函数的定义域。
• 函数应用到定义域的某个值上，也是f[x]这种写法，注意是中括号。

<<"hello", "world", "!">>

f[1] = "hello"
f[2] = "world"
f[3] = "!"

• Tuple，例如<<"hello", "world", "!">>，在TLA中就是一个函数(Function)f，Function是从定义域Domain到值域Range的映射。这个函数给1返回"hello"、给2返回"world"、给3返回"!"。
• DOMAIN也是一个Operator，这个Operator接受一个函数，它会把函数的定义域作为一个集合返回回来。对函数的调用是"函数名[参数]"，返回一个到值域的映射。

EXTENDS Sequences以后，就可以引入表格中的Operator。

Reverse(Twople) == IF Len(Twople) = 2
                       THEN <<Twople[2], Twople[1]>>
                       ELSE Assert(FALSE, "invalid tuple")

使用Assert需要引入TLC，如果是raise一个error，Assert第一个参数一定是FALSE。在调试Spec的时候特别有用。

由Tuples组成的Sets。

• chessboard_squares定义了一个国际象棋的棋盘。
• "\X"是集合的笛卡尔积。
• "1..8"要加上圆括号，即"(1..8)"。
• 笛卡尔积的括号可能会导致不同的结果。

关于集合的笛卡尔积，百度百科定义如下：

笛卡尔乘积是指在数学中，两个集合X和Y的笛卡尔积(Cartesian product)，又称直积，表示为X×Y，第一个对象是X的成员而第二个对象是Y的所有可能有序对的其中一个成员。

假设集合A={a, b}，集合B={0, 1, 2}，则两个集合的笛卡尔积为{(a, 0), (a, 1), (a, 2), (b, 0), (b, 1), (b, 2)}。

笛卡尔积的符号化为：
A×B={(x,y)|x∈A∧y∈B}

例如，A={a,b}, B={0,1,2}，则
A×B={(a, 0), (a, 1), (a, 2), (b, 0), (b, 1), (b, 2)}
B×A={(0, a), (0, b), (1, a), (1, b), (2, a), (2, b)}

• Structures和Records也是TLA中的Function。
• 注意"|->"符号。
• 可以用".属性名"访问属性，也可以用函数式的访问，即"[定义域的值]"，返回值域的值。
• 因为它们是函数，所以也可以用DOMAIN返回定义域。
• 注意应该没有";"，纯的TLA不要";"，PlusCal有";"。

如果在TLA中写，"="要换成"=="，如果直接在CONSTANTS Expression中写，要写成[a |-> 1, b |-> {2, 3}].a。

x = [a : {1}, b : {2, 3}]
x = { [a |-> 1, b |-> 2], [a |-> 1, b |-> 3]}

• 第一个式子中，是":"，":"右边必须是Set。
• 第一个式子返回的是第二个式子，首先最外层是{}，说明返回的是一个Set，Set中每一个都是前面提到的Function(中括号都是Function)，也是Record。
• 所以，第一个式子返回的是从定义域到值域的所有可能的函数的组成的集合。

• ":"后面是谓词。
• "S \X S"是两个集合的笛卡尔积。

• ":"前面是表达式。
• 第三个表达式，x是0..9，y是0..9，map以后是0..90。x和y之间打了","以后，产生类似于笛卡尔积的组合，只不过因为是Set操作，中间的重复元素会去掉，例如第二个表达式。

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

• 用DOMAIN在Tuple上运用一下，得到Tuple的定义域。
• 然后，在定义域的每个元素上都应用一下函数，就得到了对应的值域的值。

IsDoubleSubset(S1, S2) == {s1 * 2 : s1 \in S1} \subseteq S2

InSeqSets(elem, Seq) == x \in UNION Range(Seq)

• 注意引入FiniteSets。
• Cardinality用来计算有限集合的基，即元素个数。

Op(S) == { subset \in SUBSET S : Cardinality(subset) = 2 }

谓词逻辑，Predicate Logic。

HasEvenNumber(S) == \E x \in S : IsEven(x)

• "\E"是"存在"。
• 集合中是否有偶数存在。
• 用编程语言来写的话，肯定有个for循环，遍历看是否是偶数。

Add(a, b) == a + b

RECURSIVE SetReduce(_, _, _)

SetReduce(Op(_, _), S, value) == IF S = {} THEN value
                                 ELSE
                                    LET s == CHOOSE s \in S : TRUE
                                    IN SetReduce(Op, S \ {s}, Op(s, value))

Sum(S) == SetReduce(Add, S, 0)

NSubsets(S, N) == {subset \in SUBSET S : Cardinality(subset) = N}

SumsToZero(S, N) == \E s \in SUBSET S:
                         /\ Cardinality(s) = N
                         /\ Sum(s) = 0

• Cardinality前面的"/"起到括号和对齐的作用。

OnlyEvenNumber(S) == \A x \in S : IsEven(x)

\A x \in {} : FALSE = TRUE

• 第一个式子：判断集合中是否只有偶数。
• 第二个式子：因为集合是空集，也不会违反，所以都满足。

IsCommutative(Op(,), S) == \A x \in S :
                           \A y \in S : Op(x, y) = Op(y, x)

• 第一个式子：求集合中最大的元素。
• 第二个式子：求素数，除了1和它自己、没有其他的因子。
• 第三个式子：求集合中最大的素数。这里有一个蕴含(imply)。如果y是素数的话，那么y一定小于等于x；如果不是，则无所谓。换句话说，这个集合中可能有素数、可能没有素数，但如果有，肯定小于等于x。

体会一下写TLA和写程序有什么区别。

• 注意对齐的/\和/，依然起到括号和对齐的作用。

这里的训练会用在写Next，因为写Next就是在写Logic Formula。

• 全是逻辑公式，TLA用数学表达，所以表达力非常强，可以考虑一下如果编程怎么写。
• 如果把"=>"改为"/"一样吗？如果是"=>"的话，"\A"到"=>"中间这一段有可能是FALSE，但整个还是TRUE；如果是"/"的话，整个就是FALSE了。
• 用自然语言描述、用数学语言描述、用逻辑形式化描述有很大差别。如果形式化表达出你的想法，肯定是最清楚的、没有歧义的，而且强迫你做深入思考，否则你写不出来或者写出来是错的。
• TLA+的形式化数学部分的内容跟其他的形式化数学相比是非常少的，而且选了最好理解的、经典的逻辑，加上集合论一些非常初步的知识，但非常强大，足够描述计算机系统里所有的逻辑问题，Next的部分。
• 这种思考是需要大量训练的，平时这样思考得不多。在平时工作中，强迫自己多做这种训练，当你习惯这种思维之后，你就会发现，思考的清晰度和深度跟原来完全不一样。

LargestPrime和LargestPrime2的语义不一样。因为我们的本意是，y如果不是素数无所谓、没影响；只有y是素数的时候，才看是不是比x大，如果大就是FALSE，x就不是我希望的x。但在LargestPrime2中，任给y都是素数，这个条件更强，强了之后就会导致问题，因为我们不需要这么强。如果x是素数，y不是素数的话，整个就是FALSE。如果S是{3, 5, 7}，LargestPrime和LargestPrime2的结果是一样的。但如果S是{3, 4, 7}，LargestPrime是TRUE，LargestPrime2是FALSE。分析这种问题的方法是，找个小一点的S，列出来，看看结果。

从这个例子可以看到，=>和and非常微妙，有时候是对的，有时候不对，正确性是错误的。如果用自然语言表达的话，可能会造成误导。

• 在TLA+中，所有复杂的数据结构都是函数表达的。
• 函数在TLA+中有两种表示法：
  • 第一个式子："=="左边是函数名称、标识符，右边的含义是，S是函数的定义域，foo是一个表达式。例如，Doubles是一个函数，它的定义域是自然数，把所有自然数都乘以2，用数学表达可以写成"f(x) = x * 2, x属于自然数"。这里的函数完全是数学意义上的函数，不是编程语言里的函数，编程语言里的函数不可能定义出所有自然数的函数。Sum也是一样，函数有2个参数，x和y都是集合S的元素，表达式是"x + y"。调用就是"Doubles[2]"。
  • 第二个式子：这样写可能更舒服一点。一般情况下两种写法是一样的，但在定义递归的时候得用第二种写法。
  • 可以把TLA+里的函数理解成为编程语言里的HashMap，Key就是Domain，Value是Range。

因为要返回每个token对应的出现的次数，所以要定义一个函数(Map)。怎么知道Tuple中有哪些字符呢？Tuple本身也是Function，所以其实是想看到它的值域。这个值域就是要返回的Function的定义域。现在要求每个token出现的次数。提示一下，token出现的次数就是它在tuple中出现的位置的个数。

<<a, b, c, c>>
Domain Range
  a      1
  b      1
  c      2

Counter(str) == [c \in Range(str) |-> Cardinality({n \in 1..Len(str) : str[n] = c})]

编程是为了让程序在计算机上跑得更快，现在是为了把概念表达得更全、简洁，即概念本身的定义。这是完全不同的。

函数的定义域是Tuple的值域。什么叫字符在Tuple中出现的次数？数它有几个位置。怎么把这个位置表示出来呢？Tuple也是一个函数，位置是这个函数的定义域{1, 2, 3, 4}，值域是{a, b, c, c}。n \in 1..Len(str)也可以用DOMAIN写。判断这个函数(str、Tuple)在它的定义域的位置的值是c的，这些位置是一个集合，集合的Cardinality就是字符在Tuple中出现的次数。

这部分有点烧脑，但可以看到用数学表达的强大。正因为有了Function Set，很多问题觉得要用递归做的，完全不用递归，可以轻易地描述出来。

第一个式子：SetOfFunctions是一个Set，Set里的每个元素都是Function。A是一个集合，B也是一个集合。如果一个函数的定义域是A，它的值域是B的非空子集，那么这个函数就在"[A -> B]"中。

看一下例子，如果S为{1, 2}：

• [s \in S |-> S]是一个函数，这个函数的定义域是S，定义域的字面量是1或2，函数的值域只有1个，即{1, 2}，S是一个常量表达式。所以这个函数等于[1 |-> {1, 2}, 2 |-> {1, 2}]。
• [S -> S]是一个Set，Set的每个元素都是一个函数，定义域都是S，即{1, 2}，值域是S的非空子集，S的子集为{1}、{2}和{1, 2}。

[A -> B]，假设A集合的元素个数是N，B集合的元素个数是M，[A -> B]的元素个数是N个M相乘，即M^N个，顺序无关的全排列。

[A -> B]
 N    M

 x1 -> y1|y2|...|ym
 .
 .
 xn -> y1|y2|...|ym

"|"表示选择、可能性

如果N=2、M=1，Function Set只有1个函数，不是N个函数，所有的定义域的元素都映射到这一个值上。 {[x1 -> y1, x2 -> y1]}

如果N=2、M=3，Function Set如下：

{
  [x1 -> y1, x2 -> y1]
  [x1 -> y1, x2 -> y2]
  [x1 -> y1, x2 -> y3]

  [x1 -> y2, x2 -> y1]
  [x1 -> y2, x2 -> y2]
  [x1 -> y2, x2 -> y3]

  [x1 -> y3, x2 -> y1]
  [x1 -> y3, x2 -> y2]
  [x1 -> y3, x2 -> y3]
}

Cm1 * Cm1 * ... * Cm1 ------- 共n个 -------

这里谈论的函数只是一种关系，是从定义域到值域的映射，只管输入、输出。就像排序，不管是插入排序还是快速排序。只要输入、输出一样。

C语言的union是加，struct是乘。

• 三个集合：People、Animals和Preferences。
• 两个Set可以有一个Function Set来表明它们之间的关系，这个关系本身是一个Set，就可以和另外一个Set再建立关系，也就是Function Set。可以先这么直观地想。
• 第一个式子，Animals先跟Preferences建立Function Set，People再和这个Function Set建立关系。也可以People先和Animals建立关系，这个Function Set再和Animals建立关系。Pref是一个函数，给它一个定义域的值返回一个值域的值，用"[]"，例如"Pref[p]"，而"Pref[p]"还是一个Function，可以继续用"[]"，例如"Pref[p][a]"。注意第二句话前面，要CHOOSE一把。
• 第二个式子，People和Animals除了用Function Set可以建立关系以外，还可以用笛卡尔积，返回的也是一个Set，Set的每个元素都是Tuple，Tuple长度为2，跟参与笛卡尔积的集合个数是一样的。再跟Preferences集合建立一个Function Set。这是Pref定义域的值是Tuple，即"Pref[<<p, a>>]"。注意第二句话前面，要CHOOSE一把。
• 这两种写法Function Set中的函数个数，从最外层来看是一样的。

• 有序的定义是：任取两个位置i和j，i<=j，i位置的值小于等于j位置的值。

假设n=3，全排列的个数是3!=6，如下：

{1, 2, 3}, {1, 3, 2}, {2, 1, 3}, {2, 3, 1}, {3, 1, 2}, {3, 2, 1}

1. [1..n -> 1..n]这是一个Function Set，就是前面讲过的全排列。
2. 假设n=3，[1..3 -> 1..3]共有3^3=27个Function，如下面的第1列。
3. [1 -> 1, 2 -> 1, 3 -> 1]是一个Function，Tuple也是Function，写成Tuple的话就是<<1, 1, 1>>。同理，[1 -> 1, 2 -> 2, 3 -> 3]是一个Function，写成Tuple的话就是<<1, 2, 3>>。同理，[1 -> 1, 2 -> 3, 3 -> 3]是一个Function，写成Tuple的话就是<<1, 3, 3>>。如下面的第2列。
4. Range()的定义是Range(T) == {T[i] : i \in DOMAIN T}。如下面的第3列。

Range(<<1, 1, 1>>) = {1}
Range(<<1, 2, 3>>) = {1, 2, 3}
Range(<<1, 3, 3>>) = {1, 3}

5. 再根据过滤条件Range(key) = 1..3，即Range(key) = {1, 2, 3}，过滤掉长度不为3的Range，就可以得到最终结果。如下面的第5列。

假设n=3，[1..3 -> 1..3]共有3^3=27个Function，Function Set如下：

{     Function Set            Tuple(key)    Range(key)    Range(key) = {1, 2, 3}      Filtered Function           Tuple
  [1 -> 1, 2 -> 1, 3 -> 1]    <<1, 1, 1>>       {1}
  [1 -> 1, 2 -> 1, 3 -> 2]    <<1, 1, 2>>      {1, 2}
  [1 -> 1, 2 -> 1, 3 -> 3]    <<1, 1, 3>>      {1, 3}

  [1 -> 1, 2 -> 2, 3 -> 1]    <<1, 2, 1>>      {1, 2}
  [1 -> 1, 2 -> 2, 3 -> 2]    <<1, 2, 2>>      {1, 2}
  [1 -> 1, 2 -> 2, 3 -> 3]    <<1, 2, 3>>     {1, 2, 3}         {1, 2, 3}           [1 -> 1, 2 -> 2, 3 -> 3]    <<1, 2, 3>>

  [1 -> 1, 2 -> 3, 3 -> 1]    <<1, 3, 1>>      {1, 3}
  [1 -> 1, 2 -> 3, 3 -> 2]    <<1, 3, 2>>     {1, 3, 2}         {1, 3, 2}           [1 -> 1, 2 -> 3, 3 -> 2]    <<1, 3, 2>>
  [1 -> 1, 2 -> 3, 3 -> 3]    <<1, 3, 3>>      {1, 3}


  [1 -> 2, 2 -> 1, 3 -> 1]    <<2, 1, 1>>      {2, 1}
  [1 -> 2, 2 -> 1, 3 -> 2]    <<2, 1, 2>>      {2, 1}
  [1 -> 2, 2 -> 1, 3 -> 3]    <<2, 1, 3>>     {2, 1, 3}         {2, 1, 3}           [1 -> 2, 2 -> 1, 3 -> 3]    <<2, 1, 3>>

  [1 -> 2, 2 -> 2, 3 -> 1]    <<2, 2, 1>>      {2, 1}
  [1 -> 2, 2 -> 2, 3 -> 2]    <<2, 2, 2>>       {2}
  [1 -> 2, 2 -> 2, 3 -> 3]    <<2, 2, 3>>      {2, 3}

  [1 -> 2, 2 -> 3, 3 -> 1]    <<2, 3, 1>>     {2, 3, 1}         {2, 3, 1}           [1 -> 2, 2 -> 3, 3 -> 1]    <<2, 3, 1>>
  [1 -> 2, 2 -> 3, 3 -> 2]    <<2, 3, 2>>      {2, 3}
  [1 -> 2, 2 -> 3, 3 -> 3]    <<2, 3, 3>>      {2, 3}


  [1 -> 3, 2 -> 1, 3 -> 1]    <<3, 1, 1>>      {3, 1}
  [1 -> 3, 2 -> 1, 3 -> 2]    <<3, 1, 2>>     {3, 1, 2}         {3, 1, 2}           [1 -> 3, 2 -> 1, 3 -> 2]    <<3, 1, 2>>
  [1 -> 3, 2 -> 1, 3 -> 3]    <<3, 1, 3>>      {3, 1}

  [1 -> 3, 2 -> 2, 3 -> 1]    <<3, 2, 1>>     {3, 2, 1}         {3, 2, 1}           [1 -> 3, 2 -> 2, 3 -> 1]    <<3, 2, 1>>
  [1 -> 3, 2 -> 2, 3 -> 2]    <<3, 2, 2>>      {3, 2}
  [1 -> 3, 2 -> 2, 3 -> 3]    <<3, 2, 3>>      {3, 2}

  [1 -> 3, 2 -> 3, 3 -> 1]    <<3, 3, 1>>      {3, 1}
  [1 -> 3, 2 -> 3, 3 -> 2]    <<3, 3, 2>>      {3, 2}
  [1 -> 3, 2 -> 3, 3 -> 3]    <<3, 3, 3>>       {3}
}

Lamport在德国海森堡面对国际上有突出贡献的计算机科学家的演讲，他讲的是TLA+。他出了一个题目"the set of all permutations from 1 to N"。他已经解释了[1..N -> 1..N]，也讲了f[x]是函数的应用，然后就问图中的式子是什么意思。这个式子的意思也是f的值域没有缩小。因为任给y属于1..N，f都能映射过来，是一个满射，值域不会缩小。有单射、满射、双射，其实这里是一个双射，定义域和值域双向全充满。

大概有一半人举手，然后请数学家把手放下，然后就没人了。他就感慨，与会的人都是选出来的出名的研究学者，这就解释了TLA+为何没有被更广泛地采用，且为何应该被采用。很简单的数学公式不理解，宁愿写复杂的递归来表达概念，其实完全不需要，数学训练太少了。

数学上同一个概念有很多种表达方法，这个表达方法相对于前面的表达方法更加数学化。

给一个序列，返回这个序列所有的全排列。

例如，给一个<<2, 3, 4>>，返回：

<<2, 3, 4>>, <<2, 4, 3>>, <<3, 2, 4>>, <<3, 4, 2>>, <<4, 2, 3>>, <<4, 3, 2>>

PermutationKey(Len(T))是所有的排列，P是其中的一种排列方式，"P[x]"就是在这种排列方式上的位置，"T[P[x]]"是从这个位置上取出的T的东西。P给了我们排列，我们所要做的是把排列中的位置跟T中间的元素映射上得到我们要的序列。

第一次映射位置，第二次把位置作为参数传给函数。

这样做完的用处是什么？写一个排序算法，如何验证这个排序算法是对的呢？既然是排序肯定是有顺序的，还要保证排完序后里面的元素不能被修改，{1, 2, 3}排序后变成{1, 1, 1}，肯定排过序了，但元素不对了。所以，排完序的结果一定是元素全排列的一个元素。这样就可以做证明和验证，虽然性能比较低，但目标是解决正确性，所以没关系。

就是把前面写的Operator组合起来。

PermutationsOf是全排列、IsSorted保证有序。

经过系统训练，通过数学表达式，我们可以很简洁地表达对于某个概念的正确性的论断。

到目前为止，基本已经把TLA+的Plus部分讲完了，即如何在一个行为序列里的某个状态下定义里面的静态数据以及如何操作。用处在于我去解决实际问题的时候，如何用这样一些静态的元素去对我的业务进行建模。业务里可能有队列，如何表达？操作系统层面的一个等待线程队列，如何建模？这都是实际问题，就可以用这些东西做了。

函数的三种定义：

• Injection：单射。
• Surjection：满射，把值域充满。
• Bijection：双射，定义域充满、值域也充满，而且不允许相等存在。双射可以理解为一一映射，但是比一一映射强一点。

TLA+可以把微积分全部形式化，可以做很多形式化的证明、推导。

如何写长公式。

本来老师是想展示论文：《如何编写二十一世纪证明》，Calculus

一个函数f，S1到S2状态变化，f也可能会有变化，什么叫f的变化？举个例子，一个哈希表，我可能只改一个Key，如何做呢？

Function是从一个定义域映射到一个值域，当只想改变定义域中某一个或某几个值对应的值域的值、其他不变的时候，可以像上面那样做。

A是一个Function，对于A的定义域中的任意一个i，只有当i等于3的时候才对它进行修改、其他不变。

EXCEPT可以满足这样的语义。

• [A EXCEPT ![3] = 42]：除了3对应的值改为42，其他保持不变。
• [A EXCEPT ![3] = 42, ![6] = 24]：可以是某一个或某几个。
• [A EXCEPT ![i] = A[i] + 1]：对所有的定义域的值，对应值域的原值加1，其中的"A[i]"可以简写为"@"。
• EXCEPT的ASCII表示是"\EXCEPT"。

图中DivisorsOf(n)中的p \in Int改成p \in 1..n。

学了TLA+以后可以解决很多谜题。编程语言表达力再强也没有数学强，想法可以更加抽象了，用TLA+一描述答案就出来了。

一个农夫有一个40磅的石头和一个天平，如何将这个石头分成4块碎片，希望可以用这4块石头碎片以及天平去称任何1到40磅谷物的重量。

这个题目是美国一个汽车维修的节目，每次show会出一个数学谜题。这道谜题是2011年10月22日那期节目的谜题。Lamport决定上TLA+和TLC。他并不是追求一个答案，而是想看看答案中是否存在更深层次的认识。如果不知道答案、也想不清楚的情况下可能比较困难，如果知道答案了反而能有助于我思考里面蕴含了什么规律，答案对我有更多的启发。Lamport就用TLA+写了Spec来计算这个答案。他写了两个，第二个更简洁。一旦TLC告诉了答案，我们可以扩充一下，这个问题什么情况下有解、什么情况下无解。这才是真正理解这个问题。

分成4块以后，一共15种组合情况，最多能表达15个数字，还不包括可能存在的重复，15小于40，肯定是无法覆盖1..40这40种情况的，所以这4块不能只在天平的一边。所以把4块放在天平的一边，把谷物放在天平的另一边，求得天平的平衡，不行。那么4块就左右都放，4块都放在一边就是累加的加法，左右都放就是一个差值，当然不排除加法，因为可以在某一边一块石头都不放，就是说减法蕴含了加法。

重要的还是思维的训练，TLA+领域不像编程领域，我们希望尽量用数学的方式思考。

假设集合(4块石头)已经存在了，如何判断是否满足条件。我不知道怎么分，但想先知道对不对。可能放两边，可能放一边。放一边的话，给一个谷物重量放一边，从集合中选出一些元素放另外一边，加起来大小相等。放两边的话，要给两个集合、不是一个集合，这两个集合合起来是4块、而且不能重复，一个集合放这边、一个集合放那边，然后两边相等。

稍微一般化一下，任给一个w，从1到40，都能够要么在一边、要么在两边，都能找出来。但w不同，集合放的情况会不一样。任给一个w，需要给4块的集合进行一个合理的划分，所有子集。这就是数学思考。任给一个w从1到40，总可以从这个集合拿出两个子集，一个跟谷物放在一边，一个放在另外一边，两边相等，当然也包含空集的情况。这就是数学描述了。

再进一步，这个划分怎么来呢？已知会分成4块。对于集合P的所有子集，存在两个子集，一个放左边、一个放右边，两边相等。这是逻辑表达式(TRUE)。那么如何划分呢？其实就是过滤，过滤条件就是满足这个逻辑表达式。

上面是一个反向推导的过程。数学思维就是这样，从具体问题出发，然后一般化，一般化的过程保持严格性。

如何把40分成4块的划分情况全部列出来？这4块每一块都可以是1到40，定义域是1、2、3、4，值域是1到40，这就是前面描述的Function Set。这是一个特别大的集合。这4块有约束条件，要从这个Function Set中过滤出一些Function。这个约束条件是这4块加在一起应该等于40。但这4个的重量可以相同也可以不同。

所有过滤出来的4块的划分，再用逻辑表达式过滤。

• IsRepresentation：w是谷物重量，b是划分，s和t就是分别放在天平两边的石头块，s跟w放一起，t放另一边。w就是t减去s。Sum(b, s)是求s集合石头的重量，Sum(b, t)是求t集合石头的重量。而且s和t要没有交集。
• Break：P是分成多少块，每一块的重量都可能是1到40。Sum=N是约束条件。关于i、j的那一段是为了更有效地过滤，使得B集合能小一些，做了一个排序，比如{1, 2, 3, 4}可能是符合的，{4, 3, 2, 1}也是符合的，但这两个集合的意义是一样的，所以做了一个排序，希望划分出来的是一个升序排序后的。
• Sum是对划分好的石头重量做一个求和。
• IsSolution：判断划分是否是解。
• AllSolutions：从所有的划分中找出所有的解。

b是一个函数，定义域是1到4，值域是重量。s是个集合，集合是1到4的子集。Sum(b, s)就是s拿出来作为函数(b)定义域的选项，然后值域加起来的重量。可以把b当成一个哈希表，key是1、2、3、4(重量)，s是key的子集。

TLC里可以装插件，用ASCII写出来的代码打印出来，非常漂亮，pretty print。

三进制的<<1, 1, 1, 1>>，即<<3^0, 3^1, 3^2, 3^3>>。

进一步思考，对于N和P取什么值才有解呢？解是什么呢？简单点，P固定为4，N取什么值才能有解呢？

仅仅只用加，可以用4个二进制表示1到15连续的数。4个三进制都是1的话，正好就是40，但仅仅只用加就不行了。天平左右两边都放，蕴含了减法才能表示，就要用三进制。1表示1、3表示3、2可以用3-1表示，...。如果超过40，3进制可能也没办法表示了。

Function很简单，但不代表容易理解，简单和容易不是一回事，需要抽象，需要训练。

下面进入到动态部分，把State Machine的部分形式化出来。