זוהי הפקודה lts2pbes שניתן להפעיל בספק האירוח החינמי של OnWorks באמצעות אחת מתחנות העבודה המקוונות המרובות שלנו, כגון Ubuntu Online, Fedora Online, אמולטור מקוון של Windows או אמולטור מקוון של MAC OS
תָכְנִית:
שֵׁם
lts2pbes - מתרגם LTS ל-PBES
תַקצִיר
lts2pbes [אוֹפְּצִיָה]... [בקובץ [קובץ חוץ]]
תיאור
מתרגם LTS ב-INFILE וכותב את ה-PBES שנוצר ל-OUTFILE. אם OUTFILE אינו
בהווה, נעשה שימוש בפלט סטנדרטי. אם INFILE אינו קיים, נעשה שימוש בקלט סטנדרטי.
אפשרויות
אוֹפְּצִיָה יכול להיות כל אחד מהבאים:
-Dקובץ, --נתונים=קובץ
השתמש ב-FILE כמפרט הנתונים והפעולה. FILE חייב להיות קובץ .mcrl2 אשר
אינו מכיל סעיף init.
-fקובץ, --נוּסחָה=קובץ
השתמש בנוסחת המצב מ-FILE
-lקובץ, --לפס=קובץ
השתמש ב-FILE עבור מפרט הנתונים והפעולות. FILE חייב להיות קובץ .lps.
-mקובץ, --mcrl2=קובץ
השתמש ב-FILE כמפרט הנתונים והפעולה עבור ה-LTS. FILE חייב להיות .mcrl2
קובץ.
-oפורמט, --הַחוּצָה=פורמט
השתמש בפורמט פלט FORMAT: 'pbes' PBES בפורמט פנימי 'pbes_text' PBES in
פורמט טקסטואלי פנימי 'טקסט' PBES בפורמט טקסטואלי (mCRL2).
--תזמונים[=קובץ]
הוסף מדידות תזמון ל-FILE. המדידות נכתבות לפי שגיאת תקן אם
לא מסופק FILE
אפשרויות סטנדרטיות:
-q, --שֶׁקֶט
אל תציג הודעות אזהרה
-v, --מִלוּלִי
להציג הודעות ביניים קצרות
-d, --לנפות
להציג הודעות ביניים מפורטות
--רמת יומן=רמה
להציג הודעות ביניים עד וכולל רמה
-h, - עזרה
להציג מידע עזרה
--גִרְסָה
להציג מידע על הגרסה
השתמש ב-lts2pbes באופן מקוון באמצעות שירותי onworks.net
