|
|
@@ -199,19 +199,20 @@
|
|
|
|
|
|
\begin{problema}{sequ\'iaOl\'impica}{j: JJOO}{[Pa\'is]}
|
|
|
|
|
|
- \asegura{ (\forall p \leftarrow result) sequiaPais(p) == maximaSequia(j)}
|
|
|
- \asegura{ (\forall p \leftarrow listaPaisesConSequia(j), sequiaPais(p)==maximaSequia(j)) p \in result }
|
|
|
+ \asegura{ (\forall p \leftarrow result) sequiaPais(j,p) == maximaSequia(j)}
|
|
|
+ \asegura{ (\forall p \leftarrow listaPaisesConSequia(j), sequiaPais(j,p)==maximaSequia(j)) p \in result }
|
|
|
|
|
|
- \aux{sequiaPais}{p:pais}{\ent}{cerosSeguidos([ ganoEnElDia(dia,p) | dia \leftarrow [1..cantDias(j)] ])}
|
|
|
+ \aux{sequiaPais}{j:JJOO, p:pais}{\ent}
|
|
|
+ {\newline cerosSeguidos([ ganoEnElDia(j,dia,p) | dia \leftarrow [1..cantDias(j)] ])}
|
|
|
|
|
|
- \aux{ganoEnElDia}{dia,pais}{Bool}
|
|
|
+ \aux{ganoEnElDia}{j: JJOO, dia: \ent,pais: Pais}{Bool}
|
|
|
{\newline|[ 1 | c \leftarrow cronograma(j, dia), en(pais, paisesQueGanaronCompetencia(c)) ]|>0}
|
|
|
|
|
|
\aux{listaPaisesConSequia}{j: JJOO}{[(Pais, Int)]}
|
|
|
- {[(p, sequiaPais(p)) | p \leftarrow listaPaises(j)]}
|
|
|
+ {[(p, sequiaPais(j,p)) | p \leftarrow listaPaises(j)]}
|
|
|
|
|
|
\aux{maximaSequia}{j: JJOO}{\ent}
|
|
|
- {maximoLista([ sequiaPais(p) | p \leftarrow listaPaises(j)])}
|
|
|
+ {maximoLista([ sequiaPais(j,p) | p \leftarrow listaPaises(j)])}
|
|
|
|
|
|
\aux{paisesQueGanaronCompetencia}{c:Competencia}{[paises]}
|
|
|
{\newline [ pais(ranking(c)[a]) | a \leftarrow [0.. |ranking(c) |-1 ], a <= 2 ]}
|