A forum for Spin users
You are not logged in.
Hi.
I would like to use spin as a library that I link to my application. Essentially I will be constructing an automaton and would like to call spin on it during construction, so that I get early counterexamples. Would this be possible? Where should I start looking?
Thanks!
Offline
That's a great idea. I've actually tried creating something like this (a library of the core routines used by Spin).
What complicates this is that Spin highly optimizes the core routines for each specific type of model.
It relies a lot on compiler directives to get this optimization, and that makes it hard to setup a generic library.
You can of course also generate the automaton description in the right format and run Spin as is, in the background to get early feedback. At the moment we don't have a better method for this yet, alas.
Offline
Thanks for your response. If I understand correctly what you are saying, there is no easy way to use spin as a library, but I could generate the model first and then pass it to spin. But in the latter case, I would not get "early" counterexamples, since I have already generated the automaton. Or do I misunderstand?
Offline