Chapter 7
Graphical Output of Abstraction

The software is able to print the output in dot language, a language that provides a simple way of describing graphs that both humans and computer programs can use.

Two command line options are supported:

• -d produces only one graph at the end of the computation
• -ds produces a graph after each splitting step of the algorithm

There are various programs that can further process such output, for example rendering it into some image format. With the tool Graphviz the user can easily render graphics from HSolver . For example, the command

will create an image file output.gif at the moment when the number of abstract states reaches 5. Clutter can be removed by filtering the output through tred which removes edges implied by transitivity.

Nodes of the graph represent abstract states of the hybrid system. They are grouped by the mode they represent. The list of possible transitions follows a list of all nodes. The meaning of the coloring of nodes is as follows:

• green - the node may contain some initial points
• red - the node may contain some unsafe points
• blue - the node may contain both initial and unsafe points
• yellow border - the node occurs on the shortest abstract error trajectory

The produced output would look like this: