|
|
@@ -29,7 +29,7 @@
|
|
|
% \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),emjambreDrones(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)}
|
|
|
@@ -41,7 +41,7 @@
|
|
|
\begin{problema}{seExpandePlagaS}{s: Sistema}{}
|
|
|
\modifica s
|
|
|
\asegura{igualdadCampo(campo(s),campo(pre(s)))}
|
|
|
- \asegura{mismosDrones(enjambreDrones(s),emjambreDrones(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}
|
|
|
@@ -72,9 +72,18 @@
|
|
|
\end{problema}
|
|
|
|
|
|
\begin{problema}{aterrizarYCargarBateriaS}{s: Sistema, b: \ent}{}
|
|
|
+
|
|
|
\end{problema}
|
|
|
|
|
|
\begin{problema}{fertilizarPorFilas}{s: Sistema}{}
|
|
|
+ \modifica s
|
|
|
+ \asegura{ (\forall(d) \leftarrow enjambreDrones(pre(s)), !puedeMoverOeste(d)) NOCAMBIA }
|
|
|
+ \asegura{ (\forall(d) \leftarrow enjambreDrones(pre(s)), puedeMoverOeste(d)) \newline
|
|
|
+ \IfThenElse{bateria(d) == 0}{NOCAMBIA}{
|
|
|
+ if { !tieneFertilizante(d)} \newline
|
|
|
+ {NOCAMBIA}\newline
|
|
|
+ fi
|
|
|
+ }
|
|
|
\end{problema}
|
|
|
|
|
|
\begin{problema}{volarYSensarS}{s: Sistema, d: Drone}{}
|
