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

برنامه:

نام

lps2lts - یک LTS از یک LPS تولید کنید

خلاصه

lps2lts [گزینه]... [INFILE [پر از زاویه]]

شرح

یک LTS از LPS در INFILE ایجاد کنید و نتیجه را در OUTFILE ذخیره کنید. اگر INFILE نیست
عرضه شده، stdin استفاده می شود. اگر OUTFILE ارائه نشده باشد، LTS ذخیره نمی شود.

اگر از بازنویسی 'jittyc' استفاده می شود، متغیر محیطی MCRL2_COMPILEREWRITER
(مقدار پیش فرض: 'mcrl2compilerewriter') اسکریپتی را تعیین می کند که بازنویس را کامپایل می کند،
و MCRL2_COMPILEDIR (مقدار پیش فرض: '.') تعیین می کند که فایل های موقت کجا ذخیره شوند.

توجه داشته باشید که lps2lt ها می توانند چندین انتقال را با یک برچسب بین هر جفتی ارائه دهند
ایالت ها. اگر این مطلوب نیست، چنین انتقالی را می توان با استفاده از یک قوی حذف کرد
کاهش دوشبیه سازی برای مثال با استفاده از ابزار ltsconvert.

قالب OUTFILE با پسوند آن تعیین می شود (مگر اینکه توسط یک مشخص شده باشد
گزینه). فرمت های پشتیبانی شده عبارتند از:

"au" برای قالب Aldebaran (CADP)،
"نقطه" برای قالب GraphViz (دیگر به عنوان فرمت ورودی پشتیبانی نمی شود)،
'fsm' برای قالب ماشین حالت محدود، یا
'lts' برای قالب mCRL2 LTS اگر از بازنویسی jittyc استفاده شود،
متغیر محیطی MCRL2_COMPILEREWRITER (مقدار پیش‌فرض: mcrl2compilerewriter)
اسکریپتی که بازنویسی را کامپایل می کند و MCRL2_COMPILEDIR (مقدار پیش فرض:
'.') محل ذخیره فایل های موقت را تعیین می کند. توجه داشته باشید که lps2lts می تواند چندین بار ارائه دهد
انتقال با برچسب یکسان بین هر جفت حالت. اگر این مورد نظر نیست، چنین است
انتقال ها را می توان با استفاده از یک کاهش دوشبیه سازی قوی برای مثال حذف کرد
ابزار ltsconvert

OPTIONS

گزینه می تواند یکی از موارد زیر باشد:

-aنامها, --عمل=نامها
اقداماتی را در سیستم انتقال که نام کنش‌هایی از آنها وجود دارد، شناسایی و گزارش کنید
NAMES، یک لیست جدا شده با کاما. این برای مثال برای یافتن (یا اثبات آن) مفید است
عدم وجود) خطای عمل. یک پیام برای هر رخداد یکی از آنها چاپ می شود
این اسامی عمل با پرچم -t ردیابی به سمت این اقدامات ایجاد می شود

-b[NUM], -- بیت هش[=NUM]
از بیت هش برای ذخیره وضعیت ها استفاده کنید و حداکثر NUM حالت را ذخیره کنید. این به این معنی است که
به جای نگهداری یک رکورد کامل از تمام ایالت هایی که بازدید شده اند، یک آرایه بیتی
استفاده می شود که نشان می دهد هش از یک حالت قبلا دیده شده است یا خیر.
اگرچه این بدان معنی است که این گزینه ممکن است باعث شود که ایالت ها با حالت های دیگر اشتباه گرفته شوند
(چون آنها به یک هش نگاشت شده اند)، کاوش بسیار بزرگ می تواند مفید باشد
LTS هایی که در غیر این صورت قابل کاوش نیستند. مقدار پیش فرض NUM تقریباً است
2*10^8 (این مربوط به حدود 25 مگابایت حافظه است)

-- ذخیره شده
از تکنیک‌های ذخیره‌سازی شمارش برای سرعت بخشیدن به تولید فضای حالت استفاده کنید.

-c[نام], -- تلاقی[=نام]
اولویت بندی انتقال ها را با برچسب عمل NAME اعمال کنید. (زمانی که NAME وجود ندارد
ارائه شده (یعنی '-c') اولویت به عمل 'ctau' داده می شود. برای اولویت دادن به
برای tau از پرچم -ctau استفاده کنید. توجه داشته باشید که اگر فرآیند خطی تاو همسو نباشد،
فضای حالت ایجاد شده لزوماً شبیه به فضای حالت انشعاب است
lps الگوریتم تولیدی که استفاده می شود نیازی به فرآیند خطی ندارد
تاو همگرا بودن

-D, --بن بست
شناسایی بن بست ها (یعنی برای هر بن بست پیامی چاپ می شود)

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

-yبول, -- ساختگی=بول
متغیرهای رایگان در LPS را با مقادیر ساختگی بر اساس مقدار BOOL جایگزین کنید:
"بله" (پیش فرض) یا "خیر"

- ردیابی خطا
اگر در حین کاوش خطایی رخ داد، ردی را در حالتی که نمی تواند باشد ذخیره کنید
کاوش

--init-tsize=NUM
اندازه اولیه جداول هش استفاده شده داخلی را تنظیم کنید (پیش فرض 10000 است)

-lNUM, -- حداکثر=NUM
حداکثر NUM حالت را کاوش کنید

-mنامها, -- چندگانه=نامها
شناسایی و گزارش چند اقدام در سیستم انتقال از NAMES، یک کاما-
لیست جدا شده مانند -a عمل می کند، با این تفاوت که چند اکشن دقیقا مطابقت دارند،
از جمله پارامترهای داده

-- بدون اطلاعات
اطلاعات وضعیت را به OUTFILE اضافه نکنید بدون این گزینه lps2lts حالت را اضافه می کند
بردار به LTS. این گزینه باعث می شود که این اطلاعات دور ریخته شود و بیان شود
فقط با یک شماره دنباله نشان داده می شوند. اطلاعات صریح وضعیت مفید است
به عنوان مثال، اهداف تجسم، اما می تواند باعث رشد OUTFILE شود
بطور قابل توجهی توجه داشته باشید که این گزینه هنگام نوشتن با فرمت AUT به صورت ضمنی وجود دارد.

-oFORMAT, -- خارج=FORMAT
خروجی را در FORMAT مشخص شده ذخیره کنید

-- هرس کنید
از هرس جمعی برای تسریع در تولید فضای حالت استفاده کنید.

-QNUM, -qlimit=NUM
شمارش کمیت‌نماها را به NUM متغیر محدود کنید. (پیش‌فرض NUM=1000، NUM=0 برای
نامحدود).

-rنام, --بازنویس=نام
استفاده از استراتژی بازنویسی NAME: بازنویسی 'jitty' jitty (پیش فرض) 'jittyc' کامپایل شده است
بازنویسی جیتی 'جیتیپ' بازنویسی جیتی با پروور

-sنام, -- استراتژی=نام
فضای حالت را با استفاده از استراتژی NAME کاوش کنید: 'b'، 'breadth' جستجوی وسعت اول
(پیش فرض) 'd'، 'عمق' عمق-اول جستجو 'p'، 'اولویت بندی' اولویت بندی تک
اقدامات در اولین آرگومان آن از نوع Nat هستند که فقط آن اقدامات با the
کمترین مقدار برای این پارامتر انتخاب شده است. به عنوان مثال اگر اقدامات وجود دارد a(3) و
b(4) a(3) باقی می ماند و b(4) از قلم افتاده است. اقدامات بدون اولین پارامتر از نوع
Nat و چندگانه با بیش از یک عمل همیشه انتخاب می شوند (گزینه این است
تجربی) «q»، «اولویت‌بندی‌شده» اقدامات را در اولین آرگومان خود اولویت‌بندی می‌کند
Nat را مرتب کنید (به گزینه --اولویت بندی مراجعه کنید)، و به طور تصادفی یکی از آنها را انتخاب کنید تا a را بدست آورید
شبیه سازی تصادفی اولویت بندی شده (گزینه تجربی است) تصادفی 'r'، 'تصادفی'
شبیه سازی. از بین تمام حالت های بعدی، یکی به طور تصادفی مستقل از اینکه آیا انتخاب می شود
این حالت قبلاً مشاهده شده است. در نتیجه، فقط شبیه سازی تصادفی
هنگامی که با یک حالت بن بست مواجه می شوید پایان می یابد.

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

-- زمان بندی[=فایل]
اندازه گیری های زمان بندی را به FILE اضافه کنید. اندازه‌گیری‌ها با خطای استاندارد نوشته می‌شوند
هیچ فایلی ارائه نشده است

--todo-max=NUM
حداکثر NUM حالت را در لیست کارهای انجام دهید. این گزینه فقط مربوط به وسعت است-
اول جستجو، که در آن NUM حداکثر تعداد حالت ها در هر سطح و برای عمق است
اول جستجو، جایی که NUM حداکثر عمق است

-t[NUM], --پی گیری[=NUM]
برای هر حالتی که با اقدامی از NAMES از انجام می‌شود، کوتاه‌ترین ردیابی بنویسید
گزینه --action یک بن بست است که با --بن بست شناسایی می شود یا یک واگرایی است
با - واگرایی به یک فایل شناسایی می شود. بیش از NUM اثر نوشته نخواهد شد. اگر
NUM ارائه نشده است، تعداد ردیابی ها نامحدود است. برای هر ردیابی که باید باشد
نوشته شده یک فایل منحصر به فرد با پسوند .trc (ردیابی) حاوی a ایجاد خواهد شد
کوتاه ترین ردیابی از حالت اولیه تا حالت بن بست آثار می تواند باشد
بسیار زیبا چاپ شده و با استفاده از tracepp به فرمت های دیگر تبدیل شده است.

-u, - داده های استفاده نشده
قسمت های استفاده نشده از مشخصات داده را حذف نکنید

گزینه های استاندارد:

-q, --ساکت
پیام های هشدار را نمایش ندهید

-v, -- پرحرف
نمایش پیام های میانی کوتاه

-d, - رفع اشکال
نمایش پیام های میانی دقیق

---log-level=سطح
نمایش پیام های میانی تا سطح و شامل

-h, --کمک
نمایش اطلاعات راهنما

- نسخه
نمایش اطلاعات نسخه

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