C program non-progress loops s CW-a S spin -a S CW -a S CW-f S CW -f S CW-c S CW -c S CW-m S CW -m S CW-n S CW -n S CW-p S CW -p S CW-t S CW -t S CW-w S CW -w S CW-g S CW -g S CW-l S CW -l S CW-r S CW -r S CW-s S CW -s S CW-q S CW -q S Progress-State Labels End-State Lables guarded command language g Atomic Sequence s CW assert S CW block S assertion violation asynchronous communication deadlock g synchronous communication protocol g concurrent processes g pan.trail S CW break S buffer size s chan S channel s curly braces s CW do S error sequence s error trail s exhaustive validation CW goto S global variables s greatest common divisor s CW halt S hash collision s hash factor s hash table s local variables s message type s modeling language g CW null S process declaration s CW proctype S CW skip S random simulation CW run S run-time error s search depth s CW send S state space s symbolic names s system state space s unary operator s unexecutable code s unreachable state s Spin \(em A Protocol Analyzer g Introduction to \*P s Executability Data Types s Array Variables s Process Type s Process Instantiation Message Passing Rendez-Vous Communication Control Flow s Case Selection s Repetition s Unconditional Jumps s Modeling Procedures and Recursion Assertions Message Type Definitions Pseudo Statements s Introduction to Spin s Building A Validations Suite s The Simulator s The Analyzer s Full State Space s Options s Bit State Space s \*P Reference Manual Lexical Conventions s Comments s Identifiers s Keywords s IH Constants s Expressions s Declarations s IH Variables s Message Queues Message Channels s IH Processes IH Statements s Selection s Repetition and Break s IH Send s IH Receive s Timeout Macros and Include File s C| statement \f2separator s statement separator s CW init S CW run S \f2test and set\f1 problem s channel names s .CW len S composite condition s side-effects s guard s Advenced Usage s End-State Labels s Progress-State Labels s deadlocks s grep G Exhaustive Search s Bit State Space Analysis s CW if S Building A Validation Suite s Digging Deeper s propositional temporal logic