หลังจากเรียน Lecture มาพักใหญ่คราวนี้ อาจารย์ได้ให้ลองเขียน Promela บน Spin โดยให้จำลองการทำงานของไฟจราจรขึ้นมาครับ มันดูไม่น่ายากนะ ลองเขียน Code เลย ได้ Version แรกมาแล้วครับ 1 int redLight = 0; 2 int yellowLight = 0; 3 int greenLight = 0; 4 5 proctype simpleTrafficLight() 6 { 7 //Start with redLight…
หลังจากตอนที่แล้วได้ลง Spin มาแล้ว แต่ผมเหลือบในเห็นใน List ของ Tools ที่จำเป็นในวิชา Formal Verification เห็นมีลง Graphviz ด้วย ผมเลยเอามาเขียนอีก Blog แยกดีกว่าครับ เตรียมตัวก่อนลง Graphviz – สำหรับบน Windows จะลงตัว Installer (.msi) หรือ .zip แต่ถ้าอยากใช้ผ่าน Command Line ได้ ต้อง Add PATH Variable เองครับ ลง Graphviz ถ้าเป็น Installer (.msi) ลงตามขั้นตอนเลยครับ จำ Path…
สำหรับใน 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)…
