Re: Paramaterized Instantiation and Universal Quantification

[Adam Shimi <hardke...@xxxxxxxxx>]

Hi again,

Sorry to keep bothering you, but I would really like to know "how much" of parameterized instanciation is not implemented in TLC.

Because TLASany let me write such instantiations, and in all my tests (the toy example above as well as the actual speficification, which now works thanks to Stephan's idea), TLC actually model check my specification correctly.

One possibility I thought about is that TLC would conflate the variables if the same instanciation is used with different ones, and somehow mess with the result. Is it the case ?

Thanks in advance and have a good day.

Adam