Index

Symbols

# (not equals) ' (next value) .. (set interval) /\ (and) :> (map function) <- <> (eventually) <>[] = == => (implies), [1], [2] >>> @ @@ (merge) [] (always) [A -> B] [P]_x

\ (set difference) \/ (or) \A (forall) \E (exists) \in variable definition x \in set, [1] \intersect \notin \o (concat) \subseteq \union \X `!` (Namespace lookup) || ~ (not) ~>

A

Action action, [1], [2] action property always see []

Append assert ASSUME auxiliary variable await

B

Behavior

BOOLEAN box action formula

C

call see also procedure CASE

CHOOSE CONSTANT constants

D

Deadlocks define

diameter DOMAIN duplicates, [1], [2]

E

either ENABLED Enabled eventually see <>

EXCEPT see also function EXTENDS

F

Fairness fairness in PlusCal in TLA+

Formal Methods Formal Specification Language Function function function sets

G

goto

H

Head

I

IF if (pluscal) INSTANCE Parameterized Modules WITH

Invariant, [1] Model Invariants

L

Labels LAMBDA leads-to see ~> Len

LET Liveness liveness LOCAL see also INSTANCE

M

macro Model unbound models

Model checking model value model value sets symmetry sets

O

Operator operator Operators Binary Operators Higher-order operators Recursive Operators

P

pc PlusCal pluscal, [1] Predicate procedure

process local variables process sets Property property action property

Q

quantifier \A \E

R

RECURSIVE

return, [1] see also procedure

S

Safety safety self sequence sequence sets set set operators set sets sets of booleans functions model values numbers sequences sets

SF_vars skip Spec Specification State space Step Stutter Step stuttering SubSeq SUBSET

T

Tail Temporal Property Theorem Prover TLA+ TLA+ Toolbox

TLC tuple see sequence types function sequence

U

unbound models

UNCHANGED, [1]

W

WF_vars while

WITH with nondeterministic