هذا هو الأمر ltsconvert الذي يمكن تشغيله في مزود الاستضافة المجانية OnWorks باستخدام إحدى محطات العمل المجانية المتعددة على الإنترنت مثل Ubuntu Online أو Fedora Online أو محاكي Windows عبر الإنترنت أو محاكي MAC OS عبر الإنترنت
برنامج:
اسم
ltsconvert - تحويل وتقليل LTS اختياريًا
موجز
ltsconvert [OPTION] ... [ملف [النفقة]]
الوصف
قم بتحويل نظام الانتقال المسمى (LTS) من INFILE إلى OUTFILE في الملف المطلوب
بعد تطبيق طريقة التصغير المحددة (الافتراضي هو لا شيء). إذا كان OUTFILE هو
غير مزود ، يتم استخدام stdout. إذا لم يتم توفير INFILE ، فسيتم استخدام stdin.
يتم تحديد تنسيق الإخراج من خلال امتداد OUTFILE ، في حين أن تنسيق الإدخال هو
يحددها محتوى INFILE. يمكن استخدام الخيارات --in and --out لفرض الإدخال
وتنسيقات الإخراج. التنسيقات المدعومة هي:
"تلقائي" لتنسيق Aldebaran (CADP) ،
"نقطة" لتنسيق GraphViz (لم يعد مدعومًا كتنسيق إدخال) ،
"fsm" لتنسيق آلة الحالة المحدودة ، أو
'lts' لتنسيق mCRL2 LTS (افتراضي)
OPTIONS
OPTION يمكن أن يكون أيًا مما يلي:
-D, - تحديد
تحديد LTS
-eاسم, - التكافؤ=اسم
إنشاء LTS مكافئ ، مع الاحتفاظ بالتكافؤ NAME: هوية "لا شيء"
التكافؤ (الافتراضي) ثنائي التشابه القوي "bisim-sig" ثنائي التشابه القوي
باستخدام صقل التوقيع المتفرعة ثنائية التشابه المتفرعة
bisim-sig "ثنائية التشابه المتفرعة باستخدام تحسين التوقيع" dpbranching-bisim "
الاختلاف الذي يحافظ على التفرع ثنائي التشابك dpbranching-bisim-sig
الحفاظ على ثنائية التشابه المتفرعة باستخدام صقل التوقيع ضعيف
ثنائية التشابه الضعيفة ثنائية التشابه الضعيفة باستخدام تنقيح التوقيع dpweak-
اختلاف ثنائي بيسيم يحافظ على ضعف التشابه الضعيف اختلاف dpweak-bisim-sig
الحفاظ على ثنائية التشابه الضعيفة باستخدام محاكاة قوية لصقل التوقيع "sim"
التكافؤ "تتبع" قوي التتبع التكافؤ "التتبع الضعيف" معادلة التتبع الضعيفة
تخفيض نجم تاو
-iFORMAT, --في=FORMAT
استخدم FORMAT كتنسيق الإدخال
-lFILE, --lps=FILE
استخدم FILE باعتباره LPS الذي تم إنشاء LTS منه ؛ قد تكون هناك حاجة إلى هذا
تخزين أسماء المعلمات الصحيحة للحالات عند الحفظ بتنسيق fsm وإلى
تحويل غير mCRL2 LTSs إلى mCRL2 LTS
- لا تصل
لا تقم بإجراء فحص قابلية الوصول على إدخال LTS
-n, --لا دولة
اترك معلومات الحالة عند الحفظ بتنسيق نقطي
-oFORMAT, --خارج=FORMAT
استخدم FORMAT كتنسيق الإخراج
- تاو=أسماء الأفعال
اعتبر الإجراءات التي تحمل اسمًا في القائمة المفصولة بفواصل ACTNAMES داخلية
(تاو) بالإضافة إلى تلك المحددة على هذا النحو من خلال المدخلات
- توقيت[=FILE]
إلحاق قياسات التوقيت بالملف. تتم كتابة القياسات لخطأ معياري إذا
لم يتم توفير FILE
الخيارات القياسية:
-q, --هادئ
لا تعرض رسائل تحذير
-v, - الإسراف
عرض رسائل وسيطة قصيرة
-d, --Debug
عرض رسائل وسيطة مفصلة
--تسجيل مستوى=LEVEL
عرض رسائل وسيطة تصل إلى المستوى وتشمل
-h, --مساعدة
عرض معلومات المساعدة
--الإصدار
عرض معلومات الإصدار
استخدم ltsconvert عبر الإنترنت باستخدام خدمات onworks.net
