[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

Re: [tlaplus] The effect of symmetry sets on TLC performance

On Thursday, December 3, 2015 at 5:52:45 PM UTC+2, leuschel wrote:
Does the following capture your example ?

Yes, except that there is a next state where foo travels in some way over the set and bar maintains the mapping. In my actual model (the one with the profile), the mapping is an actual constant of the model (rather than any arbitrary constant variable), and I'm not interested in exploring the state space for all possible mappings.