นี่คือคำสั่ง ltsconvert ที่สามารถเรียกใช้ในผู้ให้บริการโฮสติ้งฟรีของ OnWorks โดยใช้หนึ่งในเวิร์กสเตชันออนไลน์ฟรีของเรา เช่น Ubuntu Online, Fedora Online, โปรแกรมจำลองออนไลน์ของ Windows หรือโปรแกรมจำลองออนไลน์ของ MAC OS
โครงการ:
ชื่อ
ltsconvert - แปลงและเลือกย่อขนาด LTS
เรื่องย่อ
ltsแปลง [ทางเลือกที่-อินไฟล [ภายนอก]]
DESCRIPTION
แปลงระบบการเปลี่ยนที่มีป้ายกำกับ (LTS) จาก INFILE เป็น OUTFILE ในคำขอ
รูปแบบหลังจากใช้วิธีย่อเล็กสุดที่เลือก (ค่าเริ่มต้นคือไม่มี) ถ้า OUTFILE คือ
ไม่ได้ให้มา ใช้ stdout หากไม่ได้ระบุ INFILE จะใช้ stdin
รูปแบบเอาต์พุตถูกกำหนดโดยส่วนขยายของ OUTFILE ในขณะที่รูปแบบอินพุตคือ
กำหนดโดยเนื้อหาของ INFILE สามารถใช้ตัวเลือก --in และ --out เพื่อบังคับอินพุต
และรูปแบบเอาต์พุต รูปแบบที่รองรับคือ:
'aut' สำหรับรูปแบบ Aldebaran (CADP)
'dot' สำหรับรูปแบบ GraphViz (ไม่รองรับรูปแบบอินพุตอีกต่อไป)
'fsm' สำหรับรูปแบบ Finite State Machine หรือ
'lts' สำหรับรูปแบบ mCRL2 LTS (ค่าเริ่มต้น)
OPTIONS
ทางเลือกที่ สามารถเป็นอย่างใดอย่างหนึ่งต่อไปนี้:
-D, --กำหนด
กำหนด LTS
-eชื่อ, --สมมูล=ชื่อ
สร้าง LTS ที่เทียบเท่ากัน รักษาความเท่าเทียมกัน NAME: 'ไม่มี' เอกลักษณ์
ความเท่าเทียมกัน (ค่าเริ่มต้น) 'bisim' ความเท่าเทียมกันที่แข็งแกร่ง 'bisim-sig' ความคล้ายคลึงที่แข็งแกร่ง
ใช้การปรับแต่งลายเซ็น 'branching-bisim' การแยกสาขา 'branching-
bisim-sig' การแตกแขนงทวิภาคโดยใช้การปรับแต่งลายเซ็น 'dpbranching-bisim'
ความแตกต่างที่รักษาความแตกต่างของการแตกแขนง 'dpbranching-bisim-sig' ความแตกต่าง
รักษาความคล้ายคลึงกันของการแตกแขนงโดยใช้การปรับแต่งลายเซ็น 'weak-bisim' อ่อนแอ
ความคล้ายคลึง 'อ่อนแอ-bisim-sig' ความคล้ายคลึงกันที่อ่อนแอโดยใช้การปรับแต่งลายเซ็น 'dpweak-
ความแตกต่างของ bisim ' การรักษา bisimilarity ที่อ่อนแอ 'dpweak-bisim-sig' ความแตกต่าง
รักษาความคล้ายคลึงที่อ่อนแอโดยใช้การจำลองที่แข็งแกร่ง 'ซิม' การปรับแต่งลายเซ็น
ความเท่าเทียมกัน 'ร่องรอย' การติดตามที่แข็งแกร่ง ความเท่าเทียมกัน 'การติดตามที่อ่อนแอ'
'tau-star' ลดดาวเทา
-iFORMAT, --ใน=FORMAT
ใช้ FORMAT เป็นรูปแบบอินพุต
-lไฟล์, --lps=ไฟล์
ใช้ FILE เป็น LPS ที่สร้างอินพุต LTS นี้อาจจะจำเป็นเพื่อ
เก็บชื่อพารามิเตอร์ที่ถูกต้องของสถานะเมื่อบันทึกในรูปแบบ fsm และto
แปลง LTS ที่ไม่ใช่ mCRL2 เป็น mCRL2 LTS
--ไม่ถึง
อย่าทำการตรวจสอบความสามารถในการเข้าถึงของอินพุต LTS
-n, --ไม่มีรัฐ
ละเว้นข้อมูลสถานะเมื่อบันทึกในรูปแบบจุด
-oFORMAT, --ออก=FORMAT
ใช้ FORMAT เป็นรูปแบบผลลัพธ์
--เทา=ชื่อการกระทำ
พิจารณาการดำเนินการที่มีชื่อในรายการที่คั่นด้วยเครื่องหมายจุลภาค ACTNAMES เป็นรายการภายใน
(เอกภาพ) การกระทำนอกเหนือจากที่กำหนดไว้โดยอินพุต
--กำหนดเวลา[=ไฟล์]
ผนวกการวัดเวลาเข้ากับ FILE การวัดจะถูกเขียนไปยังข้อผิดพลาดมาตรฐาน if
ไม่มีไฟล์ให้
ตัวเลือกมาตรฐาน:
-q, --เงียบ
ไม่แสดงข้อความเตือน
-v, --รายละเอียด
แสดงข้อความกลางสั้นๆ
-d, --debug
แสดงข้อความระดับกลางโดยละเอียด
--log-ระดับ=ระดับ
แสดงข้อความระดับกลางถึงและรวมถึงระดับ
-h, --ช่วยด้วย
แสดงข้อมูลช่วยเหลือ
--รุ่น
แสดงข้อมูลรุ่น
ใช้ ltsconvert ออนไลน์โดยใช้บริการ onworks.net