| 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 =============================================================================
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 On Wednesday, January 16, 2019 at 5:35:42 PM UTC+1, Jack Vanlightly wrote: 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
--
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.
|