Chapter 16. PROMELA Language Reference

 

“The infinite multitude of things is incomprehensible, and more than a man may be able to contemplate.”

 
 --(Giambattista della Porta, 1535–1615, Natural Magick)

The PROMELA manual pages that are included in this book can be grouped into seven main sections. The first five of these sections, plus the grammar description given here, describe the language proper. The entries from the sixth section cover those things that are deliberately not in the language, and contain a brief explanation of why they were left out. The entries from the seventh and last section cover the more recent extensions to the PROMELA language to support the use of embedded C code statements and data declarations. The main sections are: ...

Get Spin Model Checker, The: Primer and Reference Manual now with the O’Reilly learning platform.

O’Reilly members experience books, live events, courses curated by job role, and more from O’Reilly and nearly 200 top publishers.