mikrocontroller.net

Forum: PC-Programmierung Spin und Promela Problem


Autor: Gast (Gast)
Datum:

Bewertung
0 lesenswert
nicht lesenswert
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

Antwort schreiben

Die Angabe einer E-Mail-Adresse ist freiwillig. Wenn Sie automatisch per E-Mail über Antworten auf Ihren Beitrag informiert werden möchten, melden Sie sich bitte an.

Wichtige Regeln - erst lesen, dann posten!

  • Groß- und Kleinschreibung verwenden
  • Längeren Sourcecode nicht im Text einfügen, sondern als Dateianhang

Formatierung (mehr Informationen...)

  • [c]C-Code[/c]
  • [avrasm]AVR-Assembler-Code[/avrasm]
  • [code]Code in anderen Sprachen, ASCII-Zeichnungen[/code]
  • [math]Formel in LaTeX-Syntax[/math]
  • [[Titel]] - Link zu Artikel
  • Verweis auf anderen Beitrag einfügen: Rechtsklick auf Beitragstitel,
    "Adresse kopieren", und in den Text einfügen




Bild automatisch verkleinern, falls nötig
Bitte das JPG-Format nur für Fotos und Scans verwenden!
Zeichnungen und Screenshots im PNG- oder
GIF-Format hochladen. Siehe Bildformate.
Hinweis: der ursprüngliche Beitrag ist mehr als 6 Monate alt.
Bitte hier nur auf die ursprüngliche Frage antworten,
für neue Fragen einen neuen Beitrag erstellen.

Mit dem Abschicken bestätigst du, die Nutzungsbedingungen anzuerkennen.