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

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

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

6.6.4.2. תיאור אלמנטים בגרף באמצעות BDD

נתון BDDplot:$R\left( {\bar v,\bar v'} \right)$ המתאר קשתות בגרף כלשהו.

  • רשמו נוסחה עבור קבוצת הקשתות הדו כיווניות בגרף.

    פתרון:plot:$H\left( {\bar v,\bar v'} \right) = R\left( {\bar v,\bar v'} \right) \wedge R\left( {\bar v',\bar v} \right)$

  • רשמו נוסחה עבור אוסף זוגות הצמתים plot:$\left( {\bar v,\bar v'} \right)$ שיש ביניהם מסלול באורך 2:

    פתרון: plot:$H\left( {\bar v,\bar v'} \right) = \exists \bar v''\left[ {R\left( {\bar v,\bar v''} \right) \wedge R\left( {\bar v'',\bar v'} \right)} \right]$
  • רשמו נוסחה שתקבל ערך TRUE אם ורק אם הגרף מלא (בין כל שני צמתים יש קשת).

    פתרון: plot:$H = \forall \bar v\forall \bar v'\left[ {\left( {S\left( {\bar v} \right) \wedge S\left( {\bar v'} \right)} \right) \to R\left( {\bar v,\bar v'} \right)} \right]$

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



תגיות המסמך:

לפרק הקודם6.6.4.1. Reachable
לפרק הבא6.7. בדיקת מודל סימבולית מבוססת SAT
אין תגובות!
שיתוף:
| עוד