A forum for Spin users
You are not logged in.
Pages: 1
Is there a fundamental reason why Spin doesn't let the user send an array of structures in a message? I am somewhat surprised, as arrays are declared statically and therefore it seems to me that it shouldn't be too hard to handle by the compiler.
Are there any workarounds?
Right now the only thing I can see is to make a static array of the datatype containing my struct array, and pass along an index into this array in my message instead of the actual datatype. This seems like it would have a huge state-space blow-up; I was thinking that if I create exactly the objects I need and pass them as messages, I could avoid this blow-up as well as allowing me to be more dynamic than the static array (in that I'd create/initialize the values of my object as I need them, instead of already having everything in the array).
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!
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?
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
Pages: 1