Tag Promela

[FV] ลองใช้ LTL ใน Promela

ช่วงนี้หลังจากทำ Term Project เกี่ยวกับระบบ Lift ผมเลยอยากจดไว้ก่อนว่าตัวโปรแกรม SPIN GUI ที่เขียนโดยภาษา Promela สามารถทวนสอบ Linear time Temporal Logic(LTL) ได้อย่างไรครับ โดยทำตามขั้นตอน ดังนี้ สิ่งที่ต้องมี Promela Code – ที่เขียน Model ที่ต้องการทวนสอบ LTL – ชุดคำสั่งที่ให้สำหรับการทวนสอบ ว่า Model เรามีคุณลักษณะที่ต้องการ หรือป่าว ขั้นตอนการทวนสอบ LTL ใน Spin GUI ทำการเขียนคำสั่ง LTL ตัวอย่าง…

Spin: Simple Traffic Light

หลังจากเรียน 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…