Set within a set

25 views
Skip to first unread message

Anshu ranjan

unread,
Feb 12, 2021, 1:04:34 PM2/12/21
to tlaplus
I was wondering if it is possible to have a set within a set. I am looking for something like this:

cache = {{value1, valueIdx1, timestamp1}, {value2, valueIdx2, timestamp2} ... }

I tried to init cache using something like this:
cache = [ t \in 1..totalTime |-> {0, 0, 0} ]

The init works fine. But when I check for something like
cache[0]["value1"] < cache[1]["value1"]

I get an error saying applying function to a non function. 

Any help is appreciated. 

Stephan Merz

unread,
Feb 12, 2021, 1:19:57 PM2/12/21
to tla...@googlegroups.com
Hello,

as you observed, nesting sets poses no problem. However, I don't think this is what you really are after.

First of all, observe that {0,0,0} = {0}.

It seems to me that you intend to associate values with indexes and time stamps. So a cache entry (for a given value) could be modeled as a record

CacheEntry == [index : Nat, timestamp : Time]

and the cache can be modeled as a function from values to cache entries

Cache == [ Value -> CacheEntry ]

We can now define the initial condition as

cache = [ v \in Value |-> [index |-> 0, timestamp |-> 0] ]

and you can write something like

cache[v1].index < cache[v2].index

for comparing the index values for cache entries for values v1 and v2.

Hope this helps,
Stephan


--
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...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/187338c0-d08a-4bab-8b93-12ef87c69709n%40googlegroups.com.

Anshu ranjan

unread,
Feb 12, 2021, 1:33:12 PM2/12/21
to tla...@googlegroups.com
Great, that's exactly what I was looking for. Thanks a lot.

Reply all
Reply to author
Forward
0 new messages