هذا هو الأمر lpsinvelm الذي يمكن تشغيله في مزود الاستضافة المجانية OnWorks باستخدام إحدى محطات العمل المجانية المتعددة على الإنترنت مثل Ubuntu Online أو Fedora Online أو محاكي Windows عبر الإنترنت أو محاكي MAC OS عبر الإنترنت
برنامج:
اسم
lpsinvelm - افحص الثوابت واستخدمها لتبسيط أو حذف مجموعات LPS
موجز
lpsinvelm [OPTION] ... --invfile = INVFILE [ملف [النفقة]]
الوصف
للتحقق مما إذا كانت الصيغة المنطقية (تعبير بيانات mCRL2 لفرز Bool) مقدمة كـ
الثابت هو ثابت لمواصفات العملية الخطية (LPS) في INFILE. إن كان هذا
في الحالة ، تقوم الأداة بإزالة جميع موجزات LPS التي تنتهك حالتها
ثابت ، ويكتب النتيجة إلى OUTFILE. في حالة وجود INFILE ، يتم استخدام stdin. لو
OUTFILE غير موجود ، يتم استخدام stdout.
يمكن أيضًا استخدام الأداة لتبسيط شروط موجزات LPS المحددة.
OPTIONS
OPTION يمكن أن يكون أيًا مما يلي:
-y, - جميع الانتهاكات
لا تنتهي بمجرد العثور على انتهاك واحد للثابت ، ولكن
الإبلاغ عن جميع الانتهاكات بدلا من ذلك
-c, --مكافحة المثال
عرض تقييم يشير إلى سبب احتمال انتهاك الثابت إذا كان
غير مؤكد ما إذا كان الاستدعاء ينتهك الثابت أم لا
-o, --الحث
تطبيق الاستقراء على القوائم
-iINVFILE, - متغير=INVFILE
استخدم الصيغة المنطقية (تعبير بيانات mCRL2 لفرز منطقي) في INVFILE كـ
ثابتة
-n, --لا الاختيار
لا تتحقق مما إذا كان الثابت ثابتًا قبل التخلص من الملخصات التي يتعذر الوصول إليها
-e, - لا القضاء
لا تستبعد أو تبسط عمليات الجمع ، بل أضف الثابت لكل شرط
-pاختصار, - طباعة نقطة=اختصار
حفظ ملف .dot من BDD الناتج إذا كان من المستحيل تحديد ما إذا كان ملف
استدعاء ينتهك الثابت ؛ سيتم استخدام PREFIX كبادئة لملفات الإخراج
-QNUM, - حد=NUM
قصر تعداد المحددات الكمية على NUM متغيرات. (الافتراضية NUM = 1000 ، NUM = 0 من أجل
غير محدود).
-rاسم, - الكاتب=اسم
استخدام استراتيجية إعادة الكتابة NAME: إعادة كتابة jitty "jitty" (افتراضي) تم تجميع "jittyc"
jitty إعادة كتابة "jittyp" jitty مع prover
-l, - تبسيط الكل
تبسيط شروط جميع الجمل ، بدلاً من مجرد حذف الجمل
التي شروطها المقترنة مع الثابت هي التناقضات
-zمحلول, - SMT- حلالا=محلول
استخدم SOLVER لإزالة المسارات غير المتسقة من BDDs المستخدمة داخليًا (افتراضيًا ،
لا يتم تطبيق إزالة المسار): 'cvc' ، محلل SMT CVC3
-tمما سيحدث, - المهلة=مما سيحدث
قضاء LIMIT من الثواني على الأكثر في إثبات صيغة واحدة
- توقيت[=FILE]
إلحاق قياسات التوقيت بالملف. تتم كتابة القياسات لخطأ معياري إذا
لم يتم توفير FILE
الخيارات القياسية:
-q, --هادئ
لا تعرض رسائل تحذير
-v, - الإسراف
عرض رسائل وسيطة قصيرة
-d, --Debug
عرض رسائل وسيطة مفصلة
--تسجيل مستوى=LEVEL
عرض رسائل وسيطة تصل إلى المستوى وتشمل
-h, --مساعدة
عرض معلومات المساعدة
--الإصدار
عرض معلومات الإصدار
استخدم lpsinvelm عبر الإنترنت باستخدام خدمات onworks.net
