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

Re: [tlaplus] Checking prophecy variable constructions with TLC



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:

Hello,
when checking that a specification S1 implements a specification S2 I often
need to augment S1 with a prophecy variable, obtaining S1p.
However I quickly realized that adding prophecy variables is tricky.
I often make mistakes resulting in S1p having less behaviors than S1.
Therefore I would like to check with TLC that all behaviors of S1 are
also behaviors of S1p when the prophecy variable is hidden.
I think that it is not possible to do this with TLC. Am I correct?
Would it be realistic to try to implement a procedure to check formulas of the form S1 => \EE prophecy_var : S1p?

Giuliano

--
You received this message because you are subscribed to the Google Groups "tlaplus" group.
To unsubscribe from this group and stop receiving emails from it, send an email to tlaplus+u...@xxxxxxxxxxxxxxxx.
To post to this group, send email to tla...@xxxxxxxxxxxxxxxx.
Visit this group at http://groups.google.com/group/tlaplus.
For more options, visit https://groups.google.com/groups/opt_out.