- Types of Objects
- Processes
- Provided Clauses
- Data Objects
- Data Structures
- Message Channels
- Channel Poll Operations
- Sorted Send And Random Receive
- Rendezvous Communication
- Rules For Executability
- Assignments And Expressions
- Control Flow: Compound Statements
- Atomic Sequences
- Deterministic Steps
- Selection
- Repetition
- Escape Sequences
- Inline Definitions
- Reading Input
- Special Features
- Finding Out More
Finding Out More
This concludes our overview of the main features of the PROMELA specification language. A few more seldomly used constructs were only mentioned in passing here, but are discussed in greater detail in the manual pages that are included in Chapters 16 and 17. More examples of PROMELA models are included in Chapters 14 and 15. A definition of the operational semantics for PROMELA can be found in Chapter 7.
Alternate introductions to the language can be found in, for instance, Ruys [2001] and Holzmann [1991]. Several other tutorial-style introductions to the language can also be found on the SPIN Web site (see Appendix D).