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

برنامه:

نام

lpsinvelm - متغیرها را بررسی کنید و از آنها برای ساده‌سازی یا حذف جمع‌بندی LPS استفاده کنید.

خلاصه

lpsinvelm [گزینه]... --invfile=INVFILE [INFILE [پر از زاویه]]

شرح

بررسی می کند که آیا فرمول بولی (یک بیان داده mCRL2 از نوع Bool) به عنوان ارائه شده است یا خیر
invariant یک متغیر از مشخصات فرآیند خطی (LPS) در INFILE است. اگر این است
در این صورت، ابزار تمام جمع‌بندی‌های LPS را که شرایط آن‌ها را نقض می‌کند، حذف می‌کند
ثابت است و نتیجه را در OUTFILE می نویسد. اگر INFILE وجود داشته باشد، از stdin استفاده می شود. اگر
OUTFILE وجود ندارد، stdout استفاده می شود.

این ابزار همچنین می تواند برای ساده کردن شرایط جمع LPS داده شده استفاده شود.

OPTIONS

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

-y, --همه نقض
به محض یافتن یک نقض منفرد از ثابت خاتمه نکنید، اما
به جای آن همه تخلفات را گزارش کنید

-c, --مثال نقض
یک ارزش گذاری را نشان می دهد که نشان می دهد چرا در صورت عدم تغییر ممکن است آن را نقض کند
مطمئن نیست که یک جمع، ثابت را نقض می کند یا خیر

-o, -- القاء
اعمال استقرا در لیست ها

-iINVFILE, --ثابت=INVFILE
از فرمول بولی (یک بیان داده mCRL2 از نوع Bool) در INVFILE به عنوان استفاده کنید
ثابت

-n, -- بدون بررسی
قبل از حذف جمع‌های غیرقابل دسترس، بررسی نکنید که آیا ثابت باقی می‌ماند

-e, -- عدم حذف
جمع ها را حذف یا ساده نکنید، بلکه به هر شرطی یک متغیر را اضافه کنید

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

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

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

-l, --ساده کردن-همه
به جای حذف صرفاً جمع، شرایط همه جمع ها را ساده کنید
که شرایط آن در رابطه با نامتغیر، تناقض هستند

-zحل کننده, --smt-حل کننده=حل کننده
از SOLVER برای حذف مسیرهای ناسازگار از BDD های داخلی استفاده شده استفاده کنید (به طور پیش فرض،
هیچ حذف مسیر اعمال نمی شود): «cvc» حل کننده SMT CVC3

-tمحدود, --محدودیت زمانی=محدود
حداکثر LIMIT ثانیه را صرف اثبات یک فرمول کنید

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

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

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

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

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

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

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

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

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