Improved visualization of relational logic models

Abstract

The Alloy Analyzer includes a visualizer tool for presenting counter-examples to the user. This visualizer tool contains a wide array of settings and a "Magic Layout" feature to automatically infer values for these setting based on a static analysis of the specification being visualized. We improve both the visualizer itself and the Magic Layout feature. For example, expert users often use colour to distinguish changes of state when visualizing specifications of dynamic systems, but previously Magic Layout was not sophisticated enough to infer where state changes might be represented in the specification. We have also improved the way in which the visualizer distinguishes different but related types of atoms, as well improved the visual consistency between different frames of a projection. Finally, a quantitative evaluation is done to compare how much better the new inferred theme compares to the default theme, and a qualitative evaluation of how the inferred theme compares to the expert made themes.