[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

Sincerely
Young

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?

M.

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