ViSiDiA is a tool for implementing, simulating, testing and visualizing
distributed algorithms. It is motivated by the important
theoretical results on the use of graph relabelling systems to encode
distributed algorithms and to prove their corretness.

The high level encoding of distributed algorithms in form of rewriting
systems allows a better description and presentation of these algorithms.
The result is a formal approach to decribe and study distributed
algorithms in a unified and simple way.

ViSiDiA provides a library together with an easy interface to
implement distributed algorithms described by means of local
computations.

This tool can be used to visualize and experiment distributed
algorithms, and therefore helps in their design and their validation.

Several distributed algorithms have been already implemented and
can be directly animated.

Consider an anonymous network of processors with arbitrary topology,
represented as a connected, undirected graph where vertices denote processors,
and edges denote direct communication links. An algorithm is encoded by
means of local relabellings. Labels attached to vertices and edges are modified
locally, that is on a subgraph of fixed radius **k** of the given graph,
according to certain rules depending on the subgraph only (**k**-local
computations). The relabelling is performed until no more transformation is
possible.

The corresponding configuration is said to be in normal form. Two sequential
relabelling steps are said to be independent if they are applied on disjoint
subgraphs. In this case they may be applied in any order or even concurrently.

The model of distributed computation is an asynchronous distributed network of
processes which communicate by exchanging messages. To overcome the problem of
certain nondeterministic distributed algorithms as well as to have efficient
and easy implementations, we use randomization. Each process tries at
random to synchronize with one of its neighbours or with all of its neighbours
depending on the model we choose, then once synchronized, local computations
can be done. A synchronization between two neighbours is called a rendez-vous,
and a synchronization between a vertex and all its neighbours is called a star
synchronization. Procedures implementing synchronizations are provided by the
primitives rendezVous, starSynchro1 and starSynchro2 (given below).
These procedures allows local computations to be performed between a
processorand its neighbour(s) through a transcient synchronization. The
visualization of an algorithms shows all the synchronizations which can happen
at the same time. Exchanged messages and the processor states are also
displayed on-the-fly.

The tool provides a GUI which can be used to draw by ``drag and drop'' a
graph which will model the network. The user can add, delete, or select
vertices, edges or subgraphs. Visual attributes of vertices and edges such as
labels, colors or shapes have default values, but they can be easily
customized, for instance to assign an initial labelling to the vertices of the
graph, such as a label *A* to a particular vertex, and *N* to all
other vertices. Note that *N* is the default label of vertices.

A library of high level primitives is available to program the
corresponding local computations. The following java code shows the
implementation of the spanning tree.

*while (run) {*

* neighbour = rendezVous();*

* sendTo(neighbour,myLabel);*

* neighbourLabel=receiveFrom(neighbour);*

* if (myLabel == 'N') && (neighbourLabel == 'A'){*

* myLabel = 'A';*

* edge[neighbour]=1*

* }*

* breakSynchro();*

*}*

Note that one has to choose first the type of local computation by choosing one of the three primitives: rendezVous(), starSynchro1(), and starSynchro2()) which are implemented as follows:

- rendezVous(): a function that returns the neighbour with whom the synchronization occurs.
- starSyncho1(): returns the center of the star during a star synchronization. Only the center can update its attributes.
- starSynchro2(): returns the center of the star during a star synchronization. The center and its neighbours can update their attributes.

After compiling the module implementing the relabelling
system, the user can execute it by pressing on appropriate buttoms provided by
the interface. The system automatically creates and assigns to each vertex a
java thread which will run a copy (a clone) of the code implementing the
relabelling system. The user can observe the messages exchanged between
vertices (threads), and their states. In particular, label changes of vertices
can be seen on-line. The whole algorithm is animated in such a way that the
user can follow its execution. Moreover, the number of exchanged messages is
computed and displayed. This can be used to perform experiments on
particular distributed algorithms described within our framework.

Many examples of distributed, described by graph relabelling systems, are
given in Examples. For each of these examples, we give the relabelling
system and a few screenshots.

An interesting advantage of our approach is that we only need to
implement local rewritings to code complicated distributed algorithms.
Therefore, visualizing the execution of these algorithms consists of animating
distributed local computations.