Bigraph trace
Place graph as nesting (dashed boxes are roots), link graph as coloured curves joining ports that share a link name.
Input format
JSON: { title, states: [{ id, nodes: [{ id, ctrl, parent, root, links: [string] }], atoms: {name: bool} }],
transitions: [{ from, to, rule, tag? }], trace: [state id], traceRules?: [rule], initial, loopBack? }.
An atom's value may also be a string, shown as name: value. The optional tag of a
transition is its label in a labelled transition system: "tau" for an internal move, any other
string for a visible action. The optional traceRules names the rule of each trace step (one fewer
than the trace), for when two rules join the same pair of states. The optional
loopBack: { from, to, rule? } makes the trace a lasso: from is the last trace state,
to an earlier one, and playback goes round the loop until paused. Nodes are matched across states by
id; a node whose control is table lays its children out around a circle.
The optional track: { entities: [name], steps: [{ links: {link: entity}, nodes: {id: id}, atoms?, note? }] }
(one step per trace position) carries identity along the trace: each link named in links and every node
on it is drawn in its entity's colour, node ids are renamed by nodes so that a tracked node keeps its
id, and atoms and note replace the state's chips and annotate the step.
Keys: space = play/pause, arrows = step.