|
|
@@ -119,12 +119,29 @@
|
|
|
\end{problema}
|
|
|
|
|
|
\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]) \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
|
|
|
+ // 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))}
|
|
|
@@ -134,17 +151,17 @@
|
|
|
\asegura{(\forall dia \leftarrow [1..cantDias (j)] ) \newline
|
|
|
|cronograma(j,dia) | == |cronograma(pre(j), dia)|}
|
|
|
|
|
|
- \asegura{ (\forall dia \leftarrow [1..cantDias(j)]) \newline
|
|
|
+ \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]) \vee ( categoria(cronograma(j,dia)[x]) == (categoria(cronograma(pre(j),dia)[x])) \wedge (categoria(cronograma(j,dia)[x]) == cat )))}
|
|
|
+ ((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)
|
|
|
- (\forall( atl \leftarrow participantes(comp)) nacionalidad (atl) \neq p}
|
|
|
+ \newline (\forall( atl \leftarrow participantes(comp)) nacionalidad (atl) \neq p}
|
|
|
|
|
|
- \asegura{ mismos (participantes(competenciaFiltrada(j,cat)), [x | x \leftarrow participantes(competenciaFiltrada(pre(j),cat)), nacionalidad(x) \neq p])}
|
|
|
- \asegura{ res == |[x | comp \leftarrow todasLasCompetencias(pre(j)), x \leftarrow participantes(comp), (categoria(comp) == cat \wedge nacionalidad(x) == 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}{cab( [x | x \leftarrow todasLasCompetencias(j), c== categoria(x) ] )}
|
|
|
+ \aux{competenciaFiltrada}{j:JJOO, c:(deporte,sexo)}{competencia}{\newline cab( [x | x \leftarrow todasLasCompetencias(j), c== categoria(x) ] )}
|
|
|
\end{problema}
|
|
|
|
|
|
|