SpinEdit - Simple Promela Interpreter

Ez az oldal a korábbi SCH wikiről lett áthozva.

Ha úgy érzed, hogy bármilyen formázási vagy tartalmi probléma van vele, akkor, kérlek, javíts rajta egy rövid szerkesztéssel!

Ha nem tudod, hogyan indulj el, olvasd el a migrálási útmutatót.

Telepítése (Windows)

1. Töltsd le a honlapon található három fájlt.
   (spin.zip, MinGW-2.0.0-3.exe, !ActiveTcl8.4.1.0-2-win32-ix86.exe)
2. Indítsd el a MinGW-2.0.0-3.exe Ez a CygWin készlet minimalizált változata. Ha van Cygwin-ed, akkor ezt nem kell feltenned.
   A telepítő mindenféle szokásos kérdést tesz fel, ezeket ajánlatos alapértelmezett értékeken hagyni.
3. Indítsd el az !ActiveTcl8.4.1.0-2-win32-ix86.exe-t! Ez egy Tcl/Tk környezet, és csak a SPIN grafikus részéhez kell. A telepítés során célszerű mindent az alapértelmezett értékeken hagyni.
4. A spin.zip-et csomagold ki egy tetszőleges könyvtárba! A program indítása az xpsin401.tcl állomány segítségével történik (grafikus felület), illetve a parancssoros verzió a spin.bat segítségével érhető el.
5. A PATH-hoz hozzá kell adni a MinGW bin alkönyvtárát.
   (alapeset: c:\minGW\bin)
   Win 9x és Me esetén: az autoxec.bat-ban
   Win 2K és XP esetén: a Control Panel\System\Advanced\Enviroment Variables-ben.
6. A spin424.exe átnevezése spin.exe -re.

LTL formula ellenőrzése

1. Lépj be a run/LTL property manager-be.
2. írd meg a define-okat a Symbol definitions-ba (egy processz lokális változójára processznév:valtozonev-el hivatkozhatsz). pl: #define p5 (OsszesHibas>0 )
3. Ezután felül a Formulához tudod írni az LTL kifejezést, amiben a definiált szimbólumokra hivatkozhatsz. pl: [] (((p5) -> (<> (p6))))
4. Aztán már csak egy Generate-t, majd egy Run-t kell nyomnod. (esetleg a set advanced options-ben keresési mélységet állítanod)

-- SoTi

-- adamo - 2006.03.17.