Tag: spin,model-checking,promela
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?
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.
Sorry, I got a solution for this long time ago on uppaal Yahoo group. I paste the answer here, so it can be useful for others: There is nothing special in your model. You are probably expecting "as soon as possible" semantics where the automaton would take the transition as...
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...
random,reference,undefined,spin,promela
Seems like one or the other person stumbles upon this post, so I may as well make the answer that worked for me more visible. Go to you MinGW folder, search for stdlib.h (C:\MinGW\include) and type in (somewhere along the other #defines, e.g.: below #include <_mingw.h>): #define random rand #define...
The error was because you can't assign a complete typedef variable in one go. I tried to do that by defining local variable pub p; and then after initializing all fields in p, I tried to assign in one go here pt.table[pt.last] = p. I managed to solve it like...
The solution was extending the query with the index variable when checking for deadlock, like A[] not deadlock || indexVarble => 24 So if there is a deadlock, it should be when we run out of range. (in the example the range was [0-23])...
This is because your LTL is translated into a claim with an assert statement. See the following automaton. So, without checking for assertion violations, no error can be found. (A possible explanation of different behaviors: previous versions of Spin might translate this differently, perhaps using accept instead of assert.)...
The verification can be stuck at line 37/40 for a couple of reasons. Your code just prior to then is: 32 if 33 :: J != myID -> ch[J] ! request, myID, myNum[myID]; 34 fi; This if statement will block forever if: J == myID or if ch[J] is full...
This is an answer to my own question. If anyone can post an example for a use-case of a user-defined sort with arity > 0, I'll happily accept that as answer. After reading the SMT-LIBv2 standard more carefully I am now thinking that sort declarations with arity > 0 only...