|
|
@@ -43,7 +43,7 @@
|
|
|
|
|
|
\begin{problema}{entrenarNuevoDeporte}{a: Atleta, d: Deporte, c: \ent}{}
|
|
|
\requiere{c \geq 0 \wedge c \leq 100}
|
|
|
- \requiere{\neg (a(d,deporte(a)))}
|
|
|
+ \requiere{d \notin deportes(a)}
|
|
|
\modifica{a}
|
|
|
\asegura{mismos(deportes(a),deportes(pre(a)))}
|
|
|
\asegura{ordenada(deportes(a))}
|
|
|
@@ -58,6 +58,7 @@
|
|
|
|
|
|
\begin{problema}{finalizarCompetencia}{c: Competencia, posiciones: [Atleta], control: [(Atleta, \bool)]}{}
|
|
|
%definir mismos en Auxiliares
|
|
|
+ \requiere{\neg finalizada(c)}
|
|
|
\requiere{contenida(posiciones,participantes(c))}
|
|
|
\requiere{sinRepetidos(posiciones)}
|
|
|
\requiere{(\forall x \leftarrow control) prm(x) \in participantes(c)}
|
|
|
@@ -65,7 +66,7 @@
|
|
|
\asegura{finalizada(c)}
|
|
|
\asegura{ranking(c)==posiciones}
|
|
|
\asegura{participantes(c)==participantes(pre(c))}
|
|
|
- \asegura{LesTocoControlAntiDOpping(c)== [prm(x) | x \leftarrow control]}
|
|
|
+ \asegura{LesTocoControlAntiDopping(c)== [prm(x) | x \leftarrow control]}
|
|
|
\asegura{(\forall x \leftarrow control) leDioPositivo(prm(x))==sgn(x)}
|
|
|
\asegura{categoria(c)==categoria(pre(c))}
|
|
|
\end{problema}
|
|
|
@@ -81,21 +82,21 @@
|
|
|
|
|
|
\begin{problema}{gananLosMasCapaces}{c: Competencia}{\bool}
|
|
|
\requiere{finalizada(c)}
|
|
|
- \asegura{result==(\forall x \leftarrow[0..|ranking(c)|-2])capacidad(ranking(c)[x],deporte) \geq capacidad(ranking(c)[x+1],deporte)}
|
|
|
- Nota deporte=fem(categoria(c)) ?? no entiendo la letra
|
|
|
+ \asegura{result==(\forall x \leftarrow[0..|ranking(c)|-2]) \newline
|
|
|
+ capacidad(ranking(c)[x],prm(categoria(c))) \geq capacidad(ranking(c)[x+1],prm(categoria(c)))}
|
|
|
\end{problema}
|
|
|
|
|
|
\begin{problema}{sancionarTramposos}{c: Competencia}{}
|
|
|
\requiere{finalizada(c)}
|
|
|
- \modifica(c)
|
|
|
+ \modifica{c}
|
|
|
\asegura{finalizada(c)}
|
|
|
\asegura{categoria(c)==categoria(pre(c))}
|
|
|
\asegura{participantes(c)==participantes(pre(c))}
|
|
|
\asegura{incluida(ranking(c),participantes(c))}
|
|
|
- \asegura{incluida(LesTocoControlAntiDOpping(c),participantes(c))}
|
|
|
- \asegura{mismos(ranking(pre(c)),ranking(c)++listaDopping(c,LesTocoControlAntiDOpping(c)))}
|
|
|
- \asegura{ranking=ranking(pre(??))-listaDopping(c,LesTocoControlAntiDOpping(c))}
|
|
|
- \aux{listaDopping}{c:competencia, a:[atleta]}{[atleta]}{[x|x \leftarrow a, DioPositivo(c,x)]}
|
|
|
+ \asegura{incluida(LesTocoControlAntiDopping(c),participantes(c))}
|
|
|
+ \asegura{mismos(ranking(pre(c)),ranking(c)++listaDopping(c,LesTocoControlAntiDopping(c)))}
|
|
|
+ \asegura{ranking==ranking(pre(c))-listaDopping(c,LesTocoControlAntiDopping(c))}
|
|
|
+ \aux{listaDopping}{c:competencia, a:[atleta]}{[atleta]}{[x|x \leftarrow a, leDioPositivo(c,x)]}
|
|
|
|
|
|
\end{problema}
|
|
|
|
|
|
@@ -103,6 +104,10 @@
|
|
|
\input{tipos/jjoo.tex}
|
|
|
|
|
|
\begin{problema}{dePaseo}{j: JJOO}{[Atleta]}
|
|
|
+ \asegura{result==noParticiparon(j)}
|
|
|
+ \aux{noParticiparon}{j: JJOO}{[Atleta]}{[x | x \leftarrow atletas(j), \neg en(x, participaronConRepes(j))]}
|
|
|
+ \aux{participaronConRepes}{j: JJOO}{[Atleta]}{[atl | dia \leftarrow [1..cantDias(j)], comp \leftarrow cronograma(j, dia), atl \leftarrow atletas(j), en(atl, participantes(comp))]}
|
|
|
+
|
|
|
\end{problema}
|
|
|
|
|
|
\begin{problema}{medallero}{j: JJOO}{[(Pais, [\ent])]}
|
