pl/frap
1
0
Fork 0
mirror of https://github.com/achlipala/frap.git synced 2024-09-20 04:07:13 +00:00
Code Issues Projects Releases Packages Wiki Activity Actions

Correct definition of reachability

Browse source
This commit is contained in:
Adam Chlipala 2016-10-11 14:36:26 -04:00
parent e3128435f8
commit ee4aec520b
1 changed files with 1 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
frap_book.tex
View file

@ -1085,7 +1085,7 @@ There we have $\to^2\ns(S_0)$, $\to^3\ns(S_0)$, and $\to^4\ns(S_0$).
It follows that the set of states reachable after $n$ steps is: It follows that the set of states reachable after $n$ steps is:
\begin{eqnarray*} \begin{eqnarray*}
\mathsf{reach}(n) &=& \bigcup_{i < n} \to^i\ns(S_0) \mathsf{reach}(n) &=& \bigcup_{i \leq n} \to^i\ns(S_0)
\end{eqnarray*} \end{eqnarray*}
This iteration process is not obviously executable yet, because, a priori, we seem to need to consider all possible $n$ values, to characterize the state space fully. This iteration process is not obviously executable yet, because, a priori, we seem to need to consider all possible $n$ values, to characterize the state space fully.