Topology-Based Mobility Models for Wireless Networks.
Ansgar Fehnker, Peter Höfner, Maryam Kamali, Vinay Mehta
Quantitative Evaluation of Systems - 10th International Conference, QEST 2013, Buenos Aires, Argentina, August 27-30, 2013.
To use the Uppaal templates yourself, select an appropiate mobility model, import the MobileNode template, and add the general declarations to the general declarations of your own model.
You can now use the condition topology[i][j] to check if node i and j are connected. The template MobileNode, if included in your system, will change the topology according to the given transition probabilities. Don't change this matrix yourself, unless you know what you are doing.
Find more comments in the model/template.
Contact Ansgar Fehnker for questions or comments.