ช่วงนี้หลังจากทำ Term Project เกี่ยวกับระบบ Lift ผมเลยอยากจดไว้ก่อนว่าตัวโปรแกรม SPIN GUI ที่เขียนโดยภาษา Promela สามารถทวนสอบ Linear time Temporal Logic(LTL) ได้อย่างไรครับ โดยทำตามขั้นตอน ดังนี้ สิ่งที่ต้องมี ขั้นตอนการทวนสอบ LTL ใน Spin GUI หมายเหตุ: ในส่วนของการ #define ไม่ต้องใส่ ; ต่อท้าย
หลังจากเรียนทฤษฏีแล้ว ลงโปรแกรม แล้ว อ ให้ลองปฏิบัติจริงครับ โดยการลองใช้ตัว CPN มาเขียน Coloured Petri net ตาม Workshop แต่ละข้อครับ เกริ่นนำ Coloured Petri net ตัว Petri net เป็นการ Modeling(จำลอง) ระบบขึ้นมา เพื่อตรวจสอบเรื่อง Concurrent ครับ ส่วนประกอบ Workshop ที่ทำกันครับ ปัญหาที่เจอ หลักๆที่เจอเลย คือ ว่า Notebook ผมใช้ตัว CPN Tools เวอร์ชั่นล่าสุดไม่ได้ครับ
สำหรับ Blog นี้ หลังจากลอง Spin แบบมืนๆงงๆกันมาแล้ว คราวนี้มาลองลงตัว CPN Tools ซึ่งเป็นเครื่องมือสำหรับจัดการพวก Petri nets หรือ Colored Petri nets ครับ โดย Tools เป็นการพัฒนาด้วยภาษา Java ครับ มาเริ่มลงโปรแกรมกันดีกว่า ขั้นตอนการลงโปรแกรม สำหรับการลง CPN Tools ดูลงง่ายกว่าการลง SPIN ในครั้งก่อนเยอะครับ หรือว่า Tools ที่จำเป็นบางตัวมันลงไปแล้วตอนลง Spin โดยโปรแกรมนี้เป็น GUI แล้ววาดพวก Graph ครับ น่าจะดูง่ายและเข้าใจง่ายนะครับ (ความเห็นก่อนเรียนจริง ฮ่าๆ)…
วันนี้เรียนวิชา Formal เรื่อง Coloured Petri Net เห็นใน Slide มันเขียน n-tuple ซึ่งการเขียน n-turple กับ n turple มันสื่อความหมายต่างกันออกไปครับ โดยที่ ถ้ายังงงลองมาดูตัวอย่างเสริมกันครับ ถ้าใครอ่าน paper บ่อยๆ คำนี้ถูกใช้บ่อยมากครับ ดูเป็นศัพท์วิชาการมากกว่าคำว่า Column และ Record ครับ
ปัญหานี้มีผู้เชี่ยวชาญตรรกะ 3 คน เข้าไปกิน Beer ที่ร้าน พอเข้าไปในร้าน คำถาม คือ ทำไมผู้เชี่ยวชาญตรรกะคนสามตอบ Yes เค้ารู้ได้อย่างไรว่าอีก 2 คนจะกิน ฺBeer ด้วย คำตอบ คือ
สรุป Blog หลังจาก ได้ทำโจทย์ของอาจารย์ ในปัญหาที่ Classic ของสาขา Computer Science ครับ คือ ปัญหา Dinner Philosophers สำหรับปัญหานี้คิดโดยคุณ Edsger Dijkstra ในปี ค.ศ. 1965 ครับ ลองสังเกตุที่นามสกุลคนที่คิดครับ สำหรับคนที่เรียกวิชา Algorithm น่าจะคุ้นๆกันนะครับ Algorithm ที่ใช้แก้ปัญหา shortest paths ครับ กลับมาที่ปัญหานี้ดีกว่าครับ Dinner Philosophers ว่ามันสาระสำคัญอะไรครับ แล้วสร้างปัญหานี้มา เพื่ออะไรหละ
หลังจากเรียน 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
