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