Visualizing protocols with PAML-check

[danbryce]

PAML-check is concerned about temporal constraints in the protocol that can be visualized with graphviz. We have an internal representation of protocols that represents them as a graph. From the graph, we extract temporal constraints:

Temporal Constraint graph for protocol

We also have additional user-supplied temporal constraints that include activity durations and other relations. These are not currently rendered as part of the graph because they are temporal difference constraints combined with Boolean logic operators.

From the constraints, we find a schedule with minimum duration, and visualize it with a Gantt chart:

Schedule Visualization as Gantt Chart

We are considering additional refinements to these, including:

• embedding hyperlinks in the graphviz image to reference activities and protocols.
• adding interactive displays to either the constraint graph or gantt chart by using other tools.
  • using an interactive graph tool/library to collapse out the details of the nodes.
  • using a web-compatible library for visualizing the Gantt chart timelines, and providing a similar tool-tip or expandable representation for activities.
• We might want to link these visualizations to an editor for PAML, such as planager. Its often useful to add temporal constraints while also seeing the schedule, so that we can rule out scheduling decisions.
  • MAPGen is a good example of an interactive tool for temporal constraints.