นี่คือคำสั่ง lpsinvelm ที่สามารถเรียกใช้ในผู้ให้บริการโฮสติ้งฟรีของ OnWorks โดยใช้หนึ่งในเวิร์กสเตชันออนไลน์ฟรีของเรา เช่น Ubuntu Online, Fedora Online, โปรแกรมจำลองออนไลน์ของ Windows หรือโปรแกรมจำลองออนไลน์ของ MAC OS
โครงการ:
ชื่อ
lpsinvelm - ตรวจสอบค่าคงที่และใช้สิ่งเหล่านี้เพื่อทำให้ง่ายขึ้นหรือขจัดผลรวมของ LPS
เรื่องย่อ
แอลซินเวลม์ [ทางเลือกที่]... --invfile=INVFILE [อินไฟล [ภายนอก]]
DESCRIPTION
ตรวจสอบว่าสูตรบูลีน (นิพจน์ข้อมูล mCRL2 ของการเรียงลำดับบูล) ระบุเป็น
ค่าคงที่คือค่าคงที่ของข้อกำหนดกระบวนการเชิงเส้น (LPS) ใน INFILE ถ้านี่คือ
กรณีเครื่องมือตัดผลรวมของ LPS ที่มีเงื่อนไขละเมิด
ค่าคงที่ และเขียนผลลัพธ์ไปที่ OUTFILE หากมี INFILE จะใช้ stdin ถ้า
ไม่มี OUTFILE ใช้ stdout
เครื่องมือนี้ยังสามารถใช้เพื่อทำให้เงื่อนไขของผลรวมของ LPS ที่กำหนดได้ง่ายขึ้น
OPTIONS
ทางเลือกที่ สามารถเป็นอย่างใดอย่างหนึ่งต่อไปนี้:
-y, --all-การละเมิด
อย่ายุติทันทีที่พบการละเมิดค่าคงที่เพียงครั้งเดียว แต่
รายงานการละเมิดทั้งหมดแทน
-c, --เคาน์เตอร์-ตัวอย่าง
แสดงการประเมินค่าที่ระบุว่าเหตุใดค่าคงที่อาจถูกละเมิดได้หากมัน
ไม่แน่ใจว่า summand ละเมิดค่าคงที่หรือไม่
-o, --การเหนี่ยวนำ
ใช้การเหนี่ยวนำในรายการ
-iไฟล์แนบ, --ไม่แปรเปลี่ยน=ไฟล์แนบ
ใช้สูตรบูลีน (นิพจน์ข้อมูล mCRL2 ของการเรียงลำดับบูล) ใน INVFILE เป็น
ค่าคงที่
-n, --no-ตรวจสอบ
อย่าตรวจสอบว่าค่าคงที่ถืออยู่ก่อนที่จะกำจัด summands ที่ไม่สามารถเข้าถึงได้
-e, --no-กำจัด
อย่าตัดทอนหรือลดความซับซ้อนของผลรวม แต่เพิ่มค่าคงที่ให้กับแต่ละเงื่อนไข
-pคำนำ, --พิมพ์จุด=คำนำ
บันทึกไฟล์ .dot ของผลลัพธ์ BDD หากไม่สามารถระบุได้ว่า a
summand ละเมิดค่าคงที่ PREFIX จะถูกใช้เป็นคำนำหน้าของไฟล์ที่ส่งออก
-QNUM, --qlimit=NUM
จำกัดการแจงนับของปริมาณเป็นตัวแปร NUM (ค่าเริ่มต้น NUM=1000, NUM=0 สำหรับ
ไม่ จำกัด).
-rชื่อ, --rewrite=ชื่อ
ใช้กลยุทธ์การเขียนใหม่ NAME: 'jitty' jitty rewrite (ค่าเริ่มต้น) 'jittyc' ที่คอมไพล์แล้ว
jitty rewrite 'jittyp' jitty เขียนใหม่พร้อมตัวพิสูจน์
-l, --simplify-ทั้งหมด
ลดความซับซ้อนของเงื่อนไขของ summands ทั้งหมด แทนที่จะเพียงแค่กำจัด summands
ซึ่งเงื่อนไขร่วมกับค่าคงที่นั้นขัดแย้งกัน
-zโซลเวอร์, --smt-ตัวแก้=โซลเวอร์
ใช้ SOLVER เพื่อลบเส้นทางที่ไม่สอดคล้องกันออกจาก BDD ที่ใช้ภายใน (โดยค่าเริ่มต้น
ไม่มีการใช้การกำจัดพาธ): 'cvc' ตัวแก้ไข SMT CVC3
-tLIMIT, --เวลาที่ จำกัด=LIMIT
ใช้เวลาไม่เกิน LIMIT วินาทีในการพิสูจน์สูตรเดียว
--กำหนดเวลา[=ไฟล์]
ผนวกการวัดเวลาเข้ากับ FILE การวัดจะถูกเขียนไปยังข้อผิดพลาดมาตรฐาน if
ไม่มีไฟล์ให้
ตัวเลือกมาตรฐาน:
-q, --เงียบ
ไม่แสดงข้อความเตือน
-v, --รายละเอียด
แสดงข้อความกลางสั้นๆ
-d, --debug
แสดงข้อความระดับกลางโดยละเอียด
--log-ระดับ=ระดับ
แสดงข้อความระดับกลางถึงและรวมถึงระดับ
-h, --ช่วยด้วย
แสดงข้อมูลช่วยเหลือ
--รุ่น
แสดงข้อมูลรุ่น
ใช้ lpsinvelm ออนไลน์โดยใช้บริการ onworks.net