lpsconfcheck - ออนไลน์ใน Cloud

โครงการ:

ชื่อ

lpsconfcheck - ทำเครื่องหมายการรวม tau-summands ของ LPS

เรื่องย่อ

lpsconfcheck [ทางเลือกที่-อินไฟล [ภายนอก]]

DESCRIPTION

ตรวจสอบว่าผลรวมเอกภาพใดของ mCRL2 LPS ใน INFILE ที่บรรจบกัน ทำเครื่องหมายด้วยการเปลี่ยนชื่อ
ไปที่ ctau และเขียนผลลัพธ์ไปที่ OUTFILE ถ้า INFILE ไม่มีอยู่ stdin จะถูกใช้ ถ้า
ไม่มี OUTFILE ใช้ stdout

OPTIONS

ทางเลือกที่ สามารถเป็นอย่างใดอย่างหนึ่งต่อไปนี้:

-a, -- ตรวจสอบทั้งหมด
ตรวจสอบการบรรจบกันของ tau-summands เกี่ยวกับ summand อื่น ๆ ทั้งหมดแทน
ดำเนินการต่อด้วย tau-summand ถัดไปทันทีที่พบ summand นั่นคือ
ไม่บรรจบกับ tau-summand . ในปัจจุบัน

-c, --เคาน์เตอร์-ตัวอย่าง
แสดงการประเมินมูลค่าที่ไม่มีเงื่อนไขการบรรจบกันในกรณีที่
เงื่อนไขที่พบไม่ขัดแย้งหรือtautolgy

-g, --สร้างค่าคงที่
พยายามพิสูจน์ว่าเงื่อนไขการบรรจบกันที่ลดลงนั้นเป็นค่าคงที่ของ LPS ใน
กรณีที่เงื่อนไขการบรรจบกันไม่ใช่เรื่องซ้ำซาก

-o, --การเหนี่ยวนำ
ใช้การเหนี่ยวนำในรายการ

-iไฟล์แนบ, --ไม่แปรเปลี่ยน=ไฟล์แนบ
ใช้สูตรบูลีน (นิพจน์ข้อมูล mCRL2 ของการเรียงลำดับบูล) ใน INVFILE เป็น
ค่าคงที่

-n, --no-ตรวจสอบ
อย่าตรวจสอบว่าค่าคงที่ถือก่อนตรวจสอบการบรรจบกันหรือไม่

-m, --ไม่มีเครื่องหมาย
อย่าทำเครื่องหมายจุดรวม tau-summands; เนื่องจากไม่มีการเปลี่ยนแปลงใดๆ กับ LPS
ไม่มีอะไรเขียนถึง OUTFILE

-pคำนำ, --พิมพ์จุด=คำนำ
บันทึกไฟล์ .dot ของ BDD ที่เป็นผลลัพธ์ ในกรณีที่ไม่สามารถพิสูจน์ผลรวมสองผลได้
มาบรรจบกัน; PREFIX จะถูกใช้เป็นคำนำหน้าของไฟล์ที่ส่งออก

-QNUM, --qlimit=NUM
จำกัดการแจงนับของปริมาณเป็นตัวแปร NUM (ค่าเริ่มต้น NUM=1000, NUM=0 สำหรับ
ไม่ จำกัด).

-rชื่อ, --rewrite=ชื่อ
ใช้กลยุทธ์การเขียนใหม่ NAME: 'jitty' jitty rewrite (ค่าเริ่มต้น) 'jittyc' ที่คอมไพล์แล้ว
jitty rewrite 'jittyp' jitty เขียนใหม่พร้อมตัวพิสูจน์

-zโซลเวอร์, --smt-ตัวแก้=โซลเวอร์
ใช้ SOLVER เพื่อลบเส้นทางที่ไม่สอดคล้องกันออกจาก BDD ที่ใช้ภายใน (โดยค่าเริ่มต้น
ไม่มีการใช้การกำจัดพาธ): 'cvc' ตัวแก้ไข SMT CVC3

-sNUM, --สรุป=NUM
ขจัดหรือลดความซับซ้อนของผลรวมด้วยหมายเลข NUM เท่านั้น

-tLIMIT, --เวลาที่ จำกัด=LIMIT
ใช้เวลาไม่เกิน LIMIT วินาทีในการพิสูจน์สูตรเดียว

--กำหนดเวลา[=ไฟล์]
ผนวกการวัดเวลาเข้ากับ FILE การวัดจะถูกเขียนไปยังข้อผิดพลาดมาตรฐาน if
ไม่มีไฟล์ให้

ตัวเลือกมาตรฐาน:

-q, --เงียบ
ไม่แสดงข้อความเตือน

-v, --รายละเอียด
แสดงข้อความกลางสั้นๆ

-d, --debug
แสดงข้อความระดับกลางโดยละเอียด

--log-ระดับ=ระดับ
แสดงข้อความระดับกลางถึงและรวมถึงระดับ

-h, --ช่วยด้วย
แสดงข้อมูลช่วยเหลือ

--รุ่น
แสดงข้อมูลรุ่น

ใช้ lpsconfcheck ออนไลน์โดยใช้บริการ onworks.net