5. Structured data

Structures

tuples and arrays are represented by sequences: <<v1, ... vN>>
string hashmaps are represented by "struct":
- define: struct = [a |-> 1, b |-> {}]
  - NOT: struct = ["a" |-> 1, "b" |-> {}]
- access: struct["a"] = 1 or struct.a = 1

To generate a set of structs, define a struct with some values being sets with cardinality > 1, like:

BankTransactionType == [acct: Accounts, amnt: 1..10, type: {"deposit", "withdraw"}]

NOTICE how Accounts, 1..10, and {"deposit", "withdraw"} are sets, not singular values.

Good: BankTransactionType == [acct: Accounts, amnt: 1..10, type: {"deposit"}]
Bad: BankTransactionType == [acct: Accounts, amnt: 1..10, type: "deposit"]

WARNING: cardinality of these types is geometric, so grows very fast. For this example, with just 3 accounts, the set already contains: 3 (accounts) * 10 (amount) * 2 (type) = 60 elements.

Getting their keys

Structures don't have a Len function, but the DOMAIN keyword.
DOMAIN is the set of all KEYS of a structure
Sequences and structures are both implemented on top of sets and functions, and Len is based on DOMAIN, not the other way around.

Functions

TLA+ functions are math functions, unrelated with programming functions.

The closest TLA+ has to programming functions are operators.

As math functions, they map values in one set to another set:

Example:

F == [x \in S |-> expr]
- F is a function
- S is the DOMAIN of the function ("domaine de définition", in French)
A sequence is a function where the DOMAIN is 1..n
A struct is a function here the DOMAIN is a set of strings

In this example:

---- MODULE core5_2_function ----
EXTENDS Integers, TLC, Sequences

Prod ==
  LET
    SL == 1..5
    SR == 5..10
  IN [p \in SL, q \in SR |-> p * q]

\* Here DOMAIN Prod == SL \X SR

\* Eval == Prod[<<3, 6>>]
Eval == Prod[3, 6] \* The arguments are represented as a tuple in both cases
====

Single-value functions

There is the TLC module shortcut for the case where the domain is a single value:

x :> y = [s \in {x} |-> y]

Function merging

If two functions share a "key", @@ from module TLC merges the two functions.

TruthTable == [p, q \in BOOLEAN |-> p => q]

Evaluates to

( <<FALSE, FALSE>> :> TRUE @@ <<FALSE, TRUE>> :> TRUE @@ <<TRUE, FALSE>> :> FALSE @@ <<TRUE, TRUE>> :> TRUE )

And their combinations allows us to rebuild structs and sequences:

Sequences: 1 :> "a" @@ 2 :> "b" = <<"a", "b">>
Structs: "a" :> 1 @@ "b" :> 2 = [a |-> 1, b |-> 2]

Using functions

Functions are not useful for computations: we use operators for that.

Functions are VALUES.

Function sets

A function set is written [S -> T] and reads:

every function where the domain is S and all of the values are in T

The cardinality of such a set is Cardinality(T) to the power Cardinality(S). For example: [1..n -> BOOLEAN] is the set of all binary strings of length n, and its cardinality is 2^n: Example for n = 2 (not TLA+ notation): 1, 2 -> F, F 1, 2 -> F, T 1, 2 -> T, T 1, 2 -> T, F

3.1 KiB Raw Permalink Blame History