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

[tlaplus] Attempted to select nonexistent field from the record construted from Java

Recently I want to import some datas into TLA+ format so I construct a Java class to handle it. The class is in EdnHistoryReaderExt
But when I use it in TLA+, there are some exceptions like this

> The `Evaluate Constant _expression_ sections evaluation failed.
Attempted to select nonexistent field "type" from the record
[type |-> "read", key |-> "x", value |-> 1]

What I want to do is just construct a record by reading files. The TLA+ definition is as following:

Key == Range("abcdefghijklmnopqrstuvwxyz") \* We assume single-character keys.
Val == Nat      \* We assume values from Nat.
InitVal == 0    \* We follow the convention in POPL'2017.
Oid == Nat      \* We assume operation identifiers from Nat.

Operation == [type : {"read", "write"}, key : Key, val : Val, oid : Oid]
R(k, v, oid) == [type |-> "read", key |-> k, val |-> v, oid |-> oid]
W(k, v, oid) == [type |-> "write", key |-> k, val |-> v, oid |-> oid]

Simply, I want to generate a R(1, 1, 1) or W(1, 1, 1) record and I need to define type by myself. In RecordValue, type is one of the members of `names[]` and each member is an instance of UniqueString. However, UniqueString has 5 filed incluing internTbl, s, tok, loc and s, but I cound not figure out what they means? Could anybody help me?

Thank you very much


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+unsubscribe@xxxxxxxxxxxxxxxx.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/fcf8ab68-3a55-498e-a0f7-1db2c02c2844n%40googlegroups.com.