Spinroot

A forum for Spin users

You are not logged in.

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

feng_lei_76
Member
Registered: 2011-05-13
Posts: 43

Type casting in SPIN expression

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.

Offline

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

spinroot
forum
Registered: 2010-11-18
Posts: 695
Website

Re: Type casting in SPIN expression

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

Offline

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

feng_lei_76
Member
Registered: 2011-05-13
Posts: 43

Re: Type casting in SPIN expression

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 ****************/

Offline

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

spinroot
forum
Registered: 2010-11-18
Posts: 695
Website

Re: Type casting in SPIN expression

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...

Offline

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

feng_lei_76
Member
Registered: 2011-05-13
Posts: 43

Re: Type casting in SPIN expression

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?

Offline

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

feng_lei_76
Member
Registered: 2011-05-13
Posts: 43

Re: Type casting in SPIN expression

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.

Offline

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

spinroot
forum
Registered: 2010-11-18
Posts: 695
Website

Re: Type casting in SPIN expression

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.

Offline

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

feng_lei_76
Member
Registered: 2011-05-13
Posts: 43

Re: Type casting in SPIN expression

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

Offline

Board footer

Powered by FluxBB