volar y sensar ocmpleto

espec/sistema.tex

@@ -86,7 +86,8 @@
 	\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)))) 
+		\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
 	}
 	\begin{aux}{puedeMoverOeste}{d: Drone, s:Sistema}{\bool}{
 		\newline
@@ -96,5 +97,88 @@
 \end{problema}
 
 \begin{problema}{volarYSensarS}{s: Sistema, d: Drone}{}
+	\requiere{d \in enjambreDrones(pre(s))}
+	\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{ posicionActual(miDrone(id(d),s) \in parcelasAdyacentes(posicionActual(d)) }
+
+
+	\asegura{dimensiones(campo(s))==dimensiones(campo(pre(s)) \wedge \newline
+		(\forall i \leftarrow [0..fst(dimensionesCampo(campo(s)))-1],j \leftarrow [0..snd(dimensionesCampo(campo(s)))-1], \newline
+		contenido(campo(s),i,j)==Cultivo \wedge \newline
+		((i,j) \in parcelasAdyacentes(s,posicionActual(d)) \wedge \neg cumpleCondicionHorrible(s,d,i,j)) \vee  \newline
+		((i,j) \notin parcelasAdyacentes(s,posicionActual(d)))
+		) estadoDelCultivo(s,i,j)==estadoDelCultivo(pre(s),i,j))
+	}
+
+
+	\asegura{ If(contenido(campo(pre(s)),miParcela(s,d))== Cultivo) Then \newline 
+		If (estadoDelCultivo(pre(s), miParcela(s,d)) == NoSensado ) Then \newline
+			estadoDelCultivo(s, miParcela(s,d)) \neq NoSensado  \wedge \newline
+			bateria(miDrone(id(d),s)) == bateria(d,s) -1 \newline
+		If (estadoDelCultivo(pre(s), miParcela(s,d)) == ConMaleza \wedge tieneHerbicida(miDrone(id(d),s)) Then \newline
+			usarHerbicida(s,miDrone(id(d),s),miParcela(s,d))\newline
+		If (estadoDelCultivo(pre(s), miParcela(s,d)) == ConPlaga \wedge tienePlaguicida(miDrone(id(d),s)) Then \newline
+			usarPlaguicida(s,miDrone(id(d),s),miParcela(s,d)) \newline
+	}
 	
+	\asegura{(\forall i \leftarrow [0..fst(dimensionesCampo(campo(s)))-1],j \leftarrow [0..snd(dimensionesCampo(campo(s)))-1], \newline
+		((i,j) \in parcelasAdyacentes(s,posicionActual(d)) \wedge \newline cumpleCondicionHorrible(s,d,i,j))) \newline
+		estadoDelCultivo(s,i,j)==RecienSembrado
+	}
+
+
+	\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
+	}
+	\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
+		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])
+	}
+	\end{aux}
+	\begin{aux}{dameHerbicida}{d:Drone}{Producto}{
+		dameUna([prod| prod \leftarrow productosDisponibles(pre(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
+		estadoDelCultivo(s,pos(d))==RecienSembrado
+	}
+	\end{aux}
+	\begin{aux}{tieneHerbicida}{d:Drone}{\bool}{
+		(( Herbicida \in productosDisponibles(d)) \vee \newline
+		( 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 ) 
+	}
+	\end{aux}
+	\begin{aux}{miDrone}{id: \ent, s:Sistema}{Drone}{
+		[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))))
+	}
+	\end{aux}
+
 \end{problema}