Spin Model Checker, The: Primer and Reference Manual

Chapter 17. Embedded C Code

	“The purpose of analysis is not to compel belief but rather to suggest doubt.”
	--(Imre Lakatos, Proofs and Refutations)

SPIN, versions 4.0 and later, support the inclusion of embedded C code into PROMELA models through the following five new primitives:

c_expr, c_code, c_decl, c_state, c_track

The purpose of these new primitives is primarily to provide support for automatic model extraction from C code. This means that it is not the intent of these extensions to be used in manually constructed models. The primitives provide a powerful extension, opening SPIN models to the full power of, and all the dangers of, arbitrary C code. The contents of the embedded code fragments cannot be checked by SPIN, neither in the parsing ...