Re: [tlaplus] Set within a set

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

On 12 Feb 2021, at 19:04, Anshu ranjan <a.ranjan.cool@xxxxxxxxx> wrote:

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.

--
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/187338c0-d08a-4bab-8b93-12ef87c69709n%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/88CD96D7-A5BF-4E1F-93BA-2A3815E31D73%40gmail.com.