هذا هو الأمر mona الذي يمكن تشغيله في موفر الاستضافة المجاني OnWorks باستخدام إحدى محطات العمل المجانية المتعددة عبر الإنترنت مثل Ubuntu Online أو Fedora Online أو محاكي Windows عبر الإنترنت أو محاكي MAC OS عبر الإنترنت
برنامج:
اسم
منى - إجراء اتخاذ القرار للمنطق WS1S وWS2S
موجز
منى [ الخيارات ] منى ملف
الوصف
MONA هي أداة تترجم الصيغ في المنطق WS1S أو WS2S إلى حالة محدودة
الأتمتة التي تمثلها BDDs. قد تعبر الصيغ عن أنماط البحث المؤقتة
خصائص الأنظمة التفاعلية، وقيود شجرة التحليل، وما إلى ذلك. تقوم MONA أيضًا بتحليل
الآلي الناتج عن التجميع، ويحدد ما إذا كانت الصيغة صالحة أم لا،
إذا كانت الصيغة غير صالحة، فسيتم إنشاء مثال مضاد.
مشروع MONA هو مشروع بحثي في قسم علوم الكمبيوتر في آرهوس
Πανεπιστήμιο.
تتوفر الوثائق الكاملة وكود مصدر GPL والأوراق البحثية ذات الصلة على موقع
الصفحة الرئيسية لمشروع MONA على http://www.brics.dk/mona
OPTIONS
-w إخراج آلي كامل. الافتراضي هو إخراج حجمه فقط.
-n لا تحلل الإنسان. الافتراضي هو تحليل الصلاحية وعدم الرضا
ولإنشاء مثال مرضي ومثال مضاد.
-t طباعة الوقت المنقضي لكل مرحلة. إذا تم استخدام -s أيضًا، فإن الوقت لكل جهاز آلي
تتم طباعة العملية أيضا.
- إحصائيات الطباعة. طباعة معلومات لكل عملية تشغيل آلي وملخص.
-i طباعة أتمتة متوسطة (يعني -s).
-d تفريغ AST والرمز والرمز DAG. مفيدة لتصحيح الأخطاء.
-q هادئ، لا تطبع التقدم.
-e تمكين التجميع المنفصل. (راجع متغير بيئة MONALIB أدناه.)
-oN مستوى تحسين الكود N (0 = لا شيء، 1 = آمن، 2 = إرشادي) (الافتراضي 1).
-r تعطيل إعادة ترتيب فهرس BDD، واستخدام ترتيب الإعلان كترتيب للفهرس. تقصير
هو إعادة ترتيب مؤشرات BDD بشكل تجريبي.
-f فرض نمط إخراج وضع الشجرة العادي. ينطبق فقط على وضع WSRT.
-m محاكاة M2L-Str البديلة (نمط الإصدار 1.3).
-h تمكين تحليل القبول الموروث.
-u أتمتة الإخراج غير المقيدة. إنشاء أتمتة تقليدية عن طريق تحويل "لا أهتم"
تنص على "رفض" الحالات والتقليل منها.
-gw إخراج آلي كامل بتنسيق Graphviz (يتضمن -n -q). (جراففيز متاح
at http://www.graphviz.org/)
-gs شجرة مثال مُرضية للإخراج بتنسيق Graphviz (يعني -q).
-gc شجرة المثال المضاد للإخراج بتنسيق Graphviz (يتضمن -q).
-gd رمز التفريغ DAG بتنسيق Graphviz (يتضمن -n -q).
-xw إخراج آلي كامل بتنسيق خارجي (يعني -n -q). "التنسيق الخارجي" هو
التنسيق المستخدم بواسطة dfalib وgtalib، راجع الحزمة المصدر.
البيئة
موناليب
يحدد الدليل المستخدم لأتمتة التجميع المنفصل (الافتراضي هو الحالي
الدليل).
استخدم منى عبر الإنترنت باستخدام خدمات onworks.net
