|
|
@@ -0,0 +1,28 @@
|
|
|
+problema boicotPorDisciplna (j:JJOO, cat: (deporte,sexo), p:pais) = res : Int {
|
|
|
+
|
|
|
+ requiere finalizada (j) == false // asumimos que se saca a los participantes antes de finalizar la competencia
|
|
|
+
|
|
|
+
|
|
|
+ modifica j;
|
|
|
+
|
|
|
+ asegura finalizada ( competenciaFiltrada(j,cat) ) == finalizada ( competenciaFiltrada(pre(j),cat) );
|
|
|
+ asegura año(j) == año(pre(j));
|
|
|
+ asegura atletas(j) == atletas(pre(j));
|
|
|
+ asegura cantDIas(j) == cantDias(pre(j));
|
|
|
+ asegura jornadaActual(j)== jordnadaActual(pre(j));
|
|
|
+
|
|
|
+
|
|
|
+ asegura (ParaTodo dia <- [1..cantDias (j)] ) |cronograma(j,dia) | == |cronograma( pre(j), dia)|;
|
|
|
+
|
|
|
+ asegura (ParaTodo dia <- [1..cantDias(j)]) (ParaTodo x <- [1..(long(cronograma(j,dia))-1)]) ( (cronograma (j,dia)[x] == cronograma (pre(j),dia) [x]) O ( categoria(cronograma(j,dia)[x]) == (categoria(cronograma(pre(j),dia)[x]) ) Y (categoria(cronograma(j,dia)[x]) == cat ))
|
|
|
+
|
|
|
+ asegura ( ParaToda comp <- todasLasCompetencias(j), (prm(categoria(comp)) == prm(cat) ^ sgd(categoria(comp)) == seg(cat)) )(ParaTodo atl <- participantes(comp)) nacionalidad (atl) != p;
|
|
|
+
|
|
|
+ aegura mismos ( competenciaFiltrada(j,cat), [x| x <-participantes(competenciaFiltrada( pre(j),cat)), nacionalidad(x) != p] )
|
|
|
+
|
|
|
+ asegura res == | [x | c <- todasLasCompetencias(j), x <- participantes(c), (prm(categoria(comp)) == prm(cat) ^ sgd(categoria(comp)) == seg(cat)),nacionalidad(x) == p ] |;
|
|
|
+
|
|
|
+ aux todasLasCompetencias (j:JJOO) : [competencia] = [x | y <- [1..cantDIas(j)], x <- cronogramas(j,y) ] ;
|
|
|
+
|
|
|
+ aux competenciaFiltrada ( j:JJOO, c:(deporte,sexo) ) : competencia = cab( [x | x <- todasLasCompetencias(j), c== categoria(x) ] )
|
|
|
+}
|