\documentclass[12pt,spanish,a4]{article}
\usepackage{babel}
\usepackage{zed-csp}
\usepackage{enumerate}
\usepackage{fullpage}


\begin{document}

%
% EJERCICIO 1
%
\begin{syntax}
	[METHOD,ID,STATE] \\
\end{syntax}

\begin{axdef}
	CALL : \power METHOD \\
	RETURN : \power METHOD \\
	nullmethod : METHOD
\where
	nullmethod \in RETURN \\
	nullmethod \in CALL \\
	CALL \bigcup RETURN = METHOD \\
	CALL \bigcap RETURN = \{ nullmethod \} \\
	\#CALL = \# RETURN \\
\end{axdef}

\begin{syntax}
	PORT ::= send | receive | returned | return \\
	CONTROL ::= ready | receive\_callin | running\_callin | \\
				make\_callout | taked\_callout | receive\_return\_callout | \\
				taked\_return\_callout | send\_return\_callin 
\end{syntax}
 
\begin{schema}{Layer}
	id : ID \\
	export : CALL \\
	import : ID \cross CALL \\
	states : \power STATE \\
	start : STATE \\
	compute : STATE \rel ID \cross STATE \cross METHOD  \\
	runmethod : ID \cross STATE \cross CALL \rel STATE \\ 
	nextreturn : ID \cross STATE \cross RETURN \rel STATE \\
\where
	start \in states 
\also
	\forall m:CALL, \; i:ID \; s_1,s_2:STATE | (s_1, (i,s_2,m)) \in compute @ \\
	\t1 \{s_1, s_2\} \subset states \land \exists i:ID (i,m) \in import 
\also
	\forall i:ID, \; s_1,s_2:STATE, \; c:CALL | ((i,s_1,c),s_2) \in runmethod @ \\ 
	\t1 \{s_1, s_2\} \subset states \land \exists i:ID @ (i,c) \in import \\
\also 
	\forall i:ID, \; s_1,s_2:STATE, \; r:RETURN | ((i,s_1,r),s_2) \in nextreturn @ \\ 
	\t1 \{s_1, s_2\} \subset states \land \exists i:ID @ (c,returnby? \, r) \in import \\
\end{schema}	

\begin{schema}{Layer\_State}
	l : Layer \\
	current : STATE  \\
	in  : ID \\
	out : ID \\
	port : PORT \cross ID \pfun METHOD \\
	ctrl : CONTROL \\
\where
	current \in l.states 
\also
	out \in \{i:ID | \exists c:CALL @ (i,c) \in l.import \} \\
\also
	\forall p:PORT, i:ID | p \in \{send,receive\} \land (p,i) \in domain \, port @ \\
	\t1 port \, p \, i \; \in CALL \\
	\forall p:PORT, i:ID | p \in \{return,returned\} \land (p,i) \in domain \, port @ \\
	\t1 port \, p \, i \; \in RETURN \\
\also
	\{i:ID | (send,i) \in domain \, port\} = 
	\{i:ID | (returned,i) \in domain \, port\} \\
	\{i:ID | (receive,i) \in domain \, port\} = 
	\{i:ID | (return,i) \in domain \, port\} \\
\also 
FALTA PONER COSAS VER DESPUES!! 
\end{schema}

\begin{schema}{Layer\_InternalCompute}
	\Delta Layer\_State 
\where
	ctrl \in \{ready, running\_callin, taked\_return\_callout\} \\
\also
	l' = l  \\
	in' = in \\
	out' = out \\
	port' = port \\
	ctrl' = ctrl \\
\also
	\exists s_1,s_2 : STATE, i:ID | (s_1, (i,s_2,nullmethod)) \in compute @ \\
	\t1 current  = s_1 \land current' = s_2 \\
\end{schema}

\begin{schema}{Layer\_MakeCallOut}
	\Delta Layer\_State
\where
	ctrl \in \{ running\_callin, taked\_return\_callout \} \\
\also 
	l' = l \\
	in' = in \\
\also 
	\exists s_1,s_2 : STATE, i:ID, m:CALL | (s_1, (i,s_2,m)) \in compute @ \\
	\t1 m \neq nullmethod \\
	\t1 \land current  = s_1 \\
	\t1 \land current' = s_2 \land \\
	\t1 \land out' = i \land \\
	\t1 \land ctrl' = make\_callout \land \\
	\t1 \land port' \ndres \{(send,i)\} = port \ndres \{(send,i)\} \land \\
	\t1 \land port' \, send \, i = m \\ 	 	
\end{schema}

\begin{schema}{Layer\_TakeReturnCallOut}
	\Delta Layer\_State
\where
	ctrl \in \{ receive\_return\_callout \} \\
\also
	l' = l \\
	in' = in \\
	out' = out \\
	port' = port \\
\also
	\exists r:RETURN, \; s_1,s_2:STATE | ( (out,s_1,r), s_2) \in nextreturn @ \\
	\t1 current = s1 \\
	\t1 \land returnby? \, r = port \, send \, out \\			
	\t1 \land current' = s_2 \\
	\t1 \land ctrl' = taked\_return\_callout 
\end{schema}

\begin{schema}{Layer\_RunCallIn}
	\Delta Layer\_State 
\where
	ctrl \in \{ receive\_callin \}  
\also
	l' = l \\
	in' = in \\
	out' = out \\
	port' = port \\
\also
	\exists s_2:STATE | ( ( in, current , port \, receive \, in ),s_2) \in runmethod @ \\
	\t1 current' = s_2 \\
	\t1 \land ctrl' = running\_callin 
\end{schema}

\begin{schema}{Layer\_SendReturnCallIn}
	\Delta Layer\_State
\where
	ctrl \in \{ running\_callin \} 
\also
	l' = l  \\
	in' = in \\
	out' = out \\
\also
	\exists s_1,s_2 : STATE, r:RETURN | (s_1, (in,s_2,r)) \in compute @ \\
	\t1 current = s_1 \\
	\t1 \land r \neq nullmethod \\
	\t1 \land returnby? \, r = port \, receive \, in  \\
	\t1 \land current' = s\_2 \\
	\t1 \land port' \ndres \{(return,in)\} = port \ndres \{(return,in)\} \\
	\t1 \land port' \, return \, in = r \\
	\t1 \land ctrl' = send\_return\_callin \\
\end{schema}

\begin{syntax}
	Layer\_Compute \defs \\
	\t1 Layer\_InternalCompute \\
	\t1 \lor Layer\_MakeCallOut \\
	\t1 \lor Layer\_TakeReturnCallOut \\
	\t1 \lor Layer\_RunCallIn \\
	\t1 \lor Layer\_SendReturnCallIn \\
\end{syntax}

\begin{schema}{Connector}
	Source,Sink : Layer
\where
	Source.id \neq Sink.id \\
	Source.import \subset Sink.export \\
\end{schema}

\begin{axdef}
	layername : \power ID \\
	connectorname : \power ID \\
\where
	layername \bigcap connectorname = \emptyset \\
\end{axdef}

\begin{schema}{System}
	syslayer : layername \fun Layer \\
	sysconnector : layername \cross layername \fun Connector \\
\where
	\forall c:connectorname \exists ln_1,ln_2:layername @ \\
	\t1 sysconnector \, c .Source = syslayer \, ln_1 \land \\
	\t1 sysconnector \, c .Sink = syslayer \, ln_2 \\
\also
	\forall ln_1, ln_2:layername @ \#\{c:connectorname | \\
	\t1 sysconnector \, c.Source = syslayer \, ln_1 \land \\
	\t1 sysconnector \, c.Sink = syslayer \, ln_2 \} \leq 1 \\
\also
	\forall ln_1:layername @ syslayer \, ln_1.id = ln_1
\end{schema}

\begin{schema}{System\_State}
	sys : System \\
	syslayer\_state : layername \fun Layer\_State 
\where
	\forall ln:layername @ syslayer\_state \, ln.l = sys.syslayer \, l 
\end{schema}

\begin{schema}{System\_State\Phi Layer\_State}
	\Delta System\_State \\
	\Delta Layer\_State \\
	layer? : layername 
\where
	sys ' = sys \\
	syslayer\_state' \ndres \{ layer? \} = syslayer\_state \ndres \{ layer? \} \\
	\theta Layer\_State  = syslayer\_state \; layer? \\
	\theta Layer\_State' = syslayer\_state' \; layer? 
\end{schema}

\begin{schema}{System\_Layer\_Compute} 
	System\_State \Phi Layer\_State \\
	Layer\_Compute \\
\where
	\exists ln:layername @ layer? = ln 
\end{schema}

\begin{schema}{System \Phi 2Layer\_State}
	\Delta System\_State 
	\Delta Layer\_State_1 \\
	\Delta Layer\_State_2 \\
	ln_1?,ln_2? : layername
\where
	sys ' = sys \\
\also
	syslayer\_state' \ndres \{ ln_1?, ln_2? \} = syslayer\_state \ndres \{ ln_1?, ln_2? \} \\
\also
	\theta Layer\_State_1 = syslayer\_state \; ln_1? \\
	\theta Layer\_State_2 = syslayer\_state \; ln_2? \\
	\theta Layer\_State_1' = syslayer\_state' \; ln_1? \\
	\theta Layer\_State_2' = syslayer\_state' \; ln_2? \\
\end{schema}

\begin{schema}{System\_DeliverCallIn} 
	System \Phi 2Layer\_State \\
\where
	\exists l_1,l_2:layername @ ln_1? = l_1 \land ln_2? = l_2 \\
\also
	ctrl_1 = makecallout \\  % Listos para mandar!
	ctrl_2 = ready 
\also
	out_1 = l_2.l.id \\  % Se lo esta mandando a ese!
\also
	port_1 \; send \; out_1 \in l_2.l.export
\also
	\exists c:connectorname @ \\
	\t1 \land sys.sysconnector \; c.Source.id = l_1.id \\
	\t1 \land sys.sysconnector \; c.Sink   = l_2.id  \\
\also
	l_1' = l_1 \\
	current_1' = current_1 \\
	in_1' = in_1 \\
	out_1' = out_1  \\
	port_1' = port_1 \\
	ctrl_1' = taked\_callout \\
\also
	l_2' = l_2 \\
	current_2' = current_2 \\
	in_2' = l_1.id \\
	out_2' = out_2 \\
	port_2' \ndres \{ (receive,l_1.id) \} = port_2 \ndres \{ (receive,l_1.id) \}  \\
	port_2' \; receive \; l_1.id = port_1 \; send \; out_1 \\
	ctrl_2' = receive\_callin \\
\end{schema}

\begin{schema}{System\_DeliverReturn} 
	System \Phi 2Layer\_State \\
\where
	\exists l_1,l_2:layername @ ln_1? = l_1 \land ln_2? = l_2 \\
\also
	ctrl_1 = send\_return\_callout \\ % Estados correctos
	ctrl_2 = taked\_callout \\	
\also	
	in_1  = l_2.id \\  % Devuelvo al a quien lo puso!
	out_2 = l_1.id \\  % Devuelvo al a quien lo puso!
\also
%	(l_1.id, returnby? (port_1 \; return \; in_1) \in l_2.import \\
	port_2 \; send \; out_1 = returnby? (port_1 \; return \; in_1) \\ 	
\also
	\exists c:connectorname @ \\
	\t1 \land sys.sysconnector \; c.Source.id = l_1.id \\
	\t1 \land sys.sysconnector \; c.Sink   = l_2.id  \\
\also
	l_1' = l_1 \\
	current_1' = current_1 \\
	in_1' = in_1 \\
	out_1' = out_1  \\
	port_1' = port_1 \\
	ctrl_1' = ready \\
\also
	l_2' = l_2 \\
	current_2' = current_2 \\
	in_2' = in_2 \\
	out_2' = out_2 \\
	port_2' \ndres \{ (returned, out_2) \} = port_2 \ndres \{ (returned,out_2) \}  \\
	port_2' \; returned \; out_2 = port_1 \; return \; in_1 \\
	ctrl_2' = receive\_return\_callout \\
\end{schema}

\begin{syntax}
Total\_System\_Compute \defs \\
	\t1 System\_Layer\_Compute \\
	\t1 \lor System\_DeliverCallIn \\
	\t1 \lor System\_DeliverReturn \\
\end{syntax}
Nota: Faltaria armar lo de la traza, pero ya estoy hecho mierda! :), despues debo
explicar todas las ideas de aca puse...por que de lo contrario despues se me escapan
de la cabeza! ZZZZZZZZZZZZZZZZZ
\end{document}
%
% EJERCICIO 4
%
\section{Pilas}

Es una especificaci\'on de un dominio ``bien comprendido''.

\begin{schema}{Pila[X]}
	stack : \seq X
\end{schema}

\begin{schema}{Push[X]}
	\Delta Pila[X] 
	elem? : X
\where
	stack' = <elem?> \cat stack
\end{schema}

\begin{schema}{Top[X]}
	\Xi Pila[X]
	elem! : X
\where
	elem! = head~ stack
\end{schema}

\begin{schema}{Retract[X]}
	\Delta Pila[X]
\where
	stack' = tail~ stack
\end{schema}

\begin{schema}{Empty[X]}
	Pila[X]
\where
	stack = <> 
\end{schema}

\begin{schema}{InitPila[X]}
	Pila[X]
\where
	stack = <> 
\end{schema}

\begin{syntax}
	T\_Retract[X] = ( \lnot Empty[X] \land Restract[X] ) \lor (Empty[X] \land \Xi Pila) \\
	T\_Top[X] = ( \lnot Empty[X] \land Top[X] ) \lor (Empty[X] \land \Xi Pila) 
\also
	Stack[X] \defs InitPila[X] \lor Push[X] \lor T\_Retract[X] \lor T\_Top[X] \lor \Xi Pila[X]
\end{syntax}

\begin{itemize}
	\item ({\bf Maxi}) ?`Esta bien usado los {\it schemas} parametricos?.	
\end{itemize}


%
% EJERCICIO 5
%
\section{Base de datos cinematografica}

Voy a especificar a la base de datos, o mejor dicho el estado de la base de datos, como 
varias tablas separadas como se modela en los sistemas de base de datos reales.?`Que gano?
, poder concentrarme en las diferentes subpartes de la base de datos, modelar su estados 
respectivos, y luego unir todo. 

Empezamos con la tabla de directores, solo se presentara la operaci\'on de altas ya
que el problema no exije ninguna otra.

\begin{syntax}
	CODIGO == \nat
\also
	TITULO == TEXT
\also
	DIRECTOR == TEXT
\also
	GUIONISTA == TEXT
\also
	DIRECTORES == \power DIRECTOR
\also
	GUIONISTAS == \power GUIONISTA
\also
	TITULOS == \power TITULO
\end{syntax}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% DIRECTORES %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\begin{schema}{InDirector}
	direc? : DIRECTOR
\where
	\#direc? > 0
\end{schema}

\begin{schema}{Directores}
	directores : DIRECTORES
\where
	\forall d:directores @ d \neq <> 
\end{schema}

\begin{schema}{InitDirectores}
	Directores
\where
	directores = \varnothing
\end{schema}

\begin{schema}{AddDirector}
	\Delta Directores \\
	InDirector
\where
	directores' = directores \bigcup \{direc?\} 
\end{schema}


%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% GUIONISTA %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

Modelamos la tabla de guionistas.
\begin{syntax}
	InGuionista \defs InDirector [guion?/direc?, GUIONISTA/DIRECTOR]
\end{syntax}
	
\begin{schema}{Guionistas}
	guionistas : GUIONISTAS
\where
	\forall g:guionistas @ g \neq <>  
\end{schema}

\begin{schema}{AddGuionista}
	\Delta Guionistas
	InGuionista
\where 
	guionistas' = guionistas \bigcup \{guion?\}
\end{schema}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% TITULOS %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
	

Vamos a especificar la base de datos de los titulos de la pelicula.
\begin{schema}{InTitulo}
	tit? : TITULO 
\where
	\#tit? > 0 
\end{schema}

\begin{schema}{Titulos}
	titulos : TITULOS 
\where
	\forall t:titulos @ t \neq <>
\end{schema}

\begin{schema}{InitTitulos}
	Titulos
\where
	titulos = \varnothing 
\end{schema}

\begin{schema}{AddTitulo}
	\Delta Titulos
	InTitulo
\where
	titulos' = titulos \bigcup \{tit?\} 
\end{schema}


%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% RELACIONES %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

Vamos a especificar la relaci\'on entre guionistas y titulos de peliculas.

\begin{schema}{GuionTit} 
	guion\_tit : GUIONISTA \rel TITULO \\
	Titulos \\
	Guionistas
\where
	\forall g\_t : guion\_tit @ \exists g:guionistas @ \exists t:titulos @ g\_t = (g, t) 
\end{schema}
		
\begin{schema}{AddGuionTit}
	\Delta GuionTit \\
	InTitulo \\	
	InGuionista 
\where
	tit? \in titulos  \\
	guion? \in guionistas
\also
	guion\_tit' = guion\_tit \bigcup \{guion?, tit?\} \\
	\theta Guionistas' = \theta Guionistas \\
	\theta Titulos' = \theta Titulos
\end{schema}

\begin{schema}{InitGuionTit}
	GuionTit
\where
	guion\_tit = \varnothing
\end{schema}

Vamos a especificar la relaci\'on entre directores y titulos de peliculas.
\begin{schema}{DirecTit}
	direc\_tit : DIRECTOR \rel TITULO \\
	Titulos \\
	Directores 
\where
	\forall d\_t : direc\_tit @ \exists d:directores @ \exists t:titulos @ d\_t = (d, t)
\end{schema}

\begin{schema}{AddDirecTit}
	\Delta DirecTit \\
	InTitulo \\	
	InDirector 
\where
	tit? \in titulos  \\
	direc? \in directores
\also
	direc\_tit' = direc\_tit \bigcup \{direc?, tit?\} \\
	\theta Drectores' = \theta Directores \\
	\theta Titulos' = \theta Titulos
\end{schema}

\begin{schema}{InitDirecTit}
	DirecTit
\where
	direc\_tit = \varnothing
\end{schema}

Terminado ya de especificar las diferentes tablas necesarias de mi base de datos las voy a 
juntar para formar la misma.

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% BASE %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\begin{schema}{Peliculas}
	GuionTit \\
	DirecTit
\end{schema}

\begin{schema}{InitPeliculas}
	GuionTit \\	
	DirecTit
\where
	InitTitulos \\
	InitDirectores \\
	InitGuionistas \\
	InitDirecTit \\
	InitGuionTit 
\end{schema}

\begin{schema}{AddPeliculaPel}
	\Delta Peliculas \\
	InTitulo \\
	InDirector \\
	InGuionista
\where
	AddGuionTit \\
	AddDirecTit	
\end{schema}
	
Ahora tengo que hacer la ``promoci\'on de operadores'' de mis componentes, como debido a 
que tengo una sola de cada una puede prescindir de las funciones que operan sobre nombres
(NAME).
\begin{schema}{AddDirectorPel}
	\Delta Peliculas \\
	\Xi GuionTit \\
	AddDirector
\where
	direc\_tit' = direc\_tit
\end{schema}
	
\begin{schema}{AddGuionistaPel}
	\Delta Peliculas \\
	\Xi DirecTit \\
	AddGuionista
\where
	guion\_tit' = guion\_tit
\end{schema}

\begin{schema}{AddTituloPel}
	\Delta Peliculas \\
	\Xi Directores \\
	\Xi Guionistas \\
	AddTitulo
\where
	direc\_tit' = direc\_tit \\
	guion\_tit' = guion\_tit 
\end{schema}

Consultas sobre la base de datos.

\begin{schema}{ConsultaGuionista}
	\Xi Peliculas \\
	InGuionista \\
	titulos! : TITULOS
\where
	titulos! = guion\_tit \limg \{guion?\} \rimg 
\end{schema}

\begin{schema}{ConsultaDirector}
	\Xi Peliculas \\
	InDirector \\
	titulos! : TITULOS
\where
	titulos! = direc\_tit \limg \{direc?\} \rimg 
\end{schema}
	

\begin{schema}{ModDirectorPel}
	\Delta Peliculas \\
	InDirec_o \\
	InDirec_n 
\where
	direc?_o \in directores \\
	\exists t: titulos @ (direc?_o, t) \in direc\_pel 
\also
	directores' = directores \setminus \{direc?_o\} \bigcup \{direc?_n\} \\ 
	direc\_tit' = \{direc?_o\} \ndres direc\_tit  \\ 
		\t3 	 \bigcup \{ t : titulos | t \in direc\_tit \limg \{direc?_o\} \rimg @ \\
		\t3  	direc?_n \mapsto t \}  \\
	\Xi GuionTit 
\end{schema}	
		

\begin{schema}{InitPeliculas} 
	InitTitulos \\
	InitDirectores \\
	InitGuionistas \\
	InitDirecTit \\
	InitGuionTit \\
	InitPeliculas \\
\end{schema}

\begin{syntax}
Base \defs AddPeliculaPel \lor AddTituloPel \lor AddDirectorPel \lor AddGuionistaPel \\
\t1 \lor AddDirecTit \lor AddGuionTit \lor ConsultaGionista \lor ConsultaDirector \\
\t1 \lor ModDirectorPel \lor InitPeliculas \lor \Xi Peliculas
\end{syntax}
		  
\begin{itemize}
	\item ({\bf Maxi}) Aca hice un {\it schema} por cada entrada de datos validandolo, de
		  esta manera la validacion la escribo una sola vez pudiendolo usar varias veces.
		  Ademas puedo llegar a escribir propiedades como $\forall \, InDirector \, \dots$.
		  ?`Esta bien?.
	
	\item ({\bf Maxi}) Al principio habia pensado en una especie de c\'odigo de director, 
		  c\'odigo de guionista, etc; debido a que este es un mecanismo para evitar 
		  repeticiones en una base de datos. Pero yo aca en $Z$ lo hice mediante conjuntos, 
		  los cuales netamente no repiten datos.?`Esta bien este nivel de abstracci\'on?.

	\item ({\bf Maxi}) La semantica del sistema que yo le di con respecto al hacer alguna 
		  operacion que
		  recibe datos de entradas es: lee los datos de entrada y si estos son correctos
		  realizo la operaci\'on correspondiente, de lo contrario no cambio la base de 
		  datos. Para lograr esto solo arme {\it schemas} que funcionan sobre ciertas 
		  precondiciones, no arme {\it schemas} que me digan que pasa si estas no se 
		  cumplen ?`por qu\'e?, para eso agrego al final de la especificacion del 
		  sistema el $\Xi$. ?`Es correcto?. En el caso de que al no cumplirse las 
		  precondiciones se comportara de otra manera, emitiendo alguna alarma, si deberia
		  especificarlo ?`Es asi?. 
		   
	\item ({\bf Maxi}) Aca la semantica de ingresar algun dato repetido en no cambiar 
		  el estado de la 
		  base. ?`Esta bien?, ?`Es una opcion de especificacion a seguir?.
\end{itemize}
%
% EJERCICIO 6
%
\section{Editor y otras cositas}

\begin{enumerate}[a)]

\item 
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\begin{axdef}
	left\_arrow : CHAR
\where
	left\_arrow \nin printing
\end{axdef}

\begin{schema}{LeftArrow}
	ch?: CHAR 
\where
	ch? = left\_arrow 
\end{schema}

\begin{schema}{Backward}
	\Delta Editor \\
	LeftArrow
\where
	left' = left \cat <head~ right> \\
	right' = right
\end{schema}

\begin{schema}{BOF}
	Editor
\where
	left = <>
\end{schema}

\begin{syntax}
T\_Backward \defs (\lnot BOF \land Backward) \lor (BOF \land LeftArrow \land \Xi Editor)
\end{syntax}

\begin{axdef}
	del\_key : CHAR
\where
	del\_key \nin printing
\end{axdef}

\begin{schema}{DelKey}
	ch? : CHAR 
\where
	ch? = del\_key
\end{schema}

\begin{schema}{Delete}
	\Delta Editor
	DelKey
\where
	left' = left
	right' = tail right
\end{schema}

\begin{syntax}
T\_Delete \defs (\lnot EOF \land Delete) \lor (EOF \land DelKey \land \Xi Editor) 
\end{syntax}

\item 
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\begin{syntax}
NoOpKey \defs [ch?:CHAR | ch? \notin printing] \land \\
\t2  \lnot DelKey \land \lnot LeftArrow \land \lnot RightArrow \land \Xi Editor \\
\end{syntax}

\item 
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\begin{itemize}
	\item ({\bf Maxi}): No especifico que el archivo pertenezca al {\it filesystem} ya que 
		  al mismo lo voy a denotar por su contenido que es lo que me interesa.?`Esta bien?
	\item Ademas no todo archivo (flujo de datos) esta dentro del {\it filesystem}, recordar
		  los {\it pipes} del {\it Kernel} de Linux.
\end{itemize}
	
\begin{syntax}
	FILE == TEXT 
\end{syntax}

\begin{schema}{LoadFile}
	\Delta Editor
	file? : FILE
\where
	left' = <>
	right' = file?
\end{schema}

\item 
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

Estados del esquema $EOF$.

\begin{syntax}
	right = <> \\
	left = < \mbox{todos las posibles {\it strings}, sean o no caracteres ``imprimibles''} > 
\end{syntax}

No voy a sacar exactamente la cantidad de estado, ya que eso no me aporta mucha informaci\'on
en este nivel de abstraccion, sino que calculare el orden de los mismos. (Ver hoja anexa
escrita a mano).

\item 
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\begin{verbatim}
data Editor = Edit String String

insert:: Char -> Editor -> Editor 
printing :: Char -> Bool 

insert ch (Edit left right) | printing ch = Edit (ch:left) right
                            | otherwise = Edit left right
\end{verbatim}

\begin{itemize}
	\item Notaremos que en los esquemas {\it Insert, Delete, Fordward, Backward} 
		  siempre se agrega algo al final de {\it left}. 

	\item Representaremos nuestro editor mediante el constructor {\texttt{Editor left right}},
		  donde el primer elemento de {\it left} es el ultimo caracter en la variable 
		  {\it left} de los {\it schemas}. 

	\item el string {\texttt{right}} tiene la misma semantica que la variable {\it right} que
		  aparece en los {\it schemas}. 

	\item Viendo todo lo anterior vemos que se realizan $O(1)$ operaciones $(:)$.

	\item ({\bf Maxi}) ?`Era esto lo que habia que hacer? 
\end{itemize}
 
\item 
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\begin{syntax}
	\forall Editor | Init @ EOF \equiv \\
	\forall left, right : TEXT | left = <> \land right = <> @ right = <> 
\end{syntax}




\end{enumerate}


%
% EJERCICIO 7
%
\section{Contestador}

Vamos a tratar de definir cintas de contestador, esto se realizo as\'i despues de 
ver varias formas diferentes de especificar este ejercicio llegando a esta version 
mucho mas simplificada y clara.

\begin{syntax}
[MSG]
\end{syntax}

\begin{schema}{Cinta}
	msgs : \seq MSG
\end{schema}

\begin{schema}{InitCinta}
	Cinta
\where
	msgs = <>
\end{schema}

\begin{schema}{AddCinta}
	\Delta Cinta \\
	msg? : MSG
\where
	msgs' = msgs \cat <msg?> 
\end{schema}

\begin{schema}{RemoveCinta}
	\Delta Cinta \\
	msg! : MSG
\where
	msgs \neq <> 
\also
	msg! = head~ msgs \\
	msgs' = tail~ msgs
\end{schema}

Vamos ahora a especificar el contestador.

\begin{axdef}
	play, save : NAME  \\
	cintas : \power NAME
	max : \nat
\where
	play \in cintas \\
	save \in cintas 
\also
	max > 0 
\end{axdef}

\begin{syntax}
	LIGHT & ::= on | off 
\also
	BOTON & :: = play | save | any 
\end{syntax}

\begin{schema}{Contestador}
	cinta : cintas \fun Cinta \\
	full : LIGHT \\
	btn : BOTON \\
	speaker : MSG
\where
	btn \in \{any,save\} \Rightarrow \#( (cinta~play).msgs \cat (cinta~save).msgs ) \leq max \\
	btn \in \{play\} \Rightarrow \#( (cinta~play).msgs \cat (cinta~save).msgs ) + 1 \leq max 
\also
	btn \in \{any, save\} \land \#( (cinta~play).msgs \cat (cinta~save).msgs ) = max \\
	\t1	     \Rightarrow full = on  \\
	btn \in \{play\} \land \#( (cinta~play).msgs \cat (cinta~save).msgs ) + 1 = max  \\
	\t1		\Rightarrow full = on 
\also
	btn \in \{any, save\} \land \#( (cinta~play).msgs \cat (cinta~save).msgs ) < max \\
	\t1		     \Rightarrow full = off  \\
	btn \in \{play\} \land \#( (cinta~play).msgs \cat (cinta~save).msgs ) + 1 < max \\
	\t1		\Rightarrow full = off 
\end{schema}	
	 

Vamos a promover el {\it schema} Cinta al nivel del contestador.

\begin{schema}{Contestador \Phi Cinta}
	\Delta Contestador \\
	\Delta Cinta \\
	ct? : NAME
\where
	\{ct?\} \ndres cinta = \{ct?\} \ndres cinta \\
	\theta Cinta = cinta \{ct?\} \\
	\theta Cinta' = cinta' \{ct?\} 
\end{schema}

\begin{axdef}
	null : MSG
\end{axdef}

\begin{schema}{InitContestador}
	Contestador
\where
	btn = any \\
	speaker = null 
\also
	\forall c:cintas @ cinta~ c = \theta InitCinta
\end{schema}

\begin{schema}{Play} 
	Contestador \Phi Cinta \\
	RemoveCinta
\where
	ct?=play \iff \#(cinta~ play).msgs \neq <>  \\
	ct?=save \iff \#(cinta~ play).msgs = <>  
\also
	speaker' = msg! \\
	btn' = play
\end{schema}

\begin{schema}{Save}
	Contestador \Phi Cinta \\
	AddCinta
\where
	btn = play 
\also
	ct?=save \\
	msg? = speaker 
\also
	btn' = save \\
	speaker' = speaker 
\end{schema}

\begin{schema}{Call}
	Contestador \Phi Cinta \\
	AddCinta \\
	msg\_callin? : MSG
\where
	full = off 
\also
	ct? = play \\
	msg? = msg\_callin? \\
\also
	btn' = any \\
	speaker' = speaker
\end{schema}


\begin{syntax}
	T\_Contestador \defs InitContestador \lor Play \lor Save \lor \Xi Contestador 
\end{syntax}


\begin{itemize}
	\item ({\bf Maxi}) Cuando defino el conjunto de nombres que representan a los componentes
		  o subsistemas generalmente se hace $x \in C$, pero no se aclara nada de si en $C$
		  hay mas cosas o no se dice $\{x\}=C$ (Jacky lo hace asi!). ?` Qu\'e estilo opto?, 
		  como esta hecho el contestador o como trabaja Jacky es m\'as abstracto ya que yo 
		  pienso en la especificaci\'on no por el contenido exacto de $C$.

	\item ({\bf Maxi}) ?`Es valido poner un valor nulo de un tipo de datos como para 
		  inicializar con ese valor alguna variable de un {\it schema}? (ver el {\it schema}
		  de inicializaci\'on del contestador).

	\item ({\bf Maxi}) Aca cuando ninguna precondici\'on se cumpla en el contestador va a 
		  quedar inmutable es su estado ($\Xi$). Por lo cual solo me intereso en especificar
		  las operaciones exijiendo las precondiciones sobre las cuales son validas 
		  solamente.?`Esta bien?.

	\item ({\bf Maxi}) Ver la especificaci\'on del contestador que hice en papel, comentar
		  que a esta version llegue luego de varias especificaciones. ?`Esta mal?.
		  
\end{itemize}
		  
%
% EJERCICIO 8
%
\section{Pipes}

Primero voy a definir un {\it stream}, el cual, es la modelizaci\'on y la unidad de 
redireccionamiento en Unix.
\begin{schema}{Stream}
	stream : TEXT
\end{schema}

Una vez hecho esto, modelo la tabla de descriptores de archivos de un proceso mediante 
una funci\'on. Todo proceso debe tener almenos dos {\it streams} asociados a el, los cuales
son entrada y salida estandar.
\begin{syntax}
	PID == \nat 
\also
	STDIN == 0 \\
	STDOUT == 1 
\also
	SOURCE == 0 \\
	DEST == 1 \\
\also
	ROLL\_PROC == \{0,1\}
\end{syntax}

\begin{schema}{Proceso}
	pid : PID \\
	descrip : \nat \pfun Stream
\where
	\exists i,o:Stream @ descrip~ STDIN	= i \land descrip~ STDOUT = o 
\end{schema}

Modelamos ahora un {\it pipe} como un vinculo entre dos procesos, ese vinculo es justamente
la redireccion de la entrada/salida estandar.  
\begin{schema}{Pipe}
	proceso: ROLL\_PROC \fun Proceso
\where
	(proceso~ SOURCE).descrip~ STDOUT = (proceso~ DEST).descrip~ STDIN \\
	(proceso~ SOURCE).descrip~ STDIN = (proceso~ DEST).descrip~ STDOUT \\
\end{schema}
	

%
% EJERCICIO 9
%
\section{Despachante}

Aca voy a armar es despachante apartir de sus componentes o subsistemas. Al armar una 
especificaci\'on siguiendo este estilo es importante tener en cuenta la promoci\'on 
de operadores, los cuales me permiten ``realizar'' operaciones sobre un subsistema
desde el nivel del sistema.


Primero voy a especificar el buffer, junto con sus operaciones ofrecidas.

%%%%%%%%%%%%%%%%%%%%%%%%%%% BUFFER %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\begin{syntax}
	YESNO & ::= yes | no
\also
	MSG == TEXT
\end{syntax}

\begin{axdef}
	max\_buff: \nat \\
\where
	max\_buff > 0 
\end{axdef}

\begin{schema}{Buff}
	buffer: \seq MSG \\
	isfull: YESNO
	isempty : YESNO
\where
	\#buffer <= max\_buff  \\
	isfull = yes \iff \#buffer = max\_buff
\also
	\#buffer > 0 \iff isempty = no \\
\end{schema}

\begin{axdef}
	parity: MSG \fun YESNO
\end{axdef}

\begin{schema}{PutBuff}
	\Delta Buff \\
	msg?: MSG
\where
	isfull = no 
\also
	parity~ msg? = yes \implies buffer' = buffer \cat <msg?> \\
	parity~ msg? = no \implies buffer' = buffer 
\end{schema}

\begin{schema}{GetBuff}
	\Delta Buff \\
	msg! : MSG
\where
	isempty = no 
\also
	msg! = head~ buffer \\
	buffer' = tail~ buffer 
\end{schema}

\begin{schema}{FullBuff}
	Buffer
\where
	isfull = yes 
\end{schema}

\begin{schema}{EmptyBuff}
	Buffer
\where
	isempty = yes
\end{schema}


\begin{syntax}
Buffer \defs ( PutBuff \lor (FullBuff \land \Xi Buff) ) \lor \\
\t2 ( GetBuff \lor (EmptyBuff \land \Xi Buff) )
\end{syntax}

%%%%%%%%%%%%%%%%%%%%%%%%%%% CANALES %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

Vamos a especificar ahora los canales junto con las operaciones sobre el mismo.

\begin{axdef}
	null : MSG 
\end{axdef}


\begin{schema}{Ch}
	ch\_dato: MSG \\
	error!: YESNO
\where
	error! = parity~ ch\_dato 
\end{schema}


\begin{schema}{ReadCh}
	\Delta Ch \\
	in?: MSG
\where
	ch\_dato' = in? 
\end{schema}

\begin{schema}{PutCh}
	\Delta Ch \\
	out? : MSG
\where
	ch\_dato' = out?
\end{schema}

\begin{schema}{InitCh}
	Ch
\where
	ch\_dato = null \\
	error! = no 
\end{schema}

%%%%%%%%%%%%%%%%%%%%%%%%%%% DESPACHANTE %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

Vamos a componer los subsistemas especificados mediante las tecnicas de asignarle a cada 
componente un nombre.
\begin{axdef}
	in1, in2, out1 : NAME \\
	ChEntradas, ChSalidas : \power NAME \\
	canales : \power NAME \\
\where
	\{in1, in2\} \in ChEntradas \\
	\{out1\} \in ChSalidas \\
	canales = ChEntradas \bigcap ChSalidas \\
\end{axdef}

\begin{schema}{Despachante}
	canal: canales \fun Ch \\
	Buffer
	vaciando : YESNO
\where
	\#canal = 3 
\also
	FullBuff \implies vaciando = yes 
	EmptyBuff \implies vaciando = no
\end{schema}	

Voy a promover el {\it schema} canal al nivel del despachante para luego poder aplicar 
las operaciones del buffer al nivel del sistema.

\begin{schema}{Despachante \Phi Ch}
	\Delta Despachante \\
	\Delta Ch \\
	ch?: canales
\where
	\{ch?\} \ndres canal' = \{ch?\} \ndres canal \\
	\theta Ch = canal~ ch? \\
	\theta Ch' = canal'~ ch? 
\end{schema}

Modelamos cuando llega un dato por un canal.
\begin{schema}{ComeInCh}
	\Delta Despachante \Phi Ch \\
	ReadCh \\
	PutBuff
\where
	ch? \in ChEntradas 
\also
	msg? = in? 
\end{schema}
 
\begin{schema}{ComeOutCh}
	\Delta Despachante \Phi Ch \\
	PutCh \\
	GetBuff 
\where
	\lnot(EmptyBuff) \\
	ch? \in ChSalidas
\also
	out? = msg! 
\end{schema}


\begin{schema}{InitDespachante}
	Despachante
\where
	\forall c:canales @ canal~ c = \theta InitCh \\
	InitBuff
\end{schema}

\begin{schema}{Vaciando}
	Despachante
\where
	vaciando = yes
\end{schema}


\begin{syntax}
T\_Despachante \defs InitDespachante \lor (Vaciando \land ComeOutCh) \lor \\
\t4 (\lnot Vaciando \land ComeInCh) \lor \Xi Despachante 
\end{syntax}


\begin{itemize}
	\item ({\bf Maxi}) Aca el problema del despachante fue modelar la salida, ya que esto
		  se puede pensar como un conjunto de instrucciones secuenciales de sacar de a un 
		  elemento el buffer, por otro lado yo antes la especificacion la habia hecho de 
		  tal manera que cuando se llenaba el buffer se devolvia, mediante una variable 
		  de salida del mismo tipo del buffer, todos los mensajes. ?`Que es mejor?, la 
		  que hice aca es mas larga pero no deja de espresar que hay UN canal de salida, 
		  mientras que pensandolo de la otra manera no se sabe. 
	\item ({\bf Maxi}) Al poner el $\Xi$ al final siempre cuando defino un sistema es debido
		  a que hay estados que si me interesan a la hora de tomar las decisiones sobre las 
		  operaciones brindadas (precondiciones) pero cuando estas no se cumplen el sistema
		  no tiene que hacer nada. ?`Es por eso?.
	\item ({\bf Maxi}) Cuando poseo por ejemplo tres {\it schemas} $A,B,C$ y sus tres 
		  precondiciones se cumplen ?` Es valido?, con eso estoy denotando que me da lo 
		  mismo realizar cualquiera de las tres operaciones o que estan las tres disponibles
		  al mismo tiempo.?`Esta bien?.
\end{itemize}



%
% EJERCICIO 10
%

\section{Guardia de Hospital}

Aca nuevamente vamos a especificar las componentes del sistema junto con las operaciones que 
ellas ofrecen pero luego integrar todo en el sistema.

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% DISPOSITIVO %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
Empezamos modelando un dispositivo.
\begin{syntax}
	LECTURA == \num 
\also
	STATUS ::= ok | fault 
\also
	ALARMA ::= falla\_disp | fuera\_rango | nada
\end{syntax}

\begin{schema}{Rango}
	minimo, maximo : LECTURA
\where
	minimo \leq maximo 
\end{schema}

\begin{schema}{Dispositivo}
	Rango  \\
	lectura : LECTURA \\
	func : STATUS \\
	alarma : ALARMA \\
\where
	func = fault \iff alarma = falla\_disp  \\
	func = ok \iff alarma = nada \\
	\lnot(minimo \leq lectura \leq maximo) \iff alarma = fuera\_rango
\end{schema}
	
\begin{axdef}
	check : Dispositivo \fun STATUS
\end{axdef}
	
\begin{schema}{Lectura}
	\Delta Dispositivo \\
	\Xi Rango \\
	lectura? : LECTURA 
\where
	check~ \theta Dispositivo = ok
\also
	lectura' = lectura? \\
	func' = ok 
\end{schema}

\begin{schema}{ErrorDisp}
	\Delta Dispositivo \\
	\Xi Rango
\where
	check~ \theta Dispositivo = fault
\also
	func' = fault \\
	lectura' = lectura
\end{schema} 
	

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% BOX %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
Modelas el {\it box} de enfermeria donde van los mensajes de alarma.
\begin{syntax}
	[NAME]
\end{syntax}

\begin{axdef}
	pacientes, dispositivos : \power NAME 
\where
	pacientes \bigcap dispositivos = \varnothing 
\end{axdef}

\begin{schema}{Box}
	monitor: \seq pacientes \cross dispositivos \cross ALARMA
\end{schema}

\begin{schema}{PutBox}
	\Delta Box \\
	msg\_box? : pacientes \cross dispositivos \cross ALARMA
\where
	monitor' = monitor \cat <msg\_box?>  
\end{schema}


%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% PACIENTE %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
Modelamos a los pacientes.

\begin{syntax}
	FREC == \num
\end{syntax}

\begin{schema}{Paciente}
	frec : FREC \\
	disp\_adosados : \power Dispositivo
\where
	frec >= 0 \\
	\#disp\_adosados > 0 
\end{schema}

\begin{schema}{InitPaciente}
	Paciente
\where
	\exists frec\_seteo : FREC @ frec = frec\_seteo \\
	\exists disp\_inicial : dispositivos @ disp\_inicial \in disp\_adosados
\end{schema}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% BASE %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
Modelamos la base de datos que almacena las lecturas.
\begin{schema}{Base}
	base : \seq pacientes \cross dispositivos \cross LECTURA  \\
\end{schema}

\begin{schema}{PutBase}
	\Delta Base
	reg?: pacientes \cross dispositivos \cross LECTURA
\where	
	base' = base \cat <reg?>
\end{schema}

\begin{schema}{InitBase}
	Base
\where
	base = <>
\end{schema}

Ahora juntamos todo en el sistema.
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% GUARDIA %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\begin{schema}{Guardia}
	dispositivo : dispositivos \fun Dispositivo \\
	paciente : pacientes \fun Paciente \\
	Base \\
	Box  
\where
	\forall p_1,p_2:pacientes | p_1 \neq p_2 @  \\
\t1 (paciente p_1).disp\_adosados \bigcap (paciente p_2).disp\_adosados = \varnothing
\end{schema}
	
Vamos a promover el {\it schema} dispositivo al nivel del sistema.
\begin{schema}{Guardia \Phi Dispositivo}
	\Delta Guardia \\
	\Delta Dispositivo \\
	disp? : dispositivos
\where
	\{disp?\} \ndres dispositivo = \{disp?\} \ndres dispositivo' \\
	\theta Dispositivo = dispositivo~ disp?
	\theta Dispositivo' = dispositivo'~ disp?
\end{schema}


\begin{schema}{LecturaDisp}
	Guardia \Phi Dispositivo \\
	Lectura \\
	PutBase
\where
	\exists p:pacientes @ disp? \in (paciente p).disp\_adosados \land \\
\t2 reg? = (p, disp?, lectura?)   
\end{schema}

\begin{schema}{FalloDisp}
	Guardia \Phi Dispositivo \\
	ErrorDisp \\
	PutBox \\
	\Xi Base
\where
	\exists p:pacientes @ disp? \in (paciente p).disp\_adosados \land \\
	\t1 msg\_box? = (p, disp?, alarma') 
\end{schema}	
	
\begin{schema}{InitGuardia}
	Guardia
\where
	\forall d:dispositivos @ dispositivo~ d = \theta InitDispositivo \\
	\forall p:pacientes @ paciente~ p = \theta InitPaciente \\
\also
	InitBox \\
	InitBase 
\end{schema}


\begin{syntax}
GuardiaHospital \defs InitGuardia \lor LecturaDisp \lor FalloDisp \lor \Xi Guardia
\end{syntax}

\begin{itemize}
	\item ({\bf Maxi}) Existe una variable de {\it Dispositivo} llamada alarma, que su 
		  funci\'on es comunicar al exterior un estado del dispositivo. Si hubiese 
		  puesto como variable de estado {\it alarma!} en vez de {\it alarma}, ?` 
		  Hay alguna contradicci\'on con la convenci\'on de nombres de variables?

	\item ({\bf Maxi}) Para chequear que un dispositivo ande utilizo una funci\'on externa
		  que no la descripvo como funciona sino lo que hace. ?`Esta bien?

	\item ({\bf Maxi}) Cuando hago la lectura del dispositivo use una variable para 
		  representar un valor proveniente de ``afuera'', pero mi pregunta es: ?` Se entiende
		  que es una lectura de ese dispositivo?. ?`Tengo que especificar m\'as?. (por 
		  ejemplo una funcion que dado un dispositivo o alguna clase de id me devuelva la 
		  lectura). Es mas que nada por un tema de semantica.

	\item ({\bf Maxi}) Ver el {\it schema} paciente, ?`Cuando quiero decir algo que 
		  desconozco uso un existencial?. Ver tambi\'en {\it LecturaOk}.
\end{itemize}


\end{document}
