Tag define

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

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