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

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

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

6.4.4.1. הגדרות ודוגמאות ראשונות

נגדיר מבנה קריפקה עם הוגנות: plot:$M = \left( {S,R,L,H} \right)$

כאשר plot:$S,R,L$ כמו קודם ו-plot:${S_0}$ אופציונאלי, כמו קודם.

plot:$H = \left\{ {{h_1},{h_2},...,{h_k}} \right\} \subseteq {2^S}$

  • plot:$H$ הינה קבוצה של קבוצות מצבים המגדירה תנאי הוגנות.
  • plot:${h_i}$ - יכול להיות גם נוסחת CTL שמייצגת את קבוצת כל המצבים שמספקים אותה

מסלול plot:$\pi $ הוא הוגן אם הוא מבקר בכל plot:${h_i}$ אינסוף פעמים.

ניסוח שונה:

plot:$\inf \left( \pi  \right) = \left\{ {S|S = {S_i}{\text{ for infinite }}i} \right\}$, plot:$\pi  = {S_0},{S_1},{S_2}...$

plot:$\pi $ הוא הוגן אם לכל plot:$1 \leqslant i \leqslant k$                      plot:$\inf \left( \pi  \right) \cap {h_i} \ne \emptyset $

דוגמא:

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

מסלול הוגן יבקר ב-plot:$1,3$ אינסוף פעמים או שיבקר ב-plot:$4,6,3$ אינסוף פעמים

דוגמא: מעגל חשמלי עם קלט input. נרצה לציין שהקלט יהיה 1 אינסוף פעמים.

plot:\[H = \left\{ {input = 1,...} \right\}\]

דוגמא: 3 קלטים plot:$i{n_1},i{n_2},i{n_3}$ בכל אחד מהם 1 אינסוף פעמים (לאו דווקא באותו זמן).

plot:$H = \left\{ {i{n_1},i{n_2},i{n_3}} \right\}$



דוגמא: בכולם אינסוף פעמים 1 (באותו זמן) plot:$H = \left\{ {i{n_1} \wedge i{n_2} \wedge i{n_3}} \right\}$

נקודות:

  • כאשרplot:$H = \left\{ {} \right\}$ כל המסלולים הוגנים.
  • אם plot:$H = \left\{ {\left\{ {} \right\}} \right\}$ אז אין מסלול הוגן.

תגיות המסמך:

לפרק הקודם6.4.4. הוספת הוגנות ל-CTL
לפרק הבא6.4.4.2. סמנטיקה
אין תגובות!
שיתוף:
| עוד