นี่คือคำสั่ง lbt2dot ที่สามารถเรียกใช้ในผู้ให้บริการโฮสต์ฟรีของ OnWorks โดยใช้เวิร์กสเตชันออนไลน์ฟรีของเรา เช่น Ubuntu Online, Fedora Online, โปรแกรมจำลองออนไลน์ของ Windows หรือโปรแกรมจำลองออนไลน์ของ MAC OS
โครงการ:
ชื่อ
lbt - LTL เป็น Büchi นักแปล
เรื่องย่อ
ปอนด์ < สูตร.txt > automaton.txt
ปอนด์ 2 ดอท < automaton.txt > automaton.dot
DESCRIPTION
หน้าคู่มือนี้จัดทำเอกสารโดยสังเขปเกี่ยวกับ ปอนด์ และ ปอนด์ 2 ดอท คำสั่ง หน้าคู่มือนี้เคยเป็น
เขียนขึ้นเพื่อการแจกจ่าย Debian GNU/Linux เนื่องจากโปรแกรมดั้งเดิมไม่มี a
หน้าคู่มือ แต่มีเอกสารในรูปแบบ HTML แทน ดูด้านล่าง
ปอนด์ เป็นตัวกรองที่แปลสูตรตรรกะเวลาเชิงเส้น (LTL) เป็นค่าที่สอดคล้องกัน
หุ่นยนต์Büchiทั่วไป การแปลจะขึ้นอยู่กับอัลกอริทึมของ Gerth, Peled
และ Vardi นำเสนอที่ PSTV'95 ง่าย ในขณะที่บิน อัตโนมัติ การตรวจสอบ of เชิงเส้น
ชั่วขณะ ตรรกะ. แทบไม่มีการเพิ่มประสิทธิภาพใด ๆ และหุ่นยนต์ที่สร้างขึ้นคือ
มักจะใหญ่กว่าความจำเป็น แต่ในทางกลับกัน มันควรจะถูกต้องเสมอ
ตัวกรอง ปอนด์ 2 ดอท สามารถใช้ในการแปล Büchi automata จาก ปอนด์ รูปแบบเอาต์พุต to
รูปแบบ GraphViz สำหรับการแสดงภาพ
ตัวอย่าง
เสียงสะท้อน ก พี0 | ปอนด์ | ปอนด์ 2 ดอท | ขี้หลงขี้ลืม -
ใช้ lbt2dot ออนไลน์โดยใช้บริการ onworks.net