זוהי הפקודה lpsinvelm שניתן להפעיל בספק האירוח החינמי של OnWorks באמצעות אחת מתחנות העבודה המקוונות המרובות שלנו, כגון Ubuntu Online, Fedora Online, אמולטור מקוון של Windows או אמולטור מקוון של MAC OS
תָכְנִית:
שֵׁם
lpsinvelm - בדוק אינוריאנטים והשתמש בהם כדי לפשט או לבטל סכומים של LPS
תַקצִיר
לפסינוולם [אוֹפְּצִיָה]... --invfile=INVFILE [בקובץ [קובץ חוץ]]
תיאור
בודק אם הנוסחה הבוליאנית (ביטוי נתונים mCRL2 מסוג Bool) מסופקת כ
אינווריאנט הוא אינווריאנט של מפרט התהליך הליניארי (LPS) ב-INFILE. אם זה
במקרה זה, הכלי מבטל את כל הסיכומים של ה-LPS שמצבם מפר את
invariant, וכותב את התוצאה ל-OUTFILE. אם INFILE קיים, נעשה שימוש ב-stdin. אם
OUTFILE אינו קיים, נעשה שימוש ב-stdout.
הכלי יכול לשמש גם כדי לפשט את התנאים של הסכומים של ה-LPS הנתון.
אפשרויות
אוֹפְּצִיָה יכול להיות כל אחד מהבאים:
-y, -- כל הפרות
אל תסתיים ברגע שנמצאה הפרה בודדת של האינווריאנט, אבל
דווח על כל ההפרות במקום
-c, --דוגמה נגדית
הצג הערכת שווי המציינת מדוע הבלתי משתנה עשוי להיות מופר אם הוא
לא בטוח אם סיכום מפר את האינוריאנט
-o, --הַשׁרָאָה
להחיל אינדוקציה ברשימות
-iINNVFILE, --בלתי משתנה=INNVFILE
השתמש בנוסחה הבוליאנית (ביטוי נתונים mCRL2 מסוג Bool) ב-INVFILE as
בלתי משתנה
-n, --לא בדיקה
אל תבדוק אם האינוריאנט מתקיים לפני ביטול סיכומים בלתי ניתנים להשגה
-e, --ללא חיסול
אין לבטל או לפשט סכומים, אלא להוסיף את האינוריאנט לכל תנאי
-pPREFIX, --הדפס-נקודה=PREFIX
שמור קובץ .dot של ה-BDD המתקבל אם אי אפשר לקבוע אם א
summand מפר את האינוריאנט; PREFIX ישמש בתור קידומת של קבצי הפלט
-QNUM, --qlimit=NUM
הגבלת ספירה של מכמים ל-NUM משתנים. (ברירת מחדל NUM=1000, NUM=0 עבור
ללא הגבלה).
-rשֵׁם, - כותב מחדש=שֵׁם
השתמש באסטרטגיית שכתוב NAME: 'jitty' jitty rewriting (ברירת מחדל) 'jittyc' הידור
jitty שכתוב 'jittyp' jitty שכתוב עם מוכיח
-l, --לפשט-הכל
לפשט את התנאים של כל הסיכומים, במקום רק לבטל את הסיכומים
שהתנאים שלהם בשילוב עם האינוריאנט הם סתירות
-zפּוֹתֵר, --smt-solver=פּוֹתֵר
השתמש ב-SOLVER כדי להסיר נתיבים לא עקביים מה-BDDs בשימוש פנימי (כברירת מחדל,
לא מוחל ביטול נתיב): 'cvc' פותר SMT CVC3
-tלהגביל, --מגבלת זמן=להגביל
להשקיע לכל היותר LIMIT שניות על הוכחת נוסחה בודדת
--תזמונים[=קובץ]
הוסף מדידות תזמון ל-FILE. המדידות נכתבות לפי שגיאת תקן אם
לא מסופק FILE
אפשרויות סטנדרטיות:
-q, --שֶׁקֶט
אל תציג הודעות אזהרה
-v, --מִלוּלִי
להציג הודעות ביניים קצרות
-d, --לנפות
להציג הודעות ביניים מפורטות
--רמת יומן=רמה
להציג הודעות ביניים עד וכולל רמה
-h, - עזרה
להציג מידע עזרה
--גִרְסָה
להציג מידע על הגרסה
השתמש ב-lpsinvelm באינטרנט באמצעות שירותי onworks.net
