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!
]]>