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)] ; }