Abstract. We present a framework to automatically evaluate the performance of Mobile Ad-hoc Networks (MANETs) in terms of different kinds of metrics, such as throughput and energy consumption. We use a probabilistic process calculus to model MANETs; we translate process terms into Markov Decision Processes (MDPs) and use the probabilistic model checker PRISM to automatically evaluate the network performance. We present a case study consisting of a network which uses flooding for communicating, and we analyse how time and energy costs vary