Custom Graph

You can visualise the state of an individual B, Z, TLA+ or Alloy model using custom graph definitions which are laid out using GraphViz.

Thereby it is possible to specify general graph attributes, the nodes and the edges of the graph.

There are various ways such a custom graph can be defined. The most powerful is providing a single DEFINITION called CUSTOM_GRAPH which defines global graph properties as well as defines nodes and edges.

Suppose we have a B model with a binary relation edge and a set NODES as well as a total function ice from these nodes to BOOL. Here is an example custom graph definition:

 CUSTOM_GRAPH == rec(layout:"dot", rankdir:"TB",
                     nodes:ran( %j.(j:NODES |
                               rec(value:j, style:"filled",
                                fillcolor:IF ice(j)=TRUE THEN "mistyrose" ELSE "white" END
                              ))),
                    edges:rec(color:"gray", arrowhead:"odot",
                              arrowtail:"odot", dir:"both",
                              label:"edge",
                              edges: edge)
                    );