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 ) 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)) }
	\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)))) 
	}
	\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}{}
	
\end{problema}