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

*From*: mlj...@xxxxxxxxx*Date*: Tue, 16 Jan 2018 13:36:08 -0800 (PST)*References*: <fa294827-1ace-4045-929a-45c1b255dff2@googlegroups.com> <d0d6f597-357c-4495-a381-fe5c3d70a342@googlegroups.com>

Thank you for your help. I'm switching from Z to TLA, so still learning the differences between them.

在 2018年1月16日星期二 UTC-5下午4:16:30，saks...@xxxxxxxxxxxxxx写道：

在 2018年1月16日星期二 UTC-5下午4:16:30，saks...@xxxxxxxxxxxxxx写道：

It seems that it treats [a |-> b] as a record

>> [a |-> b] is a record. Valid access operation on this would be [a |-> b].a (or [a |-> b]["a"]). Note that a is a string here. So [a |-> b]["a"] = [a |-> b].a = b is true.

But my purpose is to add a tuple of (a, b) to the function f

>> This can be done like this: Add(a, b) == f' = [f EXCEPT![a] = b]. This is equivalent to f' = [x \in DOMAIN f |-> IF x = a THEN b ELSE f[x]].

I strongly recommend reading Lamport's Specifying Systems. Chapter 16 covers Functions and Records. Also, if I am not wrong, your TypeOK is incorrect. SUBSET [A -> B] is set of sets of functions in [A -> B]. So, f \subseteq [A -> B] means f is a set of some functions in [A -> B].

Regarding the initial question of defining a partial function, I'm not sure if syntax is available in TLA+ for partial functions, but I could be wrong. The way I specify this is:

CONSTANT None

ASSUME NoneNotInB == None \notin B

Init == f = [x \in A |-> None]

Add(a, b) == f' = [f EXCEPT![a] = b]

TypeOK == f \in [A -> B \cup {None}]

Or if you do not like None and want to express f as a set then,

Init == f = {}

Add(a, b) == f' = f \cup {[a |-> a, b |-> b]}

TypeOK == f \subseteq [a : A, b : B]

Hope this helps,

Saksham

On Tuesday, January 16, 2018 at 2:43:45 PM UTC-5, 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

**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):