\begin{ctadsol}
%
\nombrectad{Parking}
%
\operaciones
\operacion{Enter}{Void}
\operacion{Leave}{Void}
%
\semdom
\estado{ Parking =  \nat}
\invariante{self \geq 0 \land self \leq MAX}
\inicial{self}{self = 0}

\pre{\true}
\cpre{ self < MAX}
\nomop{Enter}
\post{self\sal = self\ent + 1}
\vspace{-2ex}\\

\pre{\true}
\cpre{ self > 0 }
\nomop{Leave}
\post{self\sal = self\ent - 1 }
\vspace{-2ex}
%
\end{ctadsol}
