a

espec/auxiliares.tex

@@ -3,7 +3,7 @@
 % los aux del tipo campo
 $igualdadCampo(c,c':Campo):Bool= dimensiones(c)==dimensiones(c') \wedge (\forall i \leftarrow [0..fst(dimensionesCampo(c)),$\\ $j \leftarrow [0..snd(dimensionesCampo(c)) contenido(c,i,j)==contenido(c',i,j)) $ 
 
-parcelasCampo(c:Campo):$[(\ent , \ent)]$= \newline [(x,y) \textbar x $\leftarrow$ [0..prs(dimensiones(s))),y $\leftarrow$ [0..snd(dimensiones(s)))]
+parcelasCampo(c:Campo):$[(\ent , \ent)]$= \newline [(x,y) \textbar x $\leftarrow$ [0..prs(dimensiones(c))),y $\leftarrow$ [0..snd(dimensiones(c)))]
 
 \subsection{Drone}
 
@@ -33,7 +33,7 @@ escalera3(d:Drone):Bool= ($\forall i \leftarrow$ [0..\textbar vueloRealizado(d)\
 escalera4(d:Drone):Bool= ($\forall i \leftarrow$ [0..\textbar vueloRealizado(d)\textbar -1) $prm(vueloRealizado(d)_{i}) \geq prm(vueloRealizado(d)_{i+1}$)\newline if \  $prm(vueloRealizado(d)_{i})== prm(vueloRealizado(d)_{i+1}$\  then  $snd(vueloRealizado(d)_{i})+1== snd(vueloRealizado(d)_{i+1})$\ else $snd(vueloRealizado(d)_{i})== snd(vueloRealizado(d)_{i+1}$
 \newline
 \newline
-parcelasConChoques(ds:[Drones]):[(($\ent,\ent),\ent$)]= \newline [(p,cantidadDronesenMomento(p,i,ds))\textbar d $\leftarrow$ ds, i $\leftarrow$ [0..\textbar vueloRealizado \textbar), p $\leftarrow$ vueloRealizado(d), \\ cantidadDronesEnMomento(p,i,ds) $\geq$ 2]
+parcelasConChoques(ds:[Drones]):[(($\ent,\ent),\ent$)]= \newline [(p,cantidadDronesenMomento(p,i,ds))\textbar d $\leftarrow$ ds, i $\leftarrow$ [0..\textbar vueloRealizado(d) \textbar), p $\leftarrow$ vueloRealizado(d), \\ cantidadDronesEnMomento(p,i,ds) $\geq$ 2]
 \newline
 \newline
 cantidadDronesenMomento($p:(\ent, \ent),i:\ent,ds:[Drones]): \ent$ = \\ \textbar [p \textbar d $\leftarrow$ ds, $vueloRecorrido(d)_{i} $== p] \textbar

espec/sistema.tex

@@ -1,6 +1,7 @@
 \begin{problema}{crearS}{c: Campo, ds: [Drone]}{Sistema}
 	\asegura{igualdadCamapo(campo(res),c)}
-	\asegura{(\forall d \leftarrow ds)(\exists d' \leftarrow enjambreDrones(s))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 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}
@@ -34,7 +35,7 @@
 	%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)estadoDelCultivo(s,prs(p),snd(p))==ConMaleza}
+	\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}