I'm working on modeling a "typed" refcounting system. One of the
things the refcounting system has to do, before granting a type on the
page, is look at the page and determine if the contents of the page
are suitable for the type.
Right now I have "page array" structure that looks something like
this:
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 the
page contains content suitable for the type in question.
I'd ideally like TLA to experiment with different starting values
here; i.e., so that if NPAGES = 2, I end up running with the following
runs:
<<[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, once
with `content` set to A, once with `content` set to B, and so on. If
I'd like to be able to do the same thing with that element in a
structure in an array. I've been trying to play around with the
syntax 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 until
that process had finished, but that seems inelegant.
Thanks,
-George