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

*From*: Jack Vanlightly <vanli...@xxxxxxxxx>*Date*: Wed, 16 Jan 2019 11:57:48 -0800 (PST)*References*: <2fc795d1-9680-465f-bf49-7c806920c0a8@googlegroups.com>

Hi,

*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"*

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

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, TLCCONSTANT R, NVARIABLE registerInit ==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 pendingResIN CHOOSE x \in int : TRUEINIF Cardinality(pendingRes) = 0 THEN newRegisterELSELET 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]_registerNotes:- 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.ThanksJack

**Follow-Ups**:

**References**:**Simpler method of making multiple changes to a function in a single step***From:*Jack Vanlightly

- Prev by Date:
**Re: [tlaplus] Simpler method of making multiple changes to a function in a single step** - Next by Date:
**Re: Simpler method of making multiple changes to a function in a single step** - Previous by thread:
**Re: [tlaplus] Simpler method of making multiple changes to a function in a single step** - Next by thread:
**Re: [tlaplus] Re: Simpler method of making multiple changes to a function in a single step** - Index(es):