Simpler method of making multiple changes to a function in a single step

[Jack Vanlightly]

Hi,

I have a set of nodes N, a set of resources R and a function "register" that maps N to R. The algorithm is a resource allocation algorithm that must assign the resources of R evenly across the nodes N.

So if N is { "n1", "n2", "n3"} and R is {"r1", "r2", "r3", "r4" } then once allocation has taken place a valid value for register would be:

[n1 |-> <<"r4", "r1">>, n2 |-> <<"r2">>, n3 |-> <<"r3">>]

I want to set the values of register in a single step and I have managed it, though the formula seems overly complex and I wonder if there is a simpler way of doing that would help me also gain more insight into TLA+.

I have isolated the allocation logic into a toy spec as follows:

EXTENDS Integers, FiniteSets, Sequences, TLC

CONSTANT R, N

VARIABLE register

Init ==

  register = [n \in N |-> << >>]

HasMinResources(counts, nd) ==

  \A x \in N : counts[nd] <= counts[x] 

Allocate ==

   LET newRegister == [n \in N |-> << >>]

       counts == [n \in N |-> 0]

       al[pendingRes \in SUBSET R, assignCount \in [N -> Nat]] ==

            LET n == CHOOSE nd \in N : HasMinResources(assignCount, nd)

                r == LET int == R \intersect pendingRes

                      IN CHOOSE x \in int : TRUE 

            IN

                IF Cardinality(pendingRes) = 0 THEN newRegister

                ELSE 

                    LET remaining == pendingRes \ { r }

                        newAssignCount == [assignCount EXCEPT ![n] = @ + 1]

                    IN [al[remaining, newAssignCount] EXCEPT ![n] = Append(@, r)]

   IN al[R, counts]

   

Rebalance ==

  /\ register' = Allocate

  /\ PrintT(register')

(* ignore the spec, I just wanted to run the Rebalance action once *)

Spec == Init /\ [][Rebalance]_register

Notes:

- I made Allocate recursive as that is the only way I could figure out making all the changes to register in a single step.

- I did the intersect so that I could use CHOOSE. Else it complained that is was an unbounded CHOOSE so I figured if I did an intersect with R then it would be interpretted as bounded.

Any insights or suggestions would be great.

Thanks

Jack

[Stephan Merz]

Hi,

some observations on your spec:

- Is there a good reason for representing the resource allocation to nodes using sequences rather than sets? If order is unimportant, you will probably find that your spec becomes simpler if you use sets.

- CHOOSE is deterministic, and therefore your function will always return the same result (as a function needs to do, in fact). Is that important for you or would you rather test all possible "balanced" assignments of resources to nodes?

- Nitpicks: write "pendingRes = {}" rather than "Cardinality(pendingRes) = 0", and moreover you can replace "R \intersect pendingRes" by "pendingRes" (and hence get rid of the LET expression) since pendingRes is a subset of R.

Assuming you can use sets and are interested in all possible balanced resource assignments, you could write something like

IsBalanced(reg) == \A m,n \in N : Cardinality(reg[m]) - Cardinality(reg[n]) \in {-1,0,1}

BalancedAllocations == { reg \in [N -> R] : IsBalanced(reg) }

and then write

Rebalance ==

  /\ register' \in BalancedAllocations

  /\ PrintT(register')

Note that while the above definitions are succinct and easy to understand, they will be expensive to evaluate for TLC because it will enumerate all functions in [N -> R] and filter out those that satisfy the condition. In general, it is a good idea to favor clarity over efficiency in formal specifications. Only when model checking becomes too much of a bottleneck, you may need to think about efficient evaluation of operator definitions.

Does this make sense?

Regards,

Stephan

P.S.: I didn't actually check any of the above using TLC. -s

--
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...@googlegroups.com.
Visit this group at https://groups.google.com/group/tlaplus.
For more options, visit https://groups.google.com/d/optout.

[Jack Vanlightly]

Hi,

Sets are fine and I have modified the spec accordingly, also I removed the LET \intersect as you suggested and it works. About the CHOOSE, in theory it shouldn't matter that it is deterministic, the important requirement is even distribution. But, I need to consider that point more deeply.

Regarding your much scaled down version, it is almost there but not quite.

BalancedAllocations == { reg \in [N -> R] : IsBalanced(reg) }

fails with 

Attempted to apply the operator overridden by the Java method

public static tlc2.value.IntValue tlc2.module.FiniteSets.Cardinality(tlc2.value.Value),

but it produced the following error:

Attemtped to compute cardinality of the value

"r1"

If I modify it to be:

BalancedAllocations == { reg \in [N -> SUBSET R] : IsBalanced(reg) }

Then it doesn't fail but happily makes no assignments.

If I modify it to be:

BalancedAllocations == { reg \in [N -> {R}] : IsBalanced(reg) }

then it assigns all resources to all nodes.

So it needs a tweak to make sure it assigns all resources, but without assigning the same resource twice which is an invariant of the algorithm.

I will have a crack at that tomorrow.

Thanks

Jack

[Jack Vanlightly]

I think I have it. I have updated IsBalanced and BalancedAllocations to as follows:

IsBalanced(reg) == 

  /\ \A m,n \in N : \/ m = n

                    \/ Cardinality(reg[m]) - Cardinality(reg[n]) \in {-1,0,1}

  /\ \A m,n \in N : \/ m = n

                    \/ reg[m] \intersect reg[n] = {}

  /\ \A r \in R : \E n \in N : r \in reg[n]

BalancedAllocations == 

    { reg \in [N -> SUBSET R] : IsBalanced(reg) }

It will generate a register such as: [n1 |-> {"r1"}, n2 |-> {"r2"}, n3 |-> {"r3", "r4"}]

The first line of IsBalanced ensures resources are well balanced,

The second ensures that resources are not assigned twice.

The third ensures that all resources are assigned.

It is much shorter and clearer than my first attempt, thank you very much for the help. (If you see any further improvements do let me know!)

Jack

On Wednesday, January 16, 2019 at 5:35:42 PM UTC+1, Jack Vanlightly wrote:

[Stephan Merz]

Apologies for the typo – of course it should have been [N -> SUBSET R] and I should really have checked the definitions before sending them out. For the record, the spec below works as intended. I obtain 42 distinct states (for 80053 states computed overall) when declaring N and R as symmetry sets of 3, resp. 4 elements.

Regards,

Stephan

----------------------------- MODULE Allocation -----------------------------
EXTENDS Integers, FiniteSets, TLC

CONSTANT R, N
VARIABLE register

IsBalanced(reg) == \A m,n \in N : Cardinality(reg[m]) - Cardinality(reg[n]) \in {-1,0,1}

BalancedAllocations == { reg \in [N -> SUBSET R] : IsBalanced(reg) }

Init ==
  register = [n \in N |-> {}]

Rebalance ==
  /\ register' \in BalancedAllocations
  /\ PrintT(register')

Spec == Init /\ [][Rebalance]_register

=============================================================================

[Stephan Merz]

Oh, I see, you wish to assign resources to a unique node and to use all resources: that makes sense. (Note that in the first conjunct, the disjunct "m=n" is superfluous.)

By the way, another way to define this operator is to start by computing the number of resources that each node obtains in a balanced allocation. Which one you prefer is essentially a matter of taste. TLC may be able to evaluate the predicate below a little faster, but it must still enumerate all functions in [N -> SUBSET R].

IsBalanced(reg) ==
  LET k == Cardinality(R) \div Cardinality(N)
  IN  /\ \A n \in N : Cardinality(reg[n]) \in {k, k+1}
      /\ \A m,n \in N : m=n \/ reg[m] \cap reg[n] = {}

      /\ \A r \in R : \E n \in N : r \in reg[n]

Pushing this idea further, one can define the set of balanced allocations as

BalancedAllocations ==
  LET k == Cardinality(R) \div Cardinality(N)
      kSets == { S \in SUBSET R : Cardinality(S) \in {k, k+1} }
      Disjoint(reg) == \A m,n \in N : m=n \/ reg[m] \cap reg[n] = {}
      Surjective(reg) == (UNION { reg[n] : n \in N }) = R
  IN  { reg \in [N -> kSets] : Disjoint(reg) /\ Surjective(reg) }

and this definition definitely speeds up evaluation because now TLC only enumerates functions of type [N -> kSets], of which there are much fewer. Again, as long as model checking is not a real bottleneck, I'd prefer the definition that you gave because it is easier to understand.

Stephan

[Jack Vanlightly]

Hi,

Really cool stuff thanks. I suspect that model checking will be a bottleneck as this piece is part of a larger algorithm so the more efficient version may well prove critical. I've definitely learned new techniques so thanks.

Jack