aed1-tpe/template/templateTP.tex

\documentclass[a4paper]{article}

\usepackage[spanish]{babel}
\usepackage[latin1]{inputenc}

\usepackage{framed}
\input{Algo1Macros}

\newcommand{\comen}[2]{%
\begin{framed}	
\noindent \textsf{#1:} #2
\end{framed}
}



\begin{document}

\materia{Algoritmos y Estructura de Datos I}
\cuatrimestre{2}
\anio{2016}

%\fecha{26 de agosto de 2016}

\nombre{\LARGE TPE OJOTA (Organizaci\'on de Juegos Ol\'impicos Tp de Algoritmos 1) v1.0}

\titulotp


\section{Tipos}

\input{tipos/tipos.tex}

\section{Atleta}
\input{tipos/atleta.tex}

\begin{problema}{especialidad}{a: Atleta}{Deporte}
	\asegura{res \in deportes(a)}
	\asegura{capacidad(a,res)==maximoLista(listarCapacidades(a))}
	\aux{listarCapacidades}{a:Atleta}{[\ent]}{[capacidad(a,x) | x \leftarrow deportes(a) ]}
	\aux{maximoLista}{ls:[\ent]}{\ent}{[x|x\leftarrow ls, (\forall y \leftarrow ls) x \geq y][0]}
\end{problema}

\begin{problema}{entrenarNuevoDeporte}{a: Atleta, d: Deporte, c: \ent}{}
	\requiere{c \geq 0 \wedge c \leq 100}
	\requiere{d \notin deportes(a)}
	\modifica{a}
	\asegura{nombre(a)==nombre(pre(a))}
	\asegura{sexo(a) == sexo(pre(a))}
	\asegura{anoNacimiento(a)==anoNacimiento(pre(a))}
	\asegura{nacionalidad(a)==nacionalidad(pre(a))}
	\asegura{ciaNumber(a)==ciaNumber(pre(a))}
	\asegura{(\forall d' \leftarrow deportes(pre(a)))capacidad(a,d')==capacidad(pre(a),d')}

	\asegura{mismos(deportes(a),d:deportes(pre(a)))}
	\asegura{ordenada(deportes(a))}
	\asegura{capacidad(a,d)==c}
\end{problema}



\section{Competencia}

\input{tipos/competencia.tex}

\begin{problema}{finalizarCompetencia}{c: Competencia, posiciones: [Atleta], control: [(Atleta, \bool)]}{}
	%definir mismos en Auxiliares
	\requiere{\neg finalizada(c)}
	\requiere{contenida(posiciones,participantes(c))}
	\requiere{sinRepetidos(posiciones)}
	\requiere{(\forall x \leftarrow control) prm(x) \in participantes(c)}
	\requiere{sinRepetidos([prm(x) | x \leftarrow control])}
	\modifica{c}
	\asegura{finalizada(c)}
	\asegura{ranking(c)==posiciones}
	\asegura{participantes(c)==participantes(pre(c))}
	\asegura{mismos(LesTocoControlAntiDoping(c), [prm(x) | x \leftarrow control])}
	\asegura{(\forall x \leftarrow control) leDioPositivo(prm(x))==sgn(x)}
	\asegura{categoria(c)==categoria(pre(c))}
\end{problema}

\begin{problema}{linfordChristie}{c: Competencia, a: Atleta}{}
	\requiere{\neg finalizada(c)}
	\requiere{a \in participantes(c)}
	\modifica{c}
	\asegura{mismos(participantes(pre(c)), a:participantes(c))}
	\asegura{categoria(c)==categoria(pre(c))}
	\asegura{\neg finalizada(c)}
\end{problema}

\begin{problema}{gananLosMasCapaces}{c: Competencia}{\bool}
	\requiere{finalizada(c)}
	\asegura{res==(\forall x \leftarrow[0..|ranking(c)|-2]) \newline
	capacidad(ranking(c)[x],prm(categoria(c))) \geq capacidad(ranking(c)[x+1],prm(categoria(c)))}
\end{problema}

\begin{problema}{sancionarTramposos}{c: Competencia}{}
	\requiere{finalizada(c)}
	\modifica{c}
	\asegura{finalizada(c)}
	\asegura{categoria(c)==categoria(pre(c))}
	\asegura{mismos(participantes(c),participantes(pre(c)))}
	\asegura{incluida(ranking(c),participantes(c))}
	\asegura{incluida(LesTocoControlAntiDoping(c),participantes(c))}
	\asegura{mismos(ranking(pre(c)),ranking(c)++listaDoping(c,LesTocoControlAntiDoping(c)))}
	\asegura{ranking==[ el | el \leftarrow ranking(pre(c)),el \notin listaDoping(c,LesTocoControlAntiDoping(c))]}

	\aux{listaDoping}{c:competencia, a:[atleta]}{[atleta]}{[x|x \leftarrow a, leDioPositivo(c,x)]}

\end{problema}

\section{JJOO}
\input{tipos/jjoo.tex}

\begin{problema}{dePaseo}{j: JJOO}{[Atleta]} 
	\asegura{mismos(res,noParticiparon(j))}
	\aux{noParticiparon}{j: JJOO}{[Atleta]}{[x | x \leftarrow atletas(j), \neg en(x, participaronConRepes(j))]}
	\aux{participaronConRepes}{j: JJOO}{[Atleta]}{[atl | dia \leftarrow [1..cantDias(j)], comp \leftarrow cronograma(j, dia), atl \leftarrow atletas(j), en(atl, participantes(comp))]}
\end{problema}

\begin{problema}{medallero}{j: JJOO}{[(Pais, [\ent])]}
	%Written by martu
	\asegura{mismos(result, sacarSinMedallas(crearMedallero(j)))}
	\asegura{medalleroOrdenado(result)}
	\aux{listaNacionalidadesAtletas}{j: JJOO}{[Pais]}{[nacionalidad(at) | at \leftarrow atletas(j)]}
	\aux{sacarRepeticiones}{ls : [T]}{[T]}{[ls[x] | x \leftarrow [0..|ls|-1], \neg en(ls[x], ls[0..x-1])]}
	\aux{listaPaises}{j: JJOO}{[Pais]}{sacarRepeticiones(listaNacionalidadesAtletas(j))}
	\aux{cuenta}{x: T, a: [T]}{\ent}{|[y | y \leftarrow a, y == x]|}
	\aux{nacionalidadPrimerosTres}{c:Competencia}{[Pais]}{\newline
	[ifthenelse(i \leq |ranking (c)|-1, nacionalidad(ranking(c)[i]), "Narnia") | i \leftarrow [0..2]]}
	\aux{ganadoresMTotales}{M: \ent, j: JJOO}{[Pais]}{\newline
	[nacionalidadPrimerosTres(c)[M] | dia \leftarrow [1.. jornadaActual(j)], c \leftarrow cronograma(j, dia), finalizada(c)]}
	\aux{crearMedallero}{j: JJOO}{[(Pais, [\ent])]}{\newline
	[(p, [cuenta(p, ganadoresMTotales(0,j)), cuenta(p, ganadoresMTotales(1,j)),\newline cuenta(p, ganadoresMTotales(2,j))]) | p \leftarrow listaPaises(j)]}
	\aux{sacarSinMedallas}{lista : [(Pais, [\ent])]}{[(Pais, [\ent])]}{[x | x \leftarrow lista, sgn(x) \neq [0,0,0]]}
	\aux{medalleroOrdenado}{lista : [(Pais, [\ent])]}{Bool}{\newline
	(\forall x \leftarrow [0..|lista|-2]) ((sgd(lista[x])[0] \geq sgd(lista[x+1])[0]) \newline
	\vee ((sgd(lista[x])[0]==sgd(lista[x+1])[0]) \wedge (sgd(lista[x])[1] \geq sgd(lista[x+1])[1]))\newline
	\vee ((sgd(lista[x])[0]==sgd(lista[x+1])[0]) \wedge (sgd(lista[x])[1]==sgd(lista[x+1])[1]) \wedge (sgd(lista[x])[2] \geq sgd(lista[x+1])[2])))}
\end{problema}

\begin{problema}{boicotPorDisciplina}{j: JJOO, cat: (Deporte, Sexo), p: Pais}{\ent}
	\requiere{existe (c \leftarrow todasLasCompetencias(j)) categoria(c) == cat}
	\requiere{finalizada (competenciaFiltrada(j,cat)) == false}
	// asumimos que se saca a los participantes antes de finalizar la competencia\newline
	\modifica{j}
	\asegura{finalizada ( competenciaFiltrada(j,cat) ) == finalizada (competenciaFiltrada(pre(j),cat))}
	\asegura{ano(j) == ano(pre(j))}
	\asegura{mismos(atletas(j), atletas(pre(j)))}
	\asegura{cantDias(j) == cantDias(pre(j))}
	\asegura{jornadaActual(j) == jornadaActual(pre(j))}
	\asegura{(\forall dia \leftarrow [1..cantDias (j)] ) \newline
		|cronograma(j,dia) | == |cronograma(pre(j), dia)|}

	\asegura{ (\forall dia \leftarrow [1..cantDias(j)])
		(\forall( x \leftarrow [1..(long(cronograma(j,dia))-1)])) \newline
		((cronograma((j,dia)[x] == cronograma (pre(j),dia) [x]) \newline \vee ( categoria(cronograma(j,dia)[x]) == (categoria(cronograma(pre(j),dia)[x])) \newline \wedge  (categoria(cronograma(j,dia)[x]) == cat )))}

	\asegura{ (\forall comp \leftarrow todasLasCompetencias(j), categoria(comp) == cat)
		\newline (\forall( atl \leftarrow participantes(comp)) nacionalidad (atl) \neq p}

	\asegura{ mismos (participantes(competenciaFiltrada(j,cat)), \newline[x | x \leftarrow participantes(competenciaFiltrada(pre(j),cat)), nacionalidad(x) \neq p])}
	\asegura{ res == |[x | comp \leftarrow todasLasCompetencias(pre(j)),\newline x \leftarrow participantes(comp), (categoria(comp) == cat \wedge nacionalidad(x) == p)]|}
	\aux{todasLasCompetencias}{j:JJOO}{[competencia]}{[x | y \leftarrow [1..cantDIas(j)], x \leftarrow cronogramas(j,y) ] }
	\aux{competenciaFiltrada}{j:JJOO, c:(deporte,sexo)}{competencia}{\newline cab( [x | x \leftarrow todasLasCompetencias(j), c== categoria(x) ] )}
\end{problema}



\begin{problema}{losMasFracasados}{j: JJOO, p: Pais}{[Atleta]}
	%Fixed by martu
	\asegura{noGanaronMedallas: (\forall x \leftarrow [noGanoMedallas(atl, comp)\newline
		| atl \leftarrow result, comp \leftarrow todasLasCompetencias(j), finalizada(comp)]) x}
	\asegura{todosDelPais: (\forall x \leftarrow result) nacionalidad(x) == p}
	\asegura{(\forall x \leftarrow result, y \leftarrow atletas(j), nacionalidad(y)==p)\newline
		competenciasEnLasQueParticipo(j, x) >= competenciasEnLasQueParticipo(j, y)}
	\aux{competenciasEnLasQueParticipo}{j: JJOO, a:Atleta}{\ent}{\newline
		long([z | z\leftarrow todasLasCompetencias(j), en(a, participantes(z))])}
	\aux{noGanoMedallas}{atl: Atleta, comp: Competencia}{Bool}{\newline
	ciaNumber(ranking(comp)[0]) \neq ciaNumber(atl) \wedge ciaNumber(ranking(comp)[1]) \neq ciaNumber(atl)\newline
	\wedge ciaNumber(ranking(comp)[2]) \neq ciaNumber(atl)}
\end{problema}

\begin{problema}{liuSong}{j: JJOO, a: Atleta, p: Pa\'is}{}
	\requiere{a \in atletas(j)}
	\modifica{j}
	\asegura{ano(j)==ano(pre(j))}
	\asegura{(\forall i  \leftarrow  [0..|atletas(pre(j))|-1], atletas(pre(j))_i!= a)
		atletas(pre(j))_i==atletas(j)_i}

	\asegura{(\forall x  \leftarrow atletas(j), ciaNumber(x)==ciaNumber(a))
	(nombre(x)==nombre(a) \wedge sexo(x)==sexo(a) \wedge anoNacimiento(x)==anoNacimiento(a) \wedge nacionalidad(x)==p \wedge deportes(x)==deportes(a) \wedge capacidad(x)==capacidad(a))}

	\asegura{cantDias(j)==cantDias(pre(j))}
	\asegura{jornadaActual(j)==jornadaActual(pre(j))}

	\asegura{(\forall d  \leftarrow  [1..cantDias(j)])\newline
	|cronograma(d,j)|==|cronograma(d,pre(j))| \wedge \newline
	(\forall i  \leftarrow  [0..|cronograma(d,j)|-1] )\newline
	categoria(cronograma(d,j)[i])==categoria(cronograma(d,pre(j))[i]) \wedge
		finalizada(cronograma(d,j)[i])==finalizada(cronograma(d,pre(j))[i])}

	\asegura{todosIgualesMenosLiuSong(partComp(j), $part$Comp(pre(j)))}
	\asegura{todoIgualMenosNacionalidad(partComp(j))}

	%-> Hay que ver que todos los atletas del ranking de cada competencia sean iguales menos el modificado.

	\asegura{todosIgualesMenosLiuSong(rankComp(j), $rank$Comp(pre(j)))}
	\asegura{todoIgualMenosNacionalidad(rankComp(j))}

	%-> Hay que ver que todos los atletas de lesTocoControlAntidopping de cada competencia sean iguales menos el modificado.

	\asegura{todosIgualesMenosLiuSong(doppComp(j), $dopp$Comp(pre(j)))}
	\asegura{todoIgualMenosNacionalidad(doppComp(j))}

	%-> Hay que ver que el valor antidopping para cada atleta no haya cambiado.

	\asegura{\forall(dia  \leftarrow  [1..jornadaActual(j)], comp  \leftarrow  [0..|cronograma(j, dia)-1|], finalizada(cronograma(j, dia)))
		leDioPositivo(cronograma(j, dia)[comp], atl) == leDioPositivo(cronograma(pre(j), dia)[comp], atl)}

	\aux{rankComp}{j: JJOO}{[Atleta]}{
	= [atl | dia  \leftarrow  [1..cantDias(j)], comp  \leftarrow  cronograma(j, dia), atl  \leftarrow  ranking(comp), finalizada(comp)]}
	%-> Hay que ver que todos los participantes de cada competencia sean iguales menos el modificado.
	\aux{doppComp}{j: JJOO}{[Atleta]}{
	= [atl | dia  \leftarrow  [1..cantDias(j)], comp  \leftarrow  cronograma(j, dia), atl  \leftarrow  lesTocoControlAntiDopping(comp), finalizada(comp)]}

	\aux{partComp}{j: JJOO}{[Atleta]}{
	[atl | dia  \leftarrow  [1..cantDias(j)], comp  \leftarrow  cronograma(j, dia), atl  \leftarrow  participantes(comp)]}

	\aux{todosIgualesMenosLiuSong}{ls : [Atleta], lsOld : [Atleta]}{Bool}{
		\forall(x  \leftarrow  [0..|ls|-1])\newline
	(ls[x]==lsOld[x]  \vee  ciaNumber(ls)==ciaNumber(a))}

	\aux{todoIgualMenosNacionalidad}{ls: [Atleta]}{Bool}{
	\forall(x  \leftarrow  ls, ciaNumber(x) == ciaNumber(a))\newline
	(nombre(x)==nombre(a) \wedge sexo(x)==sexo(a) \wedge anoNacimiento(x)==anoNacimiento(a) \wedge nacionalidad(x)==p \wedge deportes(x)==deportes(a) \wedge capacidad(x)==capacidad(a))}

\end{problema}

\begin{problema}{stevenBradbury}{j: JJOO}{Atleta}
	//Requiere que al menos una competencia ya haya finalizado (y, por lo tanto, se haya entregado un oro)\newline
	\requiere{algunOro: long([comp | comp \leftarrow todasLasCompetencias(j), finalizada(comp)\wedge|ranking(comp)|>0])>0}

	//Asegura que result haya ganado un oro\newline
	\asegura{ganoOro: existe(f \leftarrow [ranking(comp)[0] | comp \leftarrow todasLasCompetencias(j), finalizada(comp)\wedge|ranking(comp)|>0]) ciaNumber(result)==ciaNumber(f)}

	//Asegura que entre todos los ganadores de oro, el result es el que tiene la menor habilidad en alguna de las medallas que gano.\newline
	\asegura{esElPeor: existe(dep \leftarrow deportesEnLosQueGano(j, result)) paraTodo(f \leftarrow [ranking(comp)[0] | comp \leftarrow todasLasCompetencias(j), finalizada(comp)\wedge|ranking(comp)|>0]) capacidad(result, dep) <= capacidad(f, prm(categoria(comp))}

	\aux{deportesEnLosQueGanoOro}{j: JJOO, a: Atleta}{[Deportes]}
		{[prm(categoria(comp)) | comp \leftarrow todasLasCompetencias(j), finalizada(comp)\wedge|ranking(comp)|>0 \wedge ciaNumber(ranking(comp)[0])==ciaNumber(a)]}
\end{problema}

\begin{problema}{uyOrdenadoAs\'iHayUnPatr\'on}{j: JJOO}{\bool}
\end{problema}


\begin{problema}{sequ\'iaOl\'impica}{j: JJOO}{[Pa\'is]}

   \asegura{ (\forall p \leftarrow result) sequiaPais(j,p) == maximaSequia(j)}
   \asegura{ (\forall p \leftarrow listaPaisesConSequia(j), sequiaPais(j,p)==maximaSequia(j)) p \in result }

   \aux{sequiaPais}{j:JJOO, p:pais}{\ent}
	{\newline cerosSeguidos([ ganoEnElDia(j,dia,p) | dia \leftarrow [1..cantDias(j)] ])}

   \aux{ganoEnElDia}{j: JJOO, dia: \ent,pais: Pais}{Bool}
       {\newline|[ 1 | c \leftarrow cronograma(j, dia), en(pais, paisesQueGanaronCompetencia(c)) ]|>0}

   \aux{listaPaisesConSequia}{j: JJOO}{[(Pais, Int)]}
       {[(p, sequiaPais(j,p)) | p \leftarrow listaPaises(j)]}

   \aux{maximaSequia}{j: JJOO}{\ent}
       {maximoLista([ sequiaPais(j,p) | p \leftarrow listaPaises(j)])}

   \aux{paisesQueGanaronCompetencia}{c:Competencia}{[paises]}
       {\newline [ pais(ranking(c)[a]) | a  \leftarrow [0.. |ranking(c) |-1 ], a <= 2 ]}

	\aux{generoTodosLosParesCeroComaUno}{ls:[Bool]}{[(\ent,\ent)]}
	{\newline[ (c,c1) | c \leftarrow [0..|ls|-1], c1 \leftarrow [c.. |ls|-1], ls[c]==False \wedge ls[c1]==True ]}

	\aux{uniqPrmLista}{ls:[(\ent,\ent)]}{[(\ent,\ent)]}
		{\newline [ ls(i) | i \leftarrow [0..|ls|-1], j\leftarrow [0..|ls|-1], i \neq j, prm(ls[i]) \neq prm(ls[j]) ]}

	\aux{uniqSgdLista}{ls:[(\ent,\ent)]}{[(\ent,\ent)]}
		{\newline [ ls(i) | i \leftarrow [0..|ls|-1], j\leftarrow [0..|ls|-1], i \neq j, sgd(ls[i]) \neq sgd(ls[j]) ]}

	\aux{diferenciaPrmSgd}{ls:[(\ent,\ent)]}{[\ent]}
		{[ sgd(el) - prm(el) | el \leftarrow ls]}
	
	\aux{cerosSeguidos}{ls:[Bool]}{\ent}
		{\newline max(diferenciaPrmSgd(uniqSgdLista(uniqPrmLista(generoTodosLosParesCeroComaUno(ls)))))}
\end{problema}

\begin{problema}{transcurrirDia}{j: JJOO}{}
	%Fixed by martu
	\modifica{j}
	\asegura{cantDias(j) == cantDias(pre(j))}
	\asegura{jornadaActual(j) == jornadaActual(pre(j))+1}
	\asegura{a\tilde{n}o (j) == a\tilde{n}o(pre(j))}
	\asegura{mismos(atletas(j),atletas(pre(j)))}
	\asegura{(\forall dia \leftarrow [1..jornadaActual(j))-1])\newline mismos(cronograma(j,dia), cronograma(pre(j),dia))}
	\asegura{|cronograma(j,jornadaActual(j))|==|cronograma(pre(j),jornadaActual(j))|}
	\asegura{(\forall i \leftarrow [0, |cronograma(j, jornadaActual(j))|-1])\newline
		categoria(cronograma(j,jornadaActual(j))[i]) == categoria(cronograma(pre(j),jornadaActual(j))[i])}
	\asegura{(\forall i \leftarrow [0, |cronograma(j, jornadaActual(j))| -1])\newline
		mismos(participantes(cronograma(j,jornadaActual(j))[i]),\newline
		participantes(cronograma(pre(j),jornadaActual(j))[i]))}
	\asegura{(\forall c \leftarrow cronograma(j, jornadaActual(j)))\newline
		finalizada(c) == True \wedge incluida(ranking(c), participantes(c))\newline
		\wedge (\forall x \leftarrow [0..|ranking(c)|-2]) capacidadEnOrden(x,c)}
	\asegura{asegura (\forall c \leftarrow cronograma(j, jornadaActual(j)))\newline
		(|lesTocoControlAntiDoping(c)|==1 \wedge lesTocoControlAntiDoping(c)[0] \in atletas(c))\newline
		\vee (|lesTocoControlAntiDoping(c)|==0 \wedge |atletas(c)| == 0)}

	\asegura{(\forall c \leftarrow cronograma(j, jornadaActual(j)))\newline
		|listaDoping(c,atletas(c))|*20 \leq \newline \sum([long(lesTocoControlAntiDoping(comp))
		| comp \leftarrow cronograma(j,jornadaActual(j))])}
	\aux{capacidadEnOrden}{x: \ent, c:Competencia}{Bool}{\newline
	capacidad(ranking(c)[x], prm(categoria(c))) \geq capacidad(ranking(c)[x + 1], prm(categoria(c)))}
	\aux{listaDoping}{c:Competencia, a:[Atleta]}{[Atleta]}{[x|x \leftarrow a, leDioPositivo(c, x)]}
\end{problema}

\section{Auxiliares}

\input{auxiliaresTipos.tex}

\end{document}