PDF Archive

Easily share your PDF documents with your contacts, on the Web and Social Networks.

Share a file Manage my documents Convert Recover PDF Search Help Contact



l3 .pdf



Original filename: l3.pdf
Title: גרף תוכנית
Author: John Doil

This PDF 1.5 document has been generated by Microsoft® PowerPoint® 2010, and has been sent on pdf-archive.com on 07/11/2014 at 14:38, from IP address 79.176.x.x. The current document download page has been viewed 395 times.
File size: 1.2 MB (16 pages).
Privacy: public file




Download original PDF file









Document preview


‫גרף תוכנית (‪)Program Graph‬‬
‫גרא וייס‬
‫המחלקה למדעי המחשב‬
‫אוניברסיטת בן‪-‬גוריון‬

‫תזכורת‪ :‬בדיקות מודל (‪)Model Checking‬‬
‫מערכת‬

‫דרישות‬

‫מידול‬

‫פירמול‬

‫מודל של‬
‫המערכת‬

‫סימולציה‬

‫בדיקות מודל‬
‫(‪)Model Checking‬‬

‫דוגמה‬
‫נגדית‬

‫תכונות‬
‫פורמליות‬

‫התכונות‬
‫הוכחה‬

‫‪2‬‬

‫תזכורת‪ :‬מערכת מעברים –‪Transition System‬‬
‫מערכת מעברים נתונה על‪-‬ידי 〉𝐿 ‪ 〈𝑆, 𝐴𝑐𝑡, →, 𝐼, 𝐴𝑃,‬באשר‪:‬‬
‫𝑆 היא קבוצת המצבים‬
‫𝑆 ⊆ 𝐼 היא קבוצת המצבים ההתחלתיים‬
‫𝑡𝑐𝐴 היא קבוצת הפעולות‬

‫מצב א'‬
‫פעולה‬

‫𝑆 × 𝑡𝑐𝐴 × 𝑆 ⊆ ‪ ‬הוא יחס המעברים‬
‫מצב ב'‬

‫𝑃𝐴 היא קבוצת הפסוקים האטומיים‬
‫𝑃𝐴‪ 𝐿: 𝑆 → 2‬היא פונקצית תיוג‬

‫‪3‬‬

‫מערכות מעברים ‪ ‬אוטומטים סופיים‬
‫בניגוד לאוטומטים סופיים במערכות מעברים‪:‬‬
‫‪ ‬אין מצבים מקבלים‬
‫‪ ‬מספר המצבים והפעולות יכול להיות בן‪-‬מנייה‬
‫‪ ‬יכולים להיות אינסוף עוקבים‬
‫‪ ‬תפקיד שונה לאי‪-‬דטרמיניזם‬

‫מערכות מצבים מתאימות למידול התנהגות מערכות תגובתיות‬

‫‪4‬‬

‫‪5‬‬

‫מידול מעגלים לוגיים באמצעות מערכת מעברים‬
‫‪𝑥 = 1, 𝑟 = 0‬‬
‫}𝑥{‬

‫‪𝑥 = 0, 𝑟 = 0‬‬

‫𝑦‬

‫‪NOT‬‬

‫‪XOR‬‬

‫}𝑦{‬
‫‪OR‬‬

‫‪𝑥 = 1, 𝑟 = 1‬‬
‫}𝑦 ‪{𝑥, 𝑟,‬‬

‫‪𝑥 = 0, 𝑟 = 1‬‬
‫𝑟‬

‫}𝑟{‬

‫• תרגום מסכימת מעגל לוגי למערכת מעברים‬
‫• משתנה קלט 𝑥‪ ,‬משתנה פלט 𝑦 ואוגר (‪𝑟 )register‬‬
‫• פונקצית הפלט )𝑟‬

‫𝑥(¬ והקלט לאוגר 𝑟 ∨ 𝑥‬

‫𝑥‬

‫מידול מעברים מֻ ְתנִים באמצעות מערכת מעברים‬

‫‪6‬‬

‫‪ ‬תוכניות תלויות‪-‬נתונים בנויות מפקודות מהצורה‪:‬‬
‫‪if 𝑥%2 = 1 then 𝑥 ∶= 𝑥 + 1 else 𝑥 ∶= 2𝑥 fi‬‬
‫‪ ‬מידול כמערכת מעברים‪:‬‬
‫‪ ‬אפשר להשמיט את התנאים ולתרגם למעבר לא דטרמיניסטי‬
‫‪ ‬אפשר גם לכתוב את התנאים והפעולות על החצים‪:‬‬
‫‪𝑥%2 = 1 ∶ 𝑥 ∶= 𝑥 + 1‬‬

‫𝑥‪𝑥%2 = 0 ∶ 𝑥 ≔ 2‬‬

‫‪ ‬נקרא לזה גרף תוכנית‬
‫‪ ‬אח"כ נפרוש (‪ )unfold‬למערכת מצבים רגילה (באופן אוטומטי)‬

‫זאת לא‬
‫מערכת מעברים!‬

‫דוגמה‪ :‬שכלול מודל מכונת השתייה‬

‫‪7‬‬

‫(אנחנו בונים כאן גרף תוכנית‪ ,‬לא מערכת מעברים)‬
‫סופרים כמות בקבוקי הספרייט והבירה ומחזירים מטבע אם המכונה ריקה‪:‬‬
‫𝑡𝑟𝑎𝑡𝑠‬
‫𝑡𝑟𝑎𝑡𝑠‬

‫𝑙𝑙𝑖𝑓𝑒𝑟 ∶ ‪true‬‬

‫𝑡𝑟𝑎𝑡𝑠‬

‫𝑟𝑒𝑒𝑏_𝑡𝑒𝑔 ∶ ‪𝑛𝑏𝑒𝑒𝑟>0‬‬

‫𝑡𝑟𝑎𝑡𝑠‬

‫𝑡𝑐𝑒𝑙𝑒𝑠‬

‫𝑡𝑐𝑒𝑙𝑒𝑠‬

‫𝑡𝑟𝑎𝑡𝑠‬

‫𝑛𝑖𝑜𝑐_𝑡𝑒𝑟 ∶ ‪𝑛𝑏𝑒𝑒𝑟=0 ∧ 𝑛𝑠𝑝𝑟𝑖𝑡𝑒=0‬‬

‫פעולה‬

‫𝑛𝑖𝑜𝑐 ∶ ‪true‬‬

‫𝑒𝑡𝑖𝑟𝑝𝑠_𝑡𝑒𝑔 ∶ ‪𝑛𝑠𝑝𝑟𝑖𝑡𝑒>0‬‬

‫𝑡𝑐𝑒𝑙𝑒𝑠‬

‫השפעה על משתנים‬

‫‪coin‬‬
‫‪ret_coin‬‬
‫‪get_sprite‬‬

‫‪𝑛𝑠𝑝𝑟𝑖𝑡𝑒 ∶= 𝑛𝑠𝑝𝑟𝑖𝑡𝑒 − 1‬‬

‫‪get_beer‬‬

‫‪𝑛𝑏𝑒𝑒𝑟 ∶= 𝑛𝑏𝑒𝑒𝑟 − 1‬‬

‫‪refill‬‬

‫‪𝑛𝑠𝑝𝑟𝑖𝑡𝑒 ∶= max; 𝑛𝑏𝑒𝑒𝑟 ∶= max‬‬

‫𝑡𝑟𝑎𝑡𝑠‬

‫𝑡𝑐𝑒𝑙𝑒𝑠‬

‫‪8‬‬

‫גרף תוכנית‬
‫‪𝑥%2 = 1 ∶ 𝑥 ∶= 𝑥 + 1‬‬

‫‪ ‬כלי למידול תוכניות עם משתנים ותנאים‬
‫𝑥‪𝑥%2 = 0 ∶ 𝑥 ∶= 2‬‬

‫‪ ‬גרף מכוון עם סימונים על הקשתות‪:‬‬
‫‪ ‬הצמתים הם המקומות בתוכנית = ערך של ה‪program counter-‬‬
‫‪ ‬הקשתות מסומנות בביטויים מהצורה פעולה ‪ :‬תנאי‬
‫‪ ‬התנאים קובעים איזה קשתות "מאופשרות"‬
‫‪ ‬הפעולות מעדכנות את ערכי המשתנים‬
‫אנחנו נתרגם גרפי תוכנית למערכות מעברים שיינתנו כקלט ל‪Model Checker-‬‬

‫הגדרות פורמליות‪ :‬הצבות‪ ,‬תנאים והשפעה‬
‫‪ ‬קבוצת ההשמות (‪𝐸𝑣𝑎𝑙(𝑉𝑎𝑟) :)evaluations‬‬
‫‪ ‬השמה היא פונקציה המתאימה לכל משתנה ערך‬
‫‪ ‬למשל‪ 𝜂(𝑥) = 11 :‬ו‪𝜂(𝑦) = −8 -‬‬

‫‪ ‬קבוצת התנאים (‪𝐶𝑜𝑛𝑑(𝑉𝑎𝑟) :)conditions‬‬
‫‪ ‬נוסחאות בתחשיב פסוקים‪ .‬הפסוקים האטומיים מהצורה 𝐷 ∈ 𝑥‬
‫‪ ‬למשל‪7 < 𝑥 ≤ 19 ∧ 𝑦 = “up” ∧ (𝑥 < 2𝑧) :‬‬

‫‪ ‬השפעת (‪ )effect‬הפעולה מתוארת ע"י מיפוי‪:‬‬
‫‪‬‬
‫‪‬‬
‫‪‬‬
‫‪‬‬

‫)𝑟𝑎𝑉(𝑙𝑎𝑣𝐸 → 𝑟𝑎𝑉 𝑙𝑎𝑣𝐸 × 𝑡𝑐𝐴 ‪𝐸𝑓𝑓𝑒𝑐𝑡:‬‬
‫דוגמה‪ :‬עבור ‪ 𝛼 ≡ 𝑥 ≔ 𝑦 + 5‬ו‪ ´ -‬המוגדרת למעלה‬
‫‪𝐸𝑓𝑓𝑒𝑐𝑡(𝛼, 𝜂)(𝑥) = 𝜂(𝑦) + 5 = −3‬‬
‫‪𝐸𝑓𝑓𝑒𝑐𝑡 𝛼, 𝜂 𝑦 = 𝜂(𝑦) = −8‬‬

‫‪9‬‬


Related documents


alexa ranking checking tool whois checker tool
l3
04291042
phd dissertation proposal sample
osaki os 7075r deluxe massage chair
molecular sieve dehydration optimization


Related keywords