ช่วงนี้หลังจากทำ Term Project เกี่ยวกับระบบ Lift ผมเลยอยากจดไว้ก่อนว่าตัวโปรแกรม SPIN GUI ที่เขียนโดยภาษา Promela สามารถทวนสอบ Linear time Temporal Logic(LTL) ได้อย่างไรครับ โดยทำตามขั้นตอน ดังนี้ สิ่งที่ต้องมี Promela Code – ที่เขียน Model ที่ต้องการทวนสอบ LTL – ชุดคำสั่งที่ให้สำหรับการทวนสอบ ว่า Model เรามีคุณลักษณะที่ต้องการ หรือป่าว ขั้นตอนการทวนสอบ LTL ใน Spin GUI ทำการเขียนคำสั่ง LTL ตัวอย่าง…
หลังจากเรียนทฤษฏีแล้ว ลงโปรแกรม แล้ว อ ให้ลองปฏิบัติจริงครับ โดยการลองใช้ตัว CPN มาเขียน Coloured Petri net ตาม Workshop แต่ละข้อครับ เกริ่นนำ Coloured Petri net ตัว Petri net เป็นการ Modeling(จำลอง) ระบบขึ้นมา เพื่อตรวจสอบเรื่อง Concurrent ครับ ส่วนประกอบ Place Transition Token Arc Workshop ที่ทำกันครับ Dinner philosopher Simple Protocal Order Online ปัญหาที่เจอ หลักๆที่เจอเลย คือ ว่า Notebook…
สำหรับ Blog นี้ หลังจากลอง Spin แบบมืนๆงงๆกันมาแล้ว คราวนี้มาลองลงตัว CPN Tools ซึ่งเป็นเครื่องมือสำหรับจัดการพวก Petri nets หรือ Colored Petri nets ครับ โดย Tools เป็นการพัฒนาด้วยภาษา Java ครับ มาเริ่มลงโปรแกรมกันดีกว่า ขั้นตอนการลงโปรแกรม Download ตัวโปรแกรมมากันก่อนเลยครับ จาก สำหรับผมใช้ Windows ครับ กด Next ยาวๆไปครับ ดูรูปได้จาก Gallery ครับ ลองเปิดโปรแกรมดูครับ ถ้าไม่ขึ้นต้องลอง Set JAVA_HOME ครับ…
วันนี้เรียนวิชา Formal เรื่อง Coloured Petri Net เห็นใน Slide มันเขียน nine-tuple ซึ่งการเขียน n-turple กับ n turple มันสื่อความหมายต่างกันออกไปครับ โดยที่ n-turple หมายถึง จำนวน Element ของในแต่ละ tuple n turple หมายถึง จำนวนของ tuple ถ้ายังงงลองมาดูตัวอย่างเสริมกันครับ จากรูป n-turple = 3 แต่ n turple = 12 ถ้าใครอ่าน paper บ่อยๆ คำนี้ถูกใช้บ่อยมากครับ…
ปัญหานี้มีผู้เชี่ยวชาญตรรกะ 3 คน เข้าไปกิน Beer ที่ร้าน พอเข้าไปในร้าน พนักงานเสิร์ฟ : ทุกๆคน รับ Beer ไหม ผู้เชี่ยวชาญตรรกะคนแรก : ฉันไม่รู้ ผู้เชี่ยวชาญตรรกะคนสอง : ฉันไม่รู้ ผู้เชี่ยวชาญตรรกะคนสาม : ใช่เลยยยยย คำถาม คือ ทำไมผู้เชี่ยวชาญตรรกะคนสามตอบ Yes เค้ารู้ได้อย่างไรว่าอีก 2 คนจะกิน ฺBeer ด้วย คำตอบ คือ ผู้เชี่ยวชาญตรรกะคนแรก ไม่ชัวร์ว่า 2 คนจะกินไหมเลยตอบ I don’t know ผู้เชี่ยวชาญตรรกะคนสอง รู้เลยว่าคนแรกกินเบียร์…
หลังจากเรียน 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 – สำหรับบน 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)…
