Spinroot

A forum for Spin users

You are not logged in.

#1 2013-06-26 05:25:12

mike89
Member
Registered: 2013-06-26
Posts: 4

limit on number of channels?

When I attempt to generate a pan verifier using the "-a" flag, I get the following message from Spin when I try to create more than 255 channels: "Error: too many channel types"

Is there any way around this limit? (and is there a reason for the fixed limit?)

The verification time for assertions in my model was still fine until I reached this limit, but I realize that if I'm hitting this limit, I might be getting into the realm of it taking too long to verify.


Thanks,
Mike

Offline

#2 2013-06-26 15:46:18

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

Re: limit on number of channels?

No there's no way around that limit -- the verifier counts on being able to store a channel id into one single byte.
It pays to make models as abstract as possible, to construct "the smallest sufficient model" to prove or disprove a property.
Just like in regular mathematics: to prove something you don't want to make things more complicated than strictly necessary....!

Offline

#3 2013-06-26 16:11:06

mike89
Member
Registered: 2013-06-26
Posts: 4

Re: limit on number of channels?

Thanks, that's what I saw when looking into the source but just wanted to make sure there wasn't something I was missing.

Do you think it would be feasible for me to hack away at the source for a bit in an attempt to change the channel's datatype from byte to something bigger? Or is there enough coupling between this byte datatype for channel id (bit tricks, dependencies in the rest of the code, etc.) that make changing it from char to something else impractical?

Offline

#4 2013-06-26 16:31:35

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

Re: limit on number of channels?

It would be very challenging to change this -- same for the max nr of processes which is also 255.
A lot of the code depends on this being represented in a byte...

Offline

#5 2013-06-26 18:14:10

mike89
Member
Registered: 2013-06-26
Posts: 4

Re: limit on number of channels?

Ack, I feared that might be the case. Guess I'll have to rethink about how I'm modelling my problem.

Thanks for the quick replies!

Offline

Board footer

Powered by FluxBB