Spinroot

lz

Member

Registered: 2012-05-14

Posts: 9

A probable bug ?

In this example:
------------------------------------------------------------------------------
int traversant;
int tvs[2];
bit Feux[2];
active[2] proctype processus() { /* adapt. from Burns & Lynch ... */
   int vehic = _pid;
   L0: Feux[ vehic] = 0;
       if :: vehic==1 && Feux[0]==1 -> goto L0
          :: else -> Feux[vehic] = 1
       fi;         
       if :: vehic==1 && Feux[0]==1 -> goto L0
          :: else -> L1: if :: vehic==0 && Feux[1]==1 -> goto L1
                            :: else -> traversant++; tvs[vehic]++;
                                       progress_sc: assert(traversant==1);
                                       traversant--
                         fi
       fi;
   goto L0
}

------------------------------------------------------------------------------
If I simply replace the variable "tvs" by "t", the following error is reported ...
------------------------------------------------------------------------------

spin -a  croisement_minimal.pml
gcc -DMEMLIM=1024 -O2 -DXUSAFE -DSAFETY -DNOCLAIM -DREACH -w -o pan pan.c
In file included from pan.c:5562:0:
pan.m: In function 'do_transit':
pan.m:73:36: error: incompatible types when assigning to type 'int' from type 'Trans'
pan.m:74:89: error: invalid operands to binary + (have 'Trans' and 'int')
In file included from pan.c:6920:0:
pan.b: In function 'new_state':
pan.b:33:52: error: incompatible types when assigning to type 'Trans' from type 'int'
./pan -m10000  -i

Best regards

spinroot

forum

Registered: 2010-11-18

Posts: 700

Website

Re: A probable bug ?

sorry for the late explanation:
the array tvs[] is mapped to a "hidden" variable by spin
this happens because it is assigned to, but the value is never used
therefore, the values stored in the array cannot influence the outcome of the verification.
a hidden variable (or in this case array) is declared globally, outside the state-vector.
but it so happens that Spin internally also uses a data structured named 't' -- and that causes a
type conflict in this case.
if tvs, or t, had been used somewhere (the values stored in the array being read or used somewhere)
then it would not have been hidden, and the problem would not occur.
in this case, you can simply omit the entire array, and the increment tvs[vehic]++

lz

Member

Registered: 2012-05-14

Posts: 9

Re: A probable bug ?

Thank you, for your explanation.
(the array was used only to analyse the behavior of process in simulation)

Best regards