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.