[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

Re: [tlaplus] Re: Simpler method of making multiple changes to a function in a single step

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.


----------------------------- MODULE Allocation -----------------------------
EXTENDS Integers, FiniteSets, TLC
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


On 16 Jan 2019, at 20:57, Jack Vanlightly <vanli...@xxxxxxxxx> wrote:


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

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.


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

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
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 
                IF Cardinality(pendingRes) = 0 THEN newRegister
                    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

- 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.


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...@xxxxxxxxxxxxxxxx.
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.