6.6.3. בדיקת מודל סימבולית לפי מבנה הנוסחהאנחנו עובדים על מבנה קריפקה ונוסחה . האלגוריתם מטפל בתתי הנוסחאות של מהפשוטה למורכבת, וכשמטפלים בתת נוסחה מניחים שכל תתי הנוסחאות של כבר טופלו. נוסחה טופלה כאשר קיים BDD המייצג את קבוצת המצבים המספקים אותה. נחלק את בדיקת המודל למקרים שונים. המקרים נבדלים ביניהם על פי מבנה הנוסחה.
קבוצה זו היא קבוצת כל המצבים שיש להם בן שמספק את .
הערה חשובה: פעולת על BDD נותנת איחוד של קבוצות. האלגוריתם מחשב את נקודת השבת הקטנה ביותר. היא נקודת שבת של פונקציה אם . במקרה שלנו אנחנו מתחילים מקבוצת ממצבים ומוסיפים מצבים עד שלא ניתן להוסיף יותר. מאפיין חשוב של נקודת השבת הקטנה ביותר: מתחילים מקבוצה ריקה ומוסיפים איברים עד אשר אי אפשר להוסיף יותר. כשאי אפשר להוסיף איברים הגענו לנקודת השבת.
אלגוריתם זה הוא מטיפוס נקודת שבת קטנה ביותר (מתחילים מקבוצה שידוע שצריכה להיות בפתרון ומגדילים אותה עד לנקודת שבת). נביט בשלב הבא: זוהי קבוצת המצבים שחושבו עד כה. זוהי קבוצת המצבים שיש להם בן בקבוצה והם עצמם מספקים את .
טענה: כל מצב שנשאר בקבוצה בסוף התהליך מספק את . טענה: כל מצב שמספק את נשאר בקבוצה בסוף התהליך. מהטענות נובע כי אלגוריתם זה מספק לנו את נקודת השבת הגדולה ביותר.
אין תגובות!
|
תוכן העניינים:
קישורים רלוונטיים:שיתוף: |