1. Czy podanie \texttt{number} z zakresu [0;2] spowoduje wydrukowanie napisu \texttt{wrong number}?  TAK\\



     \begin{lstlisting}
CTLSPEC AG((number = 0 | number = 1 | number = 2) -> AX(status = wrong_number))

\end{lstlisting}
\begin{figure} [!htb]
\centering
\includegraphics[width=1\textwidth]{wr.png}
\end{figure}

\vspace{1cm}

2. Jaka może być najmniejsza i największa liczba liczb pierwszych dla \texttt{number} z zakresu [3;8]?\\
Najmniejsza: 2\\
Największa: 4 \\


\begin{itemize}
    \item dla number = 3
    \begin{lstlisting}
DEFINE number :=  3;
...
COMPUTE MAX[deadlock=1, deadlock=2]  --sciezka maksymalnej dlugosci
CTLSPEC !EBF 13..13 (deadlock=2) --sprawdzanie koncowej wartosci primes na tej sciezce


\end{lstlisting}
\newpage
\begin{figure} [!htb]
\centering
\includegraphics[width=0.8\textwidth]{primes3.png}
\end{figure}

Liczba liczb pierwszych dla number = 3 to 2 (końcowa wartość primes na tej ścieżce wynosi 2 (stan 1.1)).

\newpage
    \item dla number = 8
    \begin{lstlisting}
DEFINE number :=  8;
...
COMPUTE MAX[deadlock=1, deadlock=2]  --sciezka maksymalnej dlugosci
CTLSPEC !EBF 98..98 (deadlock=2) --sprawdzanie koncowej wartosci primes na tej sciezce

\end{lstlisting}

\begin{figure} [!htb]
\centering
\includegraphics[width=0.7\textwidth]{primes8.png}
\end{figure}

Liczba liczb pierwszych dla number = 8 to 4 (końcowa wartość primes na tej ścieżce wynosi 4 (stan 1.96)).

\end{itemize}

\vspace{0.5cm}
3. Ile razy wykona się zewnętrzna pętla \texttt{for} dla \texttt{number = 5}?

   \begin{lstlisting}
DEFINE number :=  5;
...
COMPUTE MAX[deadlock=1, deadlock=2]  --sciezka maksymalnej dlugosci
CTLSPEC !EBF 38..38 (deadlock=2) --sprawdzanie koncowej wartosci licznika wykonan petli na tej sciezce

\end{lstlisting}
\begin{figure} [!htb]
\centering
\includegraphics[width=0.7\textwidth]{petla.png}
\end{figure}

Licznik = 3 (stan 1.35). Zewnętrzna pętla \texttt{for} dla \texttt{number = 5} wykona się 3 razy.