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
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.