Creating an array of structures whose elements have different starting conditions

[dun...@gmail.com]

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

[Stephan Merz]

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,

Stephan

--
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...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/f37bb466-9413-4afb-8acd-d082f68280e3%40googlegroups.com.

[dun...@gmail.com]

Ah, great -- that did the trick, and is much easier than the convoluted things I was trying to do.  Many thanks!

 -George