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

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

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

6.3.3.3. דוגמאות לנוסחאות + משמעות אינטואיטיבית

בדוגמאות הבאות, plot:$p \in AP$.

דוגמא 1

הגרף מקיים plot:$EGp$ עבור המסלול השמאלי ביותר:

דוגמא 2

הגרף מקיים plot:$AGp$:

דוגמא 3

נסתכל על נוסחת המסלול הבאה:  plot:$\pi  \vDash GFp$.

משמעות הנוסחה: plot:$p$ מתקיים על plot:$\pi $ אינסוף פעמים. "קיימת סדרה אינסופית של plot:$p$ במסלול".



דוגמא 4

הנוסחה plot:$\pi  \vDash FGp$. קיים מצב על המסלול שממנו והלאה מסתפקplot:$p$.

דוגמא 5

הנוסחה plot:$\pi  \vDash AXp$:

דוגמא 6

הנוסחה plot:$\pi  \vDash EXp$:



דוגמאות נוספות (ללא שרטוט):

 

  1. plot:$S \vDash EGFp$

    קיים מסלול שעליו אינסוף פעמיםplot:$p$ נכון.
  2. plot:$S \vDash EGEFp$

    קיים מסלול מ-plot:$S$ שלכל מצב עליו קיים מסלול עליו מתקייםplot:$p$ (לא בהכרח המשך המסלול הראשון שיוצא מ-plot:$S$).

הגדרה:  נוסחת CTL* plot:$\varphi $ נקראת ספיקה אם קיים מבנה M כך ש-plot:$M \vDash \varphi $.

דוגמאות:

  1. האם הנוסחה plot:$\varphi  = E\left( {GEXp \wedge FX\neg p} \right)$ ספיקה?

הנוסחה ספיקה, נראה מבנה שמספק אותה:

המסלול המוכיח: plot:$\pi :{t_1} \to {t_1} \to {t_1} \to {t_1} \to ...$

2. plot:$\varphi  = EXp \wedge X\neg P$ אינה ספיקה.



תגיות המסמך:

לפרק הקודם6.3.3.2. הגדרה אינדוקטיבית שלplot:$ \vDash $
לפרק הבא6.3.4. CTL
אין תגובות!
שיתוף:
| עוד