\begin{ctadsol}

\label{especificacion-inicial}
\nombrectad{Event Manager}

\operaciones
\operacion{FireEvent}{Event\_Type[i]}
\operacion{Subscribe}{Process\_Type[i] \por Event\_Type[i]}
\operacion{Unsubscribe}{Process\_Type[i] \por Event\_Type[i]}
\operacion{Listen}{Process\_Type[i] \por Event\_Type[i]}

\semdom
\estado{Event Manager =  \\
    \hspace*{5.5em} (subscribed : Event\_Type \rightarrow \textrm{Set of} Process\_Type \por\\
    \hspace*{5.6em} unlistenedEvents : Event\_Type \rightarrow \textrm{Set of} Process\_Type)}
\tipo{
    Process\_Type = 0..N\_PROCESSES-1\\
    Event\_Type = 0..N\_EVENTS-1}

% \invariante{\forall ue \in dom(unlistenedEvents) \st\ \\
            % \hspace*{8.5em} unlistenedEvents(ue) \subseteq subscribed(ue)}
\invariante{ unlistenedEvents \subseteq subscribed}

\inicial{ self}{unlistenedEvents = \emptyset \land subscribed = \emptyset}

\pre{\true}
\cpre{\true}
\nomop{FireEvent(eid)}
\post{subscribed\ent(eid) != \emptyset \implies \exists pid \in Process\_Type \st pid \in unlistenedEvents\ent(eid) \land unlistenedEvents = unlistenedEvent - \{(eid, pid)\}}
% \post{unlistenedEvents\sal(eid) = subscribed\ent(eid) \land\\
%   \hspace*{5em}\forall e \in EID\st\ (subscribed\sal(e) = subscribed\ent(e) \land\\
%   \hspace*{10.7em}(e \neq eid \Rightarrow 
%                                   unlistenedEvents\sal(e) = unlistenedEvents\ent(e)))
% }

\pre{ \true }
\nomop{Subscribe(pid,eid)}
\post{subscribed\sal = subscribed\ent \oplus \{(eid,pid)\}}
% \post{ subscribed\sal(eid) = subscribed\ent(eid) \cup \{pid\} \land \\
%   \hspace*{5em}\forall e \in EID\st\ (unlistenedEvents(e) = 
%                                         unlistenedEvents\ent(e) \land \\
%   \hspace*{10.7em}(e \neq eid \Rightarrow subscribed\sal(e) = subscribed\ent(e)))
% }

\pre{ pid \in  subscribed(eid)}
\cpre{ \true}
\nomop{Unsubscribe(pid,eid)}
\post{ subscribed\sal = subscribed\ent - \{(eid,pid)\} \land \\
  \hspace*{5em}unlistenedEvents\sal = unlistenedEvents\ent - \{(eid,pid)\} }

\pre{\true}
\cpre{\exists e \in  EID\st\ pid \in  unlistenedEvents(e)}
\nomop{Listen(pid,eid)}
\post{ subscribed\sal = subscribed\ent \land \\
  \hspace*{5em}unlistenedEvents\sal = unlistenedEvents\ent - \{(eid,pid)\} 
}
  
\end{ctadsol}