หลังจากเรียน 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 และตัว Graphviz (เพิ่งรู้ว่ามันเอามาช่วย Spin ทำพวก Automata) มาลองเขียนโปรแกรมกันเลย ก่อนอาจารย์สอนพรุ่งนี้อีกที แปะ Code ไว้ก่อนนะครับ init{ printf(“Hello world \n Promela \n”); } สำหรับผลลัพธ์ก็ตามนี้ครับ เข้าสู่โลกของ Formal Verification ไปอีกขั้น
หลังจากตอนที่แล้วได้ลง Spin มาแล้ว แต่ผมเหลือบในเห็นใน List ของ Tools ที่จำเป็นในวิชา Formal Verification เห็นมีลง Graphviz ด้วย ผมเลยเอามาเขียนอีก Blog แยกดีกว่าครับ เตรียมตัวก่อนลง ลง Graphviz ทำให้ Graphviz ใช้กับ dos command ทดสอบ Graphviz ผูก iSpin Reference
สำหรับใน Blog ตอนนี้ผมเน้นไปทางสาวกหน้าต่างนะครับ Microsoft Windows นะครับ สำหรับบันทึกการลง Spin ในวิชา Formal Verification เตรียมตัวก่อนลง ลง Cygwin ทำให้ Cygwin ใช้กับ dos command ลง SPIN ลง ActiveTcl ผูก iSpin ถ้ามีเวลาเพิ่มเติม ผมอยากลองลงกับตัว Ubuntu Sub-System ที่มากับ Windows10 นะครับ แต่ต้องทำ VM แยก คราวก่อนลอง Docker ไป คอมเปิดไม่ติดเลย 5555 Reference
