Thank you Stephan. This makes sense.--On Thursday, October 26, 2023 at 2:12:33 AM UTC-5 Stephan Merz wrote:Hello,writing a formal specification in a language such as TLA+ is different from writing a program. In particular, efficiency is (in principle) not a concern. From what I understand, you want to maintain a set of records such that when inserting a record, you overwrite any existing record with the same key. One way to define such an insert operation is(* Insert record rcd in set S but overwrite any existing record in S with the same key *)InsertWithUpdate(S, rcd) ==(S \ {r \in S : r.key = rcd.key}) \union {rcd}A similar operation can be defined on sequences, but it is a little more cumbersome and will have to be recursive.The easiest way to denote the function with the empty domain in TLA+ is to write << >>. Remember that sequences are functions, too.Hope this helps,StephanOn 25 Oct 2023, at 01:06, thisismy...@xxxxxxxxx <thisismy...@xxxxxxxxx> wrote:HiIn last few specs that i wrote, i naturally start with using set of records for variables like set of files. Then i hit the problem that i need to deduplicate these sets based on key field of record.e.g. for set: {[fileId: Nat, cleanupTime: Nat]}, when i insert {fileId:1, cleanupTime: 2} and {fileId:1, cleanupTime: 3}, i don't want to have 2 items in set but only one. I want set to look at `field` fileId as key for set.Is this possible ? From my search, i could not find this.Then i move to using sequences and writing AppendIfNotPresent(s, x) functions myself.I realized that since sequence is a function, can i create a function [fileId |-> record] ? and then updating same fileID can't insert 2 records.I believe someone already thought about this. What are cons of this approach ?About using function, I got stuck at initializing variables with an empty function in pluscal. How do I create an empty function ?ThanksAshish--
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...@xxxxxxxxxxxxxxxx.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/c9b89fe7-8c0d-41dd-9d7a-d33b7b2287d8n%40googlegroups.com.
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/35a76524-49d1-41ae-afd7-52289c6ef2ccn%40googlegroups.com.