Hi,assuming that you want to fix the counter and the type initially, you probably want to write something along the following lines:define {  InitPageType == [count : {0}, type : {NULL}]  InitPage == [type : InitPageType, content : Content]}variable Pages \in [ (1 .. NPAGES) -> InitPage ]In particular, "[a : A, b : B]" is the set of records with two fields a' and b' with values in sets A and B, and [X -> Y] is the set of functions that map elements of domain X to values in Y.Hope this helps,StephanOn 21 Aug 2019, at 14:52, dunlapg@xxxxxxxxx wrote:I'm working on modeling a "typed" refcounting system.  One of thethings the refcounting system has to do, before granting a type on thepage, is look at the page and determine if the contents of the pageare suitable for the type.Right now I have "page array" structure that looks something likethis:variables Pages = [n \in 1..NPAGES |-> [               type      |-> [count     |-> 0,                              type      |-> NULL],               content   |-> NULL]];Here the content field is meant to be a model to say whether thepage contains content suitable for the type in question.I'd ideally like TLA to experiment with different starting valueshere; i.e., so that if NPAGES = 2, I end up running with the followingruns:<<[content |-> A], [content |-> A]>><<[content |-> B], [content |-> A]>><<[content |-> C], [content |-> A]>><<[content |-> A], [content |-> B]>><<[content |-> B], [content |-> B]>>...<<[content |-> C], [content |-> C]>>I know I can something like the following:variables content \in {A, B, C};Then TLA will (as I understand it) run the model three times, oncewith content set to A, once with content set to B, and so on.  IfI'd like to be able to do the same thing with that element in astructure in an array.  I've been trying to play around with thesyntax but haven't been able to figure it out.I could always have an "init" process start out in a random state(using eitiher or with), and have the "test" processes wait untilthat process had finished, but that seems inelegant.Thanks, -George -- 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+unsubscribe@xxxxxxxxxxxxxxxx. To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/f37bb466-9413-4afb-8acd-d082f68280e3%40googlegroups.com. -- 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+unsubscribe@xxxxxxxxxxxxxxxx. To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/3BAB2CF3-F89B-4A52-87CF-ACABCB4E8451%40gmail.com.