\begin{ctadsol}
  \nombrectad{Recycling\_Plant}
  \operaciones
    \operacion{Notify\_weight}{\nat [i]}
    \operacion{Increment\_weight}{\nat [i]}
    \operacion{Notify\_Drop}{\void}
    \operacion{Prepare\_Replacement}{}
    \operacion{Notify\_Replacement}{\nat [i]}
%
  \protoconc
  {
    Crane: Notify\_Weight; Increment\_Weight; Notify\_Drop \\
    Container: Prepare\_Replacement; Notify\_Replacement
    }
  {Crane | Container}
%
  \semdom
    \tipo{%
    Recycling\_Plant = $(weight: \nat \por state: State \por accessing: \nat)\\
    State = READY \alter TO\_REPLACE \alter REPLACING$
    %weight = MIN\_P\_GRUA .. MAX\_P\_GRUA
    }
%
    \inicial{self}{self.weight = 0 \land self.state = READY \land self.accessing = 0}
    \invariante{\forall r \in Recycling\_Plant \st\ r.weight \leq
                MAX\_W\_CONTAINER \land r.accessing \leq MAX\_CRANES \land 
                MAX\_W\_CONTAINER > 0 } 

  \cpre{self.state \neq REPLACING}
  \nomop{Notify\_weight(w)}
  \post{self\ent.weight + w > MAX\_W\_CONTAINER \rightarrow
           self\sal.state = TO\_REPLACE \land 
        self\ent.weight + w \leq MAX\_W\_CONTAINER \rightarrow
           self\sal.state = READY
        }

  \cpre{self.weight + w \leq MAX\_W\_CONTAINER \land self.state \neq REPLACING}
  \nomop{Increment\_Weight(w)}
  \post{self\sal.accessing = self\ent.accessing + 1 \land 
        self\sal.weight = self\ent.weight + w}

  \pre{accessing > 0}
  \cpre{\cierto}
  \nomop{Notify\_Drop}
  \post{self\sal.accessing = self.\ent.accessing- 1}

  \cpre{self.state = TO\_REPLACE \land self.accessing = 0} %% OJO!!
  \nomop{Prepare\_Replacement}
  \post{self\sal.state = REPLACING}

  \pre{self.state = REPLACING \land self.accesing = 0 \land m > 0}
  \cpre{\cierto}
  \nomop{Notify\_Replacement(m)}
  \post{self\sal.state = READY \land self\sal.weight = 0 \land MAX\_W\_CONTAINER = m }
%
\end{ctadsol}