plusCal语言语法
plusCal语言
[TOC]
3 The Language（plusCal语言）
statement sequence
statement sequence is a sequence of statements，以分号结束。 如while的body就是一个，但body中的if的then从句是另一个statement sequence，if语句才属于body。
control path
A control path is a path through a piece of PlusCal code that represents a syntactically possible execution sequence, if we ignore how the statements are executed.
可以包括多个label。
如下面的a - c就是一个control path
a: if (FALSE) { goto w ;
b: x := 7 ;
c: y := 8 } ;
d: x := 0 ;
step
A step is a control path that starts at a label, ends at a label, and passes through no other labels. 两个相邻label之间的control path才叫step Part of a step can never be executed by itself（print or assert statement除外）。 也就是说，要么全部执行，要么全部不执行，不能执行一个step的一部分。
注释
* 针对一行 (* *) 针对多行
3.1 Expressions
The expressions in PlusCal algorithms can be any TLA+ expressions that do not contain a PlusCal reserved word or symbol such as begin or “||” . pluscal的expression可以是任何不含pluscal关键字或begin，||的TLA+语言表达式。
可以在pluscal中写TLA+ definition，然后在expression中用这些 定义的symbol。
identifier 不能在已经有一个意义的情况下 新附另一个
语句
3.2 The Statements
algorithm, process, procedure, or macro 的body中的statement可以是pluscal定义的原始statement，或compound statement。
compound statement： 由分号分隔多个statement组成，末尾可选是否带分号，封装在{}中。
原始statement：
变量声明（含全局 或 局部）
variables u = 24; v ∈ 1.. N; \∗ ∈ is typed \in . The declaration of v asserts that its initial value is an element of the set 1 .. N of integers from 1 through N.
变量声明： 可用分号或逗号分隔。最后面可以不要分号
特殊变量
self ： 在process上下文中是process自己的id
3.2.1 Assignment
声明变量时，用 = 赋值 其他地方用 := 赋值
assignment statement由一个或多个assignment，被||分隔，结尾有分号。 multiple assignment： 含多个assignment的assignment statement。 该语句先执行所有=右边部分，然后才从左到右执行赋值（如swap） 一个label和next label之间不能存在两个独立statement来对同一个变量赋值（array不同index也不行）。 但可以在一个multiple assignment statement中赋值两次
3.2.2 If
if ( test-exp ) t-clause else e-clause if的clause里面如果有call ，return，goto，或label，则if后面必须跟一个label
3.2.3 Either （引入不确定性）
用于非确定的选择任何一个分支执行。 clause里面如果有call ，return，goto，或label，则either后面必须跟一个label。 TLC将会执行all分支，但对特定的一次来说，执行的分支是不确定的。 either clause1-statement 《–这个clause1可以省略 or clause2-statement . or clausen-statement
3.2.4 While
lb : while ( test-exp ) body-statement 等于 lb : if ( test ) { body ; goto lb } while自己必须label，但while后面的语句不需要label，即使body中有label也不需要
3.2.5 Await (When)
await exp 仅在exp为TRUE时才执行await。 即等到exp为TRUE才继续执行，否则什么都不变。 下面两个是相等的。因为一个step是atomic执行的。 x := y + 1 不会得到执行 a : x := y + 1 ; await x > 0 ;
b : …
a : await y + 1 > 0 ; x := y + 1 ; b : …
但print和assert不受await限制，都可以得到执行。
3.2.6 With（引入不确定性）
with ( id ∈ S ) body 等于 await S /= {} ; with ( id ∈ S ) body。 设置id为S中任意一个值，然后执行body S为空时不执行body。
with ( id = expr ) body 相等于 with ( id ∈ {expr} )body 《–后者是个set，与with ( id ∈ S ) body相等吗？？？ with ( id * expr1 ; … ; idn * exprn ) body 等于 with ( id1 * expr 1 ) … with ( idn * exprn ) body 《–*可以使=或\in
with的do从句不能包含label。
3.2.11 Goto
goto lab ;
下一跳语句必须要有label
skip
表示非关键noncritical的代码。该语句啥也不干。
3.3 Processes （concurrency）
process (ProcName ∈ IdSet ) process (ProcName = Id )
ProcName的value必须是唯一的，且可比较的（type一致）。 可以用self变量获取当前进程的value。
variable定义部分是可选的，是对每个process的local variable。如果variable用的是 \in someset，则TLC会遍历每个init value去检查process body部分用{}括起来，必须从一个label开始。
多进程算法中，可以有多个process，有不同的name，不同的body。 多个process的name的type应该相同（integer，或string，或set）。 进程绝不会terminate
3.4 Procedures （share code）
An algorithm may have one or more procedures.
procedure PName ( param1, . . . , paramn ) 定义一个编程语境的函数。与process语法类似，也要从label开始 call PName ( expr 1, . . . , exprn ) return 无参数
procedure要用的话，必须EXTEND Sequences。 必须定义在macro之后，在process之前
3.5 Macros（share code）
A macro is like a procedure, except that a call of a macro is expanded at translation time。
与procedure相似，但macro中不能有label，没有while, call, return, or goto。
使用procedure时不需要call语句
macro的定义放在define块之后，process之前。
尽量用macro，避免用procedure
macro和procedure里面还可以访问 process内的local var。
3.6 Definitions
write TLA+ definitions of operators that depend on the algorithm’s global variables.
--algorithm Test {
variables x ∈ 1..N ; y ;
define { zy ∆= y*(x+y) 《---此处无分号，或其他分隔符
zx(a) ∆= x*(y-a)
} 《--末尾也不用；
define语句也不用translate，只能应用variables中的变量
3.7 Labels
xxx：
They define the steps the algorithm takes.
里面的动作是同时发生的，是atomic的
everything in the label happens at once.
It’s only between labels that the model can check invariants and switch processes.
Also, you can’t assign to the same variable twice in the same label.
一些label规则：
- process中的代码 必须从一个label开始
- while语句必须label（在while前）
- with的do从句不能包含label
- 若if里面有label，则if后的语句必须有label（在if本身的label不算是if里面）
- 一个label和next label之间不能存在两个独立statement来对同一个变量赋值（array不同index也不行）。 但可以在一个multiple assignment statement中赋值两次
- label能放在 { 之前或之后。如果在之前，就表示{}内是一个step，是atomic的
- { 前后不能同时有label。 即“l1: { l2:
3.8 The Translation’s Definitions and Declarations
pc stack 多进程时
多进程情况下，为每个进程； ProcSet tuple vars of all variables The initial predicate Init. The next-state action Next and the complete specification Spec.
Optimization：
Every label specifies a branch point in your system: any process with an available label can run as the next step. For N processes with M sequential labels the total number of behaviors is (MN)!/M!^N, not counting initial states or nondeterministic labels (either or with). The more labels you have, the more exact your concurrency testing. The fewer labels you have, the faster your model will run. As always, there are tradeoffs.
5 TLA+ Expressions and Definitions(TLA+语法)
TLA+的关键字都是大写的，如TRUE，FALSE
5.1 Numbers
Naturals定义了下面运算符operators。 Integers是Naturals的超集
+ − ∗ ^ (exponentiation求幂) < > ≤ ≥ % ÷ . .
5.2 Strings
双引号括。
\ 为避义符
下面两个符号在Sequences中:
"ab"\o"c" equals "abc"
Len("abc") equals 3
5.3 Boolean Operators
∧ conjunction (and, typed “/\”)
∨ disjunction (or, typed “\/)”
¬ negation (not, typed “ ~ ”) 非
⇒ implication (typed “ => ”) 推导，隐含
≡ equivalence (typed “ <=> ”or “\equiv”) 等价
∀ x ∈ S : P(x ) 即\A ，是个表达式，如果S集合中的all元素x，都满足P(x)为TRUE，则表达式为TRUE。 如果S为{}, 结果为TRUE
∃ x ∈ S : P(x ) 即\E ，是个表达式，如果S集合中的some元素x，满足P(x)为TRUE，则表达式为TRUE。如果S为{}，结果为FALSE
∀ x ∈ S, y ∈ T : F means ∀ x ∈ S : (∀y ∈ T : F)
∃ x , y ∈ S : F means ∃ x ∈ S : (∃ y ∈ S : F)
5.4 Sets
里面的内容不重复 符号 { } { : }
运算符：
∈ (membership) 即\in e ∈ S Equals true if e is an element of the set S。返回的是bool。用在var declare中是赋值，其他都是bool
∪ (union) 并集
∩ (intersection) 交集 The set of elements in both S and T
⊆ (subset) 子集 True iff every element of S is an element of T.
\ (set difference) 差集 S \ T The set of elements in S that are not in T 只在S中有的
UNION (big U)
SUBSET (power set) 幂集。就是原集合中所有的子集（包括全集和空集）构成的集族。 SUBSET S The set of all subsets of S.
S中所有满足P(x)的元素组成的集合
{x ∈ S : P(x )} The subset of S consisting of all elements x satisfying 《---filtering。 是个filter后的subset
property P(x ). For example, the set of all odd natural
numbers can be written {n ∈ Nat : n % 2 = 1}.
{e(x ) : x ∈ S} The set of elements of the form e(x ), for all x in the 《-- Mapping。是对原有item加工后形成的new set
set S. For example, {2∗n + 1 : n ∈ 1 . . 100} is the set
{3, 5, 7, . . . , 201}.
a .. b 也是个set，is defined to equal {i \in Int : (a \leq i) /\ (i \leq b)}。 is syntatic sugar for “the set of all integers between a and b inclusive”
CHOOSE x ∈ S : P(x ) 不能用来描述不确定性的值，其虽然是随机选一次，但只会选一次。
is defined to equal some arbitrarily chosen value x in the set S such that P(x ) equals true.
例子：
money \in 1..20 ： money可取1,2,3，.... 20 之间任意值
alice_account \in {5, 10} ： money可取5或10.
{} empty set
Nat is the set of natural numbers
y \in {3, 4} y是3或4。 \in 即 ∈
z = {3, 4} z是{3,4}整个set，不是一个元素
5.5 Functions 类似编程语言的map 符号 [ |-> ]
程序员叫array，数学家叫function。 [x ∈ S |-> e] [Function f such that f [x ] = e for x ∈ S ] [S -> T ] [Set of functions f with f [x ] ∈ T for x ∈ S ]
下面的，数学家叫他a function with domain S。 但pluscal和tla+没有用数学的()，而用了程序员的[] [ v \in S |-> v + 1 ] 生成一个数组，索引是set S中的元素， 值是v+1 。 即 A[v] = v + 1
Functions are first-class values, so f [d] can be a function. [i ∈ Nat |→ [j ∈ 1 . . N |→ (2 ∗ i) % j]] 对该函数 f [3][x ] equals 6 % x
A function with multiple arguments is actually a function with a single argument that is a tuple. For example, g[3, x ] is shorthand for g[«3, x »].
[x ∈ S 7→ e] [Function f such that f [x ] = e for x ∈ S ] [S -> T ] [Set of functions f with f [x ] ∈ T for x ∈ S ]
5.6 Records 类似编程语言的struct
[foo |→ 17, bar |→ {1, 2, 3}] exp.foo = 17, exp.bar = {1, 2, 3}
record实际上是function In TLA+, a record with fields foo and bar is actually a function whose domain is the set {“foo”, “bar”}. The expression exp.bar is shorthand for exp[“bar”].
5.7 The Except Construct
用来描述function或record，一般不用，但大量用于pluscal语言translate到TLA+的过程中。
假设f为一个function： [ f EXCEPT ![c] = exp ] 等于生成了一个新function， 该新function除了 g[c] = exp以外，其他g[xx] = f[xx] 上面function也可以写为： [x ∈ DOMAIN f |→ IF x = c THEN exp ELSE f [x ]]
record类似，假设r为一个record [r EXCEPT !.c = exp] 也可以写为function形式 [r EXCEPT ![“c”] = exp]
多个感叹号
[f EXCEPT ![c] = exp1, ![d].e = exp2]
也可以写为：[ [f EXCEPT ![c] = exp1] EXCEPT ![d].e = exp2] ].
5.8 Tuples and Sequences 符号« »
有限sequence类似list。 在TLA+中实现为function «item1, item2, item3»
5.9 Miscellaneous Constructs
IF bool THEN t-expr ELSE e-expr
CASE p1 → e1 ✷ . . . ✷ pn → en 当pi等于TRUE是值为ei。 后面还可以带可选的OTHER e
let表达式： 像lamda。用于建一个 definitions local LET x == a + b y == a − b IN IF y > 0 THEN x + y ELSE x − y 等于 IF a − b > 0 THEN (a + b) + (a − b) ELSE (a + b) − (a − b)
5.10 Temporal Operators
A behavior is a nonempty sequence of states, where a state is an assignment of values to variables. A behavior of an algorithm is one that can be generated by executing the algorithm。 A temporal formula is a predicate on behaviors—in other words, it is true or false for any nonempty sequence of states. An algorithm satisfies a temporal formula F iff F is true of all behaviors of the algorithm. Temporal formulas cannot appear in a PlusCal algorithm. They are used only in the fairness properties assumed of the algorithm’s executions and in the properties asserted about the algorithm.
This section defines the TLA+ temporal operators that are used to express these fairness and liveness properties.
5.10.1 Fairness 未看懂（为了不处理stuttering情况）
An atomic operation of an algorithm consists of all control paths that start at some label l, end at a label, and do not pass through any label. 相邻label间的all control path In TLA+, an action is a formula describing how the state changes. More precisely, it is a formula that is true or false of a pair of states.
Weak Fairness： WF_vars(A) vars是algorithm的所有variable Strong Fairness： SF_vars(A)
fairness: the property that if a given label is always enabled, we will eventually run it.
5.10.2 Liveness
But safety only tells us that bad things won’t happen. 只保证了没有bad，但怎么保证有好的。 Sometimes, we want to ask a whether good things do happen. Will the trade eventually happen? Does every thread at some point get priority? Does our algorithm finish?
We call these properties Liveness. To specify these temporal properties, we use a few new operators.
一些运算符operator：
从头TRUE到尾
[] 在all state都满足P。可以在TLC的invariant检查中设置来起到该效果。 这个放在invariant中检查。 []P means that P is true for all states. In other words, an invariant. When you put P in the invariant box, TLC interprets that as the temporal property []P. The only difference is that TLC is hyper-optimized to handle invariants, so the entire invariants box is basically a convenience thing. So while [] implicitly powers all of our invariants, we almost never need to write it explicitly.
总会有TRUE的。
<> 最终，在每个behavior中，只有有一个state是P为true。 这个放在property中检查。
<> means eventually: <>P means that for every possible behavior, at least one state has P as true.
For example, the following code is wrong under the temporal property <>(x = 1)
你TRUE我就TRUE
~> means leads to: P ~> Q implies that if P ever becomes true, at some point afterwards Q must be true.
要TRUE就TRUE到底
<>[] means stays as: <>[]P says that at some point P becomes true and then stays true. If your program terminates, the final state has to have P as true. Note that P can switch between true and false, as long as it eventually becomes permanently true.
无穷多点都为TRUE
[]<>p mean P is true infinitely often
######
[A]_e定义为，系统要么执行A行为（通常A = Next，执行下一步）、要么保持目前状态/属性不变（e’ = e，e通常为系统中的所有变量）。
_e定义为，系统执行A行为（通常A = Next）、并且状态/属性发生变化（e’ /= e）。stutter字面意思是“口吃”，表示重复、状态不变。
[][Next]_v表示“系统总是执行下一步或者保持状态/属性不变”，这正是系统设计者期望的结果，因此是safety（安全）的，意味着坏事不会发生。
[]<>
5.11 TLA+ Definitions
两种operator definition的方式： F ∆= expr F(p1, . . . , pn) ∆= expr 《–pi就是参数