Spin Model Checker, The: Primer and Reference Manual

Chapter . Tables and Figures

	“An undetected error [...] is like a sunken rock at sea yet undiscovered, upon which it is impossible to say what wrecks may have taken place.”
	--(Sir John Herschel, 1842)

Tables

3.1	Basic Data Types	41
3.2	Operator Precedence	54
6.1	Frequently Used LTL Formulae	137
6.2	Formalization of Properties	138
10.1	Example of Type Abstraction	237
16.1	Index of All Manual Pages	370
16.2	Typical Data Ranges	404

Figures

1.1	Circular Blocking	3
1.2	Deadly Embrace	4
2.1	Simple Producer Consumer Example	11
2.2	Revised Producer Consumer Example	17
2.3	Dekker’s Mutual Exclusion Algorithm (1962)	20
2.4	Faulty Mutual Exclusion Algorithm	23
2.5	Peterson’s Mutual Exclusion Algorithm (1981)	26
2.6	Data Transfer Protocol	27
3.1	Simple Model of a Telephone System	63
3.2	Word Count Program ...