Re: How to define a partial function and add an element to a set of functions in TLA+?

[mlj...@xxxxxxxxx]

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日星期二 UTC-5下午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 UTC-8, 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