ماریا - آنلاین در ابر

برنامه:

نام

maria - آنالایزر قابلیت دسترسی مدولار برای شبکه های پتری سطح بالا

خلاصه

مریم [گزینه های] فایل ها...

شرح

این صفحه راهنما به اختصار مستندات مریم فرمان مستندات کاملتر است
در قالب اطلاعات گنو موجود است. زیر را ببینید.

مریم برنامه ای است که مدل های سیستم های همزمان را که در ورودی آن توضیح داده شده است، تجزیه و تحلیل می کند
زبانی که مبتنی بر شبکه های سیستم جبری است. فرمالیسم توسط Ekkart ارائه شده است
کیندلر و هاگن ولزر در ICATPN'98، انعطاف پذیری in جبری توری.
شبکه های سیستم جبری چارچوبی است که هیچ نوع داده یا جبری را تعریف نمی کند
عملیات سیستم نوع داده و عملیات در ماریا با سطح بالا طراحی شده است
زبان های برنامه نویسی و مشخصات را در نظر داشته باشید. با وجود آن، هر مدل ماریا دارای یک
باز شدن محدود
ماریا برای اطمینان از قابلیت همکاری با ابزارهای شبکه پتری سطح پایین، شناسه ها را به داخل ترجمه می کند
شبکه‌ها را به رشته‌هایی از نویسه‌های الفا عددی و زیرخط باز کرد. فیلتر
foldname.pl می توان برای بهبود خوانایی شناسه ها استفاده کرد یا تطبیق داد.

OPTIONS

ماریا از دستور خط فرمان معمول گنو پیروی می کند، با گزینه های طولانی که با دو شروع می شود
خط تیره (`-'). خلاصه ای از گزینه ها در زیر گنجانده شده است. برای توضیحات کامل رجوع کنید
فایل های اطلاعات

-a محدود کردن, --array-limit=محدود کردن
محدود کردن اندازه انواع شاخص آرایه به محدود کردن مقادیر ممکن محدودیت 0
چک ها را غیرفعال می کند

-b مدل, --breadth-first-search=مدل
نمودار دسترس پذیری را ایجاد کنید مدل با استفاده از جستجوی عرضی

-C فهرست راهنما, --کامپایل=فهرست راهنما
کد C را در فهرست راهنما برای ارزیابی عبارات و برای سطح پایین
روال های الگوریتم تجزیه و تحلیل نمونه انتقال وقتی از این گزینه استفاده می شود،
خطاهای ارزیابی به روشی کمی متفاوت گزارش می شوند. مترجم
ارزش گذاری و بیانی را نشان می دهد که باعث اولین خطا در یک حالت شده است. را
کد کامپایل شده تعداد خطاها را نشان می دهد. به دلایل عملکرد،
کد تولید شده هنگام اضافه کردن آیتم ها به چند مجموعه، خطاهای سرریز را بررسی نمی کند.

-c، --بدون کامپایل
برعکس -C. تمام عبارات را در مفسر داخلی ارزیابی کنید. این هست
رفتار پیش فرض

-D نماد, --define=نماد
نماد پیش پردازنده را تعریف کنید نماد.

-d مدل, --depth-first-search=مدل
نمودار دسترس پذیری را ایجاد کنید مدل با استفاده از جستجوی عمقی

-E فاصله, --لبه ها=فاصله
هنگام ایجاد نمودار دسترسی، اندازه نمودار را بعد از هر بار گزارش دهید
فاصله لبه های تولید شده

-e رشته, -- اجرا =رشته
اجرا کردن رشته.

-g فایل گرافیکی, -- نمودار =فایل گرافیکی
یک نمودار قابلیت دسترسی ایجاد شده قبلی را بارگیری کنید فایل گرافیکی.rgh.

-H h[,f[,t]], --هش=h[,f[,t]]
پیکربندی پارامترها برای تأیید احتمالی (-P). اختصاص دهید t جهانی
توابع هش از f عناصر و جداول هش مربوطه از h هر کدام بیت ها هر دو h
و f به مقادیر مناسب بعدی گرد خواهد شد.

-؟، -h، --کمک
خلاصه ای از گزینه های خط فرمان را در Maria چاپ کنید و خارج شوید.

-I فهرست راهنما, --شامل=فهرست راهنما
ضمیمه کردن فهرست راهنما به لیست دایرکتوری های جستجو شده شامل فایل ها.

-i ستون ها, --width=ستون ها
حاشیه سمت راست خروجی را روی ستون ها. پیش فرض 80 است.

-j فرآیندهای, -- شغل =فرآیندهای
هنگام بررسی ویژگی های ایمنی (گزینه ها -L, -M و -P) از این تعداد کارگر استفاده کنید
فرآیندهایی برای سرعت بخشیدن به تجزیه و تحلیل در یک کامپیوتر چند پردازنده ای. همچنین ببینید -k و
-Z.

-k بندر[/میزبان], --connect=بندر[/میزبان]
توزیع بررسی مدل ایمنی (گزینه‌ها -L, -M و -P) در یک شبکه TCP/IP. برای
سرور، فقط بندر به عنوان یک عدد صحیح بدون علامت 16 بیتی، معمولاً بین
1024 و 65535. برای فرآیندهای کارگر، بندر/میزبان پورت و را مشخص می کند
آدرس سرور همچنین ببینید -j.

-L مدل, --بی ضرر=مدل
بار مدل و با ساخت مجموعه ای از حالت های قابل دسترس برای تجزیه و تحلیل آن آماده شوید
در فایل های دیسک همچنین ببینید -M, -P, -j و -k.

-m مدل, --model=مدل
بار مدل و نمودار دسترسی آن را پاک کنید.

-M مدل, --md5-compacted=مدل
بار مدل و با ایجاد تقریب بیش از حد برای تجزیه و تحلیل آن آماده شوید
مجموعه ای از حالت های قابل دسترسی در حافظه اصلی همچنین ببینید -P, -L, -j و -k.

-N cregexp, --نام=cregexp
نام های مجاز در زمینه را مشخص کنید c به عنوان عبارت منظم توسعه یافته regexp.
زمینه با اولین کاراکتر رشته پارامتر مشخص می شود. را
کاراکترهای بعدی عبارت منظمی را تشکیل می دهند که نام های مجاز باید باید باشند
مطابقت داشته باشد.

-n cregexp, --no-name=cregexp
نام هایی را که در متن مجاز نیستند مشخص کنید c به عنوان عبارت منظم توسعه یافته
regexp.
اگر هر دو -N و و -n برای یک زمینه مشخص می شوند c، سپس مطابقت مجاز طول می کشد
تقدم به عنوان مثال، نیاز است که همه نام های نوع تعریف شده توسط کاربر باشد
خاتمه یافت با _t، مشخص نمودن -نه -Nt'_t$'. نقل قول در پارامتر دوم هستند
لازمه حذف معنای خاص از $ در پوسته خط فرمان شما هستید
احتمالاً برای فراخوانی ماریا استفاده می کند.

-P مدل, --احتمالی=مدل
بار مدل و با ساخت مجموعه ای از حالت های قابل دسترس برای تجزیه و تحلیل آن آماده شوید
در حافظه اصلی با استفاده از تکنیکی به نام حالت بیتی حس کردن.

-p فرمان, --property-translator=فرمان
دستور مورد استفاده برای ترجمه خودکار ویژگی را مشخص کنید. فرمان باید
یک فرمول را از ورودی استاندارد بخوانید و یک خودکار مربوطه بنویسید
توصیف خروجی استاندارد مترجم lbt با این سازگار است
گزینه.

-q محدود کردن, --quantification-limit=محدود کردن
جلوگیری از کمی سازی (مجموع چند مجموعه ای) انواع دارای بیش از محدود کردن ممکن
ارزش های. محدودیت 0، چک ها را غیرفعال می کند.

-U نماد, --تعریف=نماد
نماد پیش پردازنده را تعریف نکنید نماد.

-u [a][f[مجموعه]], --گشودن =[a][f[مجموعه]]
شبکه را با استفاده از الگوریتم باز کنید a و آن را در قالب بنویسید f به مجموعه. اگر مجموعه
مشخص نشده است، توری تا شده را به خروجی استاندارد بریزید. فرمت های ممکن
هستند m (ماریا (قابل خواندن توسط انسان)، پیش فرض)، l (LoLA)، p (PEP)، و r (PROD). آنجا
دو الگوریتم هستند: سنتی (پیش‌فرض) و با ساخت a کاهش می‌یابند قابل پوشش
علامت گذاری (M).

-V، - نسخه
شماره نسخه ماریا را چاپ کنید و خارج شوید.

-v، -- پرحرف
نمایش اطلاعات مفصل در مراحل مختلف تجزیه و تحلیل.

-W، -- هشدارها
هشدارهای مربوط به ساختارهای شبکه مشکوک را فعال کنید. این رفتار به طور پیش فرض است.

-w، -- بدون هشدار
برعکس -W. غیرفعال کردن همه هشدارها

-x پایگاه اعداد, --رادیکس=پایگاه اعداد
پایه عددی را برای خروجی تشخیصی مشخص کنید. مقادیر مجاز برای پایگاه اعداد هستند
اکتبر, اکتال, 8, هگزا, شش ضلعی, 16, دسامبر, دهدهی و 10. پیش فرض استفاده است
اعداد اعشاری

-Y، --فشرده-مخفی
با ذخیره نکردن حالت های جانشین، مجموعه حالت های قابل دسترسی را کاهش دهید
موارد انتقالی که برای آنها a پنهان کردن شرایط برقرار است جانشینان پنهان هستند
در یک مجموعه حالت جداگانه ذخیره می شود. این گزینه ممکن است حافظه را ذخیره کند (-L or -m) یا کاهش دهید
احتمال حذف حالت ها (-M or -P) و ممکن است باعث بهبود آن شود
کارایی تحلیل موازی (-j or -k، اما ممکن است به طور قابل توجهی افزایش یابد
زمان مورد نیاز پردازنده این گزینه همچنین با مدل زنده کار می کند
چک کردن، اما هیچ تضمینی وجود ندارد که ارزش حقیقت خواص زنده بودن وجود دارد
بدون تغییر باقی می ماند. این گزینه را می توان با -Z.

-y، ---بدون فشرده سازی-مخفی
برعکس -Y. این رفتار به طور پیش فرض است.

-Z، ---compress-paths
با ذخیره نکردن حالت های میانی که دارای at هستند، مجموعه حالت های قابل دسترسی را کاهش دهید
یکی از جانشینان این گزینه ممکن است حافظه را ذخیره کند (-L or -m) یا کاهش می دهد
احتمال حذف حالت ها (-M or -P، و ممکن است کارایی را بهبود بخشد
تحلیل موازی (-j or -k، اما همچنین ممکن است به میزان قابل توجهی افزایش یابد
زمان مورد نیاز پردازنده این گزینه همچنین با بررسی مدل زنده بودن کار می کند،
اما هیچ تضمینی وجود ندارد که ارزش های حقیقت خصوصیات زنده بودن باقی بماند
بدون تغییر این گزینه را می توان با -Y.

-z ، - مسیرهای بدون فشرده سازی
برعکس -Z. این رفتار به طور پیش فرض است.

از ماریا آنلاین با استفاده از خدمات onworks.net استفاده کنید