lps2lts - מקוון בענן

תָכְנִית:

שֵׁם

lps2lts - צור LTS מ-LPS

תַקצִיר

lps2lts [אוֹפְּצִיָה]... [בקובץ [קובץ חוץ]]

תיאור

צור LTS מה-LPS ב-INFILE ושמור את התוצאה ב-OUTFILE. אם INFILE אינו
מסופק, נעשה שימוש ב-stdin. אם OUTFILE אינו מסופק, ה-LTS אינו מאוחסן.

אם נעשה שימוש בכותב מחדש 'jittyc', אז משתנה הסביבה MCRL2_COMPILEREWRITER
(ערך ברירת מחדל: 'mcrl2compilerewriter') קובע את הסקריפט שמרכיב את הכותב מחדש,
ו-MCRL2_COMPILEDIR (ערך ברירת מחדל: '.') קובע היכן מאוחסנים קבצים זמניים.

שים לב ש-lps2lts יכול לספק מעברים מרובים עם אותה תווית בין כל זוג של
מדינות. אם זה לא רצוי, מעברים כאלה ניתן להסיר על ידי יישום חזק
הפחתה של bisimulation באמצעות למשל הכלי ltsconvert.

הפורמט של OUTFILE נקבע על פי הסיומת שלו (אלא אם כן הוא צוין על ידי
אוֹפְּצִיָה). הפורמטים הנתמכים הם:

'aut' עבור פורמט Aldebaran (CADP),
'נקודה' עבור פורמט GraphViz (לא נתמך עוד כפורמט קלט),
'fsm' עבור פורמט Finite State Machine, או
'lts' עבור פורמט mCRL2 LTS אם נעשה שימוש ב-jittyc rewriter, אז ה-
משתנה סביבה MCRL2_COMPILEREWRITER (ערך ברירת מחדל: mcrl2compilerewriter)
קובע את הסקריפט שמרכיב את הכותב מחדש, ואת MCRL2_COMPILEDIR (ערך ברירת מחדל:
'.') קובע היכן מאוחסנים קבצים זמניים. שים לב ש-lps2lts יכול לספק מספר
מעברים עם אותה תווית בין כל זוג מצבים. אם זה לא רצוי, כזה
ניתן להסיר מעברים על ידי יישום רדוקטון בי-סימולציה חזק באמצעות למשל
הכלי ltsconvert.

אפשרויות

אוֹפְּצִיָה יכול להיות כל אחד מהבאים:

-aשמות, --פעולה=שמות
לזהות ולדווח על פעולות במערכת המעברים שיש להן שמות פעולות
NAMES, רשימה מופרדת בפסיקים. זה למשל שימושי כדי למצוא (או להוכיח את
היעדר) של שגיאת פעולה. הודעה מודפסת עבור כל התרחשות של אחד מ
שמות הפעולות הללו. עם הדגל -t נוצרים עקבות לעבר פעולות אלו

-b[NUM], --bit-hash[=NUM]
השתמש ב-bit hashing כדי לאחסן מצבים ולאחסן לכל היותר NUM מצבים. זה אומר ש
במקום לשמור תיעוד מלא של כל המדינות שביקרו בהן, קצת מערך
משמש שמציינים אם חשיש של מדינה נראה בעבר או לא.
אם כי זה אומר שאופציה זו עלולה לגרום לטעות במדינות אחרות
(מכיוון שהם ממופים לאותו Hash), זה יכול להיות שימושי לחקור גדול מאוד
LTSs שאינם ניתנים לחקירה אחרת. ערך ברירת המחדל עבור NUM הוא בערך
2*10^8 (זה מתאים לכ-25MB של זיכרון)

- מטמון
השתמש בטכניקות מטמון ספירה כדי להאיץ את יצירת חלל המדינה.

-c[שֵׁם], --מִפגָשׁ[=שֵׁם]
החל תעדוף של מעברים עם תווית הפעולה NAME.(כאשר אין NAME
עדיפות מסופקת (כלומר, '-c') ניתנת לפעולה 'ctau'. לתת עדיפות ל
כדי tau השתמש בדגל -ctau. שימו לב שאם התהליך הליניארי אינו טאו-קונפלונטי,
מרחב המצב שנוצר בהכרח מסתעף בדומה למרחב המצב של
ה-lps. אלגוריתם היצירה בו נעשה שימוש אינו מצריך את התהליך הליניארי
להיות טאו מתכנס.

-D, --מָבוֹי סָתוּם
לזהות מבוי סתום (כלומר על כל מבוי סתום מודפסת הודעה)

-F, --הִסתַעֲפוּת
לזהות הבדלים (כלומר עבור כל מצב עם סטייה (=לולאת טאו) יש הודעה
מודפס). האלגוריתם לזיהוי הפערים הוא ליניארי עבור כל מצב, אז
חקר חלל מצב הופך ריבועי עם אפשרות זו מופעלת, וגורם למצב
חקר החלל יהפוך לאיטי כאשר אפשרות זו מופעלת.

-yBOOL, --דֶמֶה=BOOL
החלף משתנים חופשיים ב-LPS בערכי דמה המבוססים על הערך של BOOL:
'כן' (ברירת מחדל) או 'לא'

--מעקב אחר שגיאות
אם מתרחשת שגיאה במהלך החקירה, שמור מעקב למצב שלא יכול להיות
נחקרו

--init-tsize=NUM
הגדר את הגודל הראשוני של טבלאות ה-hash בשימוש פנימי (ברירת המחדל היא 10000)

-lNUM, --מקסימום=NUM
לחקור לכל היותר NUM מדינות

-mשמות, -- ריבוי פעולה=שמות
לזהות ולדווח על ריבוי פעולות במערכת המעברים מ-NAMES, פסיק
רשימה מופרדת. עובד כמו -a, פרט לכך שריבוי פעולות מותאמות בדיוק,
כולל פרמטרי נתונים.

--אין מידע
אל תוסיף מידע מצב ל-OUTFILEללא אפשרות זו lps2lts מוסיף מצב
וקטור ל-LTS. אפשרות זו גורמת למחיקת מידע זה ומציינת
מסומנים רק על ידי מספר רצף. מידע מצב מפורש שימושי עבור
למטרות הדמיה, למשל, אבל יכול לגרום ל-OUTFILE לגדול
במידה ניכרת. שים לב שהאפשרות הזו משתמעת בעת כתיבה בפורמט AUT.

-oפורמט, --הַחוּצָה=פורמט
שמור את הפלט בפורמט שצוין

--לִגזוֹם
השתמש ב- summand pruning כדי להאיץ את יצירת שטח המדינה.

-QNUM, --qlimit=NUM
הגבלת ספירה של מכמים ל-NUM משתנים. (ברירת מחדל NUM=1000, NUM=0 עבור
ללא הגבלה).

-rשֵׁם, - כותב מחדש=שֵׁם
השתמש באסטרטגיית שכתוב NAME: 'jitty' jitty rewriting (ברירת מחדל) 'jittyc' הידור
jitty שכתוב 'jittyp' jitty שכתוב עם מוכיח

-sשֵׁם, --אִסטרָטֶגִיָה=שֵׁם
חקור את מרחב המצב באמצעות האסטרטגיה NAME: 'b', 'רוחב' חיפוש רוחב ראשון
(ברירת מחדל) 'd', 'depth' עומק-ראשון חיפוש 'p', 'prioritized' מתן עדיפות ליחיד
פעולות על הטיעון הראשון שלה להיות מסוג Nat שבו רק אותן פעולות עם
הערך הנמוך ביותר עבור פרמטר זה נבחר. למשל אם יש פעולות a(3) ו
b(4), a(3) נשאר ו b(4) נדלג. פעולות ללא פרמטר ראשון מסוגו
תמיד נבחרות Nat ו-multactions עם יותר מפעולה אחת (האפשרות היא
experimental) 'q', 'rprioritized' נותנים עדיפות לפעולות על הטיעון הראשון שלו הוא של
מיין Nat (ראה אפשרות --עדיפות), ובחר באקראי אחד מאלה כדי לקבל א
סימולציה אקראית עם עדיפות (האפשרות היא ניסיונית) 'r', 'אקראי' אקראי
סימולציה. מתוך כל המצבים הבאים אחד נבחר באקראי ללא תלות בשאלה אם
מצב זה כבר נצפה. כתוצאה מכך, סימולציה אקראית בלבד
מסתיים כאשר נתקלים במצב מבוי סתום.

--לדכא
במצב מילולי, אל תדפיס הודעות התקדמות המציינות את מספר הביקורים
מדינות ומעברים. עבור שטחי מדינה גדולים, מספר הודעות ההתקדמות יכול
להיות די נורא. תכונה זו עוזרת לדכא אותם. הודעות מילוליות אחרות,
כמו המספר הכולל של מדינות שנחקרו, פשוט תישאר גלוי.

--תזמונים[=קובץ]
הוסף מדידות תזמון ל-FILE. המדידות נכתבות לפי שגיאת תקן אם
לא מסופק FILE

--todo-max=NUM
שמור לכל היותר NUM מצבים ברשימות מטלות; אפשרות זו רלוונטית רק לרוחב-
חיפוש ראשון, כאשר NUM הוא המספר המרבי של מצבים לכל רמה, ולעומק
חיפוש ראשון, כאשר NUM הוא העומק המרבי

-t[NUM], --זֵכֶר[=NUM]
כתוב את המעקב הקצר ביותר לכל מצב שמגיעים אליו עם פעולה מ-NAMES מ
option --action, הוא מבוי סתום שזוהה עם --deadlock, או שהוא סטייה
זוהה עם --divergence לקובץ. לא ייכתבו יותר מ-NUM עקבות. אם
NUM אינו מסופק, מספר העקבות אינו מוגבל. עבור כל מעקב שעתיד להיות
נכתב קובץ ייחודי עם סיומת .trc (trace) ייווצר המכיל א
המסלול הקצר ביותר מהמצב ההתחלתי למצב המבוי הסתום. העקבות יכולות להיות
די מודפס והומר לפורמטים אחרים באמצעות tracepp.

-u, --נתונים שאינם בשימוש
אל תסיר חלקים שאינם בשימוש ממפרט הנתונים

אפשרויות סטנדרטיות:

-q, --שֶׁקֶט
אל תציג הודעות אזהרה

-v, --מִלוּלִי
להציג הודעות ביניים קצרות

-d, --לנפות
להציג הודעות ביניים מפורטות

--רמת יומן=רמה
להציג הודעות ביניים עד וכולל רמה

-h, - עזרה
להציג מידע עזרה

--גִרְסָה
להציג מידע על הגרסה

השתמש ב-lps2lts באופן מקוון באמצעות שירותי onworks.net