Spinroot

In last semester I took Model checking course and decided to pursue my career in the field of Formal Verification.
Till now, I covered the internal working of Spin model checker from source code, especially the complete process of
Verification  Mode. I solved all small examples given for different keywords in "http://spinroot.com/spin/Man/promela.html"
and other tutorials from spinroot.com. But I don't know any resource which tells how to extract a model from a
given system and write it in Promela(a complete step by step example). All examples I have found already have the model
written in Promela. Can anyone please provide a complete example or link to understand the whole procedure. Thanks!