הועלה לאתר:  
מספר עמודים: 120
הורדת המסמך בגרסה להדפסהלהורדת המסמך בשלמותו

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

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

6.4.4.5. דוגמא

נביט במבנה הבא ובתנאי ההוגנות הנתון:

plot:$H = \left\{ {\left\{ {1,2} \right\},\left\{ {1,5} \right\}} \right\}$

חישוב fair - plot:$fair = {E_F}G\,\,true$

  • בניית plot:$M'$: מתקיים כי plot:$M' = M$. נשתמש בהגדרה - קבוצת המצבים המספקים את plot:${\varphi _1} = true$ היא כל המצבים.
  • מציאת הרכיבים הקשירים היטב המקסימלים:

plot:\[MSCC = \left\{ {\left\{ {2,3,4,5} \right\},\left\{ 6 \right\},\left\{ 0 \right\},\left\{ 1 \right\}} \right\}\]

כאשר plot:\[\left\{ 0 \right\},\left\{ 1 \right\}\] הם רכיבים טריויאליים.

  • מציאת הרכיבים הקשירים היטב ההוגנים:

plot:\[FMSCC = \left\{ {\left\{ {2,3,4,5} \right\},\left\{ 1 \right\}} \right\}\]

  • מציאת fair:

plot:$fair = \left\{ {2,3,4,5,0,1} \right\} = S - \left\{ 6 \right\}$



חישוב plot:${E_f}\left( {aUb} \right)$

  • על מנת לבדוק את הנוסחה נבדוק plot:$E\left( {aU\left( {b \wedge fair} \right)} \right)$.
  • מתקיים plot:$b \wedge fair = \left\{ {0,3} \right\}$
  • הולכים אחורנית למצבים המסומנים ב-plot:$a$, ונקבל: plot:$E\left( {aU\left( {b \wedge fair} \right)} \right) = \left\{ {0,3,4} \right\}$

חישוב plot:${E_f}Ga$

  • נחשב את plot:$M'$ - קבוצת המצבים המספקים את plot:$a$ והקשתות ביניהם:

  • נמצא MSCC:

plot:$MSCC = \left\{ {\left\{ {3,4} \right\},\left\{ 6 \right\},\left\{ 1 \right\}} \right\}$

  • נמצא FMSCC:

plot:$FMSCC = \emptyset $



תגיות המסמך:

לפרק הקודם6.4.4.4. טיפול ב-plot:${E_F}\left( {{\varphi _1}U{\varphi _2}} \right),\, & {E_F}X{\varphi _1}$
לפרק הבא6.5. BDD - Binary Decision Diagram
אין תגובות!
שיתוף:
| עוד