|
|
@@ -3,7 +3,7 @@
|
|
|
\asegura {mismos(productosDisponibles(res),pd)}
|
|
|
\asegura {bateria(res)==100}
|
|
|
\asegura {enVuelo==False}
|
|
|
-% \asegura {vuelosRealizados(res)==[]}
|
|
|
+ \asegura {|vuelosRealizados(res)|==0}
|
|
|
\end{problema}
|
|
|
|
|
|
\begin{problema}{idD}{d: Drone}{\ent}
|
|
|
@@ -19,7 +19,7 @@
|
|
|
\end{problema}
|
|
|
|
|
|
\begin{problema}{vueloRealizadoD}{d: Drone}{[(\ent, \ent)]}
|
|
|
- \asegura{res==vueloRealizado(d)}
|
|
|
+ \asegura{mismos(res,vueloRealizado(d))}
|
|
|
\end{problema}
|
|
|
|
|
|
\begin{problema}{posicionActualD}{d: Drone}{(\ent, \ent)}
|
|
|
@@ -35,8 +35,9 @@
|
|
|
\end{problema}
|
|
|
|
|
|
\begin{problema}{vuelosCruzadosD}{ds: [Drone]}{[$((\ent, \ent), \ent)]$}
|
|
|
+ \requiere{|ds| > 0 }
|
|
|
\requiere{(\forall d \leftarrow ds)\mid VueloRealizado(d) \mid == \mid VueloRealizado(d)_{0} \mid}
|
|
|
\asegura{\mid res \mid == \mid quitarRepetidos(parcelasConChoques(ds)) \mid}
|
|
|
\asegura{estaOrdenadoPorLaSugundaCoordenada(res)}
|
|
|
\asegura{(\forall e \leftarrow parcelasConChoques(ds))e \in res }
|
|
|
-\end{problema}
|
|
|
+\end{problema}
|
