Merge branch 'master' of https://gogs.davidventura.com.ar/david/aed1-tpe

template/templateTP.tex

@@ -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}
 
@@ -199,19 +260,20 @@
 
 \begin{problema}{sequ\'iaOl\'impica}{j: JJOO}{[Pa\'is]}
 
-   \asegura{ (\forall p \leftarrow result) sequiaPais(p) == maximaSequia(j)}
-   \asegura{ (\forall p \leftarrow listaPaisesConSequia(j), sequiaPais(p)==maximaSequia(j)) p \in result }
+   \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}{p:pais}{\ent}{cerosSeguidos([ ganoEnElDia(dia,p) | dia \leftarrow [1..cantDias(j)] ])}
+   \aux{sequiaPais}{j:JJOO, p:pais}{\ent}
+	{\newline cerosSeguidos([ ganoEnElDia(j,dia,p) | dia \leftarrow [1..cantDias(j)] ])}
 
-   \aux{ganoEnElDia}{dia,pais}{Bool}
+   \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(p)) | p \leftarrow listaPaises(j)]}
+       {[(p, sequiaPais(j,p)) | p \leftarrow listaPaises(j)]}
 
    \aux{maximaSequia}{j: JJOO}{\ent}
-       {maximoLista([ sequiaPais(p) | p \leftarrow listaPaises(j)])}
+       {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 ]}