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

*From*: Andrew Helwer <andrew...@xxxxxxxxx>*Date*: Tue, 16 Jan 2018 13:23:10 -0800 (PST)*References*: <fa294827-1ace-4045-929a-45c1b255dff2@googlegroups.com>

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:

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

**Follow-Ups**:

**References**:

- Prev by Date:
**Re: How to define a partial function and add an element to a set of functions in TLA+?** - Next by Date:
**Re: How to define a partial function and add an element to a set of functions in TLA+?** - Previous by thread:
**Re: How to define a partial function and add an element to a set of functions in TLA+?** - Next by thread:
**Re: How to define a partial function and add an element to a set of functions in TLA+?** - Index(es):