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.