|
|
@@ -34,6 +34,7 @@
|
|
|
\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))}
|
|
|
@@ -41,6 +42,7 @@
|
|
|
\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)}
|
|
|
@@ -58,13 +60,12 @@
|
|
|
\end{problema}
|
|
|
|
|
|
|
|
|
-
|
|
|
\section{Competencia}
|
|
|
|
|
|
\input{tipos/competencia.tex}
|
|
|
|
|
|
+%Seen by martu
|
|
|
\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)}
|
|
|
@@ -79,6 +80,7 @@
|
|
|
\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)}
|
|
|
@@ -88,12 +90,14 @@
|
|
|
\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)))}
|
|
|
+ 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}
|
|
|
@@ -102,24 +106,24 @@
|
|
|
\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)]}
|
|
|
-
|
|
|
+ \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}{[Atleta]}{[atl | dia \leftarrow [1..cantDias(j)], comp \leftarrow cronograma(j, dia), atl \leftarrow atletas(j), en(atl, participantes(comp))]}
|
|
|
+ \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])]}
|
|
|
- %Written by martu
|
|
|
\asegura{mismos(result, sacarSinMedallas(crearMedallero(j)))}
|
|
|
\asegura{medalleroOrdenado(result)}
|
|
|
\aux{listaNacionalidadesAtletas}{j: JJOO}{[Pais]}{[nacionalidad(at) | at \leftarrow atletas(j)]}
|
|
|
@@ -136,7 +140,8 @@
|
|
|
\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])))}
|
|
|
+ \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}
|
|
|
@@ -165,10 +170,8 @@
|
|
|
\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]}
|
|
|
- %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}
|
|
|
@@ -177,12 +180,12 @@
|
|
|
\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
|
|
|
+ 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}{}
|
|
|
- %Fixed by martu
|
|
|
\requiere{a \in atletas(j)}
|
|
|
\modifica{j}
|
|
|
\asegura{ano(j)==ano(pre(j))}
|
|
|
@@ -209,7 +212,7 @@
|
|
|
[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)]}
|
|
|
+ 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
|
|
|
@@ -220,62 +223,52 @@
|
|
|
\wedge capacidad(x)==capacidad(a))}
|
|
|
\end{problema}
|
|
|
|
|
|
+%Fixed by martu
|
|
|
\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)]}
|
|
|
+ \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}
|
|
|
\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|[ 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)))))}
|
|
|
+ \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}{}
|
|
|
- %Fixed by martu
|
|
|
\modifica{j}
|
|
|
\asegura{cantDias(j) == cantDias(pre(j))}
|
|
|
\asegura{jornadaActual(j) == jornadaActual(pre(j))+1}
|