Install Spin – Formal Verification Tools

สำหรับใน Blog ตอนนี้ผมเน้นไปทางสาวกหน้าต่างนะครับ Microsoft Windows นะครับ สำหรับบันทึกการลง Spin ในวิชา Formal  Verification

เตรียมตัวก่อนลง

  • SPIN ผมลง 6.4.6 โดยผมสนใจ Full distribution, with sources ครับ
    • Spin - เป็น Core
    • iSpin - เป็น GUI เหมือนฝั่ง Java ก็จะเป็น jSpin
    • UPDATE ตั้งแต่ปี 2019 เวอร์ชั่น 6.5 ย้ายไป Tags · nimble-code/Spin (github.com)
  • Cygwin - ตัวที่ทำให้ใช้คำสั่ง Linux บน Windows ได้
  • Tcl/Tk - ทำให้เปิด iSpin ได้
  • Graphviz - เอาไว้ทำ Graph ถ้าสนใจแล้ว ไปดู Blog อีกตอนได้เลย
  • มี Internet ด้วยครับ ตัว Cygwin ผมให้มันไปหา Package จาก Internet ครับ
  • ตัว Setup บางตัวมี Version 32 bit กับ 64 bit ระวังด้วยนะ เป็นไปได้ให้ลงเหมือนๆกัน

ลง Cygwin

  • Double Click ลงเลยครับ
  • จำ Path ที่ลงไว้ครับ อย่างผมลงตัว 64 bits ที่ Path C:\cygwin64\bin
  • เลือก Category ในกลุ่ม Devel ครับ
  • ตอนลง Package สำคัญครับ โดยตัวที่ผมเลือก มีดังนี้
    • ต้องลง Package "gcc-core:GNU Compiler Collection (C,OpenMP)"
    • Mintty - เอาไว้ใช้ Cygwin Terminal
    • Make กับ bison(yacc) - เอามาบิ้ว
    • ตัว lex  ผมลงตาม Link ใน Reference ไม่รู้ว่าต้องใช้ไหม ลงเผื่ออนาคตก่อนครับ
  • เปิด Cygwin Terminal
    • ถ้ามี Error เกี่ยวกับ Mintty ลองไปคลิกขวาที่ Shortcut เติม .exe ลงไป ดังรูป
  • ก่อนไป Step ถัดไป มา Test ก่อนว่าใช้ได้ไหม ลองด้วย
gcc-version
  • ถ้าไม่มั่นใจ ดูตาม Wizard ที่ Capture ไว้ก่อนลงครับ

ทำให้ Cygwin ใช้กับ dos command

  • เราต้องเอาไป Cygwin ผูกใน Enviroment PATH
  • คลิกขวาที่ This PC (Window 10 ++) หรือ My Computer (Window XP, 7, 8) เลือก property
  • ไปที่ tab Advance >> Enviroment Variables
  • เพิ่ม Path ที่ผมลงไว้ตอนแรกนะครับ ซึ่งก็คือ C:\cygwin64\bin (ชอบหน้าจอการจัดการ Enviroment Variable ของ Window 10 ของ version เก่าๆนี่ดูยากมากกกกกกก) จากนั้นกด OK
  • Test โดยการเปิด Command Line Test gcc-version
  • ถ้าไม่ได้ทดสอบ โดยการ Logoff แล้ว Login แล้วลองใหม่อีกครั้ง

ลง SPIN

  • ผมสร้าง Folder C:\FV\Spin
  • แตกไฟล์ที่ Download มา อย่างของผมใช้ 6.4.6 เป็นไฟล์ชื่อ spin646.tar.gz
  • ผมใช้ 7-Zip แตกไฟล์ เอา tar กับ gz ออกไป
  • ข้างใน Folder มีโครงสร้างประมาณนี้
C:\FV\Spin
>> Spin
--->> Doc
--->> Examples
--->> iSpin
--->> Man
--->> Src6.4.6 (แล้วแต่เวอร์ชันที่ Download ครับ)
  • เปิด Cygwin Terminal จาก Path ข้างต้น C:\FV\Spin ให้พิมพ์คำสั่ง ดังนี้
//เข้าไปที Drive C
cd /cygdrive/c
//เข้าไปที่ FV/Spin
cd FV/Spin
//ตรวจว่าใช่ข้อมูลในโพลเดอร์ มี srcX.X.X หรือไม่ ด้วยคำสั่ง ls
ls 
//เตรียมเข้าไปที่ Source Code
cd Src6.4.6
//บิ้วโปรแกรม
make
  • เราสนใจที่ SRC บิ้วมันเลย ด้วยคำสั่ง make
    • ถ้าขึ้น make: yacc: Command not found แสดงว่าลง Package ไม่ครบ ให้ไปลง bison กับ make ด้วย
    • หรือ ถ้ามี Error ลองใช้คำสั่งนี้แทนครับ
yacc -v -d spin.y; cc -o spin *.c
  • จะได้ไฟล์ spin.exe
  • Add ทำให้มันใช้งานที่ไหนก็ได้ ด้วยคำสั่ง
cp spin.exe /usr/bin/spin.exe
  • ลอง Test ว่า Exe มันใช้ได้ไหม โดยลองเรียก spin ตรงๆ มันบอกเลข Version และบอกว่าเราใส่ Parameter ผิด ตามรูป

ลง ActiveTcl

  • คลิกขวา Run as Admin ก่อนครับ
  • ตั้งตามค่า Default ครับ
  • ถ้าไม่มั่นใจ ดูตาม Wizard ที่ Capture ไว้ก่อนลงครับ

ผูก iSpin

  • ตอนนี้ใน Cygwin เรามาสนใจที่ C:\FV\Spin\iSpin
  • เปิด GUI ได้นะ โดยการพิมพ์คำสั่ง
wish ispin.tcl หรือ wish86 ispin.tcl
  • ปรับให้สามารถ execute ได้ โดยใช้คำสั่ง
chmod +x ispin.tcl
  • ได้หน้าตา GUI มาแล้ว แต่ไม่รู้ว่าใช้ตัวเดียวกับที่ อาจารย์ใช้ หรือป่าว ?
  • ทำ Shortcut ไปที่ Desktop เผื่อเรียกใช้ง่ายๆ

ถ้ามีเวลาเพิ่มเติม ผมอยากลองลงกับตัว Ubuntu Sub-System ที่มากับ Windows10 นะครับ แต่ต้องทำ VM แยก คราวก่อนลอง Docker ไป คอมเปิดไม่ติดเลย 5555

Reference

Discover more from naiwaen@DebuggingSoft

Subscribe to get the latest posts sent to your email.

Tags

Related Posts