V10/vol2/spin/spin.ind

assertion violation, spin,  439-441, 446-449
Assertions, spin,  436, 446, 449
asynchronous communication, spin,  433, 445
C preprocessor, spin,  445
C program, spin,  429, 434, 438
communication protocol, spin,  429, 445	g
concurrent processes, spin,  429	g
deadlock, spin,  436-437, 439, 446	g
Executability, spin,  429, 432, 443, 445
exhaustive validation, spin,  429, 438
grep, spin,  439-441	G
guarded command language, spin,  445	g
Message Passing, spin,  432, 445
Message Type Definitions, spin,  437
modeling language, spin,  429, 436, 445	g
Modeling Procedures and Recursion, spin,  436
Process Instantiation, spin,  430, 432, 443
Processes, spin,  443
PROMELA Reference Manual, spin,  442
propositional temporal logic, spin,  449
random simulation, spin,  429, 438-439
Rendez-Vous Communication, spin,  433-435
Spin \(em A Protocol Analyzer, spin,  429	g
spin, !,  432	S
spin, -a,  437-438, 440, 446-449	S
spin, -c,  441, 449	S
spin, -g,  438	S
spin, -l,  437-438, 441	S
spin, -m,  438, 441	S
spin, -n,  438-439	S
spin, -p,  438	S
spin, -q,  438, 444	S
spin, -r,  438	S
spin, -s,  438	S
spin, -t,  439-440, 447	S
spin, -w,  441-442	S
spin, ?,  432	S
spin, Analyzer,  437-442, 445
spin, Array Variables,  430
spin, assert,  436-437, 439, 444	S
spin, assertion violation,  439-441, 446-449
spin, Assertions,  436, 446, 449
spin, asynchronous communication,  433, 445
spin, Atomic Sequence,  431-434, 444
spin, Bit State Space,  429, 438, 440-442
spin, Bit State Space Analysis,  441
spin, block,  437, 444	S
spin, break,  434, 436-437, 444	S
spin, buffer size,  433
spin, Building A Validation Suite,  446
spin, C preprocessor,  445
spin, C program,  429, 434, 438
spin, Case Selection,  434, 444
spin, chan,  430, 432-439, 442-445, 448	S
spin, channel,  429-436, 438-441, 443-445, 449
spin, channel names,  432
spin, Comments,  442
spin, composite condition,  433
spin, Constants,  442
spin, Control Flow,  434, 440-441
spin, curly braces,  430, 432, 443
spin, Data Types,  430-431, 443, 445
spin, deadlocks,  429, 436-437, 441
spin, Declarations,  430-431, 442-443, 445
spin, Digging Deeper,  439, 449
spin, do,  435, 444	S
spin, End-State Labels,  436
spin, error sequence,  439-440
spin, error trail,  439, 447, 449-450
spin, Executability,  429, 432, 443, 445
spin, Exhaustive Search,  440-441
spin, exhaustive validation,  429, 438
spin, Expressions,  442-445
spin, Full State Space,  440-442
spin, global variables,  429, 431, 438, 443
spin, goto,  435, 437, 444	S
spin, greatest common divisor,  435
spin, guard,  434, 436-437, 445
spin, halt,  437, 444	S
spin, hash collision,  440-441
spin, hash factor,  438, 442
spin, hash table,  441
spin, Identifiers,  442-443
spin, if,  444	S
spin, init,  431, 435	S
spin, Keywords,  442, 444
spin, Lexical Conventions,  442
spin, local variables,  430, 432, 438-439, 443, 449
spin, Macros and Include File,  445
spin, Message Channels,  429, 432-433, 436, 443
spin, Message Passing,  432, 445
spin, message type,  432, 437-439, 443
spin, Message Type Definitions,  437
spin, Modeling Procedures and Recursion,  436
spin, non-progress loops,  437, 441, 449
spin, Options,  434-435, 438-441, 444
spin, pan.trail,  439-440, 442, 447, 449	S
spin, process declaration,  430, 443
spin, Process Instantiation,  430, 432, 443
spin, Process Type,  430-431, 435-436
spin, Processes,  443
spin, proctype,  430-431, 443	S
spin, Progress-State Labels,  437
spin, PROMELA,  429
spin, PROMELA Reference Manual,  442
spin, propositional temporal logic,  449
spin, Pseudo Statements,  437
spin, random simulation,  429, 438-439
spin, Receive,  444
spin, Rendez-Vous Communication,  433-435
spin, Repetition,  434, 443-444
spin, Repetition and Break,  444
spin, run,  431, 437-438	S
spin, run-time error,  432, 444
spin, search depth,  441
spin, Selection,  434, 443-445
spin, Send,  444
spin, side-effects,  429, 433, 445
spin, Simulator,  439-440
spin, skip,  431, 435-437, 444	S
spin, Spin,  438
spin, state space,  429, 438, 440-442
spin, statement separator,  430, 442
spin, Statements,  443
spin, symbolic names,  442-443
spin, synchronous communication,  429, 433, 445
spin, system state space,  429, 438, 440-441, 449
spin, test and set problem,  432
spin, Timeout,  436-437, 442-445, 448
spin, unary operator,  431, 437, 443
spin, Unconditional Jumps,  434-435
spin, unexecutable code,  429
spin, unreachable state,  441
spin, Variables,  443
synchronous communication, spin,  429, 433, 445
Timeout, spin,  436-437, 442-445, 448