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:

trace

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.

projected

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?

Nuno Macedo · Accepted Answer · 2014-03-16 21:27:02Z

2

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.

answered Mar 16, 2014 at 21:27

Nuno Macedo

1245 bronze badges

Sign up to request clarification or add additional context in comments.

Collectives™ on Stack Overflow

Visualizing projections with Alloy

1 Answer 1

Comments

Your Answer

Hot Network Questions

Collectives™ on Stack Overflow

1 Answer 1

Comments

Your Answer

Sign up or log in

Post as a guest

Related