pbes2bool - מקוון בענן

תָכְנִית:

שֵׁם

pbes2bool - צור BES מ-PBES ופתור אותו.

תַקצִיר

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

תיאור

פותר (P)BES מ-INFILE. אם INFILE אינו קיים, נעשה שימוש ב-stdin.

אפשרויות

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

-c, --דֶלְפֵּק
להדפיס בסוף עץ המסומן עם מופעים של הצד השמאלי של
משוואות; העץ הזה הוא אינדיקציה לאופן שבו pbes2bool הגיע לתוקף או
אי תקפות ה-PBES

-eרמה, --לִמְחוֹק=רמה
השתמש ברמת הסר LEVEL כדי להסיר משתני bes 'אין' אל תסיר bes שנוצר
משתנים. זה יכול להוביל לשימוש מופרז בזיכרון. (ברירת מחדל) 'חלק' להסיר
נוצרו משתני bes שאינם בשימוש, למעט אם הצד הימני שלו
המשוואה נכונה או לא נכונה. יש לחשב מחדש את rhss של משתנים, אם
נתקל שוב, וזה די נורמלי. 'הכל' מסיר כל משתנה bes כלומר
לא בשימוש יותר באף משוואה. זה די יעיל בזיכרון, אבל זה יכול להיות
זמן רב מאוד, שכן ה-rhss של משתני bes שהוסרו עשוי להיות חייב להיות
מחושב מחדש לעתים קרובות למדי.

-H, -- טבלאות hashtables
השתמש ב-hashtables בעת החלפה במשוואות bes, ותרגם פנימי
ביטויים לדיאגרמות החלטה בינאריות (לא מעודדים בגלל ביצועים)

-iפורמט, --ב=פורמט
השתמש בפורמט קלט FORMAT: 'pbes' PBES בפורמט פנימי 'pbes_text' PBES in
פורמט טקסטואלי פנימי 'טקסט' PBES בפורמט טקסטואלי (mCRL2) 'bes' BES פנימי
פורמט 'bes_text' BES בפורמט טקסטואלי פנימי 'cwi' BES בפורמט CWI 'pgsolver'
BES בפורמט PGSolver

-oפורמט, --תְפוּקָה=פורמט
השתמש בפורמט פלט FORMAT (אפשרות זו הוצאה משימוש. השתמש בכלי pbes2bes
במקום).

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

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

-zלחפש, --לחפש=לחפש
השתמש באסטרטגיית חיפוש SEARCH: 'breadth-first' חשב את הצד הימני של ה-
משתנים בוליאניים על בסיס כל הקודם זוכה. זה ניתן להשוואה עם א
חיפוש רוחב ראשון. זה טוב ליצירת דוגמאות נגד. (בְּרִירַת מֶחדָל)
'עומק-ראשון' חשב את הצד הימני של משתנים בוליאניים שבהם האחרון
המשתנה שנוצר נחקר תחילה. זה מתאים לעומק ראשון
לחפש. זה יכול לעלות באופן משמעותי על חיפוש רוחב ראשון כאשר התוקף של
נוסחה נקבעת לאחר עומקים גדולים יותר. 'ב' יד קצרה לרוחב-ראשון.
'd' יד קצרה לעומק-ראשון.

-sSTRAT, --אִסטרָטֶגִיָה=STRAT
השתמש באסטרטגיית החלפה STRAT: '0' חשב את כל המשוואות הבוליאניות שיכולות להיות
להגיע מהמצב ההתחלתי, ללא אופטימיזציה. זה הכי הרבה נתונים
אפשרות יעילה לכל משוואה שנוצרה. (ברירת מחדל) '1' בצע אופטימיזציה מידית
החלפת צד ימין במשתנים שכבר נחקרו שהם נכונים
או שקר בעת יצירת ביטוי. זה יעיל בזיכרון כמו 0. '2' In
בנוסף ל-1, החליפו גם משתנים שהם אמיתיים או שקריים ב-כבר
נוצר בצד ימין. המשמעות יכולה להיות שמשתנים מסוימים הופכים בלתי ניתנים להשגה
(למשל X0 ב-X0 וב-X1, כאשר X1 הופך לא נכון, בהנחה ש-X0 לא מתרחש במקום אחר.
יישמר אילו משתנים הפכו לבלתי ניתנים להשגה מכיוון שלא היו אלה
להיחקר. בהתאם ל-PBES, זה יכול להקטין את גודל ה-
יצר BES באופן מהותי אך דורש טביעת זיכרון גדולה יותר. '3' ב
בנוסף ל-2, בדוק עבור משתנים שנוצרו אם הם מתרחשים בלולאה,
כך שניתן להגדיר אותם כ-true או False, בהתאם לסמל הנקודה הקבועה.
זה יכול להגדיל את הזמן הדרוש ליצירת משוואה באופן משמעותי.

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

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

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

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

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

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

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

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

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

השתמש ב-pbes2bool באינטרנט באמצעות שירותי onworks.net