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