Visualizing projections with Alloy

Question

I have an Alloy model that looks like this:

open util/ordering[Time] as timeOrder

sig Time {
    database: one Database
}

sig Database {}
{
    #Database>1
    some database.this
}

pred show {}

run show

I want to use the Alloy Analyzer to view the state of the system at each time. I assumed that if I projected over "Time", then I would be able to see this. However, if I project over time, when I'm looking at Time0, it shows me databases that are associated with other times.

To be specific, I have a trace that looks like this:

if I project over Time, I would assume that Time0 would show me only Database1, and Time1 would show me only Database0. However, when I project over Time and look at Time0, it shows me both Database0 and Database1. It does annotate Database1 with (database), but what I really want is for it to only show Database1 in this view.

Clearly, projection isn't doing what I am expected. Why not? Is there any way that I can just view the elements associated with the element that I am projecting over?

Answer 1

Projection over a signature reduces the arity of the drawn relations but does not hide disconnected atoms.

This can however be achieved by customizing the visualizer theme:

• uncheck the property "Show" of sig Database
• check the property "Show" of the set database (the binary relation database became a set under projection)

Also, if you wish you can also uncheck the property "Show as label" to avoid the tag (database) on the nodes.