Attempted to select nonexistent field from the record construted from Java

30 views
Skip to first unread message

Ouyang Tsuna

unread,
Aug 4, 2021, 1:38:49 AM8/4/21
to tlaplus
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

Sincerely
Young


Markus Kuppe

unread,
Aug 4, 2021, 1:58:10 PM8/4/21
to tla...@googlegroups.com

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

Paulo Feodrippe

unread,
Aug 4, 2021, 2:43:45 PM8/4/21
to tla...@googlegroups.com
Hi Young,

Yes, I have done something similar, you can also ping me at https://twitter.com/pfeodrippe?s=09 if you want or open an issue in the tla-edn repo so we can discuss what you need (if the library does not provide it already).

Thanks for pinging me, Markus. 

Best o/

--
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+u...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/ce6447fe-c1fa-bb6f-f478-0e0f7dbab387%40lemmster.de.
Reply all
Reply to author
Forward
0 new messages