TLA+ data model observations

[fhackett]

Here are some notes on invariants from TLA+ that might be useful when compiling to Go.

• "functions" can never grow or shrink their domain. This means that records will never gain members. It is an error to try to add a member to a record in TLC.
• this also applies to tuples, though the subtleties may make that situation a little more complex
• only finite sets can be iterated over according to TLC. an infinite set can be compiled to a predicate with no penalty. TLA+ supports a small number of predefined infinite sets that may be used.

[fhackett]

Update:

• sets of functions (generated using the [ a -> b ] syntax) are not iterable, and in fact cannot even be checked for membership if a or b is a non-enumerable set

[fhackett]

This has already been incorporated into PGo's design by this point.