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

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

6.6.4.1. Reachable

אלגוריתם סימבולי למציאת כלל המצבים הישיגים מקבוצת מצבים $plot:$P\left( {\bar v} \right)$$ :

$plot:\[\begin{gathered} {\text{reachable}}\left( {P\left( {\bar v} \right)} \right) \hfill \\ \{ \hfill \\ & new \leftarrow P \hfill \\ & reach \leftarrow P \hfill \\ & {\text{while }}\left( {new \ne \emptyset } \right) \hfill \\ & \{ \hfill \\ & & reach \leftarrow reach \vee new \hfill \\ & & new\left( {\bar v'} \right) \leftarrow \exists \bar v\left[ {R\left( {\bar v,\bar v'} \right) \wedge new\left( {\bar v} \right)} \right] \hfill \\ & & new \leftarrow new \wedge \neg reach \hfill \\ & \} \hfill \\ \} \hfill \\ \end{gathered} \]$

הרעיון בגדול: plot:$new$ מכיל בכל פעם את הצמתים האחרונים שהוספנו, שמהם אנחנו רוצים לחפש קשתות חדשות. בכל פעם אנחנו מוסיפים את כל הצמתים שישיגים מ-, ומרחיבים את למעגל רחב יותר.

נקודות:

$plot:\[new \wedge \neg reach\]$ משמעותו שאנחנו לא לוקחים צמתים שאינם "מהמעגל האחרון" של הצמתים הנסרקים.
$plot:\[new\left( {\bar v'} \right)\]$ בא לציין כי המשתנים החדשים ב- הם מעל $plot:$\bar v'$$