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

[Markus Kuppe <tlaplus-google-group@xxxxxxxxxxx>]

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.