มาแก้ puzzle จาก die hard 3 ด้วย formal verification กัน Water puzzle คืออะไร ? เป็นปัญหาที่ว่าด้วยถ้าเรามีแกลลอนน้ำ 2 ใบ คือ 3 ลิตร และ 5 ลิตร (เป็นแกลลอนเปล่าทั้งคู่) เราจะสามารถทำให้แกลลอน 5 ลิตร มีน้ำ 4 ลิตร เป๊ะๆได้หรือไม่ โดยกำหนดสิ่งที่สามารถทำได้คือ เทน้ำใส่แกลลอน 3 ลิตรจนเต็ม เทน้ำใส่แกลลอน 5 ลิตรจนเต็ม เทน้ำจากแกลลอน 3 ลิตร ใส่แกลลอน 5 ลิตร จนแกลลอน 5 ลิตรเต็ม เทน้ำจากแกลลอน 5 ลิตร ใส่แกลลอน 3 ลิตร จนแกลลอน…