Spin und Promela Problem

[Gast (Gast)]

Hi

Bin gerade dabei mich ein wenig mit formaler Verifikation zu 
beschäftigen und schaue mir dazu das Tool Spin mit der Sprache Promela 
an. Die Syntax von Promela ist mir eigentlich klar und ich habe im 
Internet eine Beispiel zum „Schaf, Wolf, Kohl“ Problem gefunden 
(http://user.it.uu.se/~bengt/ARTES07/Models/wolf) welches ich rein von 
der Syntax her auch verstehe aber mir ist nicht klar wie ich Spin nun 
dazu bringe das Problem zu lösen. Wenn ich auf random Simulation gehe 
bekomme ich meistens ein time out von folgender Zeile:

((!S1[sheep]) || (!S1[wolf] && !S1[cabbage]));

Mein Ziel ist es nun zu sagen das er beim assert ankommen muss. 
Vielleicht hat jemand von euch Erfahrung mit Spin und Promela und kann 
mir helfen oder eine Link geben mit dem ich mein Problem lösen kann?? 
Danke im Vorhinein!

MFG Gast