Re: Paramaterized Instantiation and Universal Quantification

Hi again,

Stephan :

In fact, I did not read carefully enough your previous answer : I thought you could only define the next-state value of a function by specifying all the function in one declaration (hence my comment about the atomic part). Since it is apparently possible to define values of the function one by one (as long as TLC knows the domain and all the value of the function in the domain, before the end of the next-state computation), I can probably use it. Thanks again for the tip !

Also, thanks for the answer to my other question.

Leslie :

Hum, but my toy example (with t's definition replaced by the one in the comment) actually use parameterized instantiation, and yet TLC behave exactly as it should (generates the good states and checks the temporal property). Is it because my example is so ridiculously simple ?

Also, is there a conceptual reason why parameterized instantiation are not handled (meaning is it conceptually hard to find an algorithm to do so) or is it simply a feature missing by lack of time and manpower ?

Thanks in advance.

Adam