هذا هو الأمر maria الذي يمكن تشغيله في مزود الاستضافة المجانية OnWorks باستخدام إحدى محطات العمل المجانية المتعددة عبر الإنترنت مثل Ubuntu Online أو Fedora Online أو محاكي Windows عبر الإنترنت أو محاكي MAC OS عبر الإنترنت
برنامج:
اسم
ماريا - محلل قابلية الوصول المعياري لشبكات بتري عالية المستوى
موجز
ماري [الخيارات] ملفات
الوصف
توثق صفحة الدليل هذه بإيجاز ملف ماري أمر. وثائق أكثر اكتمالا هي
متوفر بتنسيق GNU Info ؛ انظر أدناه.
ماري هو برنامج يحلل نماذج الأنظمة المتزامنة الموضحة في مدخلاته
اللغة التي تعتمد على شبكات النظام الجبري. تم تقديم الشكلية من قبل Ekkart
Kindler و Hagen Völzer في ICATPN'98 ، مرونة in جبري شبكات.
Algebraic System Nets عبارة عن إطار عمل لا يحدد أي أنواع بيانات أو أشكال جبرية
عمليات. تم تصميم نظام نوع البيانات والعمليات في Maria بمستوى عالٍ
لغات البرمجة والمواصفات في الاعتبار. على الرغم من ذلك ، كل نموذج ماريا لديه
متناهية تتكشف.
لضمان إمكانية التشغيل البيني مع أدوات شبكة بتري منخفضة المستوى ، تترجم Maria المعرفات بتنسيق
شبكات مكشوفة لسلاسل من الأحرف الأبجدية الرقمية والشرطات السفلية. مرشح
Foldname.pl يمكن استخدامها أو تكييفها لتحسين قابلية قراءة المعرفات.
OPTIONS
تتبع Maria صيغة سطر أوامر GNU المعتادة ، مع خيارات طويلة تبدأ بخيارين
شرطات (`-'). يتم تضمين ملخص من الخيارات أدناه. للحصول على وصف كامل ، انظر
ملفات المعلومات.
-a قصر, - حدود الصف =قصر
تحديد حجم أنواع فهرس الصفيف بـ قصر القيم الممكنة. حد 0
يعطل الشيكات.
-b نموذج, - اتساع البحث الأول =نموذج
إنشاء الرسم البياني للوصول إلى نموذج باستخدام بحث واسع النطاق.
-C دليل, --جمع =دليل
قم بإنشاء كود C بتنسيق دليل لتقييم التعبيرات وللمستوى المنخفض
إجراءات خوارزمية تحليل المثيل الانتقالي. عند استخدام هذا الخيار ،
يتم الإبلاغ عن أخطاء التقييم بطريقة مختلفة قليلاً. المترجم
يعرض التقييم والتعبير الذي تسبب في الخطأ الأول في الولاية ؛ ال
تعرض التعليمات البرمجية المترجمة عدد الأخطاء. لأسباب تتعلق بالأداء ، فإن
لا يتحقق الرمز الذي تم إنشاؤه من أخطاء تجاوز السعة عند إضافة عناصر إلى مجموعات متعددة.
-c ، --لا تجميع
على العكس من -C. قيم كل التعبيرات في المترجم المضمن. هذا هو
السلوك الافتراضي.
-D رمز, - تعريف =رمز
حدد رمز المعالج رمز.
-d نموذج, - العمق - البحث الأول =نموذج
إنشاء الرسم البياني للوصول إلى نموذج باستخدام بحث العمق أولاً.
-E الفاصلة, - الحواف =الفاصلة
عند إنشاء الرسم البياني لإمكانية الوصول ، قم بالإبلاغ عن حجم الرسم البياني بعد كل شيء
الفاصلة ولدت الحواف.
-e سلسلة, --تنفيذ =سلسلة
تنفيذ سلسلة.
-g ملف الرسم البياني, - الرسم =ملف الرسم البياني
قم بتحميل رسم بياني لقابلية الوصول تم إنشاؤه مسبقًا من ملف الرسم البياني.rgh.
-H h[,f[,t]], - الحلقات =h[,f[,t]]
تكوين معلمات التحقق الاحتمالي (-P). تخصيص t بالمذيب
وظائف التجزئة من f العناصر وجداول التجزئة المقابلة لـ h بت لكل منهما. على حد سواء h
و f سيتم تقريبه إلى القيم المناسبة التالية.
- ؟، -ح ، --مساعدة
اطبع ملخصًا لخيارات سطر الأوامر إلى Maria واخرج.
-I دليل, - تشمل =دليل
ألحق دليل إلى قائمة الدلائل التي تم البحث عنها لتضمين الملفات.
-i الأعمدة, - العرض =الأعمدة
اضبط الهامش الأيمن للإخراج على الأعمدة. الافتراضي هو 80.
-j العمليات, - وظائف =العمليات
عند فحص خصائص الأمان (خيارات -L, -M و -P) ، استخدم هذا العدد الكبير من العمال
عمليات لتسريع التحليل على جهاز كمبيوتر متعدد المعالجات. أنظر أيضا -k و
-Z.
-k ميناء[/مضيف], - ربط =ميناء[/مضيف]
توزيع فحص نموذج الأمان (خيارات -L, -M و -P) في شبكة TCP / IP. ل
الخادم فقط ميناء يتم تحديده على أنه عدد صحيح 16 بت بدون إشارة ، وعادة ما يكون بين
1024 و 65535. للعمليات العاملة ، ميناء/مضيف يحدد المنفذ و
عنوان الخادم. أنظر أيضا -j.
-L نموذج, - عديم الخسارة =نموذج
حمل نموذج والاستعداد لتحليلها من خلال بناء مجموعة من الحالات التي يمكن الوصول إليها
في ملفات القرص. أنظر أيضا -M, -P, -j و -k.
-m نموذج, - الطراز =نموذج
حمل نموذج ومسح الرسم البياني الخاص بإمكانية الوصول.
-M نموذج, --md5- مضغوط =نموذج
حمل نموذج والاستعداد لتحليلها من خلال بناء تقريب مفرط لـ
مجموعة من الحالات التي يمكن الوصول إليها في الذاكرة الرئيسية. أنظر أيضا -P, -L, -j و -k.
-N com.cregexp, - الاسم =com.cregexp
حدد الأسماء المسموح بها في السياق c كتعبير عادي موسع REGEXP.
يتم تحديد السياق من خلال الحرف الأول من سلسلة المعلمة ؛ ال
تشكل الأحرف التالية التعبير العادي الذي يجب أن تسمح به الأسماء
المباراة.
-n com.cregexp, --لا اسم =com.cregexp
حدد الأسماء غير المسموح بها في السياق c كتعبير عادي موسع
REGEXP.
إذا كان كل من -N و و -n محددة للسياق c، ثم تأخذ مباراة السماح
الأولوية. على سبيل المثال ، للمطالبة بأن تكون جميع أسماء الأنواع المعرفة من قبل المستخدم
تم إنهاؤه ب _t، حدد -لا -Nt'_t $ '. الاقتباسات في المعلمة الأخيرة هي
المطلوب لإزالة المعنى الخاص من $ في قذيفة سطر الأوامر أنت
ربما تستخدم لاستدعاء ماريا.
-P نموذج, - احتمالية =نموذج
حمل نموذج والاستعداد لتحليلها من خلال بناء مجموعة من الحالات التي يمكن الوصول إليها
في الذاكرة الرئيسية باستخدام تقنية تسمى bitstate الثرم.
-p أمر, - خاصية مترجم =أمر
حدد الأمر المراد استخدامه لترجمة الخاصية التلقائية. يجب على الأمر
اقرأ صيغة من الإدخال القياسي واكتب آليًا مطابقًا
وصف الإخراج القياسي. المترجم LBT متوافق مع هذا
الخيار.
-q قصر, - حد الكم =قصر
منع التقدير الكمي (مجموع مجموعات متعددة) للأنواع التي تحتوي على أكثر من قصر ممكن
القيم. يؤدي حد 0 إلى تعطيل الشيكات.
-U رمز, --undefine =رمز
قم بإلغاء تحديد رمز المعالج رمز.
-u [a][f[ملف]], - غير مطوي =[a][f[ملف]]
افتح الشبكة باستخدام الخوارزمية a واكتبها في شكل f إلى ملف. إذا ملف
لم يتم تحديده ، قم بتفريغ الشبكة غير المطوية إلى الإخراج القياسي. الأشكال الممكنة
. m (ماريا (يمكن قراءتها بواسطة الإنسان) ، افتراضي) ، l (لولا) ، p (PEP) و r (همز). هناك
نوعان من الخوارزميات: التقليدية (الافتراضية) ويتم تقليلها من خلال إنشاء ملف قابل للتغطية
وسم (M).
-الخامس، --الإصدار
اطبع رقم إصدار Maria واخرج.
-الخامس، - الإسراف
اعرض معلومات مطولة عن مراحل مختلفة من التحليل.
-W ، - تحذيرات
تفعيل التحذيرات حول بنيات الشبكة المشبوهة. هذا هو السلوك الافتراضي.
-w ، --لا تحذيرات
على العكس من -W. تعطيل كافة التحذيرات.
-x قاعدة الأرقام, - راديكس =قاعدة الأرقام
حدد رقم الأساس لإخراج التشخيص. القيم المسموح بها لـ قاعدة الأرقام .
أكتوبر, ثماني, 8, عرافة, عشري, 16, ديسمبر, عدد عشري و 10. الافتراضي هو استخدام
أرقام عشرية.
- ص ، - ضغط مخفي
قلل مجموعة الحالات التي يمكن الوصول إليها من خلال عدم تخزين الحالات اللاحقة لـ
حالات الانتقال التي من أجلها أ إخفاء الشرط يحمل. الخلفاء المخفيين هم
المخزنة في مجموعة حالة منفصلة. هذا الخيار قد يحفظ الذاكرة (-L or -m) أو تقليل
احتمال حذف الحالات (-M or -P) ، وقد يؤدي إلى تحسين
كفاءة التحليل المتوازي (-j or -k) ، ولكنها قد تزيد أيضًا بشكل كبير
متطلبات وقت المعالج. يعمل الخيار أيضًا مع نموذج الحياة
التحقق ، ولكن ليس هناك ما يضمن أن القيم الحقيقية لخصائص الحياة
يبقى على حاله. يمكن دمج هذا الخيار مع -Z.
-ص ، --لا ضغط مخفي
على العكس من -Y. هذا هو السلوك الافتراضي.
-Z ، - مسارات الضغط
قلل مجموعة الحالات التي يمكن الوصول إليها من خلال عدم تخزين الحالات الوسيطة التي لها في
أكثر من خلف واحد. هذا الخيار قد يحفظ الذاكرة (-L or -m) أو تقليل
احتمال حذف الحالات (-M or -P) ، وقد يحسن الكفاءة
من التحليل الموازي (-j or -k) ، ولكنه قد يزيد أيضًا بشكل كبير من
متطلبات وقت المعالج. يعمل الخيار أيضًا مع فحص النموذج الحي ،
ولكن ليس هناك ما يضمن بقاء القيم الحقيقية لخصائص الحياة
دون تغيير. يمكن دمج هذا الخيار مع -Y.
-z ، - لا ضغط المسارات
على العكس من -Z. هذا هو السلوك الافتراضي.
استخدم ماريا عبر الإنترنت باستخدام خدمات onworks.net
