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

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

6.5.2. יצוג מבנה קריפקה על ידי פונקציה בוליאנית - דוגמא

קידוד של מצבים

נשתמש במשתנים $plot:${v_1},{v_2}$$ כדי לייצג קידוד של מצבים. לדוגמא:

$plot:${f_{\left\{ {{S_1}} \right\}}}\left( {{v_1},{v_2}} \right) = \neg {v_1} \wedge \neg {v_2}$$

נוסחה $plot:${f_A}$$ מייצגת קבוצה A אמ"מ ההשמות המספקות ל- $plot:${f_A}$$ מתאימות בדיוק לקידוד של איברי A.

$plot:\[{f_{\left\{ {{S_3}} \right\}}}\left( {{v_1},{v_2}} \right) = \neg {v_1} \wedge {v_2}\]$

$plot:\[{f_{\left\{ {{S_1},{S_3}} \right\}}}\left( {{v_1},{v_2}} \right) = \left( {\neg {v_1} \wedge {v_2}} \right) \vee \left( {\neg {v_1} \wedge \neg {v_2}} \right) = \neg {v_1}\]$

$plot:${f_{\left\{ {{S_2}} \right\}}}\left( {{v_1},{v_2}} \right) = {v_1} \wedge {v_2}$$

ייצוג רלציית המעברים

אם נתונים המשתנים $plot:${v_1},...{v_n}$$ לתיאור מצב אזי נוסיף משתנים $plot:${v_1}^\prime ,...{v_n}^\prime $$ לתיאור "המצב הבא" (המצב הסופי ברשת). בדוגמא:

$plot:${f_{\left\{ {{S_1} \to {S_2}} \right\}}}\left\{ {{v_1},{v_2},{v_1}^\prime ,{v_2}^\prime } \right\} = \underbrace {\neg {v_1} \wedge \neg {v_2}}_{{S_1}} \wedge \underbrace {{v_1}^\prime \wedge {v_2}^\prime }_{{S_2}}$$

ונוכל אף לייצג את כל הרלציה:

$plot:\[{f_R}\left( {{v_1},{v_2},{v_1}^\prime ,{v_2}^\prime } \right) = \left( {\neg {v_1} \wedge \neg {v_2} \wedge {v_1}^\prime \wedge {v_2}^\prime } \right) \vee \left( {\neg {v_1} \wedge \neg {v_2} \wedge \neg {v_1}^\prime \wedge {v_2}^\prime } \right) \vee \]$

$plot:$\left( {{v_1} \wedge {v_2} \wedge \neg {v_1}^\prime \wedge {v_2}^\prime } \right) \vee \left( {\neg {v_1} \wedge {v_2} \wedge \neg {v_1}^\prime \wedge \neg {v_2}^\prime } \right)$$