"Convenience-Scripts" für typische SPIN Use Cases
Verfasst: 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
hinzu. Danach entweder System neustarten oder mit
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
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
Code: Alles auswählen
. ~/.profileViele Grüße,
Dominic