6.6.1. מבוא והגדרותבדיקת מודל סימבולית עוסקת באלגוריתמים המשתמשים ביצוג של מכונת קריפקה כ-BDD על מנת לבצע בדיקות מודל. אלגוריתם בדיקת המודל נקרא סימבולי מכיוון שהוא מבוסס על מניפולציות מתמטיות על הנוסחאות הבוליאניות המייצגות את המכונה. BDD מייצג תמיד קבוצות של מצבים ומעברים, ולכן הפעולות שנציג יפעלו על קבוצות שלמות ולא על מצבים בודדים. אנחנו עובדים על מבנה קריפקה את
כמו כן, לפעמים נתונים גם:
באלגוריתם הלא סימבולי
"טיפלנו" בכל פעם בתת נוסחה של
בהמשך נציג אלגוריתמים לבדיקת מודל מבוססת BDD. כאשר נכתוב אלגוריתמים נוספים משלנו חשוב לא לבנות אלגוריתם המבוסס BFS או DFS. אלגוריתמים אלה עוברים בכל פעם על מצב בודד, ואלו פעולות מאוד לא יעילות כשאנו מתעסקים עם BDD. האלגוריתמים בהם נשתמש צריכים להיות מבוססים על פעולות על קבוצות כדי לנצל את מבנה הנתונים בצורה הטובה ביותר.
אין תגובות!
|
תוכן העניינים:
קישורים רלוונטיים:שיתוף: |