|
|
@@ -176,6 +176,67 @@
|
|
|
\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}
|
|
|
|
