Merge branch 'master' of https://gogs.davidventura.com.ar/david/Algo1_TP1.git

espec/auxiliares.tex

@@ -6,12 +6,15 @@ $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
 \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'))$
+$dronesIgualesSinPosicionNiBat(d,d':Drone):Bool= id(d)==id(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)$

espec/sistema.tex

@@ -76,17 +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 dronesIgualesSinPosicion(d,pre(d)) \wedge \newline posicionActual(d)==(pri(posicionActual(pre(d)-1)),sgd(posicionActual(pre(d)))) 
+		\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
@@ -96,5 +103,92 @@
 \end{problema}
 
 \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)) igualdadDrone(d', miDronePre(s,id(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(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(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(miDronePre(s,id(d))), prod == Plaguicida \vee prod == PlaguicidaBajoConsumo])
+	}
+	\end{aux}
+	\begin{aux}{dameHerbicida}{d:Drone}{Producto}{
+		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(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}
+	\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}

resolucion.tex

@@ -13,13 +13,11 @@
 \titulo{TPE - Agricultura con drones} 
 \fecha{\today}
 \materia{Algoritmos y Estructuras de Datos I}
-\grupo{Grupo ?}
+\grupo{Grupo 26}
 
 % Completar con cuantos integrantes quieran :)
-\integrante{Apellido, Nombre1}{001/01}{email1@dominio.com}
-\integrante{Apellido, Nombre2}{002/01}{email2@dominio.com}
-\integrante{Apellido, Nombre3}{003/01}{email3@dominio.com}
-\integrante{Apellido, Nombre4}{004/01}{email4@dominio.com}
+\integrante{Cab\'an, Alejandro}{???/??}{cabanalejandro@gmail.com}
+\integrante{Ventura, David}{673/13}{davidventura27@gmail.com}
 
 \maketitle