[tlaplus] Set vs Functions for modelling

["thisismy...@xxxxxxxxx" <thisismyidashish@xxxxxxxxx>]

Hi

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

Thanks

Ashish

-- 
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/c9b89fe7-8c0d-41dd-9d7a-d33b7b2287d8n%40googlegroups.com.