|
|
@@ -13,7 +13,7 @@
|
|
|
\end{problema}
|
|
|
|
|
|
\begin{problema}{enjambreDronesS}{s: Sistema}{[Drone]}
|
|
|
- \asegura{res==enjambreDrones(s)}
|
|
|
+ \asegura{mismos(res,enjambreDrones(s))}
|
|
|
\end{problema}
|
|
|
|
|
|
\begin{problema}{crecerS}{s: Sistema}{}
|
|
|
@@ -26,12 +26,16 @@
|
|
|
\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}
|
|
|
+% \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{(\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)estadoDelCultivo(s,prs(p),snd(p))==ConMaleza}
|
|
|
+ %le pongo maleza
|
|
|
\end{problema}
|
|
|
|
|
|
\begin{problema}{seExpandePlagaS}{s: Sistema}{}
|
