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

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

On 8/3/21 10:38 PM, Ouyang Tsuna wrote:
Recently I want to import some datas into TLA+ format so I construct a Java class to handle it. The class is in EdnHistoryReaderExt <https://github.com/Tsunaou/CommunityModules/blob/master/modules/tlc2/overrides/EdnHistoryReaderExt.java>
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


Hi Young,

do not create your own util.InternTable on line 31 in EdnHistoryReaderExt . Create instances of UniqueString via UniqueString.of :

final static UniqueString[] names = { UniqueString.of("type"), UniqueString.of("key"), UniqueString.of("value") };

By the way, perhaps you and Paulo Feodrippe want to work together to evolve and contribute Paulo's tla-end [1] to the CommunityModules for broader reach?


[1] https://github.com/pfeodrippe/tla-edn

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/ce6447fe-c1fa-bb6f-f478-0e0f7dbab387%40lemmster.de.