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

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

6.4.4.4. טיפול ב- $plot:${E_F}\left( {{\varphi _1}U{\varphi _2}} \right),\, & {E_F}X{\varphi _1}$$

נוסיף נוסחה אטומית חדשה plot:$fair$ , שנכונה במצב plot:$S$ אמ"ם מ- יוצא מסלול הוגן.

$plot:$S{ \vDash _F}EG\,\,true$$ (נוסחה שקולה $plot:$S \vDash {E_F}G\,true$$ ) אמ"מ קיים מסלול הוגן $plot:$\pi $$ מ- plot:$S$ המספק $plot:$G\,\,true$$

דרך נוספת להגדיר את plot:$fair$ :

$plot:$fair \triangleq {E_F}G\,\,true$$

אבחנות:

אם $plot:$\pi $$ מסלול הוגן אז כל סיפא של $plot:$\pi $$ היא מסלול הוגן.
אם $plot:$\pi $$ הוגן אז הוספת רישא סופית להתחלת $plot:$\pi $$ $plot:$\pi ' = {\pi _1} \cdot \pi $$ גם כן חישוב הוגן.

בעזרת plot:$fair$ אנו מבצעים באלגוריתמים הבאים רדוקציה מ-CTLF ל-CTL ופותרים את הבעיה בכלים שאנו מכירים:

אלגורתים לטיפול ב- $plot:${E_F}X{\varphi _1}$$

כדי לסמן את המצבים שמספקים $plot:${E_F}X{\varphi _1}$$ נבדוק (ללא הוגנות) $plot:$EX\left( {{\varphi _1} \wedge fair} \right)$$

אלגוריתם לטיפול ב- $plot:${E_F}\left( {\varphi {{\kern 1pt} _1}U{\varphi _2}} \right)$$

כדי לסמן את המצבים שמספקים $plot:${E_F}\left( {\varphi {{\kern 1pt} _1}U{\varphi _2}} \right)$$ נסמן (ללא הוגנות) $plot:$E\left( {{\varphi _1}U\left( {{\varphi _2} \wedge fair} \right)} \right)$$