มาเรีย - ออนไลน์ในคลาวด์

โครงการ:

ชื่อ

maria - ตัววิเคราะห์การเข้าถึงแบบแยกส่วนสำหรับ Petri nets ระดับสูง

เรื่องย่อ

มาเรีย [ตัวเลือก] ไฟล์...

DESCRIPTION

หน้าคู่มือนี้จัดทำเอกสารโดยสังเขปเกี่ยวกับ มาเรีย สั่งการ. เอกสารเพิ่มเติมที่สมบูรณ์คือ
มีอยู่ในรูปแบบข้อมูล GNU; ดูด้านล่าง

มาเรีย เป็นโปรแกรมที่วิเคราะห์แบบจำลองของระบบพร้อมกันที่อธิบายไว้ในอินพุต
ภาษาที่ใช้ Nets ระบบพีชคณิต พิธีมอบโดย Ekart
Kindler และ Hagen Völzer ที่ ICATPN'98 ความยืดหยุ่น in พีชคณิต อวน.
Algebraic System Nets เป็นเฟรมเวิร์กที่ไม่ได้กำหนดประเภทข้อมูลหรือพีชคณิตใดๆ
การดำเนินงาน ระบบประเภทข้อมูลและการดำเนินการใน Maria ได้รับการออกแบบด้วยระดับสูง
ภาษาการเขียนโปรแกรมและข้อกำหนดเฉพาะ อย่างไรก็ตาม มาเรียแต่ละรุ่นมี
แฉ จำกัด
เพื่อให้มั่นใจในการทำงานร่วมกันกับเครื่องมือ Petri net ระดับต่ำ Maria แปลตัวระบุใน
กางตาข่ายเป็นสตริงของอักขระที่เป็นตัวอักษรและตัวเลขและขีดล่าง ตัวกรอง
foldname.pl สามารถใช้หรือดัดแปลงเพื่อปรับปรุงความสามารถในการอ่านของตัวระบุ

OPTIONS

Maria ปฏิบัติตามไวยากรณ์บรรทัดคำสั่งของ GNU ตามปกติ โดยมีตัวเลือกแบบยาวขึ้นต้นด้วย two
ขีดกลาง (`-') สรุปตัวเลือกอยู่ด้านล่าง ดูรายละเอียดได้ที่
ไฟล์ข้อมูล

-a จำกัด, --array-จำกัด=จำกัด
จำกัดขนาดของประเภทดัชนีอาร์เรย์เป็น จำกัด ค่าที่เป็นไปได้ ขีด จำกัด 0
ปิดใช้งานการตรวจสอบ

-b แบบ, --กว้างก่อนค้นหา=แบบ
สร้างกราฟความสามารถในการเข้าถึงของ แบบ โดยใช้การค้นหาแบบกว้างๆ

-C ไดเรกทอรี, --คอมไพล์=ไดเรกทอรี
สร้างรหัส C ใน ไดเรกทอรี สำหรับการประเมินนิพจน์และสำหรับระดับต่ำ
รูทีนของอัลกอริธึมการวิเคราะห์อินสแตนซ์การเปลี่ยนแปลง เมื่อใช้ตัวเลือกนี้
ข้อผิดพลาดในการประเมินจะถูกรายงานในลักษณะที่แตกต่างกันเล็กน้อย ล่าม
แสดงการประเมินค่าและนิพจน์ที่ทำให้เกิดข้อผิดพลาดครั้งแรกในสถานะ NS
รหัสที่คอมไพล์จะแสดงจำนวนข้อผิดพลาด ด้วยเหตุผลด้านประสิทธิภาพ
รหัสที่สร้างขึ้นไม่ตรวจสอบข้อผิดพลาดล้นเมื่อเพิ่มรายการไปยังชุดหลายชุด

-ค, --no-คอมไพล์
ตรงกันข้ามกับ -C. ประเมินนิพจน์ทั้งหมดในล่ามในตัว นี่คือ
พฤติกรรมเริ่มต้น

-D เครื่องหมาย, --กำหนด=เครื่องหมาย
กำหนดสัญลักษณ์พรีโปรเซสเซอร์ เครื่องหมาย.

-d แบบ, --deep-first-search=แบบ
สร้างกราฟความสามารถในการเข้าถึงของ แบบ โดยใช้การค้นหาเชิงลึกเป็นอันดับแรก

-E ระยะห่าง, --ขอบ=ระยะห่าง
เมื่อสร้างกราฟความสามารถในการเข้าถึง ให้รายงานขนาดของกราฟหลังทุกๆ
ระยะห่าง ขอบที่สร้างขึ้น

-e เชือก, --ดำเนินการ=เชือก
ดำเนินงาน เชือก.

-g กราฟไฟล์, --กราฟ=กราฟไฟล์
โหลดกราฟความสามารถในการเข้าถึงที่สร้างไว้ก่อนหน้านี้จาก กราฟไฟล์.rgh.

-H h[,f[,t]], --แฮช=h[,f[,t]]
กำหนดค่าพารามิเตอร์สำหรับการตรวจสอบความน่าจะเป็น (-P). จัดสรร t สากล
ฟังก์ชันแฮชของ f องค์ประกอบและตารางแฮชที่สอดคล้องกันของ h บิตแต่ละ ทั้งคู่ h
และ f จะถูกปัดขึ้นเป็นค่าที่เหมาะสมถัดไป

- -ชม, --ช่วยด้วย
พิมพ์สรุปตัวเลือกบรรทัดคำสั่งให้ Maria และออก

-I ไดเรกทอรี, --รวม=ไดเรกทอรี
ผนวก ไดเรกทอรี ไปที่รายการไดเร็กทอรีที่ค้นหาไฟล์รวม

-i คอลัมน์, --ความกว้าง=คอลัมน์
ตั้งค่าระยะขอบขวาของผลลัพธ์เป็น คอลัมน์. ค่าเริ่มต้นคือ 80

-j กระบวนการ, --งาน=กระบวนการ
เมื่อตรวจสอบคุณสมบัติความปลอดภัย (ตัวเลือก -L, -M และ -P) ใช้คนงานจำนวนมากนี้
กระบวนการเพื่อเพิ่มความเร็วในการวิเคราะห์บนคอมพิวเตอร์มัลติโปรเซสเซอร์ ดูสิ่งนี้ด้วย -k และ
-Z.

-k พอร์ต[/เจ้าภาพ], --เชื่อมต่อ=พอร์ต[/เจ้าภาพ]
แจกจ่ายการตรวจสอบแบบจำลองความปลอดภัย (ตัวเลือก -L, -M และ -P) ในเครือข่าย TCP/IP สำหรับ
เซิฟเวอร์เท่านั้น พอร์ต ถูกระบุเป็นจำนวนเต็ม 16 บิตที่ไม่ได้ลงนาม โดยปกติอยู่ระหว่าง
1024 และ 65535 สำหรับกระบวนการของผู้ปฏิบัติงาน พอร์ต/เจ้าภาพ ระบุพอร์ตและ
ที่อยู่ของเซิร์ฟเวอร์ ดูสิ่งนี้ด้วย -j.

-L แบบ, --ไม่สูญเสีย=แบบ
โหลด แบบ และเตรียมวิเคราะห์โดยสร้างชุดสถานะที่เข้าถึงได้
ในไฟล์ดิสก์ ดูสิ่งนี้ด้วย -M, -P, -j และ -k.

-m แบบ, --รุ่น=แบบ
โหลด แบบ และล้างกราฟความสามารถในการเข้าถึง

-M แบบ, --md5-กระชับ=แบบ
โหลด แบบ และเตรียมวิเคราะห์โดยสร้างการประมาณค่าเกินของ
ชุดของสถานะที่เข้าถึงได้ในหน่วยความจำหลัก ดูสิ่งนี้ด้วย -P, -L, -j และ -k.

-N เคร็กเอ็กซ์, --ชื่อ=เคร็กเอ็กซ์
ระบุชื่อที่อนุญาตในบริบท c เป็นนิพจน์ทั่วไปแบบขยาย regexp.
บริบทถูกระบุโดยอักขระตัวแรกของสตริงพารามิเตอร์ NS
อักขระที่ต่อท้ายเป็นนิพจน์ทั่วไปที่อนุญาตให้ชื่อต้อง
การจับคู่.

-n เคร็กเอ็กซ์, --ไม่มีชื่อ=เคร็กเอ็กซ์
ระบุชื่อที่ไม่อนุญาตในบริบท c เป็นนิพจน์ทั่วไปแบบขยาย
regexp.
ถ้าทั้งสองอย่าง -N และและ -n ถูกกำหนดไว้สำหรับบริบท cจากนั้นการจับคู่ที่อนุญาตจะใช้เวลา
ลำดับความสำคัญ ตัวอย่างเช่น กำหนดให้ชื่อประเภทที่ผู้ใช้กำหนดทั้งหมดเป็น
ลงท้ายด้วย _t, ระบุ -nt -Nt'_t$'. เครื่องหมายคำพูดในพารามิเตอร์หลังคือ
จำเป็นต้องถอดความหมายพิเศษออกจาก $ ในเชลล์บรรทัดคำสั่งคุณคือ
คงจะใช้เรียกมาเรีย

-P แบบ, --ความน่าจะเป็น=แบบ
โหลด แบบ และเตรียมวิเคราะห์โดยสร้างชุดสถานะที่เข้าถึงได้
ในหน่วยความจำหลักโดยใช้เทคนิคที่เรียกว่า สถานะบิต hashing.

-p คำสั่ง, --คุณสมบัติ-นักแปล=คำสั่ง
ระบุคำสั่งที่จะใช้สำหรับการแปลคุณสมบัติ automata คำสั่งควร
อ่านสูตรจากอินพุตมาตรฐานและเขียนหุ่นยนต์ที่เกี่ยวข้อง
คำอธิบายไปยังเอาต์พุตมาตรฐาน นักแปล ปอนด์ เข้ากันได้กับสิ่งนี้
ตัวเลือก

-q จำกัด, --ปริมาณ-จำกัด=จำกัด
ป้องกันการหาปริมาณ (ผลรวมหลายชุด) ของประเภทที่มีมากกว่า จำกัด เป็นไปได้
ค่านิยม ขีด จำกัด 0 ปิดการใช้งานการตรวจสอบ

-U เครื่องหมาย, --define=เครื่องหมาย
ยกเลิกการกำหนดสัญลักษณ์พรีโปรเซสเซอร์ เครื่องหมาย.

-u [a][f[ออกจากไฟล์]], --แฉ=[a][f[ออกจากไฟล์]]
กางเน็ตโดยใช้อัลกอริธึม a และเขียนในรูปแบบ f ไปยัง ออกจากไฟล์. ถ้า ออกจากไฟล์
ไม่ได้ระบุไว้ ให้ดัมพ์เน็ตที่กางออกไปยังเอาต์พุตมาตรฐาน รูปแบบที่เป็นไปได้
เป็น m (Maria (มนุษย์สามารถอ่านได้) ค่าเริ่มต้น) l (โลลา) p (PEP) และ r (แยง). ที่นั่น
เป็นอัลกอริธึมสองแบบ: ดั้งเดิม (ค่าเริ่มต้น) และลดลงโดยการสร้าง a ปกปิดได้
เครื่องหมาย (M).

-วี --รุ่น
พิมพ์หมายเลขเวอร์ชันของ Maria แล้วออก

-ใน, --รายละเอียด
แสดงข้อมูลอย่างละเอียดในขั้นตอนต่างๆ ของการวิเคราะห์

-ว, --คำเตือน
เปิดใช้งานคำเตือนเกี่ยวกับโครงสร้างเน็ตที่น่าสงสัย นี่เป็นพฤติกรรมเริ่มต้น

-w, --ไม่มีคำเตือน
ตรงกันข้ามกับ -W. ปิดการใช้งานคำเตือนทั้งหมด

-x ฐานตัวเลข, --รัศมี=ฐานตัวเลข
ระบุฐานตัวเลขสำหรับเอาต์พุตการวินิจฉัย ค่าที่อนุญาตสำหรับ ฐานตัวเลข เป็น
ตุลาคม, ฐานแปด, 8, ฐานสิบหก, เลขฐานสิบหก, 16, ธันวาคม, ทศนิยม และ 10. ค่าเริ่มต้นคือการใช้
เลขฐานสิบ

-ใช่ --บีบอัด-ซ่อน
ลดชุดของสถานะที่เข้าถึงได้โดยไม่เก็บสถานะสืบทอดของ
กรณีเปลี่ยนผ่านซึ่ง a ซ่อน สภาพถือ. ผู้สืบทอดที่ซ่อนอยู่คือ
เก็บไว้ในชุดสถานะแยกต่างหาก ตัวเลือกนี้อาจบันทึกหน่วยความจำ (-L or -m) หรือ ลด
ความน่าจะเป็นที่รัฐจะถูกละเว้น (-M or -P) และอาจปรับปรุง
ประสิทธิภาพของการวิเคราะห์แบบขนาน (-j or -k) แต่ก็อาจเพิ่มขึ้นได้มากเช่นกัน
ข้อกำหนดด้านเวลาของโปรเซสเซอร์ ตัวเลือกยังใช้งานได้กับโมเดลความมีชีวิตชีวา
ตรวจสอบแต่ไม่มีหลักประกันว่าความจริงมีค่าของคุณสมบัติความมีชีวิตชีวา
ยังคงไม่เปลี่ยนแปลง ตัวเลือกนี้สามารถใช้ร่วมกับ -Z.

-y, --no-บีบอัด-ซ่อน
ตรงกันข้ามกับ -Y. นี่เป็นพฤติกรรมเริ่มต้น

-Z, --บีบอัดเส้นทาง
ลดชุดของสถานะที่เข้าถึงได้โดยไม่เก็บสถานะขั้นกลางที่มี at
ผู้สืบทอดมากที่สุดคนหนึ่ง ตัวเลือกนี้อาจช่วยประหยัดหน่วยความจำ (-L or -m) หรือลด
ความน่าจะเป็นที่รัฐจะถูกละเว้น (-M or -P) และอาจเพิ่มประสิทธิภาพได้
ของการวิเคราะห์คู่ขนาน (-j or -k) แต่ก็อาจเพิ่มขึ้นอย่างมากเช่นกัน
ความต้องการเวลาของโปรเซสเซอร์ ตัวเลือกยังใช้งานได้กับการตรวจสอบโมเดลความมีชีวิตชีวา
แต่ไม่มีหลักประกันว่าค่าความจริงของคุณสมบัติความมีชีวิตชีวาจะยังคงอยู่
ไม่เปลี่ยนแปลง ตัวเลือกนี้สามารถใช้ร่วมกับ -Y.

-z, --no-บีบอัดเส้นทาง
ตรงกันข้ามกับ -Z. นี่เป็นพฤติกรรมเริ่มต้น

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