|
|
@@ -8,27 +8,40 @@ parcelasCampo(c:Campo):$[(\ent , \ent)]$= \newline [(x,y) \textbar x $\leftarrow
|
|
|
\subsection{Drone}
|
|
|
|
|
|
% los aux del tipo drone
|
|
|
-$igualdadDrone(d,d':Drone):Bool= id(d)==id(d') \wedge bateria(d)==bateria(d') \wedge enVuelo(d)==enVuelo(d') \wedge vueloRealizado(d)==vueloRealizado(d') \wedge mismos(productosDisponibles(d),productosDisponibles(d'))$
|
|
|
-
|
|
|
+$igualdadDrone(d,d':Drone):Bool= id(d)==id(d') \wedge bateria(d)==bateria(d') \wedge enVuelo(d)==enVuelo(d') \wedge vueloRealizado(d)==vueloRealizado(d') \wedge \newline posicionActual(d)==posicionActual(d') \wedge mismos(productosDisponibles(d),productosDisponibles(d'))$
|
|
|
+\newline
|
|
|
+\newline
|
|
|
+$dronesIgualesSinPosicion(d,d':Drone):Bool= id(d)==id(d') \wedge bateria(d)==bateria(d') \wedge enVuelo(d)==enVuelo(d') \wedge vueloRealizado(d)==vueloRealizado(d') \wedge mismos(productosDisponibles(d),productosDisponibles(d'))$
|
|
|
+\newline
|
|
|
+\newline
|
|
|
mismosDrones(ds,xs:[Drone]):Bool= \textbar ds \textbar == \textbar xs \textbar $ \wedge ( \forall d \leftarrow ds)cantidadAparicionesD(d,ds)==cantidadAperecionesD(d,xs)$
|
|
|
-
|
|
|
+\newline
|
|
|
+\newline
|
|
|
$cantidadAparicionesD(d:Drones,ds:[Drones])=$\textbar $[x $\textbar$ x \leftarrow ds, iguadadDrone(x,d)]$\textbar
|
|
|
%│[x │ x\leftarrow ds, iguadadDrone(x,d)]│$
|
|
|
-
|
|
|
+\newline
|
|
|
+\newline
|
|
|
escalera1(d:Drone):Bool= ($\forall i \leftarrow$ [0..\textbar vueloRealizado(d)\textbar -1) $prm(vueloRealizado(d)_{i}) \leq prm(vueloRealizado(d)_{i+1}$)\newline if \ $prm(vueloRealizado(d)_{i})== prm(vueloRealizado(d)_{i+1}$\ then $snd(vueloRealizado(d)_{i})+1== snd(vueloRealizado(d)_{i+1}$\ else $snd(vueloRealizado(d)_{i})== snd(vueloRealizado(d)_{i+1}$
|
|
|
-
|
|
|
+\newline
|
|
|
+\newline
|
|
|
escalera2(d:Drone):Bool= ($\forall i \leftarrow$ [0..\textbar vueloRealizado(d)\textbar -1) $prm(vueloRealizado(d)_{i}) \geq prm(vueloRealizado(d)_{i+1}$)\newline if \ $prm(vueloRealizado(d)_{i})== prm(vueloRealizado(d)_{i+1}$\ then $snd(vueloRealizado(d)_{i})-1== snd(vueloRealizado(d)_{i+1})$\ else $snd(vueloRealizado(d)_{i})== snd(vueloRealizado(d)_{i+1}$
|
|
|
-
|
|
|
+\newline
|
|
|
+\newline
|
|
|
escalera3(d:Drone):Bool= ($\forall i \leftarrow$ [0..\textbar vueloRealizado(d)\textbar -1) $prm(vueloRealizado(d)_{i}) \leq prm(vueloRealizado(d)_{i+1}$)\newline if \ $prm(vueloRealizado(d)_{i})== prm(vueloRealizado(d)_{i+1}$\ then $snd(vueloRealizado(d)_{i})-1== snd(vueloRealizado(d)_{i+1})$\ else $snd(vueloRealizado(d)_{i})== snd(vueloRealizado(d)_{i+1}$
|
|
|
-
|
|
|
+\newline
|
|
|
+\newline
|
|
|
escalera4(d:Drone):Bool= ($\forall i \leftarrow$ [0..\textbar vueloRealizado(d)\textbar -1) $prm(vueloRealizado(d)_{i}) \geq prm(vueloRealizado(d)_{i+1}$)\newline if \ $prm(vueloRealizado(d)_{i})== prm(vueloRealizado(d)_{i+1}$\ then $snd(vueloRealizado(d)_{i})+1== snd(vueloRealizado(d)_{i+1})$\ else $snd(vueloRealizado(d)_{i})== snd(vueloRealizado(d)_{i+1}$
|
|
|
-
|
|
|
+\newline
|
|
|
+\newline
|
|
|
parcelasConChoques(ds:[Drones]):[(($\ent,\ent),\ent$)]= \newline [(p,cantidadDronesenMomento(p,i,ds))\textbar d $\leftarrow$ ds, i $\leftarrow$ [0..\textbar vueloRealizado \textbar), p $\leftarrow$ vueloRealizado(d), \\ cantidadDronesEnMomento(p,i,ds) $\geq$ 2]
|
|
|
-
|
|
|
+\newline
|
|
|
+\newline
|
|
|
cantidadDronesenMomento($p:(\ent, \ent),i:\ent,ds:[Drones]): \ent$ = \\ \textbar [p \textbar d $\leftarrow$ ds, $vueloRecorrido(d)_{i} $== p] \textbar
|
|
|
-
|
|
|
+\newline
|
|
|
+\newline
|
|
|
quitarRepetidos(xs:[($\ent,\ent),\ent$)])=[$x_{i}$ \textbar i $\leftarrow$ [0.. \textbar xs \textbar), ($\forall$ j $\leftarrow$ [0.. \textbar xs \textbar), i $\leq$ j)$x_{i}$ $\lneq$ $x_{j}$]
|
|
|
-
|
|
|
+\newline
|
|
|
+\newline
|
|
|
estaOrdenadoPorLaSugundaCoordenada(xs:[($\ent,\ent),\ent$)]):Bool = ($\forall$ x $\leftarrow$ xs)($\forall$ i,j $\leftarrow$ [0.. \textbar xs \textbar), i$\leq$j)$snd(x_{i})$ $\leq$ $snd(x_{j})$ $\vee$ $snd(x_{i})$ $\geq$ $snd(x_{j})$
|
|
|
|
|
|
\subsection{Sistema}
|
