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

Re: Checking prophecy variable constructions with TLC

I have heard of two attempts to implement model checking of properties of the form \EE x : G(x).  I believe that neither of them was able to handle any but the most trivial of examples.  If you think about what is required to check such a property, you will understand why.

On Monday, August 12, 2013 5:53:10 AM UTC-8, Giuliano wrote:
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?