มาลองเล่น TLA+ กันเถอะ
We can’t get systems right if we don’t understand them — Leslie Lamport
tla+ เป็นภาษาที่ทำงานด้วยหลักการ state machine
ซึ่งต่างจากการทำงานของภาษาอื่นๆที่เราใช้ในปัจจุบัน
เช่นจากโปรแกรมภาษา c อันนี้
เราจะวาดโปรแกรมออกมาในลักษณะ state machine ได้ยังไง ?
โดยหลักการในการเขียน state machine คือ
- ระบุตัวแปรทั้งหมด
- ระบุค่าเริ่มต้นที่เป็นไปได้ของตัวแปร
- ระบุความสัมพันธ์ระหว่าง ค่าของตัวแปรใน state นี้ และ ค่าที่เป็นไปได้ของตัวแปรใน state หน้า
โอเค มาเริ่มกันทีละบรรทัด
- ระบุตัวแปรทั้งหมด => i, pc (เราจะมาอธิบาย pc กันภายหลัง)
- ค่าเริ่มต้นที่เป็นไปได้ของตัวแปร => ใน c เมื่อประกาศ int จะมีค่าเริ่มต้นเป็น 0 ดังนั้น i = 0, pc = “start” (เราจะอธิบายภายหลังเช่นกัน)
- ความสัมพันธ์ระหว่างค่าใน state นี้ และ ค่าที่เป็นไปได้ใน state หน้า =>
โอเค ในขั้นนี้ เราจะมาใช้ pc กันละ
โดย pc จะใช้กำหนดเฟสของการ assign ตัวแปร
เช่น
pc = start แสดงว่าในเฟสหน้า การ assign ค่าตัวแปรครั้งแรกจะเกิดขึ้น
pc = middle แสดงว่าในเฟสหน้า การ assign ค่าตัวแปรครั้งต่อไปจะเกิดขึ้น
pc = done แสดงว่าโปรแกรมทำงานเสร็จแล้ว
โอเค มาเริ่มระบุความสัมพันธ์ของค่าในแต่ละ state กัน
ในบรรทัดแรกถ้า pc = start
- ค่าที่เป็นไปได้ของ i คือค่าที่ return จาก someNumber ซึ่งอยู่ในช่วง 0–1000
- ค่าของ pc จะเปลี่ยนเป็น middle
จากนั้นเมื่อ pc เป็น middle
- ค่าของ i คือ ค่าของ i ปัจจุบัน + 1
- ค่าของ pc เปลี่ยนเป็น done
จากนั้นเมื่อ pc เป็น done แสดงว่าไม่มี state ต่อไป และโปรแกรมจบการทำงาน
โอเค มาลองเขียนเป็น diagram กัน
โอเค แต่ว่าเราจะเอาไปเขียนเป็น state machine ให้คอมเข้าใจได้ยังไง ?
เหมือนว่าจะต้องแปลงเป็น math model ก่อน
มาลองดูกัน
กลับมาดูที่วิธีการในการเขียน state machine
- ระบุตัวแปรทั้งหมด
- ค่าเริ่มต้นที่เป็นไปได้ของตัวแปร
- ความสัมพันธ์ระหว่างค่าใน state นี้ และ ค่าที่เป็นไปได้ใน state หน้า
โอเค
ระบุตัวแปรทั้งหมด และ ค่าเริ่มต้นที่เป็นไปได้ของตัวแปร
ก่อนหน้านี้เราเขียนเป็นประโยคตรงๆประมาณนี้
ถ้าแปลงเป็น math model จะได้เป็น
ความสัมพันธ์ระหว่างค่าใน state นี้ และ ค่าที่เป็นไปได้ใน state หน้า
จริงๆก่อนหน้านี้เราได้ทำขั้นนี้โดยออกมาเป็นประโยคประมาณนี้
ถ้าเราแทนคำด้วยสัญลักษณ์ไปเรื่อยๆ จะได้แบบนี้
โอเค การแปลงเป็น math symbol จบละ
ต่อมาจะทำการ รวมการแปลง state เข้าด้วยกัน เนื่องจากทำพร้อมกันอยู่แล้ว
ตอนนี้โปรแกรมจะกลายเป็น math model เต็มตัวแล้ว
นั่นหมายความว่า
เราจะมองโปรแกรมเป็นสมการนึง ไม่ใช่ การทำงานแบบ sequence อีกแล้ว
เช่น
จากสมการ
ค่าเหล่านี้เป็นจริง
ยังไง ?
เมื่อ pc เป็น start แสดงว่า state ต่อไปคือ then i in 0..100 ^ pc` = middle
ซึ่งก็เป็นจริง
แต่ถ้าเราลองมาดูค่าที่ทำให้ math formula เป็น false บ้าง
เนื่องจาก pc = middle ดังนั้น state ต่อไปของโปรแกรมจะอยู่ในวงสีฟ้า
โดยเราจะพบว่าใน state ต่อไป i` ควรเป็น 535 ซึ่งค่า i` ในรูปผิดอยู่
ดังนั้นด้วยโปรแกรมนี้ state นี้เป็นไปไม่ได้
โอเค เราเข้าใจเรื่อง state และ ค่าที่เป็นไปได้ใน state ละ
แล้ว no next values หรือจุดที่โปรแกรมควร terminate ควรจะเขียนเป็น math formula ยังไงดี ?
เอาตรงๆ หาวิธีอธิบายลำบากแหะ
เอาเป็นว่า ในจุดที่โปรแกรม terminate tla+จะใช้คำว่า FALSE
สุดท้าย เปลี่ยนคำสั่งเป็นพิมพ์ใหญ่ให้หมด
จริงๆแล้วอันนี้ยังไม่ใช่ syntax tla+ ซะทีเดียว เพราะ ^ และ in ยังไม่อยู่ในตาราง ascii
โดยเราจะแปลงเครื่องหมายทั้งหมดเป็น ascii
โอเค เราได้ math formula ละ
แล้วเราจะแปลงเป็นภาษา tla+ ได้ยังไง ?
ก่อนอื่นเพื่อให้ง่ายมาทำเป็น block ใหญ่ๆกันก่อน
จากนั้น จาก math formula เราเนี่ย เราจะมองเป็นก้อน boolean
โดย IF THEN กับ ELSE IF THEN จะมองเป็นก้อนเดียวกัน
ส่วน ELSE จะเป็นก้อนแยก
ซึ่งวิธีการทำให้ math formula เป็นจริง จะเหลือแค่ 2 ก้อน ตามรูป
ดังนั้นเราสามารถเริ่มได้ที่ pc = start หรือ pc = middle อย่างใดอย่างหนึ่ง
เราสามารถแปลงเป็นภาษา tla+ โดยให้ในก้อนเดียวกันใช้ and และ ต่างก้อนกันใช้ or ได้ตามรูป
โอเค เอา IF ELSE IF ELSE ออกละ
ต่อมาแปลง A B กลับเป็น math formula
การนำวงเล็บออก ให้ใช้ logic operator เดียวกันกับข้างในมาต่อข้างหน้า
โดยภาษา tla+ จะใช้ space ข้างหน้าในการแบ่งวงเล็บ ดังนั้นเพื่อครอบวงเล็บนอกสุดเราจะใช้หลักการเดียวกันคือใส่ logic operator เดียวกันกับข้างในมาต่อข้างหน้า
โอเค ถ้าเรารวม part ต่างๆเข้าด้วยกันจะได้ดังนี้
- ระบุตัวแปรทั้งหมด
- ค่าเริ่มต้นที่เป็นไปได้ของตัวแปร
- ความสัมพันธ์ระหว่างค่าใน state นี้ และ ค่าที่เป็นไปได้ใน state หน้า
และเมื่อนำไปเขียนเป็นภาษา tla+ เต็มๆจะได้เป็น
โอเค ซึ่งเราสามารถทำการ reuse code โดยประกาศชื่อแทน logic ก้อนต่างๆได้
โอเค code เสร็จละ มารันกัน
ก่อนรันต้องมี ide ก่อน
ลง vscode extension
ลง java และ set path
โอเค จาก code
การ compile ใช้คำสั่ง parse module
จากนั้นแปลง spec เป็น tlc โดยใช้คำสั่ง check model
โดยจะมี error ให้สร้างไฟล์ model ก็กดสร้างตามนั้น
โดยไฟล์ model เอาไว้กำหนด syntax ที่ใช้ในไฟล์ spec นั่นเอง
โดยเมื่อรัน model จะพบ error deadlock
ซึ่งแปลว่าพอไปถึง done ก็จะไม่มี state ต่อไปให้ไปนั่นเอง
ซึ่งเพื่อให้ model checker เข้าใจว่าเราอยาก terminate program ต้องตั้งค่าไม่ให้เช็ค deadlock เพิ่ม
โอเค รันผ่านละ
โอเค การสร้าง model ด้วย tla+ จะประมาณนี้ โดยเราจะนำ model นี้ไปพิสูจน์การทำงานผ่าน formal proof ต่อไปนั่นเอง
Referrences
https://lamport.azurewebsites.net/video/video1.html
https://lamport.azurewebsites.net/video/video2.html
https://lamport.azurewebsites.net/video/video3.html
