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

Re: [tlaplus] The implementation of records and functions in TLC

Dear Hai Tran Thanh,

as others have answered before, TLC is meant for evaluating properties of finitary objects that arise in finite-state instances of specifications. In your example, neither FcnSet nor RcdSet are finitary values. The implementation of TLC makes different optimizations based on the kind of values (such as integers, functions or records). You appear to observe an optimization in the implementation of TLC that makes it evaluate successfully the equation about FcnSet (given that the right-hand side is textually identical to the definition of the operator), whereas an analogous optimization does not appear to be applied in the equation about RcdSet. I would consider this as an accidental difference and would not expect TLC to be able to evaluate any of the two equations.

However, note that TLC is able to successfully evaluate both predicates

  fcn \in FcnSet    and    rcd \in RcdSet

(i.e. when you comment out the equations in the type correctness predicates) and this is the essential capability for verifying type correctness of your specification.

Hope this helps,

On 20 Nov 2015, at 10:09, Hai Tran Thanh <thanhh...@xxxxxxxxx> wrote:

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[a] 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


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 



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

EXTENDS Integers


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 below error 

Attempted to enumerate a set of the form [l1 : v1, ..., ln : vn],
but can't enumerate the value of the `h1' field:
While 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


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

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 http://groups.google.com/group/tlaplus.
For more options, visit https://groups.google.com/d/optout.