lps2lts - عبر الإنترنت في السحابة

برنامج:

اسم

lps2lts - إنشاء LTS من LPS

موجز

lps2lts [OPTION] ... [ملف [النفقة]]

الوصف

قم بإنشاء LTS من LPS في INFILE واحفظ النتيجة في OUTFILE. إذا INFILE ليست كذلك
زودت ، ويستخدم stdin. إذا لم يتم توفير OUTFILE ، فلن يتم تخزين LTS.

إذا تم استخدام معيد الكتابة 'jittyc' ، فإن متغير البيئة MCRL2_COMPILEREWRITER
(القيمة الافتراضية: 'mcrl2compilerewriter') تحدد البرنامج النصي الذي يجمع معيد الكتابة ،
و MCRL2_COMPILEDIR (القيمة الافتراضية: ".") تحدد مكان تخزين الملفات المؤقتة.

لاحظ أن lps2lts يمكن أن تقدم انتقالات متعددة بنفس التسمية بين أي زوج من
تنص على. إذا لم يكن ذلك مرغوبًا فيه ، يمكن إزالة هذه التحولات عن طريق تطبيق قوي
اختزال المحاكاة باستخدام أداة ltsconvert على سبيل المثال.

يتم تحديد تنسيق OUTFILE من خلال امتداده (ما لم يتم تحديده بواسطة ملف
اختيار). التنسيقات المدعومة هي:

"تلقائي" لتنسيق Aldebaran (CADP) ،
"نقطة" لتنسيق GraphViz (لم يعد مدعومًا كتنسيق إدخال) ،
"fsm" لتنسيق آلة الحالة المحدودة ، أو
'lts' لتنسيق mCRL2 LTS إذا تم استخدام إعادة كتابة jittyc ، فسيتم استخدام ملف
MCRL2_COMPILEREWRITER متغير البيئة (القيمة الافتراضية: mcrl2compilerewriter)
يحدد البرنامج النصي الذي يجمع معيد الكتابة ، و MCRL2_COMPILEDIR (القيمة الافتراضية:
'.') حيث يتم تخزين الملفات المؤقتة. لاحظ أن lps2lts يمكن أن يقدم عدة ملفات
انتقالات بنفس التسمية بين أي زوج من الحالات. إذا لم يكن هذا هو المطلوب ، مثل
يمكن إزالة التحولات عن طريق تطبيق اختزال قوي ثنائي المحاكاة باستخدام على سبيل المثال
أداة ltsconvert.

OPTIONS

OPTION يمكن أن يكون أيًا مما يلي:

-aأسماء, --عمل=أسماء
الكشف والإبلاغ عن الإجراءات في نظام الانتقالات التي لها أسماء الإجراءات من
NAMES ، قائمة مفصولة بفواصل. هذا مفيد على سبيل المثال للعثور على (أو إثبات ملف
غياب) خطأ عمل. تتم طباعة رسالة لكل تكرار لواحد من
أسماء العمل هذه. مع -t يتم إنشاء تتبعات الراية تجاه هذه الإجراءات

-b[NUM], - بت-تجزئة[=NUM]
استخدام تجزئة البت لتخزين الحالات وتخزينها في أكثر من NUM حالات. هذا يعني ذاك
بدلاً من الاحتفاظ بسجل كامل لجميع الحالات التي تمت زيارتها ، مصفوفة بت
يستخدم للإشارة إلى ما إذا كان قد تم رؤية تجزئة حالة من قبل أم لا.
على الرغم من أن هذا يعني أن هذا الخيار قد يتسبب في الخلط بين الدول وغيرها
(نظرًا لأنه يتم تعيينها إلى نفس التجزئة) ، قد يكون من المفيد استكشاف حجم كبير جدًا
LTSs التي لا يمكن استكشافها بخلاف ذلك. القيمة الافتراضية لـ NUM هي تقريبًا
2 * 10 ^ 8 (هذا يتوافق مع حوالي 25 ميجابايت من الذاكرة)

- مخبأ
استخدام تقنيات التخزين المؤقت للتعداد لتسريع توليد مساحة الدولة.

-c[اسم], --التقاء نهرين[=اسم]
تطبيق تحديد أولويات الانتقالات مع تسمية الإجراء NAME. (عندما لا يكون NAME
يتم توفير الأولوية (على سبيل المثال ، "-c") للإجراء "ctau". لإعطاء الأولوية ل
لاستخدام العلم -ctau. لاحظ أنه إذا لم تكن العملية الخطية متكدسة ،
فضاء الحالة الناتج هو بالضرورة متفرع ثنائي التشابه مع فضاء حالة
ليرة لبنانية. لا تتطلب خوارزمية التوليد المستخدمة عملية خطية
لتكون متقاربة تاو.

-D, --قفل
كشف حالات الجمود (أي يتم طباعة رسالة لكل حالة توقف تام)

-F, --تشعب
كشف التباعد (أي لكل حالة مع اختلاف (= حلقة تاو) الرسالة
مطبوعة). الخوارزمية لاكتشاف الاختلافات هي خطية لكل حالة ، لذلك
يصبح استكشاف الفضاء الحالة من الدرجة الثانية مع تشغيل هذا الخيار ، مما يتسبب في حدوث حالة
يصبح استكشاف الفضاء بطيئًا عند تمكين هذا الخيار.

-yBOOL, --غبي=BOOL
استبدل المتغيرات المجانية في LPS بقيم وهمية بناءً على قيمة BOOL:
"نعم" (افتراضي) أو "لا"

- تتبع الخطأ
إذا حدث خطأ أثناء الاستكشاف ، فاحفظ أي أثر للحالة التي لا يمكن أن تكون
استكشاف

--init-tsize=NUM
تعيين الحجم الأولي لجداول التجزئة المستخدمة داخليًا (الافتراضي هو 10000)

-lNUM, --الأعلى=NUM
استكشاف في حالات NUM على الأكثر

-mأسماء, --متعددة العمل=أسماء
كشف والإبلاغ عن حالات متعددة في نظام الانتقالات من NAMES ، فاصلة-
قائمة منفصلة. يعمل مثل -a ، باستثناء أن الإجراءات المتعددة مطابقة تمامًا ،
بما في ذلك معلمات البيانات.

--لا معلومات
لا تقم بإضافة معلومات الحالة إلى OUTFILEW بدون هذا الخيار يضيف lps2lts الحالة
المتجه إلى LTS. يؤدي هذا الخيار إلى تجاهل هذه المعلومات وتحديد حالتها
يشار إليها فقط برقم تسلسلي. معلومات الحالة الصريحة مفيدة لـ
أغراض التصور ، على سبيل المثال ، ولكن يمكن أن تتسبب في نمو OUTFILE
إلى حد كبير. لاحظ أن هذا الخيار يكون ضمنيًا عند الكتابة بتنسيق AUT.

-oFORMAT, --خارج=FORMAT
احفظ الإخراج بالشكل المحدد

--تقليم
استخدام التقليم التجميعي لتسريع توليد الفضاء.

-QNUM, - حد=NUM
قصر تعداد المحددات الكمية على NUM متغيرات. (الافتراضية NUM = 1000 ، NUM = 0 من أجل
غير محدود).

-rاسم, - الكاتب=اسم
استخدام استراتيجية إعادة الكتابة NAME: إعادة كتابة jitty "jitty" (افتراضي) تم تجميع "jittyc"
jitty إعادة كتابة "jittyp" jitty مع prover

-sاسم, --إستراتيجية=اسم
استكشف فضاء الولاية باستخدام إستراتيجية NAME: بحث "b" ، بحث "اتساع" عرض أول
(افتراضيًا) 'd' ، بحث 'العمق' العمق أولاً 'p' ، إعطاء الأولوية لـ 'الأولوية'
الإجراءات على حجتها الأولى من نوع Nat حيث فقط تلك الإجراءات مع
تم تحديد أدنى قيمة لهذه المعلمة. على سبيل المثال إذا كانت هناك إجراءات a(3) و
b(4) a(3) يبقى و bتم تخطي (4). الإجراءات بدون المعلمة الأولى من الفرز
يتم دائمًا اختيار Nat و multactions مع أكثر من إجراء واحد (الخيار هو
تجريبي) "q" ، تعطي الأولوية "لإعادة ترتيب الأولويات" للأفعال على حجةها الأولى
قم بفرز Nat (انظر الخيار - ذات الأولوية) ، واختر عشوائيًا واحدًا من هؤلاء للحصول على ملف
محاكاة عشوائية ذات أولوية (الخيار تجريبي) "r" ، عشوائي "عشوائي"
محاكاة. من بين جميع الحالات التالية ، يتم اختيار واحد عشوائيًا بشكل مستقل عما إذا كان
هذه الحالة قد لوحظت بالفعل. وبالتالي ، التزامن العشوائي فقط
ينتهي عند مواجهة حالة الجمود.

--كبح
في الوضع المطول ، لا تطبع رسائل تقدم تشير إلى عدد الزيارات التي تمت زيارتها
الدول والتحولات. بالنسبة لمساحات الحالة الكبيرة ، يمكن لعدد رسائل التقدم
كن مروعًا جدًا. هذه الميزة تساعد على قمع هؤلاء. رسائل مطولة أخرى ،
مثل العدد الإجمالي للحالات التي تم استكشافها ، تظل مرئية فقط.

- توقيت[=FILE]
إلحاق قياسات التوقيت بالملف. تتم كتابة القياسات لخطأ معياري إذا
لم يتم توفير FILE

--تودو ماكس=NUM
الاحتفاظ على الأكثر NUM حالات في قوائم المهام ؛ هذا الخيار مناسب فقط لاتساع-
البحث الأول ، حيث NUM هو الحد الأقصى لعدد الحالات لكل مستوى ، وللعمق
البحث الأول ، حيث NUM هو أقصى عمق

-t[NUM], --أثر[=NUM]
اكتب أقصر تتبع لكل حالة يتم الوصول إليها بإجراء من NAMES من
الخيار - العمل ، هو طريق مسدود تم اكتشافه مع --deadlock ، أو هو اختلاف
تم الكشف عنها باستخدام - اختلاف في ملف. لن تتم كتابة أكثر من NUM من التتبع. لو
لم يتم توفير NUM ، فإن عدد عمليات التتبع غير محدد. لكل عملية تتبع يجب أن تكون
كتب ملفًا فريدًا بامتداد .trc (تتبع) سيتم إنشاؤه يحتوي على ملحق
أقصر أثر من الحالة الأولية إلى حالة الجمود. يمكن أن تكون الآثار
جميلة مطبوعة وتحويلها إلى تنسيقات أخرى باستخدام tracepp.

-u, - بيانات غير مستخدمة
لا تقم بإزالة الأجزاء غير المستخدمة من مواصفات البيانات

الخيارات القياسية:

-q, --هادئ
لا تعرض رسائل تحذير

-v, - الإسراف
عرض رسائل وسيطة قصيرة

-d, --Debug
عرض رسائل وسيطة مفصلة

--تسجيل مستوى=LEVEL
عرض رسائل وسيطة تصل إلى المستوى وتشمل

-h, --مساعدة
عرض معلومات المساعدة

--الإصدار
عرض معلومات الإصدار

استخدم lps2lts عبر الإنترنت باستخدام خدمات onworks.net