| 12345678910111213141516171819202122232425262728293031323334353637383940414243444546474849505152 |
- problema transcurrirDia(j:JJOO) {
-
- //Modificar:
- // * Resultados (AKA Ranking) de la competencias ( dados por capacidades )
- // * Realizar antidoping a un atleta de cada competencia (al azar)
- // * El control antidoping le da positivo a lo sumo a 5% de los controles
- modifica j;
- asegura jornadaActual(j) \in [jornadaActual(pre(j))+1,cantDias(pre(j))]
- asegura año (j) == año(pre(j));
- asegura mismos(atletas(j),atletas(pre(j)));
- asegura cantDias(j)==cantDias(pre(j));
-
- asegura (\forall dia <- [1..jornadaActual(j))-1] )
- mismos(cronograma(j,dia), cronograma(pre(j),dia));
- asegura |cronograma(j,jornadaActual(j))|==|cronograma(pre(j),jornadaActual(j))|
- -- Cambian las competencias de jornadaActual
- asegura (\forall i <- [0, |cronograma(j, jornadaActual(j))| -1])
- categoria(cronograma(j,jornadaActual(j))[i]) ==
- categoria(cronograma(pre(j),jornadaActual(j))[i])
- asegura (\forall i <- [0, |cronograma(j, jornadaActual(j))| -1])
- mismos(
- participantes(cronograma(j,jornadaActual(j))[i]),
- participantes(cronograma(pre(j),jornadaActual(j))[i]))
- asegura (\forall c <- cronograma(j, jornadaActual(j)))
- finalizada(c)==True \wedge
- mismos(ranking(c), participantes(c)) \wedge
- (∀x ← [0..|ranking(c)| − 2])
- capacidadEnOrden(x,c)
- asegura (\forall c <-cronograma(j, jornadaActual(j)))
- ( |lesTocoControlAntiDoping(c)|==1 \wedge lesTocoControlAntiDoping(c)[0] \in atletas(c)) \vee
- |lesTocoControlAntiDoping(c)|==0
- asegura (\forall c <-cronograma(j, jornadaActual(j)))
- |listaDoping(c,atletas(c))|*20 <=
- sum( [ |lesTocoControlAntiDoping(comp)| | comp <- cronograma(j,jornadaActual(j))])
- aux capacidadEnOrden(x: ent, c:competencia) : Bool =
- capacidad(ranking(c)[x], prm(categoria(c))) ≥ capacidad(ranking(c)[x + 1], prm(categoria(c)));
- aux listaDoping (c:competencia, a:[atleta]) : [atleta] =
- [x|x ← a, leDioPositivo(c, x)] ;
- }
|
