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