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

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

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

6.3.2. אופרטורים טמפורליים

  1. Globally (מסומן ב-G) - תכונה שמתקיימת לכל אורך התוכנית.

    לדוגמה: plot:$G\left( {\neg at\_critica{l_1} \vee \neg at\_critica{l_2}} \right)$.

    (לא יתכן ששני חוטים יהיו בקטע הקריטי בו זמנית).
  2. Future (Eventually) - תכונה שתתקיים מתישהו בעתיד.

    לדוגמה: plot:$request \to F\left( {granted} \right)$

    (אם תהליך ביקש משאב כלשהו, בסופו של דבר הוא יקבל אותו מתישהו).

דוגמאות:

  • מתקיים: plot:$G\left( p \right) = \neg F\left( {\neg p} \right)$  כלומר ש P מתקיים תמיד זה כמו לומר שלא יקרה בעתיד שיתקיים "לא P".
  • plot:$GFp$ - בכל רגע בתוכנית מתקיים שמתישהו בעתיד יתקיים P.
  • plot:$FGp$ - החל מרגע מסוים בעתיד, P יתקיים לנצח.
  1. neXt(p) - plot:$p$ יתקיים בצעד הבא. יסומן ב-plot:$X$.

דוגמאות:

  • plot:$XGp$ - החל מהצעד הבא, p יתקיים תמיד.
  • plot:$GXp$ - בכל מצב יתקיים שבמצב הבא לאחריו p יתקיים.
  • קיבלנו: plot:$XGp = GXp$\$

  1. (p) Until (q) - יסומן ב-U.

    plot:$pUq$ - מתישהו בעתיד plot:$q$ מתקיים, ועד אז בהכרח plot:$p$ מתקיים.

דוגמא:

"אם הודעה 1 נשלחה לפני הודעה 2 אזי הודעה 1 תגיע לפני הודעה 2".

    • האטומים הם plot:$sen{t_1},sen{t_2},receive{d_1},receive{d_2}$.
    • הביטוי המתאים: plot:$\neg sen{t_2}Usen{t_1} \to \neg receive{d_2}Ureceive{d_1}$

  1. (p) Release (q) – יסומן ב-R.

    plot:$pRq$ - plot:$q$ מתקיים עד שיתקיים plot:$p$, כולל המצב הראשון שבו יתקיים plot:$p$. לא בהכרח יתקיים בעתידplot:$p$.


טענה: האופרטורים plot:$U,X$ מספיקים כדי להגדיר את plot:$R,F,G$.

  • plot:$F\left( p \right) = \left( {True} \right)U\left( p \right)$
  • plot:$G\left( p \right) = \neg F\left( {\neg p} \right) = \neg \left( {\left( {True} \right)U\left( {\neg p} \right)} \right)$

כמתי מסלול:  plot:\[E - exist, &  & A - for\,\,all\]

דוגמא:

מתקיים: plot:$EXp$ אבל לא מתקיים plot:$AXp$. כלומר: קיים מסלול בו מתקיים plot:$Xp$ אבל לא בכל מסלול מתקיים plot:$Xp$.



תגיות המסמך:

לפרק הקודם6.3.1. מרכיבי הלוגיקות הטמפורליות
לפרק הבא6.3.3. CTL*
אין תגובות!
שיתוף:
| עוד