|
|
@@ -0,0 +1,61 @@
|
|
|
+problema liuSong (j:JJOO, a:Atleta, p:Pais) {
|
|
|
+
|
|
|
+requiere en(a, atletas(j));
|
|
|
+
|
|
|
+modifica j;
|
|
|
+
|
|
|
+asegura año(j)==año(pre(j));
|
|
|
+asegura(paraTodo i <- [0..|atletas(pre(j))|-1], atletas(pre(j))[i]!= a)
|
|
|
+atletas(pre(j))[i]==atletas(j)[i];
|
|
|
+
|
|
|
+asegura(paraTodo x <-atletas(j), ciaNumber(x)==ciaNumber(a))
|
|
|
+(nombre(x)==nombre(a) && sexo(x)==sexo(a) && añoNacimiento(x)==añoNacimiento(a) && nacionalidad(x)==p && deportes(x)==deportes(a) && capacidad(x)==capacidad(a));
|
|
|
+
|
|
|
+asegura cantDias(j)==cantDias(pre(j));
|
|
|
+asegura jornadaActual(j)==jornadaActual(pre(j));
|
|
|
+
|
|
|
+asegura(paraTodo d <- [1..cantDias(j)])
|
|
|
+|cronograma(d,j)|==|cronograma(d,pre(j))| ^
|
|
|
+(paraTodo i <- [0..|cronograma(d,j)|-1] )
|
|
|
+categoria(cronograma(d,j)[i])==categoria(cronograma(d,pre(j))[i]) ^
|
|
|
+finalizada(cronograma(d,j)[i])==finalizada(cronograma(d,pre(j))[i])
|
|
|
+
|
|
|
+-> Hay que ver que todos los participantes de cada competencia sean iguales menos el modificado.
|
|
|
+
|
|
|
+aux partComp(j: JJOO) : [Atleta]
|
|
|
+= [atl | dia <- [1..cantDias(j)], comp <- cronograma(j, dia), atl <- participantes(comp)];
|
|
|
+
|
|
|
+aux todosIgualesMenosLiuSong(ls : [Atleta], lsOld : [Atleta]) : Bool =
|
|
|
+ paraTodo(x <- [0..|ls|-1])
|
|
|
+(ls[x]==lsOld[x] || ciaNumber(ls)==ciaNumber(a));
|
|
|
+
|
|
|
+aux todoIgualMenosNacionalidad(ls: [Atleta]) : Bool =
|
|
|
+paraTodo(x <- ls, ciaNumber(x) == ciaNumber(a))
|
|
|
+(nombre(x)==nombre(a) && sexo(x)==sexo(a) && añoNacimiento(x)==añoNacimiento(a) && nacionalidad(x)==p && deportes(x)==deportes(a) && capacidad(x)==capacidad(a));
|
|
|
+
|
|
|
+asegura todosIgualesMenosLiuSong(partComp(j), partComp(pre(j)));
|
|
|
+asegura todoIgualMenosNacionalidad(partComp(j));
|
|
|
+
|
|
|
+-> Hay que ver que todos los atletas del ranking de cada competencia sean iguales menos el modificado.
|
|
|
+
|
|
|
+aux rankComp(j: JJOO) : [Atleta]
|
|
|
+= [atl | dia <- [1..cantDias(j)], comp <- cronograma(j, dia), atl <- ranking(comp), finalizada(comp)];
|
|
|
+
|
|
|
+asegura todosIgualesMenosLiuSong(rankComp(j), rankComp(pre(j)));
|
|
|
+asegura todoIgualMenosNacionalidad(rankComp(j));
|
|
|
+
|
|
|
+-> Hay que ver que todos los atletas de lesTocoControlAntidopping de cada competencia sean iguales menos el modificado.
|
|
|
+
|
|
|
+aux doppComp(j: JJOO) : [Atleta]
|
|
|
+= [atl | dia <- [1..cantDias(j)], comp <- cronograma(j, dia), atl <- lesTocoControlAntiDopping(comp), finalizada(comp)];
|
|
|
+
|
|
|
+asegura todosIgualesMenosLiuSong(doppComp(j), doppComp(pre(j)));
|
|
|
+asegura todoIgualMenosNacionalidad(doppComp(j));
|
|
|
+
|
|
|
+-> Hay que ver que el valor antidopping para cada atleta no haya cambiado.
|
|
|
+
|
|
|
+ asegura paraTodo(dia <- [1..jornadaActual(j)], comp <- [0..|cronograma(j, dia)-1|], finalizada(cronograma(j, dia)))
|
|
|
+ leDioPositivo(cronograma(j, dia)[comp], atl) == leDioPositivo(cronograma(pre(j), dia)[comp], atl);
|
|
|
+
|
|
|
+}
|
|
|
+
|
