

\begin{ctadsol}

  \nombrectad{WarehouseAccessControl}
  \operaciones
  \operacion{enterWarehouse}{\nat[i] \por \nat[i]}
  \operacion{exitWarehouse} {\nat[i] \por \nat[i]}
  
  \semdom
  \estado{
      (weight: Warehouse \tfun Weight \por \\
      occupied: Warehouse \tfun \bool)}

  \tipo{
    Warehouse = $0 \ldots \NW - 1$\\
    Weight = $0 \ldots \MWIW$}

  \inicial{self}{\forall n \in Warehouse \st weight(n) = 0 \land 
    \neg occupied(n)}
  \invariante{\forall n \in Warehouse \st weight(n) \leq \MWIW}
  
  \pre{n \in \{0 \ldots \NW - 1 \} \land \\\hspace*{.8cm}
       w \in \{ 0 \ldots \MWIW - 1 \}}
  \cpre{w + weight(n) \leq \MWIW}
  % \waiting{     
  %   \forall w \in 0..\MWIW \st\\
  %   \hspace*{2.5cm}\bigcup_{i=0}^{n}waiting(enterWarehouse(i,w) \cup\\
  %   \hspace*{2.7cm}\bigcup_{i=0}^{n}waiting(exitWarehouse(i,w) = \emptyset
  % }
  \nomop{enterWarehouse(n,w)}
  \post{weight\sal = weight\ent \oplus \{ n \mapsto weight\ent(n) + w \} \land
    \\\hspace*{.8cm}
    (n > 0 \implies occupied\sal = occupied\ent \oplus \{ n \mapsto \falso \}) 
    \land 
    \\\hspace*{.8cm}
    (n = 0 \implies occupied\sal = occupied\ent)}
  
  \pre{n \in \{ 0 \ldots \NW - 1 \} \land 
       \\\hspace*{.8cm} 
       w \in \{ 0 \ldots \MWIW - 1 \} }
  \cpre{n = \NW - 1 \lor \neg occupied(n)}
  % \waiting{     
  %   \forall w \in 0..\MWIW \st\\
  %   \hspace*{2.5cm}\bigcup_{i=0}^{n}waiting(enterWarehouse(i,w) \cup\\
  %   \hspace*{2.7cm}\bigcup_{i=0}^{n}waiting(exitWarehouse(i,w) = \emptyset
  % }
  \nomop{exitWarehouse(n,w)}
  \post{weight\sal = weight\ent \oplus \{ n \mapsto weight\ent(n) - w \}\land 
    \\\hspace*{.8cm}
    (n < \NW - 1 \implies 
    \\\hspace*{1.2cm} occupied\sal = occupied\ent \oplus \{ n \mapsto \cierto \}) 
    \land
    \\\hspace*{.8cm}
    (n = \NW - 1 \implies occupied\sal = occupied\ent)}
\end{ctadsol}
