Spinroot

A forum for Spin users

You are not logged in.

#2 General » problem with replaying trail file » 2018-10-09 03:10:28

haozheng
Replies: 1

When I  re-play a trail file using "spin -p -t a1_3.pml.trail" , I got an message on screen shown below.
spin: a1_3.pml.trail:1, Error: syntax error    saw ''-' = 45'
spin: cannot find trail file

From the trail file, the first line is "-4:-4:-4". Seems that spin does not like negative numbers in the trail file.

Can you please shed some light on how to get around or fix this issue? I use spin version 648.

Thank you.

#3 Re: General » Excessive memory usage with bitstate hashing » 2018-10-09 03:07:50

When I  re-play a trail file using "spin -p -t a1_3.pml.trail" , I got an message on screen shown below.

spin: a1_3.pml.trail:1, Error: syntax error    saw ''-' = 45'
spin: cannot find trail file

From the trail file, the first line is "-4:-4:-4"

Can you please shed some light on this issue? I use spin version 648.

Thank you.

#4 Re: General » Excessive memory usage with bitstate hashing » 2015-04-18 03:32:45

Thank you for the reply and pointing out the problem in my model.

What this example confuses me is the difference usages by -DCOLLAPSE and -DBITSTATE options. The results printed when pan is executed in those two modes are shown below for comparison.

Command:
gcc -DCOLLAPSE -DSAFETY -o pan pan.c
pan -m10000000
-------------------------------------------------------
Depth= 1023340 States=    1e+06 Transitions= 1.05e+06 Memory=   726.316    t=     2.15 R=   5e+05
Depth= 2046488 States=    2e+06 Transitions=  2.1e+06 Memory=   790.476    t=     4.33 R=   5e+05
Depth= 3069635 States=    3e+06 Transitions= 3.15e+06 Memory=   854.636    t=      6.5 R=   5e+05
Depth= 4092784 States=    4e+06 Transitions=  4.2e+06 Memory=   918.698    t=     8.62 R=   5e+05
^CInterrupted

Command:
gcc -DBITSTAE -DSAFETY -o pan pan.c
pan -w32 -k4 -m10000000
--------------------------------------------------------
Depth= 1023340 States=    1e+06 Transitions= 1.05e+06 Memory=  1690.223    t=     2.53 R=   4e+05
Depth= 2046488 States=    2e+06 Transitions=  2.1e+06 Memory=  2257.996    t=     5.62 R=   4e+05
Depth= 3069635 States=    3e+06 Transitions= 3.15e+06 Memory=  2825.770    t=     10.7 R=   3e+05
Depth= 4092784 States=    4e+06 Transitions=  4.2e+06 Memory=  3393.543    t=     16.6 R=   2e+05
^CInterrupted

From both runs, the depths of the stack are the same in each step of the printout, so I suppose the memory consumed by the stack should be about the same.

However, I do notice that large amount of memory is consumed by other (proc and chan stacks) when pan is executed in bitstate hashing mode which is shown in the stats on memory usage printed out at the end.  Can you explain what that memory is used for?

Stats on memory usage (in Megabytes):
2378.990    equivalent memory usage for states (stored*(State-vector + overhead))
  512.000    memory used for hash array (-w32)
   76.294    memory used for bit stack
  534.058    memory used for DFS stack (-m10000000)
2389.794    other (proc and chan stacks)
    2.784    memory lost to fragmentation
3514.930    total actual memory usage


Thank you very much.

#5 Re: General » Excessive memory usage with bitstate hashing » 2015-04-17 16:59:14

In fact, I had to kill the processes using -DCOLLAPSE and -DBITSTATE after they reach about 4e+06 states.  So my question should be phrased more precisely like this: why the memory used with bitstate hashing grows more quickly than that with -DCOLLAPSE?  Suppose that there are only 4GB memory. Then bitstate hashing can actually search less states.  This is what confuses me.

The .pml model is attached.

Thank you for your help.

- Hao

==========================================
/* 3_csv.pml */

#define N 3

chan E_chan[(N*N)] = [1] of {byte};
chan W_chan[(N*N)] = [1] of {byte};
chan N_chan[(N*N)] = [1] of {byte};
chan S_chan[(N*N)] = [1] of {byte};
byte Recevier[N*N];
int Success;
byte Rand_x,Rand_y;

proctype Process(byte x,y)
{
byte Dx,Dy,Dest_Id;
bool is_message,msg_send;
byte fault;
byte Cx=x,Cy=y;
byte Id,rN,rS,rE,rW,s;
Id=(x*N)+y;
rN=((x+1)*N)+y;
rS=((x-1)*N)+y;
rE=(x*N)+y+1;
rW=(x*N)+y-1;
start:
s=Success;
is_message=false;
msg_send=false;
loop:
atomic{
if
    ::(Rand_x<=N-2) -> Rand_x++;
    ::(Rand_x<=N-1) -> Rand_x=0;
    ::(Rand_y<=N-2) -> Rand_y++;
    ::(Rand_y==N-1) -> Rand_y=0;
fi}
assert(Rand_x<N)
assert(Rand_y<N)
if
    ::atomic{Recevier[Id]==0 ->if
                        ::((Rand_x!=x)&&(Rand_y!=y)) -> Dest_Id=(Rand_x*N)+Rand_y;is_message=true;
                        ::else-> skip;
                   fi}
    ::Recevier[Id]>=0 ->if
          ::(x==0) -> if
                ::(y==0) -> do
                        ::     empty(S_chan[rN]) -> break;
                        ::     atomic{S_chan[rN]?Dest_Id;  if
                                                                                        ::Recevier[Id]!=0 ->Recevier[Id]--;
                                                                                fi}
                        printf("message received is %d\n",Dest_Id);is_message=true;break;
                        ::     empty(W_chan[rE]) -> break;
                        ::     atomic{W_chan[rE]?Dest_Id;  if
                                                                                        ::Recevier[Id]!=0 ->Recevier[Id]--;
                                                                                fi}
                        printf("message received is %d\n",Dest_Id);is_message=true;break;
                        od
                ::(y==(N-1)) -> do
                        ::     empty(S_chan[rN]) -> break;
                        ::     atomic{S_chan[rN]?Dest_Id;  if
                                                                                        ::Recevier[Id]!=0 ->Recevier[Id]--;
                                                                                fi}
                        printf("message received is %d\n",Dest_Id);is_message=true;break
                        ::     empty(E_chan[rW]) -> break;
                        ::     atomic{E_chan[rW]?Dest_Id;  if
                                                                                        ::Recevier[Id]!=0 ->Recevier[Id]--;
                                                                                fi}
                        printf("message received is %d\n",Dest_Id);is_message=true;break
                        od
                ::else ->   do   
                        ::     empty(S_chan[rN]) -> break;
                        ::     atomic{S_chan[rN]?Dest_Id;  if
                                                                                        ::Recevier[Id]!=0 ->Recevier[Id]--;
                                                                                fi}
                        printf("message received is %d\n",Dest_Id);is_message=true;break;
                        ::     empty(E_chan[rW]) -> break;
                        ::     atomic{E_chan[rW]?Dest_Id;   if
                                                                                        ::Recevier[Id]!=0 ->Recevier[Id]--;
                                                                                fi}
                        printf("message received is %d\n",Dest_Id);is_message=true;break;
                        ::     empty(W_chan[rE]) -> break;
                        ::     atomic{W_chan[rE]?Dest_Id;  if
                                                                                        ::Recevier[Id]!=0 ->Recevier[Id]--;
                                                                                fi}
                        printf("message received is %d\n",Dest_Id);is_message=true;break;
                        od
                 fi
          ::(x==(N-1)) ->if
                ::(y==0) -> do
                        ::     empty(N_chan[rS]) -> break;
                        ::     atomic{N_chan[rS]?Dest_Id;  if
                                                                                        ::Recevier[Id]!=0 ->Recevier[Id]--;
                                                                                fi}
                        printf("message received is %d\n",Dest_Id);is_message=true;break;
                        ::     empty(W_chan[rE]) -> break;
                        ::     atomic{W_chan[rE]?Dest_Id;  if
                                                                                        ::Recevier[Id]!=0 ->Recevier[Id]--;
                                                                                fi}
                        printf("message received is %d\n",Dest_Id);is_message=true;break;
                        od
                ::(y==(N-1)) -> do
                        ::     empty(N_chan[rS]) -> break;
                        ::     atomic{N_chan[rS]?Dest_Id;  if
                                                                                        ::Recevier[Id]!=0 ->Recevier[Id]--;
                                                                                fi}
                        printf("message received is %d\n",Dest_Id);is_message=true;break;   
                        ::     empty(E_chan[rW]) -> break;
                        ::     atomic{E_chan[rW]?Dest_Id;  if
                                                                                        ::Recevier[Id]!=0 ->Recevier[Id]--;
                                                                                fi}
                        printf("message received is %d\n",Dest_Id);is_message=true;break;
                        od
                ::else ->   do   
                        ::     empty(N_chan[rS]) -> break;
                        ::     atomic{N_chan[rS]?Dest_Id;  if
                                                                                        ::Recevier[Id]!=0 ->Recevier[Id]--;
                                                                                fi}
                        printf("message received is %d\n",Dest_Id);is_message=true;break;
                        ::     empty(E_chan[rW]) -> break;
                        ::     atomic{E_chan[rW]?Dest_Id;  if
                                                                                        ::Recevier[Id]!=0 ->Recevier[Id]--;
                                                                                fi}
                        printf("message received is %d\n",Dest_Id);is_message=true;break;
                        ::     empty(W_chan[rE]) -> break;
                        ::     atomic{W_chan[rE]?Dest_Id;  if
                                                                                        ::Recevier[Id]!=0 ->Recevier[Id]--;
                                                                                fi}
                        printf("message received is %d\n",Dest_Id);is_message=true;break;
                        od
                fi
          ::else -> if
                ::(y==0) -> ;do
                        ::     empty(S_chan[rN]) -> break;
                        ::     atomic{S_chan[rN]?Dest_Id;  if
                                                                                        ::Recevier[Id]!=0 ->Recevier[Id]--;
                                                                                fi}
                        printf("message received is %d\n",Dest_Id);is_message=true;break;
                        ::     empty(N_chan[rS]) -> break;
                        ::     atomic{N_chan[rS]?Dest_Id;  if
                                                                                        ::Recevier[Id]!=0 ->Recevier[Id]--;
                                                                                fi}
                        printf("message received is %d\n",Dest_Id);is_message=true;break;
                        ::     empty(W_chan[rE]) -> break;printf("i'm waiting,.....\n");
                        ::     atomic{W_chan[rE]?Dest_Id;  if
                                                                                        ::Recevier[Id]!=0 ->Recevier[Id]--;
                                                                                fi}
                        printf("message received is %d\n",Dest_Id);is_message=true;break;
                        od
                ::(y==(N-1)) ->; do   
                        ::     empty(S_chan[rN]) -> break;
                        ::     atomic{S_chan[rN]?Dest_Id;  if
                                                                                        ::Recevier[Id]!=0 ->Recevier[Id]--;
                                                                                fi}
                        printf("message received is %d\n",Dest_Id);is_message=true;break;
                        ::     empty(N_chan[rS]) -> break;
                        ::     atomic{N_chan[rS]?Dest_Id;  if
                                                                                        ::Recevier[Id]!=0 ->Recevier[Id]--;
                                                                                fi}
                        printf("message received is %d\n",Dest_Id);is_message=true;break;
                        ::     empty(E_chan[rW]) -> break;
                        ::     atomic{E_chan[rW]?Dest_Id;  if
                                                                                        ::Recevier[Id]!=0 ->Recevier[Id]--;
                                                                                fi}
                        printf("message received is %d\n",Dest_Id);is_message=true;break;
                        od
                ::else ->   do   
                        ::     empty(S_chan[rN]) ->break;
                        ::     atomic{S_chan[rN]?Dest_Id;  if
                                                                                        ::Recevier[Id]!=0 ->Recevier[Id]--;
                                                                                fi}
                        printf("message received is %d\n",Dest_Id);is_message=true;break;
                        ::     empty(N_chan[rS]) -> break;
                        ::     atomic{N_chan[rS]?Dest_Id;  if
                                                                                        ::Recevier[Id]!=0 ->Recevier[Id]--;
                                                                                fi}
                        printf("message received is %d\n",Dest_Id);is_message=true;break;
                        ::     empty(E_chan[rW]) -> break;
                        ::     atomic{E_chan[rW]?Dest_Id;  if
                                                                                        ::Recevier[Id]!=0 ->Recevier[Id]--;
                                                                                fi}
                        printf("message received is %d\n",Dest_Id);is_message=true;break;
                        ::     empty(W_chan[rE]) -> break;
                        ::     atomic{W_chan[rE]?Dest_Id;    if
                                            ::Recevier[Id]!=0 ->Recevier[Id]--;
                                        fi}
                        printf("message received is %d\n",Dest_Id);is_message=true;break;
                           od
              fi
        fi
fi
if
    :: is_message==true -> skip;
    :: else -> goto loop;                   
fi
do
::(msg_send==true) -> break;
::else -> Dx=Dest_Id/N;Dy=Dest_Id%N;
    if
    ::(Cx<Dx) -> if
        ::(Cy<Dy) -> do
                ::empty(N_chan[Id]) ->     atomic{N_chan[Id]!Dest_Id;
                            Recevier[rN]++;}
                            printf("message is send on %d... destination is %d,%d\n",Id,Dx,Dy);
                            msg_send=true;break;
                ::empty(E_chan[Id]) ->     atomic{E_chan[Id]!Dest_Id;
                            Recevier[rE]++;}
                            printf("message is send on %d... destination is %d,%d\n",Id,Dx,Dy);
                            msg_send=true;break;
                 od
        ::(Cy>Dy) -> do
                ::empty(W_chan[Id]) ->     atomic{W_chan[Id]!Dest_Id;
                            Recevier[rW]++;}
                            printf("message is send on %d... destination is %d,%d\n",Id,Dx,Dy);
                            msg_send=true;break;
                 od
        ::else ->    do
                ::empty(N_chan[Id]) ->     atomic{N_chan[Id]!Dest_Id;
                            Recevier[rN]++;}
                            printf("message is send on %d... destination is %d,%d\n",Id,Dx,Dy);
                            msg_send=true;break;
                 od
         fi
    ::(Cx>Dx) -> if   
        ::(Cy<Dy) -> do
                ::empty(S_chan[Id]) ->    atomic{S_chan[Id]!Dest_Id;
                            Recevier[rS]++;}
                            printf("message is send on %d... destination is %d,%d\n",Id,Dx,Dy);
                            msg_send=true;break;
                 od
        ::(Cy>Dy) -> do
                ::empty(S_chan[Id]) ->    atomic{S_chan[Id]!Dest_Id;
                            Recevier[rS]++;}
                            printf("message is send on %d... destination is %d,%d\n",Id,Dx,Dy);
                            msg_send=true;break;
                ::empty(W_chan[Id]) ->     atomic{W_chan[Id]!Dest_Id;
                            Recevier[rW]++;}
                            printf("message is send on %d... destination is %d,%d\n",Id,Dx,Dy);
                            msg_send=true;break;
                      od
        ::else ->    do
                ::empty(S_chan[Id])->    atomic{S_chan[Id]!Dest_Id;
                            Recevier[rS]++;}
                            printf("message is send on %d... destination is %d,%d\n",Id,Dx,Dy);
                            msg_send=true;break
                 od
         fi
    :: else ->   if
        ::(Cy<Dy) -> do
                ::empty(E_chan[Id]) ->    atomic{E_chan[Id]!Dest_Id;
                            Recevier[rE]++;}
                            printf("message is send on %d... destination is %d,%d\n",Id,Dx,Dy);
                            msg_send=true;break;
                 od
        ::(Cy>Dy) -> do
                ::empty(W_chan[Id]) ->    atomic{W_chan[Id]!Dest_Id;
                            Recevier[rW]++;}
                            printf("message is send on %d... destination is %d,%d\n",Id,Dx,Dy);
                            msg_send=true;break;
                 od
        ::else ->     Success++;
                printf("msg-%d has reached destination %d node...No.of Destination reached is %d\n",Dest_Id,Id,Success);
                msg_send=true;
         fi
    fi   
od
goto start
}


init
{
byte x=0,y=0;
atomic{
do
:: skip;
    if
    :: (x<N)->if
            ::(y<N) -> run Process(x,y);y++;//printf("process created with x=%d y=%d\n",x,y);
            ::else -> x++;y=0;
          fi
    ::else -> break;
    fi
od}   
}

#6 General » Excessive memory usage with bitstate hashing » 2015-04-17 00:59:32

haozheng
Replies: 9

Hi, I used bitstate hashing for a NoC project I am working on with the impression that bitstate hashing is fast and covers more states within a fixed memory limit. But the results show me the opposite story. I used the following commands to compile and run the model.
spin -a 3_csv.pml
gcc -O2 -DSAFETY -DBITSTATE -o pan pan.c
./pan -w32 -k4 -m10000000

The results are shown below.

Depth= 1023340 States=    1e+06 Transitions= 1.05e+06 Memory=  1690.223    t=     2.84 R=   4e+05
Depth= 2046488 States=    2e+06 Transitions=  2.1e+06 Memory=  2257.996    t=     6.06 R=   3e+05
Depth= 3069635 States=    3e+06 Transitions= 3.15e+06 Memory=  2825.770    t=     9.32 R=   3e+05
Depth= 4092784 States=    4e+06 Transitions=  4.2e+06 Memory=  3393.543    t=     14.1 R=   3e+05
^CInterrupted

(Spin Version 6.4.3 -- 16 December 2014)
Warning: Search not completed
    + Partial Order Reduction

Bit statespace search for:
    never claim             - (none specified)
    assertion violations    +
    cycle checks           - (disabled by -DSAFETY)
    invalid end states    +

State-vector 572 byte, depth reached 4206042, errors: 0
  4110696 states, stored
   209444 states, matched
  4320140 transitions (= stored+matched)
    95379 atomic steps

hash factor: 1044.83 (best if > 100.)

bits set per state: 4 (-k4)

Stats on memory usage (in Megabytes):
2320.797    equivalent memory usage for states (stored*(State-vector + overhead))
  512.000    memory used for hash array (-w32)
   76.294    memory used for bit stack
  534.058    memory used for DFS stack (-m10000000)
2331.365    other (proc and chan stacks)
    2.717    memory lost to fragmentation
3456.434    total actual memory usage


It is strange to find out that much less memory is used when the model is compile with -DCOLLAPSE instead.

I would highly appreciate if comments can be given to explain this phenomenon. The above run was done on a Macbook Air with 4GB memory.


Thank you very much.

Hao

#7 Re: General » Cannot find invalid end state in dinning philosopher » 2013-12-23 18:00:48

Thanks a lot for the comment.  I tried the revised model as suggested, and it worked with an invalid end state found for model 2.

#8 General » Cannot find invalid end state in dinning philosopher » 2013-12-16 17:35:51

haozheng
Replies: 2

Hi, I am new to SPIN, and the following two Promela models for the dinning philosopher problem confuse me.  I attached the two models below.  To me, they are the same except the different ways on how processes are created. However, SPIN finds an invalid end state for model 1, but none for model 2.  The version of the SPIN I use is 6.2.5.  The commands used to compile the models are

../Src6.2.5/spin -a $1
gcc -O2 -DNOFAIR -DNOBOUNDCHECK -DSAFETY -o pan pan.c
./pan -m10000000 -n -Q5

Any insight and help would be very appreciated.

HZ 



/*
             Model 1
*/
byte fork[5];


active proctype phil_0() {

think: if
::  d_step {fork[0]==0;fork[0] = 1;}  goto one;

fi;
one: if
::  d_step {fork[1]==0;fork[1] = 1;}  goto eat;

fi;
eat: if
:: fork[0] = 0; goto finish;

fi;
finish: if
:: fork[1] = 0; goto think;

fi;
}

active proctype phil_1() {

think: if
::  d_step {fork[1]==0;fork[1] = 1;}  goto one;

fi;
one: if
::  d_step {fork[2]==0;fork[2] = 1;}  goto eat;

fi;
eat: if
:: fork[1] = 0; goto finish;

fi;
finish: if
:: fork[2] = 0; goto think;

fi;
}

active proctype phil_2() {

think: if
::  d_step {fork[2]==0;fork[2] = 1;}  goto one;

fi;
one: if
::  d_step {fork[3]==0;fork[3] = 1;}  goto eat;

fi;
eat: if
:: fork[2] = 0; goto finish;

fi;
finish: if
:: fork[3] = 0; goto think;

fi;
}

active proctype phil_3() {

think: if
::  d_step {fork[3]==0;fork[3] = 1;}  goto one;

fi;
one: if
::  d_step {fork[4]==0;fork[4] = 1;}  goto eat;

fi;
eat: if
:: fork[3] = 0; goto finish;

fi;
finish: if
:: fork[4] = 0; goto think;

fi;
}

active proctype phil_4() {

think: if
::  d_step {fork[4]==0;fork[4] = 1;}  goto one;

fi;
one: if
::  d_step {fork[0]==0;fork[0] = 1;}  goto eat;

fi;
eat: if
:: fork[4] = 0; goto finish;

fi;
finish: if
:: fork[0] = 0; goto think;

fi;
}




/* ================================================= */

/*
      Model 2
*/


byte fork[5];


proctype phil(byte left; byte right) {

think: if
::  d_step {left==0; left = 1;}  goto one;

fi;
one: if
::  d_step {right ==0; right = 1;}  goto eat;

fi;
eat: if
:: left = 0; goto finish;

fi;
finish: if
:: right = 0; goto think;

fi;
}

init {         atomic {run phil(fork[0], fork[1]);
                 run phil(fork[1], fork[2]);
            run phil(fork[2], fork[3]);
                 run phil(fork[3], fork[4]);
            run phil(fork[4], fork[0]) }
}

Board footer

Powered by FluxBB