TLA+ 相关笔记。
TLA+ 相关资源
 The TLA+ Home Page by Leslie Lamport
 TLA+ Reading and Resource List
 TLA+ IDE
 TLA+ Toolbox User’s Guide
Operators of standard modules (P272)
Typeset symbols of TLA+ (P273)
Operator  meaning 

\* 
line comment 
(* 
block comment 
= 
is assignment in the variables block, 
is the equality check in everywhere else  
:= 
assignment 
/= or # 
not equal 
/\ 
and 
\/ 
or 
~ 
not 
== 
define an operator 
<<...>> 
Specify tuples and they are 1indexed 
\o 
Combine two sequences 
\X 
Cartesian product operator: set1 \X set2 is the set of 
all tuples t where t[1] \in set1 and t[2] \in set2 . 

{...} 
set 
\in 
in set 
\notin 
not in set 
\subseteq 
is subset 
\union 
set union 
\intersect 
set intersection 
S1 \ S2 
the elements in S1 not in S2 
\E 
exists 
~\E 
not exists 
\A 
all 
~\A 
not all 
P => Q 
If P is true, then Q must also be true 
It’s equivalent to writing ~P \/ Q 

P <=> Q 
Either both P and Q are true or both are false 
It’s equivalent to writing (~P /\ ~Q) \/ (P /\ Q) 

> , > 
map. use > when you want one function that maps 
the domain to a specific range. Use > when you want 

the set of functions that maps the domain to the range.  
 
lets multiple assignments all use the old values 
[] 
an invariant. []P means that P is true for all states 
<> 
eventually. <>P means that for every possible behavior, 
at least one state has P as true  
~> 
leads to. P ~> Q implies that if P ever becomes true, 
at some point afterwards Q must be true.  
<>[] 
stays. <>[]P says that at some point P becomes true 
and then stays true. 