|
|
@@ -176,67 +176,58 @@
|
|
|
\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.
|
|
|
-
|
|
|
+ \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{todosIgualesMenosLiuSong(rankComp(j), $rank$Comp(pre(j)))}
|
|
|
-\asegura{todoIgualMenosNacionalidad(rankComp(j))}
|
|
|
+ \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))}
|
|
|
|
|
|
-%-> Hay que ver que todos los atletas de lesTocoControlAntidopping de cada competencia sean iguales menos el modificado.
|
|
|
+ \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(doppComp(j), $dopp$Comp(pre(j)))}
|
|
|
-\asegura{todoIgualMenosNacionalidad(doppComp(j))}
|
|
|
+ \asegura{todosIgualesMenosLiuSong(partComp(j), $part$Comp(pre(j)))}
|
|
|
+ \asegura{todoIgualMenosNacionalidad(partComp(j))}
|
|
|
|
|
|
-%-> Hay que ver que el valor antidopping para cada atleta no haya cambiado.
|
|
|
+ %-> Hay que ver que todos los atletas del ranking de cada competencia sean iguales menos el modificado.
|
|
|
|
|
|
-\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)}
|
|
|
+ \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.
|
|
|
|
|
|
-\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)]}
|
|
|
+ \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.
|
|
|
|
|
|
-\aux{partComp}{j: JJOO}{[Atleta]}{
|
|
|
-[atl | dia \leftarrow [1..cantDias(j)], comp \leftarrow cronograma(j, dia), atl \leftarrow participantes(comp)]}
|
|
|
+ \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{todosIgualesMenosLiuSong}{ls : [Atleta], lsOld : [Atleta]}{Bool}{
|
|
|
- \forall(x \leftarrow [0..|ls|-1])\newline
|
|
|
-(ls[x]==lsOld[x] \vee ciaNumber(ls)==ciaNumber(a))}
|
|
|
+ \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{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))}
|
|
|
+ \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}
|
|
|
|
|
|
@@ -313,7 +304,8 @@ categoria(cronograma(d,j)[i])==categoria(cronograma(d,pre(j))[i]) \wedge
|
|
|
\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]),participantes(cronograma(pre(j),jornadaActual(j))[i]))}
|
|
|
+ mismos(participantes(cronograma(j,jornadaActual(j))[i]),\newline
|
|
|
+ participantes(cronograma(pre(j),jornadaActual(j))[i]))}
|
|
|
|
|
|
%Esta no compila
|
|
|
\asegura{(\forall c \leftarrow cronograma(j, jornadaActual(j)))\newline
|
|
|
@@ -325,7 +317,8 @@ categoria(cronograma(d,j)[i])==categoria(cronograma(d,pre(j))[i]) \wedge
|
|
|
\vee (|lesTocoControlAntiDoping(c)|==0 \wedge |atletas(c)| == 0)}
|
|
|
|
|
|
\asegura{(\forall c \leftarrow cronograma(j, jornadaActual(j)))\newline
|
|
|
- |listaDoping(c,atletas(c))|*20 \leq \sum([|lesTocoControlAntiDoping(comp)| | comp \leftarrow cronograma(j,jornadaActual(j))])}
|
|
|
+ |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)))}
|
Martu