Floating point calculations in Promela

Question

I want to model projectile trajectory of an object in Promela, and verify some properties of the model. But, Promela doesn't have floating point data type. So, it can't for example, calculate the projectile motion parameters. For example it can't compute trignometric functions like sine/cosine, so I can't model a projectile motion.

What is the workaround for this? How do we go about modelling such systems in Promela?

Answer 1

In Promela/SPIN you can embed arbitrary C code including the specification of what C memory should be considered part of the exhaustively-explored state-space. Look into the language constructs: c_code, c_decl, c_state, c_track and c_expr.

Note that it is usually trouble to include floating point numbers; even one, but certainly any more than one. You either need to find a way to make the floating point value NOT part of the state space in which case they are intermediate computational values or you need to discretize your problem space. This is a specific example of an important model-checking concept - finding the proper abstraction level between an exact but computationally impossible mode and a near-contentless high-level model.

In light of this, the omission of floating-point numbers was a VERY conscious design decision in the original PROMELA/SPIN design.

Note: in your case, perhaps you have some input parameters and a single output parameter of 'hit the target'. Then all the floating point calculations are intermediate and your correctness claim finds, for example, combinations of parameters that lead to a missed target.