\begin{ctadsol}
  \nombrectad{ReadersWriters}
%
  \operaciones
  \operacion{BeforeRead}{\void}
  \operacion{AfterRead}{\void}
  \operacion{BeforeWrite}{\void}
  \operacion{AfterWrite}{\void}

  \protoconc
  {
    Read: BeforeRead; AfterRead \\
    Write: BeforeWrite; AfterWrite
    }
  {(Read+|Write)*}
%
  \semdom
  \estado{(readers : \nat \por writers : \nat)}
  \invariante{(readers > 0 \rightarrow writers = 0) \land \\
              (writers = 1 \rightarrow readers = 0) \land \\
              (writers = 0 \lor writers = 1)}
  \inicial{\self}{writers = 0 \land readers = 0}

  \pre{\true}
  \cpre{\self.writers = 0}
  \nomop{BeforeRead}
  \post{\self = ( 1 + \self.readers\ent, \self.writers\ent)}

  % \pre{reader > 0}
  \pre{\true}
  \cpre{\true}
  \nomop{AfterRead}
  \post{\self = ( -1 + \self.readers\ent, \self.writers\ent)}

  \pre{\true}
  \cpre{\self = (0,0)}
  \nomop{BeforeWrite}
  \post{\self = (0, 1)}

  \pre{\true}
  \cpre{\true}
  \nomop{AfterWrite}
  \post{\self = (0, 0)}
\end{ctadsol}
