|
|
@@ -0,0 +1,327 @@
|
|
|
+\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}
|
|
|
+
|
|
|
+%Seen by martu
|
|
|
+\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}
|
|
|
+
|
|
|
+%Seen by martu
|
|
|
+\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}
|
|
|
+
|
|
|
+%Seen by martu
|
|
|
+\begin{problema}{finalizarCompetencia}{c: Competencia, posiciones: [Atleta], control: [(Atleta, \bool)]}{}
|
|
|
+ \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}
|
|
|
+
|
|
|
+%Seen by martu
|
|
|
+\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}
|
|
|
+
|
|
|
+%Fixed by martu
|
|
|
+\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}
|
|
|
+
|
|
|
+%Fixed by martu
|
|
|
+\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}
|
|
|
+
|
|
|
+%Fixed by martu
|
|
|
+\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}{\newline
|
|
|
+ [Atleta]}{[atl | dia \leftarrow [1..cantDias(j)], comp \leftarrow cronograma(j, dia), atl \leftarrow atletas(j), en(atl, participantes(comp))]}
|
|
|
+\end{problema}
|
|
|
+
|
|
|
+%Written by martu
|
|
|
+\begin{problema}{medallero}{j: JJOO}{[(Pais, [\ent])]}
|
|
|
+ \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])\newline
|
|
|
+ \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}
|
|
|
+
|
|
|
+%Fixed by martu
|
|
|
+\begin{problema}{losMasFracasados}{j: JJOO, p: Pais}{[Atleta]}
|
|
|
+ \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}
|
|
|
+
|
|
|
+%Fixed by martu
|
|
|
+\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))\newline
|
|
|
+ (nombre(x)==nombre(a) \wedge sexo(x)==sexo(a) \wedge a\tilde{n}oNacimiento(x)==a\tilde{n}oNacimiento(a)\newline
|
|
|
+ \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)]) |cronograma(d,j)|==|cronograma(d,pre(j))|\newline
|
|
|
+ \wedge (\forall i \leftarrow [0..|cronograma(d,j)|-1] )\newline
|
|
|
+ categoria(cronograma(d,j)[i])==categoria(cronograma(d,pre(j))[i])\newline
|
|
|
+ \wedge finalizada(cronograma(d,j)[i])==finalizada(cronograma(d,pre(j))[i])}
|
|
|
+ \asegura{todosIgualesMenosLiuSong(partComp(j), $part$Comp(pre(j)))}
|
|
|
+ \asegura{todoIgualMenosNacionalidad(partComp(j))}
|
|
|
+ \asegura{todosIgualesMenosLiuSong(rankComp(j), $rank$Comp(pre(j)))}
|
|
|
+ \asegura{todoIgualMenosNacionalidad(rankComp(j))}
|
|
|
+ \asegura{todosIgualesMenosLiuSong(doppComp(j), $dopp$Comp(pre(j)))}
|
|
|
+ \asegura{todoIgualMenosNacionalidad(doppComp(j))}
|
|
|
+ \asegura{\forall(dia \leftarrow [1..jornadaActual(j)], comp \leftarrow [0..|cronograma(j, dia)-1|], finalizada(cronograma(j, dia)))\newline
|
|
|
+ leDioPositivo(cronograma(j, dia)[comp], atl) == leDioPositivo(cronograma(pre(j), dia)[comp], atl)}
|
|
|
+ \aux{rankComp}{j: JJOO}{[Atleta]}{\newline
|
|
|
+ [atl | dia \leftarrow [1..cantDias(j)], comp \leftarrow cronograma(j, dia), atl \leftarrow ranking(comp), finalizada(comp)]}
|
|
|
+ \aux{doppComp}{j: JJOO}{[Atleta]}{\newline
|
|
|
+ [atl | dia \leftarrow [1..cantDias(j)], comp \leftarrow cronograma(j, dia),\newline
|
|
|
+ atl \leftarrow lesTocoControlAntiDopping(comp), finalizada(comp)]}
|
|
|
+ \aux{partComp}{j: JJOO}{[Atleta]}{\newline
|
|
|
+ [atl | dia \leftarrow [1..cantDias(j)], comp \leftarrow cronograma(j, dia), atl \leftarrow participantes(comp)]}
|
|
|
+ \aux{todosIgualesMenosLiuSong}{ls : [Atleta], lsOld : [Atleta]}{Bool}{\newline
|
|
|
+ \forall(x \leftarrow [0..|ls|-1]) (ls[x]==lsOld[x] \vee ciaNumber(ls)==ciaNumber(a))}
|
|
|
+ \aux{todoIgualMenosNacionalidad}{ls: [Atleta]}{Bool}{\newline
|
|
|
+ \forall(x \leftarrow ls, ciaNumber(x) == ciaNumber(a)) (nombre(x)==nombre(a) \wedge sexo(x)==sexo(a)\newline
|
|
|
+ \wedge anoNacimiento(x)==anoNacimiento(a) \wedge nacionalidad(x)==p \wedge deportes(x)==deportes(a)\newline
|
|
|
+ \wedge capacidad(x)==capacidad(a))}
|
|
|
+\end{problema}
|
|
|
+
|
|
|
+%Fixed by martu
|
|
|
+\begin{problema}{stevenBradbury}{j: JJOO}{Atleta}
|
|
|
+ \requiere{algunOro:\newline
|
|
|
+ long([comp | comp \leftarrow todasLasCompetencias(j), finalizada(comp)\wedge|ranking(comp)|>0])>0}
|
|
|
+ \asegura{ganoOro:\newline
|
|
|
+ existe(f \leftarrow [ranking(comp)[0] | comp \leftarrow todasLasCompetencias(j),\newline
|
|
|
+ finalizada(comp)\wedge|ranking(comp)|>0]) ciaNumber(result)==ciaNumber(f)}
|
|
|
+ \asegura{esElPeor:\newline
|
|
|
+ existe(dep \leftarrow deportesEnLosQueGano(j, result))\newline
|
|
|
+ paraTodo(f \leftarrow [ranking(comp)[0] | comp \leftarrow todasLasCompetencias(j),\newline
|
|
|
+ finalizada(comp)\wedge|ranking(comp)|>0]) capacidad(result, dep) <= capacidad(f, prm(categoria(comp))}
|
|
|
+ \aux{deportesEnLosQueGanoOro}{j: JJOO, a: Atleta}{[Deportes]}{\newline
|
|
|
+ [prm(categoria(comp)) | comp \leftarrow todasLasCompetencias(j), finalizada(comp)\newline
|
|
|
+ \wedge|ranking(comp)|>0 \wedge ciaNumber(ranking(comp)[0])==ciaNumber(a)]}
|
|
|
+\end{problema}
|
|
|
+
|
|
|
+\begin{problema}{uyOrdenadoAs\'iHayUnPatr\'on}{j: JJOO}{\bool}
|
|
|
+
|
|
|
+\asegura { res == ifthenelse |mejoresPaises(j)|== |sinRepes(mejoresPaises(j))|, true, \newline ifthenelse (contar(cab(mejoresPaises(j)))==\,1\, \wedge\, |mejoresPaises(j)|>|sinRepes(mejoresPaises(j)))|, false, \newline (\forall i \leftarrow [0..|mejorespaises(j)|-1], k \leftarrow [0..|mejoresPaises(j)|-1], i\,mod \newline |patron(mejoresPaises(j))| == k\,mod |patron(mejoresPaises(j))|) s[i] == s[k]}
|
|
|
+
|
|
|
+
|
|
|
+ \aux{mejoresPaises}{j :JJOO}{[Pais]}{ [ cab(ordenar(masOrosDelDia(j,d) ) \newline | d \leftarrow [1.. jornadaActual(j) - 1], cronograma(j,d) \neq [\;\;], masOrosDelDia(j,d) \neq [\;\;] ]}
|
|
|
+
|
|
|
+ \aux{patron}{(ls: [T])}{[T]}{\newline ifthenelse(|ls|==1, ls, sub(ls, 0, min ( [ i | i \leftarrow [1..|ls|-1], ls[i] == ls[0] ] ) )}
|
|
|
+
|
|
|
+
|
|
|
+ \aux{masOrosDelDia}{j:JJOO, d: dia}{[Pais]}{\newline filtrarTuplaPorPrmMax(j, uniqSgdLista( tuplasMedallOroComaPais(j,d) ), d)}
|
|
|
+
|
|
|
+ \aux{tuplasMedallaOroComaPais}{j : JJOO, d: Dia}{[(\ent, Pais)]}{\newline [( contar(pais,PaisesConOroTalDia(j,d)), p ) | p \leftarrow paisesConOroTalDia(j,d) ]}
|
|
|
+
|
|
|
+ \aux{paisesConOroTalDia}{j:JJOO, d: Dia}{[Pais]}{\newline [pais(cab(ranking(c)) | c \leftarrow cronograma (j,d), finalizada(c) \wedge |ranking(c)|>0 ]}
|
|
|
+
|
|
|
+ \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{filtrarTuplaPorPrmMax}{j:JJOO, ls:[(\ent,Pais)], d:Dia}{[Pais]}{\newline [sgd(tupla) | tupla \leftarrow tuplasMedallaOroComaPais(j,d), prm(tupla) \geq \newline maxListaTuplas(tuplasMedallaOroComaPais(j,d))]}
|
|
|
+
|
|
|
+ \aux{maxListaTuplas}{ ls: [(ent, Pais)]}{\ent}{max([ prm(tupla) | tupla \leftarrow ls ])}
|
|
|
+
|
|
|
+
|
|
|
+
|
|
|
+\end{problema}
|
|
|
+
|
|
|
+%Fixed by martu
|
|
|
+\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
|
|
|
+ long([ 1 | c \leftarrow cronograma(j, dia), en(pais, paisesQueGanaronCompetencia(c)) ])>0}
|
|
|
+ \aux{listaPaisesConSequia}{j: JJOO}{[(Pais, Int)]}{\newline
|
|
|
+ [(p, sequiaPais(j,p)) | p \leftarrow listaPaises(j)]}
|
|
|
+ \aux{maximaSequia}{j: JJOO}{\ent}{\newline
|
|
|
+ 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}
|
|
|
+
|
|
|
+%Fixed by martu
|
|
|
+\begin{problema}{transcurrirDia}{j: JJOO}{}
|
|
|
+ \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}
|
|
|
+
|
pepi