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

Re: Checking prophecy variable constructions with TLC

Sorry for the delay in replying; I was on vacation.
The only work I remember is described at http://ls4-www.cs.tu-dortmund.de/RVS/P-TLA/welcome.html .

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?