นี่คือโมนาคำสั่งที่สามารถเรียกใช้ในผู้ให้บริการโฮสต์ฟรีของ OnWorks โดยใช้เวิร์กสเตชันออนไลน์ฟรีของเรา เช่น Ubuntu Online, Fedora Online, โปรแกรมจำลองออนไลน์ของ Windows หรือโปรแกรมจำลองออนไลน์ของ MAC OS
โครงการ:
ชื่อ
mona - ขั้นตอนการตัดสินใจสำหรับลอจิก WS1S และ WS2S
เรื่องย่อ
mona [ ตัวเลือก ] ไฟล์ mona
DESCRIPTION
MONA เป็นเครื่องมือที่แปลสูตรในลอจิก WS1S หรือ WS2S เป็น finite-state
ออโตมาตะแสดงโดย BDD สูตรอาจแสดงรูปแบบการค้นหาชั่วคราว
คุณสมบัติของระบบปฏิกิริยา การแยกวิเคราะห์ข้อจำกัดต้นไม้ ฯลฯ MONA ยังวิเคราะห์
หุ่นยนต์ที่เกิดจากการรวบรวมและกำหนดว่าสูตรถูกต้องหรือไม่และ
หากสูตรไม่ถูกต้อง ให้สร้างตัวอย่างที่ขัดแย้ง
โครงการ MONA เป็นโครงการวิจัยที่ Department of Computer Science, Aarhus
มหาวิทยาลัย
เอกสารฉบับเต็ม ซอร์สโค้ด GPL และเอกสารการวิจัยที่เกี่ยวข้องมีให้จาก
หน้าแรกของโครงการ MONA ที่ http://www.brics.dk/mona
OPTIONS
-w ส่งออกทั้งหุ่นยนต์ ค่าเริ่มต้นคือการส่งออกขนาดเท่านั้น
-n อย่าวิเคราะห์หุ่นยนต์ ค่าเริ่มต้นคือการวิเคราะห์ความถูกต้องและไม่น่าพอใจ
และเพื่อสร้างตัวอย่างและตัวอย่างที่น่าพึงพอใจ
-t พิมพ์เวลาที่ผ่านไปสำหรับแต่ละเฟส หากใช้ -s เวลาสำหรับหุ่นยนต์แต่ละตัว
พิมพ์การดำเนินการด้วย
-s สถิติการพิมพ์ พิมพ์ข้อมูลสำหรับการทำงานของหุ่นยนต์แต่ละรายการและสรุป
-i พิมพ์ออโตมาตาระดับกลาง (หมายถึง -s)
-d Dump AST, symboltable และรหัส DAG มีประโยชน์สำหรับการดีบัก
-q เงียบ ไม่ต้องพิมพ์คืบหน้า
-e เปิดใช้งานการรวบรวมแยกต่างหาก (ดูตัวแปรสภาพแวดล้อม MONALIB ด้านล่าง)
-oN ระดับการเพิ่มประสิทธิภาพโค้ด N (0=ไม่มี, 1=ปลอดภัย, 2=ฮิวริสติก) (ค่าเริ่มต้น 1)
-r ปิดใช้งานการจัดลำดับดัชนี BDD ใหม่ ใช้ลำดับการประกาศเป็นลำดับดัชนี ค่าเริ่มต้น
คือการจัดลำดับดัชนี BDD ใหม่โดยศึกษาแบบสำนึก
-f บังคับรูปแบบเอาต์พุตโหมดต้นไม้ปกติ ใช้ได้กับโหมด WSRT เท่านั้น
-m การจำลองทางเลือก M2L-Str (รูปแบบ v1.3)
-h เปิดใช้งานการวิเคราะห์การยอมรับที่สืบทอดมา
-u ไม่จำกัดเอาท์พุตออโตมาตา สร้างออโตมาตาธรรมดาโดยแปลง "ไม่สนใจ"
ระบุว่าจะ "ปฏิเสธ" สถานะและย่อให้เล็กสุด
-gw เอาต์พุตอัตโนมัติทั้งหมดในรูปแบบ Graphviz (หมายถึง -n -q) (Graphviz สามารถใช้ได้
at http://www.graphviz.org/)
-gs เอาต์พุตต้นไม้ตัวอย่างที่น่าพอใจในรูปแบบ Graphviz (หมายถึง -q)
-gc เอาต์พุตตัวอย่างเคาน์เตอร์ในรูปแบบ Graphviz (หมายถึง -q)
-gd Dump code DAG ในรูปแบบ Graphviz (หมายถึง -n -q)
-xw ส่งออกออโตมาทั้งหมดในรูปแบบภายนอก (หมายถึง -n -q) "รูปแบบภายนอก" คือ
รูปแบบที่ใช้โดย dfalib และ gtalib ดูแพ็คเกจต้นทาง
และพวกเรา
โมนาลิบ
กำหนดไดเร็กทอรีที่ใช้สำหรับการคอมไพล์ออโตมาตาแยกกัน (ค่าเริ่มต้นคือปัจจุบัน
ไดเร็กทอรี)
ใช้ mona ออนไลน์โดยใช้บริการ onworks.net
