Take a random Object in Alloy

Question

Let's say you have a basic elevator system defined in Alloy... You have a set of floors and a set of people waiting on the elevator on each floor. You work with State to show the progress the elevator makes. How can you send the elevator in the initial state to a random floor to pick up his first person? (aka; how can you randomise the element alloy takes?)

Answer 1

I think what you want to do here is to leave the initial state unspecified. That is, describe its existence, clarify that there is exactly one, but leave it unspecified which of the possible states is the initial state.

The Alloy Analyzer will then check your assertions and predicates for all possible initial states, and will (eventually) generate instances of the model for all possible initial states. This resembles the behavior of a good random number generator, in that the likelihood of any given state being chosen as the initial state is equal to the likelihood of any other given state being chosen -- it's just that the likelihood here becomes 1.0, not 1/n for n possible states.

Answer 2

And better to say an arbitrary floor, rather than a random floor.