spin model checker

Dining philosophers problem is a typical example of dead-lock situation, in this case, we already know that in this dining philosophers model, there exists a dead-lock problem. But most of practical cases, it is pretty hard to figure out dead-lock problem.

Spin can make us test a model before we implement that model.

the following is Promela code which describe dining philosophers problem.
then we can simulate it with spin.

  • spin file.prom — simulate the system (one randomly selected run)
  • spin -a file.prom — generate a verifier (in pan.c)
  • gcc pan.c — compile the verifier
  • a. out — run the verifier (exhaustive searching of all possible runs)
  • spin -t -p file.prom — make the simulator follow the failure trace if the verifier found an error. without ‘-p’ it only prints the final state; with ‘-p’ te whole state trce is printed (can be long!)
  • gcc -DNP pan.c — compile the verifier for liveness (need “progress” labels in your promela code)
[ diningphil.prom ]

#define   N 4
byte Fork[N];
#define Think( I )  printf( "Think %dn", I )
#define Eat( I )    printf( "Eat %dn", I )

proctype Philosopher( byte I ) {
:: Think( I ) ;
atomic { (Fork[I] > 0);       Fork[I]-- } ;
atomic { (Fork[(I+1)%N] > 0); Fork[(I+1)%N]-- } ;
Eat( I ) ;

init {
byte   ind ;
assert( N > 2 ) ;
atomic {
ind = 0;
:: (ind >= N) ->
:: else ->
Fork[ind] = 1;
ind = 0;
:: (ind >= N) ->
:: else ->
run Philosopher( ind );

One Response to “spin model checker”

  1. Javier Ernesto Says:

    No me sirve esta mierda!!! si hacen una cosa haganla bien perros de mierda!!!

Leave a Reply

Fill in your details below or click an icon to log in:

WordPress.com Logo

You are commenting using your WordPress.com account. Log Out / Change )

Twitter picture

You are commenting using your Twitter account. Log Out / Change )

Facebook photo

You are commenting using your Facebook account. Log Out / Change )

Google+ photo

You are commenting using your Google+ account. Log Out / Change )

Connecting to %s

%d bloggers like this: