Re: Checking prophecy variable constructions with TLC

[Giuliano <giulia...@xxxxxxx>]

Hello, do you have any reference to those attempts ?

On Tuesday, August 13, 2013 9:42:02 PM UTC+2, Leslie Lamport wrote:

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.

 

Leslie

 

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