Re: [tlaplus] Excessively long run time - How to reduce the number of states?

[Alon Be <alo...@xxxxxxxxx>]

Hello Stephan,

First of all thanks a lot for your help, I really appreciate it.

I didn't exactly use a set of bins and players, I used a set of indices for the bins = {1,2,3,4,5}, and the bins themselves are a function (or an array) which I called Omega.

Initially I have:

Omega = [x \in bins |-> {}]

and generally Omega is a function from bins to SUBSET {p1, p2, p3, p4, p5}.

Perhaps this is a wrong approach, but I didn't know how else to maintain the state of all of the bins through different machine states.

(This way I easily use the notation:

Omega' = [Omega EXCEPT ![x] = Omega[x] \ {next'}]

for some x \in {1,2,3,4,5} ) 

I think that this approach is what makes the symmetry sets hard for me to understand.

 

Regards,

Alon

On Sunday, September 3, 2017 at 12:33:11 PM UTC+3, Stephan Merz wrote:

Hello,

I'm assuming that your module has CONSTANT declarations for the sets of bins and players. When you define your model that you give to TLC to check, choose "set of model values" for the bins (e.g., name them {b1,b2,b3,b4,b5}), and tick the checkbox "symmetry set".

Observe that it's the user's responsibility to ensure that the specification is indeed symmetric in the parameters instantiated by symmetry sets. As long as your bins only occur in quantified formulas, and in particular, you don't use an _expression_ such as

   CHOOSE b \in Bin : ...

to identify a particular bin, you should be on the safe side. You may also be able to declare players as a symmetry set in addition to the bins.

Hope this helps,

Stephan

On 3 Sep 2017, at 11:01, Alon Be <alo...@xxxxxxxxx> wrote:

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

--
You received this message because you are subscribed to the Google Groups "tlaplus" group.
To unsubscribe from this group and stop receiving emails from it, send an email to tlaplus+u...@googlegroups.com.
To post to this group, send email to tla...@xxxxxxxxxxxxxxxx.
Visit this group at https://groups.google.com/group/tlaplus.
For more options, visit https://groups.google.com/d/optout.