Hi everyone,
I'm really new to TLA+ and TLC, so forgive me if this is a silly question:
I have a model resembling the binpacking problem: I have 5 players P = {p1, p2, ..., p5} and 5 bins {b1, b2, ... , b5}.
Each bin contains some subset of P (initally the empty set).
In each round, the next player is chosen according to some rule, and the player chosen can add himself or remove itself from one of the bins.
I'm using TLC to check for some invariant (for example, whether at any time in the run, there exists a player who is exclusive in 3 bins - in other words, if there are 3 bins containing the same player and only him).
I have some more complex invariants as well, but I'd like to first understand the solution given the above simpler invariant.
In the most general form (if the next player was chosen uniformly), each bin has 2^5 = 25 options, and there are 5 bins so we have 2^25 ~ 32 million options.
The run takes far too long to complete on 32 cores.
(granted, the rules for choosing the next player are complex).
However, I want to "abuse" the fact that the 'name' of the bin isn't interesting to me.
I don't care if the current state is: [ b1 = {p1, p2} | b2 = {p1} | b3, b4, b5 = empty ]
Or if it is: [b1 = empty | b2 = {p1, p2} | b3,b4 = empty | b5 = {p1} ]
These are equivalent to me and thus I can skip checking many states.
I read the section of symmetry sets, as it sounded similar, but didn't come up with an idea of how to use this.
I'd appreciate any help,
Thanks a lot!
Alon