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

[Ouyang Tsuna <tsunaouyang@xxxxxxxxx>]

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

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