Hello, your assumption is correct: in general TLC doesn't support checking formulas involving the \EE quantifier over flexible (state) variables. Instead of checking F => \EE x : G(x) you have to ask TLC to check F => G(e) where e is the "witness" for the inner variable (the refinement mapping). Unfortunately, it is hard or impossible to explicitly define the values of a prophecy variable, even for a finite-state system, so this doesn't work for you. It would be nice if TLC could check the existence of the variable without you having to construct it. In principle, the problem is decidable for finite-state systems, and one could try implementing this for restricted classes of formulas that limit the search to a finite domain, as is typically the case with history and prophecy variables. Doing this in a way that would work in practice looks to me like a significant (but worthwhile) challenge. Stephan On Aug 12, 2013, at 3:53 PM, Giuliano <giulia...@xxxxxxx> wrote:
|