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:
Int
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
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