"Convenience-Scripts" für typische SPIN Use Cases

rindphi
Mausschubser
Mausschubser
Beiträge: 55
Registriert: 3. Sep 2009 20:52
Kontaktdaten:

"Convenience-Scripts" für typische SPIN Use Cases

Beitrag von rindphi » 25. Nov 2013 12:32

[Für Linux-Benutzer]

Hallo,

hiermit löse ich ein versprechen ein, das ich in meiner letzten Übungsgruppe gegeben habe: Im Anhang befinden sich die von mir eingesetzten Scripts, die den Tipp-Aufwand für die häufigsten Anwendungsfälle von SPIN erleichtern. Alles natürlich ohne Gewähr, und für besondere Aufgaben (Suchtiefe verändern etc.) wäre es sinnvoll dennoch in der Lage zu sein, SPIN/gcc/pan direkt aufrufen zu können.

Die Scripts sollten im PATH sein. Wenn sie nicht in /usr/bin oder so (root-Rechte erforderlich) liegen sollen, empfiehlt sich das Anlegen bspw. eines Verzeichnisses "bin" im Home-Verzeichnis ("/home/XXX/bin"). Dann fügt man zu Datei "/home/XXX/.profile" (anlegen falls nicht existent) die Zeilen

Code: Alles auswählen

PATH=$PATH:/home/XXX/bin
export PATH
hinzu. Danach entweder System neustarten oder mit

Code: Alles auswählen

. ~/.profile
die Änderungen sofort verfügbar machen. Ausführbare Script-Dateien (ausführbar machen mit "chmod +x DATEI") in diesem Ordner sollten dann von überall aufrufbar sein, bspw. "spin_safety test.pml".

Viele Grüße,
Dominic
Dateianhänge
SPIN_convenience.tar.gz
spin_(safety|lifeness|guided|safety_noinvalidendstates)
(351 Bytes) 8-mal heruntergeladen

Zurück zu „Archiv“