David 10 år sedan
förälder
incheckning
48b0430297
1 ändrade filer med 52 tillägg och 0 borttagningar
  1. 52 0
      textoPlano/punto 15

+ 52 - 0
textoPlano/punto 15

@@ -0,0 +1,52 @@
+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)] ;
+}