Type casting in SPIN expression

feng_lei_76 · 2013-01-24 10:22:53

In book, The SPIN Model Checker: The Primer and Reference Manual, Chapter 3, Section "Assignments and Expressions", a few paragraphs above Table 3.2, a sentence reads

"the values of all operands used in the expression on the right-hand side of the assignment operator are first cast to singed integers, before any of the operands are applied."

I wonder if this rule is specific for SPIN or inherited from C standard. It seems that C/C++ doesn't do the same thing when calculating operands with different data types. C/C++ dynamically promotes the shorter data type to the longer data type during the calculation.

The difference between SPIN and C/C++ may create confusion when building SPIN models.

spinroot · 2013-01-24 16:13:49

The evaluation that actually takes place is conform the C standard (since it is executed after mapping to C code)

feng_lei_76 · 2013-01-31 09:35:00

If the rule of casting everything to signed integers were correct, a conflict would be what if the operands are unsigned integers and the values are larger than the upper bound of signed integer. I wrote two identical programs in both Promela and C++. The results seem contradictory. I used MSVS 2012 Express for compiling the C++ program.

/****** The Promela code: ***********/

#define LENGTH 31 /* The largest length of unsigned data type in Promela */

active proctype test()
{
unsigned x : LENGTH;
byte abyte=2;
int sum_int;
unsigned sum_unsigned:LENGTH;

x = (1 << LENGTH)-1; /* The value is the upperbound of int, 2^31-1 */
sum_int = x + abyte; /* x+abyte = 2^31+1, exceeds the upperbound of int. sum_int should be negative */
assert(sum_int < 0); /* Spin does not find any error here */

sum_unsigned = x + abyte; /* x+abyte = 2^31+1 exceeds the upper bound of unsigned, but after the truncation the value is still positive. It is 1 actually */
assert(sum_unsigned > 0); /* Spin does not find any error here */

assert(x + abyte < 0); /* Which datatype is the sum if not explicit given? By Spinroot, it is int and should be < 0. By C standard, it is unsigned int and should be > 0 */
/* Indeed, Spin does not find any error here */
}
/*********** End of Promela code *************/

/********** Start of CPP code ***************/
#include <iostream>
using namespace std;
#define LENGTH 31

int main()
{
unsigned int x, sum_unsigned; /* The range of unsigned int is larger than that in Promela */
char abyte = 1;
int sum_int;

x=(1<<LENGTH)-1; /* The value is the upperbound of int, 2^31-1 */
sum_int = x + abyte; /* x+abyte = 2^31+1, exceeds the upperbound of int. sum_int should be negative */
if (sum_int < 0)
cout <<"sum_int is negative! OK!"<<endl;
else
cout << "sum_int is positive! Why?" << endl;

sum_unsigned = x + abyte; /* x+abyte = 2^31+1 is still a valid value of unsigned int. */
if (sum_unsigned > 0)
cout << "sum_unsigned is positive! OK!"<<endl;
else
cout << "sum_unsigned is negative! Why?"<<endl;

if (x + abyte > 0) // If this is true, then x and abyte are not first cast into signed integers. x remains unsigned integer.
cout << "x + abyte is positive! Different from SPIN!"<<endl; //This statement is reached. The computation between Spin and C++ are different!
else
cout << "x + abyte is negative! Same as SPIN!"<<endl;

cin >> abyte;
return 0;
}
/********** End of CPP code ****************/

spinroot · 2013-01-31 19:41:02

the size of an integer data type in Promela is determined by the platform you execute the code on -- just like it is in C. So if you're using a 64-bit machine, then an int is 64 bits...

feng_lei_76 · 2013-01-31 23:11:11

My computer is 64 bit W7, but when compiling the code, I choose the target as Win32. I checked the length of int and unsigned int with sizeof. They are both 4, i.e., 32 bits.

Could you please try to run the C++ code with gcc on a 32 bit machine?

feng_lei_76 · 2013-01-31 23:13:19

I forgot to say that I run Spin with Cygwin. Gcc in Cygwin only supports 32-bit program. So int must be 32 bits in pan.c.

spinroot · 2013-02-01 00:54:31

if you generate the pan.c from the model: spin -a model.pml
and look at how that last assertion is encoded in C, you find:

spin_assert(((((int)((P0 *)this)->x)+((int)((P0 *)this)->abyte))<0) ...

so, yes, spin wins and it forces casting to integers, so the manpage is correct.

feng_lei_76 · 2013-02-01 08:43:23

Thanks for pointing that out. Now I see. SPIN indeed explicitly casts everything into int type. All puzzles for me are clear.

Spinroot

#1 2013-01-24 10:22:53

Type casting in SPIN expression

#2 2013-01-24 16:13:49

Re: Type casting in SPIN expression

#3 2013-01-31 09:35:00

Re: Type casting in SPIN expression

#4 2013-01-31 19:41:02

Re: Type casting in SPIN expression

#5 2013-01-31 23:11:11

Re: Type casting in SPIN expression

#6 2013-01-31 23:13:19

Re: Type casting in SPIN expression

#7 2013-02-01 00:54:31

Re: Type casting in SPIN expression

#8 2013-02-01 08:43:23

Re: Type casting in SPIN expression

Board footer