Spinroot

A forum for Spin users

You are not logged in.

#1 2011-02-03 21:04:33

Galv
Member
Registered: 2011-02-03
Posts: 1

Question about queues

Hello,

  I'm new in Spin. I'm trying to make verification on algorithm which uses semaphores and I have a problem with liveliness.
  Is there any way to model a queues in Promela? I've tried buffered channels but I've got memory problem (maybe state explosion - I don't know, as I said I'm new:) ). The same problem I have when I'm trying to use my own queue implementation (using "inline... " and array implementation). I whould be gratefull for Your suggestions.

Thank You!

Offline

#2 2011-02-04 05:27:56

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

Re: Question about queues

It's difficult to know what to suggest, without seeing a simple example that doesn't work for you.
Read about complexity issues in the Help menus from iSpin or Xspin and in the book to discover what types of things introduce complexity and what you can do to avoid it....

Offline

Board footer

Powered by FluxBB