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

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

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

variables Pages = [n \in 1..NPAGES |-> [
|-> [count     |-> 0,
|-> NULL],
|-> 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

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


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.