Given the following model

abstract sig Object {}

sig File extends Object {}

sig Dir extends Object {contents: set Object}
one sig Root extends Dir { }

fact {
 Object in Root.*contents

assert RootTop {
 no o: Object | Root in o.contents
check RootTop // This assertion should produce a counterexample
fact “demo” {
let unroot = Dir - Root |

contents = Root -> unroot + unroot -> Dir + ((Dir - Root) -> File)


One counterexample to RootTop is a directory that contains the root. In the Visualizer, this looks like


This page will cover all functionality of the visualizer.


The XML for this example can be downloaded here.


The model visualizer names atoms like Atom$0, Atom$1, etc. This can sometimes be hard to follow in the visualizer. To give things qualified names, instead write:

abstract sig Base {
 -- relations here

lone A, B, C, D extends Base {}

run {} for 2 Base

This will guarantee the values have better names.

Output options

The standard view is the visualizer. The other three options are

  • Text

seq/Int={0, 1, 2, 3}
this/Object={Dir$0, File$0, Root$0}
this/Dir={Dir$0, Root$0}
this/Dir<:contents={Dir$0->Dir$0, Dir$0->File$0, Dir$0->Root$0, Root$0->Dir$0}
skolem $RootTop_o={Dir$0}
  • Tree

  • Table

│Dir⁰    │Dir⁰    │
│        ├────────┤
│        │File⁰   │
│        ├────────┤
│        │Root⁰   │
│Root⁰   │Dir⁰    │



The table view shows the atoms in a human readable form, for example, writing Root⁰ instead of Root$0. In the evaluator, however, you need to write Root$0.


See Themes.

Magic Layout

Automatically generates an appropriate theme for the visualization.


The evaluator can be used to run arbitrary commands against the existing model. It cannot create new signatures, only investigate the current signatures and relations you currently have. You cannot define new functions or predicates in the evaluator, only evaluate Expressions.



While the evaluator can evaluate most expressions, it does not have the full capacity of the alloy analyzer. For example, polymorphic domain restriction will not work. Additionally, integer overflow will wrap instead of raising an error.


Projections break a complex model into multiple subviews. Instead of showing relations from the projected signature, each relation will be represented as a text label on the corresponding targets of the relation.