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

โครงการ:

ชื่อ

lps2lts - สร้าง LTS จาก LPS

เรื่องย่อ

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

DESCRIPTION

สร้าง LTS จาก LPS ใน INFILE และบันทึกผลลัพธ์ไปที่ OUTFILE ถ้า INFILE ไม่ใช่
ให้มา ใช้ stdin หากไม่ได้ระบุ OUTFILE ระบบจะไม่จัดเก็บ LTS

หากใช้ตัวเขียนใหม่ 'jittyc' แสดงว่าตัวแปรสภาพแวดล้อม MCRL2_COMPILEREWRITER
(ค่าเริ่มต้น: 'mcrl2compilerewriter') กำหนดสคริปต์ที่คอมไพล์ตัวเขียนใหม่
และ MCRL2_COMPILEDIR (ค่าเริ่มต้น: '.') กำหนดตำแหน่งที่เก็บไฟล์ชั่วคราว

โปรดทราบว่า lps2lts สามารถส่งทรานซิชันได้หลายแบบโดยใช้ป้ายกำกับเดียวกันระหว่างคู่ของ
รัฐ หากไม่ต้องการ การเปลี่ยนแปลงดังกล่าวสามารถลบออกได้โดยใช้สัญลักษณ์ที่แข็งแกร่ง
การลดระดับทวิตอนโดยใช้เครื่องมือ ltsconvert

รูปแบบของ OUTFILE ถูกกำหนดโดยส่วนขยาย (เว้นแต่จะระบุโดย an
ตัวเลือก). รูปแบบที่รองรับคือ:

'aut' สำหรับรูปแบบ Aldebaran (CADP)
'dot' สำหรับรูปแบบ GraphViz (ไม่รองรับรูปแบบอินพุตอีกต่อไป)
'fsm' สำหรับรูปแบบ Finite State Machine หรือ
'lts' สำหรับรูปแบบ mCRL2 LTS หากใช้ตัวเขียนใหม่ jittyc แสดงว่า
ตัวแปรสภาพแวดล้อม MCRL2_COMPILEREWRITER (ค่าเริ่มต้น: mcrl2compilerewriter)
กำหนดสคริปต์ที่คอมไพล์ตัวเขียนใหม่และ MCRL2_COMPILEDIR (ค่าเริ่มต้น:
'.') กำหนดตำแหน่งที่เก็บไฟล์ชั่วคราว โปรดทราบว่า lps2lts สามารถส่งได้หลายรายการ
การเปลี่ยนผ่านด้วยป้ายกำกับเดียวกันระหว่างรัฐคู่ใดๆ หากไม่เป็นที่ต้องการ เช่น
การเปลี่ยนแปลงสามารถลบออกได้โดยใช้การลด bisimulation ที่แข็งแกร่งโดยใช้ตัวอย่างเช่น
เครื่องมือ ltsconvert

OPTIONS

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

-aชื่อ, --การกระทำ=ชื่อ
ตรวจจับและรายงานการดำเนินการในระบบการเปลี่ยนที่มีชื่อการดำเนินการจาก
NAMES รายการที่คั่นด้วยเครื่องหมายจุลภาค ตัวอย่างเช่นมีประโยชน์ในการค้นหา (หรือพิสูจน์
ไม่มี) ข้อผิดพลาดในการดำเนินการ มีการพิมพ์ข้อความสำหรับทุกเหตุการณ์ของ
ชื่อการกระทำเหล่านี้ ด้วยแฟล็ก -t การติดตามการกระทำเหล่านี้จะถูกสร้างขึ้น

-b[NUM], --บิต-แฮช[=NUM]
ใช้การแฮชบิตเพื่อจัดเก็บสถานะและจัดเก็บได้ไม่เกิน NUM สถานะ หมายความว่า
แทนที่จะเก็บบันทึกสถานะทั้งหมดที่เคยเยี่ยมชม บิต array
ถูกใช้เพื่อบ่งชี้ว่า hash of a state เคยเห็นมาก่อนหรือไม่
แม้ว่านี่หมายความว่าตัวเลือกนี้อาจทำให้สถานะผิดพลาดสำหรับผู้อื่น
(เนื่องจากถูกแมปไปยังแฮชเดียวกัน) จึงเป็นประโยชน์ในการสำรวจขนาดใหญ่มาก
LTS ที่ไม่สามารถสำรวจได้ ค่าเริ่มต้นสำหรับ NUM คือประมาณ
2*10^8 (ซึ่งสอดคล้องกับหน่วยความจำประมาณ 25MB)

--แคช
ใช้เทคนิคการแจงนับแคชเพื่อเพิ่มความเร็วในการสร้างพื้นที่ของรัฐ

-c[ชื่อ], --บรรจบกัน[=ชื่อ]
ใช้การจัดลำดับความสำคัญของการเปลี่ยนด้วยป้ายกำกับการดำเนินการ NAME (เมื่อไม่มี NAME คือ
จัดลำดับความสำคัญ (เช่น '-c') ให้กับการกระทำ 'ctau' ให้ความสำคัญกับ
เอกภาพใช้แฟล็ก -ctau โปรดทราบว่าหากกระบวนการเชิงเส้นไม่ไหลมารวมกันเป็นเอกภาพ
พื้นที่ของรัฐที่สร้างขึ้นจำเป็นต้องแตกแขนงออกจากพื้นที่ของรัฐ
lps อัลกอริทึมการสร้างที่ใช้ไม่ต้องการกระบวนการเชิงเส้น
ที่จะมาบรรจบกัน

-D, --ทางตัน
ตรวจจับการชะงักงัน (เช่น ทุกครั้งที่มีการพิมพ์ข้อความหยุดชะงัก)

-F, --ไดเวอร์เจนซ์
ตรวจจับไดเวอร์เจนซ์ (เช่น สำหรับทุกสถานะที่มีไดเวอร์เจนซ์ (=tau loop) ข้อความคือ
พิมพ์) อัลกอริธึมในการตรวจจับไดเวอร์เจนซ์เป็นแบบเชิงเส้นสำหรับทุกสถานะ ดังนั้น
การสำรวจอวกาศของรัฐจะกลายเป็นกำลังสองเมื่อเปิดตัวเลือกนี้ ทำให้เกิดสถานะ
การสำรวจอวกาศจะช้าลงเมื่อเปิดใช้งานตัวเลือกนี้

-yบูล, --ดัมมี่=บูล
แทนที่ตัวแปรอิสระใน LPS ด้วยค่าจำลองตามค่าของ BOOL:
'ใช่' (ค่าเริ่มต้น) หรือ 'ไม่ใช่'

- การติดตามข้อผิดพลาด
หากเกิดข้อผิดพลาดระหว่างการสำรวจให้บันทึกการติดตามไปยังสถานะที่ไม่สามารถ
สำรวจ

--init-tsize=NUM
กำหนดขนาดเริ่มต้นของตารางแฮชที่ใช้ภายใน (ค่าเริ่มต้นคือ 10000)

-lNUM, --สูงสุด=NUM
สำรวจมากที่สุด NUM รัฐ

-mชื่อ, --มัลติแอคชั่น=ชื่อ
ตรวจจับและรายงานหลายการกระทำในระบบการเปลี่ยนจาก NAMES ซึ่งเป็นเครื่องหมายจุลภาค
แยกรายการ. ทำงานเหมือน -a ยกเว้นว่าการทำงานหลายอย่างตรงกันทุกประการ
รวมถึงพารามิเตอร์ข้อมูล

--ไม่มีข้อมูล
อย่าเพิ่มข้อมูลสถานะลงใน OUTFILE หากไม่มีตัวเลือกนี้ lps2lts เพิ่ม state
เวกเตอร์ไปยัง LTS ตัวเลือกนี้ทำให้ข้อมูลนี้ถูกยกเลิกและระบุ
จะถูกระบุด้วยหมายเลขลำดับเท่านั้น ข้อมูลสถานะที่ชัดเจนเป็นประโยชน์สำหรับ
วัตถุประสงค์ในการมองเห็น เช่น แต่อาจทำให้ OUTFILE เติบโตได้
อย่างมาก โปรดทราบว่าตัวเลือกนี้มีความหมายโดยนัยเมื่อเขียนในรูปแบบ AUT

-oFORMAT, --ออก=FORMAT
บันทึกผลลัพธ์ใน FORMAT . ที่ระบุ

--พรุน
ใช้การตัดแต่งกิ่งเพื่อเร่งการสร้างพื้นที่ของรัฐ

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

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

-sชื่อ, --กลยุทธ์=ชื่อ
สำรวจพื้นที่ของรัฐโดยใช้กลยุทธ์ NAME: 'b', 'breadth' การค้นหาแบบกว้างก่อน
(ค่าเริ่มต้น) 'd', 'ความลึก' การค้นหาครั้งแรกในเชิงลึก 'p', 'จัดลำดับความสำคัญ' จัดลำดับความสำคัญของซิงเกิ้ล
การกระทำกับอาร์กิวเมนต์แรกเป็นแบบแนทที่เฉพาะการกระทำเหล่านั้นกับ
เลือกค่าต่ำสุดสำหรับพารามิเตอร์นี้ เช่นหากมีการกระทำ a(3) และ
b(4) a(3) ยังคงอยู่และ b(4) ข้ามไป การดำเนินการที่ไม่มีพารามิเตอร์ sort . ตัวแรก
Nat และ multactions ที่มีมากกว่าหนึ่งการกระทำจะถูกเลือกเสมอ (ตัวเลือก is
ทดลอง) 'q', 'rprioritized' จัดลำดับความสำคัญของการดำเนินการกับอาร์กิวเมนต์แรกที่เป็นของ
จัดเรียงแนท (ดูตัวเลือก --จัดลำดับความสำคัญ) และสุ่มเลือกหนึ่งในนั้นเพื่อรับ
จัดลำดับความสำคัญการจำลองแบบสุ่ม (ตัวเลือกอยู่ในการทดลอง) 'r', 'สุ่ม' สุ่ม
การจำลอง จากสถานะถัดไปทั้งหมดหนึ่งรายการจะถูกสุ่มเลือกโดยไม่ขึ้นกับว่า
สถานะนี้ได้รับการสังเกตแล้ว ดังนั้นการจำลองแบบสุ่มเท่านั้น
สิ้นสุดลงเมื่อพบสถานะการชะงักงัน

--ปราบปราม
ในโหมด verbose อย่าพิมพ์ข้อความแสดงความคืบหน้าระบุจำนวนการเยี่ยมชม
รัฐและช่วงการเปลี่ยนภาพ สำหรับพื้นที่สถานะขนาดใหญ่ จำนวนข้อความความคืบหน้าสามารถ
จะค่อนข้างน่ากลัว คุณลักษณะนี้ช่วยระงับสิ่งเหล่านั้น ข้อความละเอียดอื่นๆ
เช่นจำนวนรัฐที่สำรวจทั้งหมดยังคงมองเห็นได้

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

--todo-สูงสุด=NUM
เก็บได้มากที่สุด NUM รัฐในรายการสิ่งที่ต้องทำ ตัวเลือกนี้เกี่ยวข้องกับความกว้างเท่านั้น
การค้นหาครั้งแรก โดยที่ NUM คือจำนวนสถานะสูงสุดต่อระดับ และสำหรับความลึก
การค้นหาครั้งแรก โดยที่ NUM คือความลึกสูงสุด

-t[NUM], --ติดตาม[=NUM]
เขียนการติดตามที่สั้นที่สุดไปยังแต่ละสถานะที่เข้าถึงได้ด้วยการดำเนินการจาก NAMES จาก
ตัวเลือก --action เป็นการหยุดชะงักที่ตรวจพบด้วย --deadlock หรือเป็นไดเวอร์เจนซ์
ตรวจพบด้วย --divergence ไปยังไฟล์ จะเขียนไม่เกิน NUM ร่องรอย ถ้า
ไม่ได้ระบุ NUM จำนวนของการติดตามไม่มีขอบเขต สำหรับแต่ละการติดตามที่จะเป็น
เขียนไฟล์เฉพาะที่มีนามสกุล .trc (ร่องรอย) จะถูกสร้างขึ้นโดยประกอบด้วย a
การติดตามที่สั้นที่สุดจากสถานะเริ่มต้นไปยังสถานะการหยุดชะงัก ร่องรอยสามารถ
พิมพ์สวยและแปลงเป็นรูปแบบอื่นโดยใช้ tracepp

-u, --ไม่ได้ใช้ข้อมูล
อย่าลบส่วนที่ไม่ได้ใช้ของข้อกำหนดข้อมูล

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

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

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

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

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

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

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

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