Spinroot

A forum for Spin users

You are not logged in.

#1 2011-10-04 16:22:46

nikos
Member
Registered: 2011-10-04
Posts: 2

Spin as a library/on-the-fly checker -- where to start?

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

#2 2011-10-05 01:52:25

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

Re: Spin as a library/on-the-fly checker -- where to start?

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

#3 2011-10-05 08:14:26

nikos
Member
Registered: 2011-10-04
Posts: 2

Re: Spin as a library/on-the-fly checker -- where to start?

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

#4 2011-10-05 15:03:21

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

Re: Spin as a library/on-the-fly checker -- where to start?

Yes. Of course you could try to generate partial automata during the construction, as long as they are syntactically correct...

Offline

Board footer

Powered by FluxBB