Hello,
one of the differences between the set theories underlying Z (or B / EventB) and TLA+ lies in the representation of functions. In TLA+, functions are primitive (i.e., not defined as sets of pairs), they always total, and they have an explicit domain. In your original posting you said that you want to represent a partial function f from A to B. There are two ways to do so in TLA+:
1. As suggested by Saksham, represent f as a total function from A to B \cup {None} with a null value None. In order to test if f is defined for some a \in A, you write f[a] # None.
2. Represent f as a function from a subset of A to B. The operator
PFun(S,T) == UNION { [ AS > T ] : AS \in SUBSET S }
defines the set of partial functions in this representation. Your operators can then be written as follows
TypeOK == f \in PFun(A,B) Init == f = [x \in {} > {}] Add(a,b) == f' = (a :> b) @@ f \* need to EXTEND TLC
Note that in the definition of Init, the value on the righthand side of the arrow is irrelevant (you could also use some value of B, perhaps write CHOOSE b \in B : TRUE). Because the function with empty domain also represents the empty sequence, you can alternatively write
Init == f = << >>
but this is perhaps a little obscure. The operators :> and @@ that appear in the definition of Add are defined in the TLC module. In this approach, you write
a \in DOMAIN f
in order to test if the function is defined for a.
Which of the two approaches you prefer depends on taste and sometimes on how TLC evaluates expressions: you don't want TLC to enumerate the set PFun(A,B), although testing if f \in PFun(A,B) holds (as in evaluating the typing invariant) is fine.
Regards, Stephan
Now, I understand that I should use \in instead of \subseteq in TypeOK. Declaring a Null value will solve my question, but I still feel a little bit strange.
In Z, we often use partial functions and define an "Add" function to add new elements. But it looks like we should use total functions and update values in functions in TLA+. 在 2018年1月16日星期二 UTC5下午4:20:14，Andrew Helwer写道： You are correct that functions can be represented as sets of
tuples, but in TLA+ they are instead represented as a record. The two
representations are equivalent. Use this syntax to define f on a new
input value:
Add(a, b) == f' = [f EXCEPT ![a] = b]
Unfortunately, this makes your TypeOK a bit weird  your function f does not start off as a member of the set [A > B]. You should define a Null value as follows:
Null == CHOOSE b : b \notin B
TypeOK == f \in [A > B \cup {Null}]
Init == f = [a \in A > Null]
On Tuesday, January 16, 2018 at 11:43:45 AM UTC8, mlj...@xxxxxxxxx wrote: Hi guys,I've met some problems of function definitions. For instance, in math, I've got two sets A and B; and I'd like to define a partial function f as A > B. Also, I want to define an operation that adding an element to the set, like f' = f \cup {(a, b)}, where a \in A and b \in B. So in TLA+, I tried to write the spec like: CONSTANT A, B VARIABLES f TypeOK == f \subseteq [A > B] Init == f = {} Add(a, b) == f' = f \cup {[a > b]} Next == \E a \in A, b \in B : Add(a, b) However, I got errors when running model checking in TLC. It seems that it treats [a > b] as a record. But my purpose is to add a tuple of (a, b) to the function f, where f should be a set of tuples as it defined in math, like {(a1, b1), (a2, b2)}. So how can I write it in TLA+? Best Regards, Changjian Zhang

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...@xxxxxxxxxxxxxxxx.
To post to this group, send email to tla...@xxxxxxxxxxxxxxxx.
Visit this group at https://groups.google.com/group/tlaplus.
For more options, visit https://groups.google.com/d/optout.
