מבוא לאימות תוכנה

ספר אלקטרוני מאת: ניר אדר

6.6.3. בדיקת מודל סימבולית לפי מבנה הנוסחה

אנחנו עובדים על מבנה קריפקה $plot:$M\left( {S,R,L} \right)$$ ונוסחה plot:$f$ . האלגוריתם מטפל בתתי הנוסחאות של מהפשוטה למורכבת, וכשמטפלים בתת נוסחה plot:$g$ מניחים שכל תתי הנוסחאות של כבר טופלו. נוסחה טופלה כאשר קיים BDD המייצג את קבוצת המצבים המספקים אותה.

נחלק את בדיקת המודל למקרים שונים. המקרים נבדלים ביניהם על פי מבנה הנוסחה.

$plot:$f = a \in AP$$ : נשתמש ב- $plot:$a\left( {\bar v} \right)$$ הנתון. נחזיר $plot:$f\left( {\bar v} \right) = a\left( {\bar v} \right)$$ .
אם $plot:$f = {f_1} \wedge {f_2}$$ (וכבר חישבנו BDDs $plot:${f_1}\left( {\bar v} \right)$$ עבור $plot:${f_1}$$ ו- $plot:${f_2}\left( {\bar v} \right)$$ עבור $plot:${f_2}$$ ), אזי

ה-BDD עבור יסומן $plot:$f\left( {\bar v} \right)$$ ויתקבל על ידי הפעלת $plot:$ \wedge $$ על ה-BDDs של $plot:${f_1},{f_2}$$ .

הסבר: למה החישוב הזה נכון?

ה-BDD $plot:${f_1}\left( {\bar v} \right)$$ מייצג את הפונקציה האופיינית של קבוצת המצבים המספקים את $plot:${f_1}$$ (נסמן קבוצה זו ב- $plot:${S_{{f_1}}}$$ ). נכתוב:

$plot:${f_1}\left( {\bar v} \right) = \left\{ {\begin{array}{*{20}{c}} 1 \hfill & {\bar v{\text{ is an encoding of state in }}{S_{{f_1}}}} \hfill \\ 0 \hfill & {{\text{else}}} \hfill \\ \end{array} } \right.$$

$plot:${f_2}\left( {\bar v} \right) = \left\{ {\begin{array}{*{20}{c}} 1 \hfill & {\bar v{\text{ is an encoding of state in }}{S_{{f_2}}}} \hfill \\ 0 \hfill & {{\text{else}}} \hfill \\ \end{array} } \right.$$

$plot:$f\left( {\bar v} \right) = \left\{ {\begin{array}{*{20}{c}} 1 \hfill & {\left\{ \begin{gathered} \bar v{\text{ is an encoding of state in }}{S_{{f_1}}} \hfill \\ and \hfill \\ \bar v{\text{ is an encoding of state in }}{S_{{f_2}}} \hfill \\ \end{gathered} \right.} \hfill \\ 0 \hfill & {{\text{else}}} \hfill \\ \end{array} } \right.$$

אם $plot:$f = \neg {f_1}$$ וגם נתון BDD $plot:${f_1}\left( {\bar v} \right)$$ עבור $plot:${f_1}$$ (שמייצג $plot:${S_{{f_1}}}$$ ), אזי נחזיר את ה-BDD המתקבלת מהפעלת פעולת $plot:$\neg $$ על $plot:${f_1}\left( {\bar v} \right)$$ .

$plot:$f = EX{f_1}$$ וגם נתון BDD $plot:${f_1}\left( {\bar v} \right)$$ עבור $plot:${f_1}$$ (שמייצג $plot:${S_{{f_1}}}$$ ).

ה-BDD של הנוסחה הבאה מייצג את קבוצת המצבים שמספקים את $plot:$EX{f_1}$$ :

$plot:$f\left( {\bar v} \right) = \exists \bar v'\left[ {{f_1}\left( {\bar v'} \right) \wedge R\left( {\bar v,\bar v'} \right)} \right]$$

קבוצה זו היא קבוצת כל המצבים שיש להם בן שמספק את $plot:${f_1}$$ .

הגדרנו כאן אופרטור BDD חדש (pre-image): $plot:$EX{f_1}\left( {\bar v} \right)$$ . האופרטור יוגדר כך: $plot:$EX{f_1}\left( {\bar v} \right) = \exists \bar v'\left[ {{f_1}\left( {\bar v'} \right) \wedge R\left( {\bar v,\bar v'} \right)} \right]$$ . מביא את כל האבות של מצבים המקיימים $plot:${f_1}$$ .

ניתן להגדיר אופרטורים נוספים: $plot:$EG,EF{f_1}$$ וכן אופרטורים אחרים באותו הרעיון.

$plot:$f = EF{f_1}$$ . הטיפול במקרה זה יהיה באופן הבא: מתחילים מקבוצת המצבים שבמרחק 0 ממצבים שמספקים את $plot:${f_1}$$ . באופן איטרטיבי עולים כל פעם רמה למעלה, בתחילה אל מצבים במרחק 1 ממצבים המספקים את $plot:${f_1}$$ וכך הלאה, עד ליצירת כל קבוצת המצבים המבוקשת. בכל פעם נאסוף את כל האבות בהם אנו נתקלים בדרך.

אלגוריתם לחישוב קבוצת המצבים המספקים $plot:$f = EF{f_1}$$ :

$plot:$\begin{gathered} Q: = \emptyset \hfill \\ Q': = {f_1}\left( {\bar v} \right) \hfill \\ {\text{while }}Q \ne Q'{\text{ do}} \hfill \\ & Q: = Q' \hfill \\ & Q'\left( {\bar v} \right) = Q\left( {\bar v} \right) \vee EXQ\left( {\bar v} \right) \hfill \\ {\text{end while}} \hfill \\ f\left( {\bar v} \right) = Q\left( {\bar v} \right) \hfill \\ \end{gathered} $$

הערה חשובה: פעולת $plot:$ \vee $$ על BDD נותנת איחוד של קבוצות.

האלגוריתם מחשב את נקודת השבת הקטנה ביותר. plot:$x$ היא נקודת שבת של פונקציה plot:$f$ אם $plot:$f\left( x \right) = x$$ . במקרה שלנו אנחנו מתחילים מקבוצת ממצבים ומוסיפים מצבים עד שלא ניתן להוסיף יותר. מאפיין חשוב של נקודת השבת הקטנה ביותר: מתחילים מקבוצה ריקה ומוסיפים איברים עד אשר אי אפשר להוסיף יותר. כשאי אפשר להוסיף איברים הגענו לנקודת השבת.

$plot:$f = E\left( {{f_1}U{f_2}} \right)$$ .

אלגוריתם לחישוב קבוצת המצבים המספקים $plot:$f = E\left( {{f_1}U{f_2}} \right)$$ :

$plot:\[\begin{gathered} Q: = \emptyset \hfill \\ Q': = {f_2}\left( {\bar v} \right) \hfill \\ {\text{while }}Q \ne Q'{\text{ do}} \hfill \\ & Q: = Q' \hfill \\ & Q'\left( {\bar v} \right) = Q\left( {\bar v} \right) \vee \left( {EXQ\left( {\bar v} \right) \wedge {f_1}\left( {\bar v} \right)} \right) \hfill \\ {\text{end while}} \hfill \\ f\left( {\bar v} \right) = Q\left( {\bar v} \right) \hfill \\ \end{gathered} \]$

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

נביט בשלב הבא:

$plot:\[Q'\left( {\bar v} \right) = Q\left( {\bar v} \right) \vee \left( {EXQ\left( {\bar v} \right) \wedge {f_1}\left( {\bar v} \right)} \right)\]$

$plot:\[Q\left( {\bar v} \right)\]$ זוהי קבוצת המצבים שחושבו עד כה. $plot:\[\left( {EXQ\left( {\bar v} \right) \wedge {f_1}\left( {\bar v} \right)} \right)\]$ זוהי קבוצת המצבים שיש להם בן בקבוצה $plot:\[Q\left( {\bar v} \right)\]$ והם עצמם מספקים את $plot:\[{f_1}\left( {\bar v} \right)\]$ .

טיפול ב- $plot:$EG{f_1}$$

נתחיל מקבוצת המצבים המספקים את $plot:${f_1}$$ (נתונים על ידי $plot:${f_1}\left( {\bar v} \right)$$ ). נזרוק צמתים שכל הבנים שלו מספקים את $plot:$\neg {f_1}$$ ואז בסריקה אחורנית נזרוק צמתים שזרקנו בן שלהם.

אלגוריתם:

$plot:\[\begin{gathered} Q: = S\left( {\bar v} \right) \hfill \\ Q': = {f_1}\left( {\bar v} \right) \hfill \\ {\text{while }}Q \ne Q'{\text{ do}} \hfill \\ & Q: = Q' \hfill \\ & Q' = EXQ \wedge Q \hfill \\ {\text{end while}} \hfill \\ f\left( {\bar v} \right) = Q\left( {\bar v} \right) \hfill \\ \end{gathered} \]$