|
|
@@ -72,11 +72,18 @@
|
|
|
\end{problema}
|
|
|
|
|
|
\begin{problema}{aterrizarYCargarBateriaS}{s: Sistema, b: \ent}{}
|
|
|
-
|
|
|
+ \modifica s
|
|
|
+ \asegura{igualdadCampo(campo(pre(s)),campo(s))}
|
|
|
+ \asegura{(\forall(i,j) \leftarrow parcelasDelSistema(s),contenido(campo(s),i,j)==Cultivo)\newline estadoDelCultivo(pre(s),i,j)==estadoDelCultivo(s,i,j)}
|
|
|
+ \asegura{ (\forall d \leftarrow enjambreDrones(pre(s)), bateria(d) \geq b ) igualdadDrone(d,pre(d)) }
|
|
|
+ \asegura{ (\forall d \leftarrow enjambreDrones(pre(s)), bateria(d) < b ) \newline
|
|
|
+ id(d) == id(pre(d)) \wedge bateria(d)==100 \wedge enVuelo(d)==False \wedge vueloRealizado(d)==[] \wedge \newline posicionActual(d)==Granero(pre(s)) \wedge mismos(productosDisponibles(d),productosDisponibles(pre(d)))
|
|
|
+ }
|
|
|
\end{problema}
|
|
|
|
|
|
\begin{problema}{fertilizarPorFilas}{s: Sistema}{}
|
|
|
- \modifica s \asegura{ (\forall(d) \leftarrow enjambreDrones(pre(s)), !puedeMoverOeste(d)) igualdadDrone(d,pre(d)) }
|
|
|
+ \modifica s
|
|
|
+ \asegura{ (\forall(d) \leftarrow enjambreDrones(pre(s)), !puedeMoverOeste(d)) igualdadDrone(d,pre(d)) }
|
|
|
\asegura{ (\forall(d) \leftarrow enjambreDrones(pre(s)), puedeMoverOeste(d))
|
|
|
\newline dronesIgualesSinPosicion(d,pre(d)) \wedge \newline posicionActual(d)==(pri(posicionActual(pre(d)-1)),sgd(posicionActual(pre(d))))
|
|
|
}
|
|
|
@@ -88,4 +95,5 @@
|
|
|
\end{problema}
|
|
|
|
|
|
\begin{problema}{volarYSensarS}{s: Sistema, d: Drone}{}
|
|
|
+
|
|
|
\end{problema}
|
