Custom Graph: Difference between revisions

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: {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)
                    );

Here layout and rankdir are GraphViz attributes for the entire graph. Other values, e.g., for layout are: neato, circo, fdp, sfdp, twopi, patchwork, nop, nop2. Values for rankdir are: TB, BT, LR, RL. More graph attributes can be found here: [1].

The nodes field specifies the nodes of our graph. Here nodes evaluates to a set of records with the value field specifying the B identity of the node and the other fields style and fillcolor being GraphViz attributes. Supported attributes for nodes can be found here: [2]. Note that there can be other nodes fields, called nodes0, nodes1, ..., nodes9.

The edges field here is itself a record with GraphViz attributes. These are default attributes for the edges field, which here is a straightforward B relation (but it could again be a set of records with attributes). We could have used a similar record with default attributes in the nodes description above. Supported attributes for edges can be found here: [3]. Note that there can be other edges fields, called edges0, ..., edges9.

The resulting visualisation can be seen here: File:IceCream Generic.pdf

The full model for experimentation is here:

MACHINE IceCream_Generic
//  a dominating set example: 
// place ice cream vans so that every house (node) is at most one block away from a van
DEFINITIONS
 N == 24;
 CUSTOM_GRAPH == rec(layout:"dot", rankdir:"TB",
                     nodes: {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)
                    );

      bi_edge == (edge \/ edge~);

  SET_PREF_SMT == TRUE;
  SET_PREF_TIME_OUT == 50000;
  SET_PREF_SOLVER_STRENGTH == 300;
  SET_PREF_SOLVER_FOR_PROPERTIES == "prob";
SETS
  NODES = {n1,n2,n3,n4,n5,n6,n7,n8,n9,n10,
           n11,n12,n13,n14,n15,n16,n17,n18,n19,n20,n21,n22,n23,n24}
CONSTANTS edge, ice, vans, neighbours
PROPERTIES
 edge: NODES <-> NODES &
 edge = { n1|->n2, n1|->n4,
          n2|->n3,
          n3|->n4, n3|->n5, n3|->n7,
          n4|->n7,
          n5|->n6, n5|->n9,
          n6|->n7, n6|->n8,
          n7|->n8,
          n8|->n10, n8|->n13,
          n9|->n10, n9|->n11, n9|->n12,
          n11|->n12, n11|->n14,
          n12|->n13,
          n13|->n16,
          n14|->n15, n14|->n17,
          n15|->n16, n15|->n17, n15|->n18, n15|->n21,
          n16|->n18, n16|->n19,
          n17|->n19,
          n18|->n19, n18|->n20, n18|->n21,
          n19|->n20, n19|->n21,
          n20|->n21, n20|->n22,
          n21|->n22, n21|->n23, n21|->n24,
          n22|->n23, n21|->n24,
          n23|->n24
          } &
 ice : NODES--> BOOL &
 neighbours = %x.(x:NODES|bi_edge[{x}]) &
 !x.(x:NODES =>
      (ice(x)=TRUE or
        #neighbour.(neighbour: neighbours(x) & ice(neighbour)=TRUE)
                 )
    )

 & vans = card(ice~[{TRUE}])
 & card({x|x:NODES & ice(x)=TRUE})<=6
  /* minimal solution requires 6 vans */

OPERATIONS
  v <-- NrVans = BEGIN v := vans END;
  xx <-- Get(yy) = PRE yy:NODES THEN xx:= ice(yy) END;
  v <-- Vans = BEGIN v:= ice~[{TRUE}] END
END