module exersizes/elevator
//sig Elevator {location: Location, direction: Direction}
sig Floor {next: set Floor}
sig BetweenFloor{above: Floor}
fact FloorsLinear {
//floors don't lead to themselves
all f: Floor | !(f.next = f)
//elevator shafts don't branch
all f: Floor | sole g: Floor | g in f.next
//there is a top floor
one f: Floor | #f.next = 0
//there is a bottom floor
one f: Floor | no g: Floor | g.next = f
//floors don't converge (the opposite of branch)
all f: Floor | sole g: Floor | g.next = f
//floors can't have cycles
no f: Floor | f in f.^next
all b: BetweenFloor | #b.above = 1
}
fun runme() {
#Floor = 5
#BetweenFloor = #Floor - 1
}
run runme for 5