Define elevator floors (symmetry, ordering) in Alloy

Question

I'm trying to specify an ordered set of floors in Alloy 6, so that I can later simulate an elevator visiting those floors.

Ultimately, I want to generate a graph that looks like the image below:

Ideally, I could support any amount of floors more than two.

At first, I thought I should have an abstract set:

abstract sig Floor {}

sig MidFloor extends Floor {
    up : one Floor,
    down : one Floor
} {
    this not in up
    this not in down
    // cannot be above top floor
    up in Floor - TopFloor
    // cannot be below bottom floor
    down in Floor - BottomFloor
}

one sig TopFloor extends Floor {
    up : one Floor
} {
    this not in up
}

one sig BottomFloor extends Floor {
    down : one Floor
} {
    this not in down
}

But then I couldn't figure out how to further constrain the up/down relationships. So instead, I thought I would only use a single set:

sig Floor {
  up : lone Floor,
  down : lone Floor
}

one sig bottom, top in Floor {}

fact {
  no top.up
  no bottom.down
  // all floors are reachable from the bottom or the top
  Floor in bottom.*up
  Floor in top.*down
}

But then I couldn't figure out how to implement Up/Down symmetry. Where the set of

From either of these starting points, how do I get the desired graph?

Answer 1

First of all, you might not even need to model it this way: you can use the ordering module:

open util/ordering[Floor]
sig Floor {}

Then the bottom floor is first, the bottom floor is last, up is next, and down is prev.

Unfortunately, you'll have trouble getting the layout you want, since Alloy's visualizer doesn't give you a lot of control over the specific layout of nodes. You can try laying out the down arrows backwards in the Theme option, but that only gets you so far.

I'd consider defining just one field, up, and then defining down as the reverse of up:

sig Floor {
  up : lone Floor,
}

one sig bottom, top in Floor {}

fun down: Floor -> Floor { ~up }
fact {
  no top.up
  Floor in bottom.*up
}