\begin{ctadsol}
%
\nombrectad{Semaphore}
%  
\operaciones
  \operacion{Init}{\nat[i]}
  \operacion{V}{\void}
  \operacion{P}{\void}
%  
\semdom
  \estado{Semaphore = \nat}
  \invariante{\self == 0 \lor \self == 1 }
  \inicial{\self}{0}

  \pre{v == 0 \lor v == 1}
  \cpre{\true}
  \nomop{Init(v)}
  \post{\self\sal = v}

  \pre{\true}
  \cpre{\self == 0}
  \nomop{V()}
  \post{\self\sal = \self\ent + 1}

  \pre{\true}
  \cpre{\self == 1}
  \nomop{P()}
  \post{\self\sal = \self\ent - 1}
%
\end{ctadsol}
