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

*From*: Stephan Merz <stephan.merz@xxxxxxxxx>*Date*: Wed, 21 Aug 2019 15:00:57 +0200*References*: <f37bb466-9413-4afb-8acd-d082f68280e3@googlegroups.com>

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+unsubscribe@xxxxxxxxxxxxxxxx. To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/3BAB2CF3-F89B-4A52-87CF-ACABCB4E8451%40gmail.com. |

**Follow-Ups**:

**References**:

- Prev by Date:
**[tlaplus] Creating an array of structures whose elements have different starting conditions** - Next by Date:
**Re: [tlaplus] Scope of the QED keyword** - Previous by thread:
**[tlaplus] Creating an array of structures whose elements have different starting conditions** - Next by thread:
**Re: [tlaplus] Creating an array of structures whose elements have different starting conditions** - Index(es):