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

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

6.4.4.3. אלגוריתם לחישוב קבוצת המצבים המספקים $plot:${E_F}G{\varphi _1}$$

רכיב קשיר היטב הוגן – רכיב קשיר היטב plot:$C$ הינו הוגן אם לכל $plot:${h_i} \in H$$ $plot:$C \cap {h_i} \ne \emptyset $$

נבנה $plot:$M' = \left( {S',R',L',H'} \right)$$ באופן הבא (נשים לב כי plot:$S',R',L'$ מוגדרים כמו קודם):

$plot:\[\begin{gathered} M' = \left( {S',R',L',H'} \right) \hfill \\ S' = \left\{ {\left. S \right|M,S{ \vDash _F}{\varphi _1}} \right\} \hfill \\ R' = \left( {S' \times S'} \right) \cap R \hfill \\ L'\left( s \right) = L\left( s \right),s \in S' \hfill \\ H' = \left\{ {\underbrace {{h_i} \cap S'}_{{{h'}_i}}\left| {{h_i} \in H} \right.} \right\} \hfill \\ \end{gathered} \]$

הערה: אם $plot:${h'_i} = \emptyset $$ נסיק כי M מסלול הוגן המספק את $plot:$G\varphi $$ (אין מסלולים הוגנים).

למה: $plot:$M,s{ \vDash _F}EG{\varphi _1}$$ אמ"ם מתקיימים 2 התנאים:

$plot:$s \in S'$$
יש מסלול ב- מ- למצב ברכיב קשיר היטב מקסימאלי, לא טריוויאלי והוגן.

טיפול ב- $plot:${E_F}G{\varphi _1}$$

האלגוריתם:

בנו $plot:$\left| H \right| + \left| R \right| + \left| S \right|$$
מצאו את הרכיבים הקשירים היטב המקסימאליים, כולל הטריוויאלים $plot:$\left| S \right| + \left| R \right|$$
מצאו את הרכיבים הקשירים היטב המקסימאליים, הלא טריוויאליים וההוגנים. $plot:$\left| S \right| \cdot \left| H \right|$$
סמנו את כל המצבים מ-3 ב- $plot:${\varphi _1}$$ וכן בסריקה אחורנית סמנו את כל המצבים שמהם ישיגים מצבים שמסומנים ב- $plot:${\varphi _1}$$ . $plot:$\left| S \right| + \left| R \right|$$