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