Predefined Set in Alloy

I am trying to learn alloy spec. lang. . I can not find a way out about a question. My question is related with predefined number of elements.

theater_seat set should have 4 members. Audience set should have 10 members.

There is a theater which is 4 seats available only. But there are 10 people who want to watch the theater. Only 4 of them can have the seat. The rest will go home back. I am in trouble. Could you help me about that please?

Thanks in advance.

EDIT

Here is my code :

module Example
sig Audiance{
   result: lone Seat
}

some sig Seat {}

pred validassignment {
   '#'Seat=4
   '#'Audiance=10
   all a:Audiance | lone a.result
}

run validassignment

EDIT

How can I eliminate that problem? (Seating on the same seat)

Regards

Solution

You might want to show us what you already did, and pinpoint to where you are stuck exactly. A vague answer to that vague question would be : think "declaratively".

EDIT

Here it doesn't work for two reasons:

First, what you wrote is syntactically wrong. The cardinality operator is # and not '#'. (I redirect you to there : http://www.monperrus.net/martin/alloy-quick-ref.pdf for a nice overview of the main concepts and associated syntax in Alloy)

Then, the default scope when you run a command is 3. Meaning each set defined by a signature will have a cardinality of at most 3. You need thus in your case to increase your scope in order to find relevant instances.

You can specify the number of seats and audiances directly in the scope, as follows :

  run validassignment for exactly 4 Seat, exactly 10 Audiance

There are still other issues in your model. In its current state, it is possible to have everybody in the audience seating on the same seat. I guess you don't want that to happen.

Good luck