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

*From*: Hai Tran Thanh <thanhh...@xxxxxxxxx>*Date*: Fri, 20 Nov 2015 01:12:47 -0800 (PST)*References*: <688c3da6-56e3-47df-a338-32235faf1f2a@googlegroups.com>

Hi all,

I am very sorry that I didn't say my questions clearly.

The first question is about the implementation of functions and records. I know that a record in TLA+ is also a function, but their implementation is different. The function evalAppl(...) of Tool.java has conditions:

case OPCODE_fa:{...if ((fval instanceof FcnRcdValue) ||

(fval instanceof FcnLambdaValue)) { ... }

else if ((fval instanceof TupleValue) ||

(fval instanceof RecordValue)) { ... }

...}

If the value of fval is from an _expression_ such as the function application, or f[1] with a function f = [ x \in {1, 2} |-> 1 ] , then fval is an instance of FcnRcdValue. And if the value of fval is from an _expression_ such as the record application, or rcd["f1"] with a record rcd = [ f1 |-> 1, f2 |-> 1 ], then fval is an instance of RecordValue. However, I don't know when fval is an instance of FcnLambdaValue.

The second question is about how TLC evaluates expressions when it can't evaluate all subexpressions. I just ran two "toy" examples

with TLC:

------------------------------- MODULE FcnSet -------------------------------

EXTENDS Integers

VARIABLE fcn

S == { 1, 2 }

FcnSet == [ S -> Int ]

Init == fcn = [ x \in S |-> 0 ]

Next == UNCHANGED fcn

Spec == Init /\ [Next]_fcn

TypeOK ==

/\ FcnSet = [ S -> Int ]

/\ fcn \in FcnSet

=============================================================================

and

------------------------------- MODULE RcdSet -------------------------------

EXTENDS Integers

VARIABLE rcd

RcdSet == [ h1 : Int, h2 : Int ]

Init == rcd = [ h1 |-> 0, h2 |-> 0 ]

Next == UNCHANGED rcd

Spec == Init /\ [Next]_rcd

TypeOK2 ==

/\ RcdSet = [ h1 : Int, h2 : Int ]

/\ rcd \in RcdSet

=============================================================================

TLC didn't show any error for the first example. However, for the second one, I received the error

Attempted to enumerate a set of the form [l1 : v1, ..., ln : vn],but can't enumerate the value of the `h1' field:IntWhile working on the initial state:rcd = [h1 |-> 0, h2 |-> 0]

And I don't know why TLC tries to enumerate RcdSet, but not FcnSet. If I remove the _expression_ of RcdSet from TypeOK2, now there is no error. Moreover, if I change the definition of RcdSet to a set of functions from a finite set of strings to integers as following, again no error. I want to ask why TLC needs to change its behavior when evaluating the set of records.

------------------------------ MODULE RcdSet1 ------------------------------

EXTENDS Integers

VARIABLE rcd

S == { "h1", "h2" }

RcdSet == [ S -> Int ]

Init == rcd = [ h1 |-> 0, h2 |-> 0 ]

Next == UNCHANGED rcd

Spec == Init /\ [Next]_rcd

TypeOK3 ==

/\ RcdSet = [ S -> Int ]

/\ rcd \in RcdSet

=============================================================================

Thank you very much,

Thanh Hai

**Follow-Ups**:**Re: [tlaplus] The implementation of records and functions in TLC***From:*Stephan Merz

**References**:**The implementation of records and functions in TLC***From:*Hai Tran Thanh

- Prev by Date:
**Re: [tlaplus] some help needed in running tlc in distributed mode** - Next by Date:
**Re: [tlaplus] The implementation of records and functions in TLC** - Previous by thread:
**Re: The implementation of records and functions in TLC** - Next by thread:
**Re: [tlaplus] The implementation of records and functions in TLC** - Index(es):