Re: [tlaplus] Creating an array of structures whose elements have different starting conditions

On 21 Aug 2019, at 14:52, dunlapg@xxxxxxxxx wrote:

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

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