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

*To*: TENEVA G Ms -NUCLEAR <galina.teneva@opg.com>*Subject*: RE: PVS Problem*From*: John Rushby <rushby@csl.sri.com>*Date*: Tue, 1 May 2001 10:10:20 PDT*Cc*: "'John Rushby'" <rushby@csl.sri.com>, pvs-help@csl.sri.com*In-Reply-To*: Your message of Tue, 1 May 2001 12:25:35 -0400*Sender*: pvs-help-owner@csl.sri.com

Dear Galina, > Just a small question: I have my user-defined strategy. It works > (thanks to your help). When I type it after the prompt "rule?" for > each theorem, in the *pvs* buffer there are details from the proof ( > which I need for documentation purposes). In the case I use (C-c C-p > U) or (M-x prut) commands a nice proof status appears, but in *pvs* > buffer the proof details are missing. Which command to use, that I > have the user-strategy applied to all theorems in the .pvs file and > also the proof details written in the *pvs* buffer/ .prf file? I > looked in the pvs-help, but didn't find anything helpful. I'm afraid there's no way to do this using PVS in the normal, interactive, way, but you can do it if you use PVS in batch mode. This is described in Chapter 5 of the PVS User guide. At verbose level 3, batch mode produces full details of proof replays. Note that the inner details of proof strategies are not given (neither interactively nor in batch) unless the strategies call their inner strategies in their $ form, and are themselves called in their $ form (see prover guide, page 14). You may need to tinker with this to get the level of detail you want. I'm cc'ing this to the pvs-help list in case it's useful to others. Regards, John

- Prev by Date:
**Re: PVS Problem** - Next by Date:
**Length of proof** - Prev by thread:
**Re: PVS Problem** - Next by thread:
**Substitution** - Index(es):