\begin{tipo}{Sistema}
	\observador{campo}{s: Sistema}{Campo}
	\observador{estadoDelCultivo}{s: Sistema, i, j: \ent}{EstadoCultivo}
		\requiere{enRango(dimensiones(s), i, j) \land contenido(campo(s), i,j) == Cultivo}
	\observador{enjambreDrones}{s: Sistema}{[Drone]}

	\medskip

	\invariante[identificadoresUnicos]{sinRepetidos(\comp{id(d)}{d \selec enjambreDrones(s)})}
	\invariante[unoPorParcela]{(\forall d, d' \selec dronesEnVuelo(s), id(d) \neq id(d')) posicionActual(d) \neq posicionActual(d')}
	\invariante[siNoVuelanEstanEnGranero]{(\forall d \selec enjambreDrones(s), \neg enVuelo(d)) \\ posicionActual(d) == posicionGranero(campo(s))}
	\invariante[siEstanEnVueloElVueloEstaEnRango]{(\forall d \selec dronesEnVuelo(s)) (\forall v \selec vueloRealizado(d))\\ enRango(dimensiones(campo(s), prm(v), sgd(v))} 
\end{tipo}

\aux{dronesEnVuelo}{s: Sistema}{[Drone]}{\comp{d}{d \selec enjambreDrones(s), enVuelo(d)}}