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

*From*: Adam Shimi <hardke...@xxxxxxxxx>*Date*: Fri, 19 May 2017 05:44:50 -0700 (PDT)*References*: <b60fab65-1be5-40a4-ae73-05d61de7a616@googlegroups.com> <60b8c405-582e-41fd-857b-c807db1b3ffa@googlegroups.com>

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

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

**Follow-Ups**:**Re: Paramaterized Instantiation and Universal Quantification***From:*Adam Shimi

**References**:**Paramaterized Instantiation and Universal Quantification***From:*Adam Shimi

**Re: Paramaterized Instantiation and Universal Quantification***From:*Leslie Lamport

- Prev by Date:
**Re: Paramaterized Instantiation and Universal Quantification** - Next by Date:
**TLC not handling disjunction correctly in special case?** - Previous by thread:
**Re: Paramaterized Instantiation and Universal Quantification** - Next by thread:
**Re: Paramaterized Instantiation and Universal Quantification** - Index(es):