asiodjfklasjf

espec/auxiliares.tex

@@ -6,7 +6,10 @@ $igualdadCampo(c,c':Campo):Bool= dimensiones(c)==dimensiones(c') \wedge (\forall
 parcelasCampo(c:Campo):$[(\ent , \ent)]$= \newline [(x,y) \textbar x $\leftarrow$ [0..prs(dimensiones(c))),y $\leftarrow$ [0..snd(dimensiones(c)))]
 
 \subsection{Drone}
-
+\begin{aux}{miDronePre}{id: \ent, s:Sistema}{Drone}{
+	[d | d \leftarrow enjambreDrones(pre(s)), id(d) ==id ][0]
+}
+	\end{aux}
 % 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 \newline posicionActual(d)==posicionActual(d') \wedge mismos(productosDisponibles(d),productosDisponibles(d'))$
 \newline

espec/sistema.tex

@@ -76,18 +76,24 @@
 	\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)))
+	\asegura{ (\forall d \leftarrow enjambreDrones(pre(s)), bateria(d) \geq b ) d \in enjambreDrones(s)  }
+	\asegura{ (\forall d \leftarrow enjambreDrones(pre(s)), bateria(d) < b )(\exists d' \leftarrow enjambreDrones(s)) \newline
+		id(d) == id(d') \wedge bateria(d)==100 \wedge enVuelo(d)==False \wedge vueloRealizado(d)==[] \wedge \newline contenido(campo(s),prim(posicionActual(d')), sgd(posicionActual(d')))==Granero \wedge mismos(productosDisponibles(d),productosDisponibles(d')) 
 	}
+	\asegura{ mismos(enjambreDrones(pre(s)), enjambreDrones(s)) }
+
 \end{problema}
 
 \begin{problema}{fertilizarPorFilas}{s: Sistema}{}
 	\modifica s
-	\asegura{ (\forall(d) \leftarrow enjambreDrones(pre(s)), !puedeMoverOeste(d)) igualdadDrone(d,pre(d)) }
+	\asegura{igualdadCampo(campo(pre(s)),campo(s))}
+	\asegura{ (\forall(d) \leftarrow enjambreDrones(pre(s)), !puedeMoverOeste(d)) igualdadDrone(d,miDronePre(s,id(d))) }
 	\asegura{ (\forall(d) \leftarrow enjambreDrones(pre(s)), puedeMoverOeste(d))
-		\newline dronesIgualesSinPosicionNiBat(d,pre(d)) \wedge \newline posicionActual(d)==(pri(posicionActual(pre(d)-1)),sgd(posicionActual(pre(d))))  \wedge
-		\newline bateria(d)==bateria(pre(d))-1
+		\newline dronesIgualesSinPosicionNiBat(d,miDronePre(s,id(d))) \wedge \newline posicionActual(d)==(pri(posicionActual(miDronePre(s,id(d))-1)),sgd(posicionActual(miDronePre(s,id(d)))))  \wedge
+		\newline bateria(d)==bateria(miDronePre(s,id(d)))-1 \wedge \newline
+		(estadoDelCultivo(pre(s),pri(posicionActual(d)),sgd(posicionActual(d))) \in [RecienSensado, EnCrecimiento ] \wedge \newline
+		estadoDelCultivo(s,pri(posicionActual(d)),sgd(posicionActual(d)))==ListoParaCosechar \wedge \newline
+		mismos(productos(d)++[Fertilizante],productos(miDronePre(s,id(d))))
 	}
 	\begin{aux}{puedeMoverOeste}{d: Drone, s:Sistema}{\bool}{
 		\newline
@@ -98,9 +104,10 @@
 
 \begin{problema}{volarYSensarS}{s: Sistema, d: Drone}{}
 	\requiere{d \in enjambreDrones(pre(s))}
+	\requiere{ \exists p \leftarrow parcelasAdyacentes(pri(posicionActual(d)), sgd(posicionActual(d))) ( \forall d' \leftarrow enjambreDrones(pre(s))) id(d') \neq id(d) }
 	\modifica s
 	\asegura{igualdadCampo(campo(pre(s)),campo(s))}
-	\asegura{ (\forall d' \leftarrow enjambreDrones(pre(s)), id(d') \neq id(d)) d' == pre(d') }
+	\asegura{ (\forall d' \leftarrow enjambreDrones(pre(s)), id(d') \neq id(d)) igualdadDrone(d', miDronePre(s,id(d'))) }
 	\asegura{ posicionActual(miDrone(id(d),s) \in parcelasAdyacentes(posicionActual(d)) }
 
 
@@ -132,32 +139,32 @@
 	\begin{aux}{cumpleCondicionHorrible}{s:Sistema, d:Drone, i:\ent,j:\ent)}{\bool}{
 		\newline
 		estadoDelCultivo(pre(s), i,j)==ConMaleza \wedge \newline
-		bateria(pre(d)) > 5 \wedge \newline
-		dameHerbicida(pre(d)) == HerbicidaLargoAlcance
+		bateria(miDronePre(s,id(d))) > 5 \wedge \newline
+		dameHerbicida(miDronePre(s,id(d))) == HerbicidaLargoAlcance
 	}
 	\end{aux}
 
 	\begin{aux}{usarPlaguicida}{s:Sistema, d:Drone, p: (\ent,\ent)}{}{
 		\newline
-		( \IfThenElse{damePlaguicida(d)==Plaguicida}{\newline bateria(d)==bateria(pre(d))-10}{\newline bateria(d)==bateria(pre(d))-5} ) \wedge \newline
-		productosDisponibles(d)==sinUna(damePlaguicida(pre(d)),productosDisponibles(pre(d))) \wedge \newline
+		( \IfThenElse{damePlaguicida(d)==Plaguicida}{\newline bateria(d)==bateria(miDronePre(s,id(d)))-10}{\newline bateria(d)==bateria(miDronePre(s,id(d)))-5} ) \wedge \newline
+		mismos(productosDisponibles(d),sinUna(damePlaguicida(miDronePre(s,id(d))),productosDisponibles(miDronePre(s,id(d))))) \wedge \newline
 		estadoDelCultivo(s,pos(d))==RecienSembrado
 	}
 	\end{aux}
 
 	\begin{aux}{damePlaguicida}{d:Drone}{Producto}{
-		dameUna([prod| prod \leftarrow productosDisponibles(pre(d)), prod == Plaguicida \vee prod == PlaguicidaBajoConsumo])
+		dameUna([prod| prod \leftarrow productosDisponibles(miDronePre(s,id(d))), prod == Plaguicida \vee prod == PlaguicidaBajoConsumo])
 	}
 	\end{aux}
 	\begin{aux}{dameHerbicida}{d:Drone}{Producto}{
-		dameUna([prod| prod \leftarrow productosDisponibles(pre(d)), prod == Herbicida \vee prod == HerbicidaLargoAlcance])
+		dameUna([prod| prod \leftarrow productosDisponibles(miDronePre(s,id(d))), prod == Herbicida \vee prod == HerbicidaLargoAlcance])
 	}
 	\end{aux}
 
 	\begin{aux}{usarHerbicida}{s:Sistema, d:Drone, p: (\ent,\ent)}{}{
 		\newline
-		bateria(d)==bateria(pre(d))-5 \wedge \newline
-		productosDisponibles(d)==sinUna(dameHerbicida(pre(d)), productosDisponibles(pre(d))) \wedge \newline
+		bateria(d)==bateria(miDronePre(s,id(d)))-5 \wedge \newline
+		mismos(productosDisponibles(d),sinUna(dameHerbicida(miDronePre(s,id(d))), productosDisponibles(miDronePre(s,id(d))))) \wedge \newline
 		estadoDelCultivo(s,pos(d))==RecienSembrado
 	}
 	\end{aux}
@@ -166,6 +173,7 @@
 		( HerbicidaLargoAlcance \in productosDisponibles(d))) \wedge bateria(d) > 5
 	}
 	\end{aux}
+
 	\begin{aux}{tienePlaguicida}{d:Drone}{\bool}{
 		( Plaguicida \in productosDisponibles(d) \wedge bateria(d) > 10) \vee \newline
 		( PlaguicidaBajoConsumo \in productosDisponibles(d) \wedge bateria(d) > 5 ) 
@@ -175,6 +183,8 @@
 		[d | d \leftarrow enjambreDrones(s), id(d) ==id ][0]
 	}
 	\end{aux}
+
+
 	\begin{aux}{miParcela}{s:Sistema, d:Drone}{(\ent,\ent)}{
 	\newline
 		(pri(posicionActual(miDrone(id(d),s))),  sgd(posicionActual(miDrone(id(d),s))))