\begin{ctadsol}
%
\nombrectad{BoundedSemaphore}
%  
\operaciones
  \operacion{Init}{\nat[i]\por \nat[i]}
  \operacion{V}{\void}
  \operacion{P}{\void}
%  
\semdom
  \estado{BoundedSemaphore = (value: \nat \por upperBound: \nat)}
  \invariante{value \geq 0 \land upperBound \geq value \land upperBound > 0}
  \inicial{\self}{\true}

  %\pre{\true}
  \cpre{v \geq 0 \land upperBound \geq v}
  \nomop{Init(v)}
  \post{value\sal= v}

  %\pre{\true}
  \cpre{upperBound \geq value }
  \nomop{V()}
  \post{value\sal = value\ent + 1}

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