Algo1_TP1/espec/sistema.tex

\begin{problema}{crearS}{c: Campo, ds: [Drone]}{Sistema}
	\asegura{igualdadCamapo(campo(res),c)}
	\asegura{(\forall d \leftarrow ds)(\exists d' \leftarrow enjambreDrones(res))id(d)==id(d') \wedge bateria(d')==100 \wedge \neg enVuelo(d') \wedge \newline enRango(dimesiones(campo(res)), prs(posicionActual(d')),snd(posicionActual(d'))) \wedge \newline contenido(campo(res), prs(posicionActual(d')),snd(posicionActual(d')))==Granero}
	\asegura{(\forall (i,j) \leftarrow parcelasCampo(campo(res), contenido(campo(res),i,j)==Cultivo)\\ estadoDelCultivo(res,i,j)==NoSensado}
\end{problema}

\begin{problema}{campoS}{s: Sistema}{Campo}
	\asegura {res==campo(s)}
\end{problema}

\begin{problema}{estadoDelCultivoS}{s: Sistema, i, j: \ent}{EstadoCultivo}
	\requiere {enRango(dimensiones(campo(s)),i,j) \wedge contenido(campo(s),i,j)==cultivo}
	\asegura {res==estadoDelCultivo(s,i,j)}
\end{problema}

\begin{problema}{enjambreDronesS}{s: Sistema}{[Drone]}
	\asegura{mismos(res,enjambreDrones(s))}
\end{problema}

\begin{problema}{crecerS}{s: Sistema}{}
	\modifica s
	\asegura{igualdadCampo(campo(s),campo(pre(s)))}
	\asegura{ mismosDrones(enjambreDrones(s),enjambreDrones(pre(s)))}
	\asegura{(\forall i \leftarrow [0..prs(dimensiones(s)),j \leftarrow [0..snd(dimensiones(s)), enRango(dimensiones(campo(s)),i,j), \newline contenido(campo(s),i,j)==Cultivo, estadoDelCultivo(pre(s),i,j)==RecienSembrado )\newline estadoDelCultivo(s,i,j)==EnCrecimiento }
	\asegura{(\forall i \leftarrow [0..prs(dimensiones(s)),j \leftarrow [0..snd(dimensiones(s)), enRango(dimensiones(campo(s)),i,j), \newline contenido(campo(s),i,j)==Cultivo, estadoDelCultivo(pre(s),i,j)==EnCrecimiento ) \newline estadoDelCultivo(s,i,j)==ListoParaCosechar} 
	\asegura {(\forall i \leftarrow [0..prs(dimensiones(s)),j \leftarrow [0..snd(dimensiones(s)), enRango(dimensiones(campo(s)),i,j), \newline contenido(campo(s),i,j)==Cultivo, (estadoDelCultivo(pre(s),i,j)\neq EnCrecimiento \wedge \newline estadoDelCultivo(pre(s),i,j)\neq RecienSembrado  )) \newline estadoDelCultivo(s,i,j)==estadoDelCultivo(pre(s),i,j)}
\end{problema}

\begin{problema}{seVinoLaMalezaS}{s: Sistema, ps: [(\ent, \ent)]}{}
%	\requiere{(\forall p \leftarrow ps) enRango(dimensiones(campo(pre(s)),prs(p),snd(p))) \wedge \newline contenido(campo(pre(s)),prs(p),sgd(p))==Cultivo}
	\modifica s
	\asegura{igualdadCampo(campo(s),campo(pre(s)))}
	\asegura{ mismosDrones(enjambreDrones(s),enjambreDrones(pre(s)))}
	\asegura{(\forall i \leftarrow [0..prs(dimensiones(campo(s))), j \leftarrow [0..snd(dimensiones(campo(s))), \newline contenido(campo(s),i,j)!=Cultivo \wedge (i,j) \notin ps) contenido(campo(s),i,j)==contenido(campo(pre(s)),i,j)}
	%si no es cultivo, lo dejo igual
	\asegura{(\forall i \leftarrow [0..prs(dimensiones(campo(s))), j \leftarrow [0..snd(dimensiones(campo(s))), \newline contenido(campo(s),i,j)==Cultivo \wedge (i,j) \notin ps) estadoDelCultivo(s,i,j)==estadoDelCultivo(pre(s),i,j)}  
	%si es cultivo y no esta en ps lo dejo igual
	\asegura{(\forall p \leftarrow ps,enRango(dimension(s),prs(p),snd(p)) \wedge contenido(campo(s),prs(p),snd(p)))\\ estadoDelCultivo(s,prs(p),snd(p))==ConMaleza}
	%le pongo maleza
\end{problema}

\begin{problema}{seExpandePlagaS}{s: Sistema}{}
	\modifica s
	\asegura{igualdadCampo(campo(s),campo(pre(s)))}
	\asegura{mismosDrones(enjambreDrones(s),enjambreDrones(pre(s)))}
	\asegura{(\forall i \leftarrow [0..prs(dimensiones(campo(pre(s)))), j \leftarrow [0..snd(dimensiones(campo(pre(s))))\newline contenido(campo(pre(s)),i,j) \wedge estadoDelCultivo(pre(s),i,j)==ConPlaga)\newline estadoDelCultivo(s,i,j)==ConPlaga \wedge parcelaAdyacenteConPlaga(s,i,j)}
	\asegura{(\forall i \leftarrow [0..prs(dimensiones(campo(pre(s)))), j \leftarrow [0..snd(dimensiones(campo(pre(s))))\newline contenido(campo(pre(s)),i,j)==Cultivo \wedge estadoDelCultivo(pre(s),i,j)\neq ConPlaga \wedge \newline  \neg algunAdyacenteConPlaga(s,i,j)) estadoDelCultivo(s,i,j)==estadoDelCultivo(pre(s),i,j)}
\end{problema}

\begin{problema}{despegarS}{s: Sistema, d: Drone}{}
	\requiere{bateria(d)==100}
	\requiere{d \in enjambreDrones(pre(s))}
	\requiere{hayParcelaAdyacenteAlGraneroLibre(pre(s))}
	\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{\mid enjambreDrones(pre(s)) \mid == \mid enjambreDrones(s) \mid}
	\asegura{(\forall d' \leftarrow enjambreDrones(pre(s)), id(d')==id(d))(\exists d'' \leftarrow enjambreDones(s))igualdadDrones(d',d'')}
	\asegura{(\exists d' \leftarrow enjambreDrones(s))id(d)==id(d') \wedge enVuelo(d') \wedge bateria(d')==99 \wedge \newline enRango(dimensiones(s),prs(posicionActual(d')),snd(posicionActual(d'))) \wedge \newline soloUnDrone(s,posicionActual(d')) \wedge estaAdyacenteAlGranero(s,(posicionActual(d')) \wedge \newline vueloRealizado(d')==[posicionActual(d')] \wedge  mismos(productosDisponibles(d),productosDisponibles(d'))}
\end{problema}

\begin{problema}{listoParaCosecharS}{s: Sistema}{\bool}
	\asegura { res == ( contarCultivosListos/contarCultivos(s) \geq 0.9 ) }

	\begin{aux}{contarCultivos}{s: Sistema}{\ent}
	{ |[ 1 | \newline i \leftarrow [0..prs(dimensiones(campo(s))) \newline j \leftarrow [0..snd(dimensiones(campo(s))), \newline contenido(campo(s),i,j)==Cultivo)  ]| }
	\end{aux}
	\begin{aux}{contarCultivosListos}{s: Sistema}{\ent}
	{ |[ 1 | \newline i \leftarrow [0..prs(dimensiones(campo(s))) \newline j \leftarrow [0..snd(dimensiones(campo(s))), \newline contenido(campo(s),i,j)==Cultivo \wedge
	estadoDelCultivo(s,i,j) == ListoParaCosechar )  ]| }
	\end{aux}

\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 ) 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{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,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
		\IfThenElse{ bateria(d) == 0 \vee noTieneFertilizante(d) \vee \newline contenido(campo(pre(s)),pri(posicionActual(d)),sgd(posicionActual(d))) \neq Cultivo \vee \newline pri(posicionActual(d)) == 0 }{\newline False \newline }{\newline True}
	}
	\end{aux}
\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}