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.

You can generate the custom graph for the current state in ProB Tcl/Tk by right-clicking in the "State Properties" pane and selecting "View State as Custom Graph" or by going to the State submenu of the Visualisation menu. In ProB2-UI you can view the custom graph via the "Graph Visualisation" dialog in the Visualisation menu. The resulting visualisation can be seen here:

File:IceCream Generic.pdf

The full model for experimentation is below. Some of the examples in the user manual also use this feature, for example the Bridges Puzzle (Hashiwokakero) (Jupyter notebook) or the Argumentation Theory example. These examples may use the older style definition, with two separate definitions CUSTOM_GRAPH_NODES and CUSTOM_GRAPH_EDGES, which is also supported by ProB.

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