Re: [tlaplus] Set vs Functions for modelling

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,
Stephan

On 25 Oct 2023, at 01:06, thisismy...@xxxxxxxxx <thisismy...@xxxxxxxxx> wrote:

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+u...@xxxxxxxxxxxxxxxx.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/c9b89fe7-8c0d-41dd-9d7a-d33b7b2287d8n%40googlegroups.com.