wRebeca is an actor-based modeling language, an extension of Rebeca, proposed for modeling and verification of Mobile Ad Hoc Networks (MANETs). It is supported by the tool, which efficiently generates the state spaces of models. Several techniques have been exploited to reduce the state spaces like counting abstraction (which is sound in case the underlying topology is static), and removal of un-observable transitions (which preserves the ACTL-X properties of the original model).