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
8	    redLight = 1;
9	    do
10	       ::(redLight ==1) -> 
11			redLight = 0; 
12			yellowLight = 0; 
13			greenLight =1;
14	       ::(greenLight ==1) ->
15			redLight = 0; 
16			yellowLight = 1; 
17			greenLight =0;
18	       ::(yellowLight == 1) -> 
19			redLight = 1; 
20			yellowLight = 0; 
21			greenLight =0;
22	    od
23	}
24	
25	
26	init { 
27	  run simpleTrafficLight()
28	}

• มาดู Automata ครับ
  
• ทดสอบ Simulate
• ทดสอบ Vertification

Code ดูอ่านยาก เปลี่ยนไปใช้ Enum ดีกว่าครับ

1	mtype = { RED, YELLOW, GREEN } ;
2	
3	proctype SimpleTrafficLight() {
4	   mtype state = RED;
5	   do
6	      :: (state == RED) -> state = GREEN;
7	      :: (state == GREEN) -> state = YELLOW;
8	      :: (state == YELLOW) -> state = RED;
9	   od;
10	}
11	
12	init {
13	   run SimpleTrafficLight();
14	}

• มาดู Automata ครับ
  
• ทดสอบ Simulate
• ทดสอบ Vertification

ตอนนี้ได้รู้เรื่องเกี่ยวกับ Spin หลายเรื่องเลยครับ ^_^