Spinroot

Hi,

I'm considering to use SPIN as an underlying model checker for an integrated verification procedure. During this procedure, I obtain a model that I would like to verify which is very close to a Büchi Automaton. Thus, it would be very easy to actually transform the model into a Büchi automaton. Now, I would like to verify a LTL formula on this Büchi Automaton.

Therefore, I have the question: Is it possible to load a Büchi automaton as a model for verification (in whatever format) into spin? In case it is possible, is there any documentation on this?

I only found out that I can enter never claim directly in terms of a Büchi automaton, but I did not find a similar function for the model to be verified.

Best regards,

Christian