lpsinvelm - ออนไลน์ในคลาวด์

โครงการ:

ชื่อ

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