Grounded Language Design for Lightweight Diagramming for Formal Methods

TL;DR

Alloy-style model finding relies on default, domain-agnostic visualizations that often hinder understanding for large or complex instances. The authors introduce Cope and Drag (CnD), a lightweight diagramming language built from cognitive-diagramming principles and empirical practice, to refine visualizations by applying a small set of orthogonal primitives (cyclic/orientation/grouping constraints and directives) incrementally. Through domain examples and user studies, CnD demonstrates improved instance understanding and more effective bad-inference detection compared with Alloy's default visualizers, while maintaining a low-friction workflow that can be extended across Alloy-like tools. The work defines a practical niche between generic visualizers and fully programmable diagram tools, with potential applicability to other lightweight formal methods beyond Alloy.

Abstract

Model finding, as embodied by SAT solvers and similar tools, is used widely, both in embedding settings and as a tool in its own right. For instance, tools like Alloy target SAT to enable users to incrementally define, explore, verify, and diagnose sophisticated specifications for a large number of complex systems. These tools critically include a visualizer that lets users graphically explore these generated models. As we show, however, default visualizers, which know nothing about the domain, are unhelpful and even actively violate presentational and cognitive principles. At the other extreme, full-blown visualizations require significant effort as well as knowledge a specifier might not possess; they can also exhibit bad failure modes (including silent failure). Instead, we need a language to capture essential domain information for lightweight diagramming. We ground our language design in both the cognitive science literature on diagrams and on a large number of example custom visualizations. This identifies the key elements of lightweight diagrams. We distill these into a small set of orthogonal primitives. We extend an Alloy-like tool to support these primitives. We evaluate the effectiveness of the produced diagrams, finding them good for reasoning. We then compare this against many other drawing languages and tools to show that this work defines a new niche that is lightweight, effective, and driven by sound principles.

Figures (18)

• Figure 1: Cope and Drag is a language built to support lightweight diagramming for lightweight formal methods. A small set of orthogonal primitives allows users to incrementally refine model finder output into more effective diagrams. This figure shows how grouping (A), orientation (B), and icons (C) can be incrementally applied to model-finder output describing a face.
• Figure 2: The Massachusetts Bay Transportation Authority (MBTA) transit map MBTA1973Map (public domain image from Wikimedia Commons) prioritizes ease of navigation over geographic precision.
• Figure 3: A student-drawn diagram illustrating the layout of their spec. This layout relies on relative positioning, grouped elements, and iconography.
• Figure 4: Abstract syntax of Cope and Drag.
• Figure 5: ring-lights Alloy Default Visualizer and CnD visualizations of a light-switching puzzle instance involving 5 lights in a ring from the Forge examples repository. Lights that are lit are colored red, while unlit lights are colored grey.