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

Re: [PVS-Help] PVS batch mode



Hello all,
I try to work on batch.el and batch.pvs as follows:

------batch.el----
(pvs-validate "batch.log" "~/Batch")
(pvs-message "Proving batch")
(typecheck "batch")
(let ((current-prefix-arg t))
 (prove-untried-theory "batch" "(grind)"))
(status-proof-theory "test")
(pvs-message "Completed")

-------batch.pvs---
batch: THEORY
BEGIN
x: VAR real
batch: LEMMA x > 1 IMPLIES x > 0
END batch

Then I run:
>pvs -batch -load batch.el -v 3

The results make me confused, so, I have some questions below:
Question 1) As I expected, PVS needs to display the result in
"batch.log"  as I declared in "batch.el" ? But in "batch.log", it
displays only the content:
"PVS Version 3.1
Context changed to ~/Batch/"

And all the resulting, it displays to the terminal, for e.g, it
dispalys the following to the terminal:
batch :
  |-------
{1}   FORALL (x: real): x > 1 IMPLIES x > 0

Rerunning step: (grind)
Trying repeated skolemization, instantiation, and if-lifting,
Q.E.D.

Question 2) When the batch process finishes, it automatically
generates the file "batch.prf". However, when I attempt to change the
content of "batch.pvs" file and then run batch again, the content of
"batch.prf" does not change and there is a warning in the terminal
"Every attempted formula of theory batch has an existing proof and
failed to prove with the given strategy.No formulas attempted"

Is there any way if I change the content of specification file
'batch.pvs" and run batch, the file ".prf" and ".log" is automatically
updated?

Thanks for any help.

S.



On 9/8/06, Sam Owre <owre@csl.sri.com> wrote:
> Hi Sara,
>
> For that you need to do two things; first, add a command to
> prove-all.el to display the information you want, for
> example
>
> (status-proof-theory "test")
>
> Then you need to invoke PVS with the verbosity argument set
> above 0 - I usually set it to 3.  Just add '-v 3' to your
> invocation of pvs - anywhere after the '-batch' flag.
>
> Regards,
> Sam
>
>
> Sara Kenedy <sarakenedy@gmail.com> wrote:
>
> > Thanks a lot for Sam to recognize the error for me. However, I do not
> > know why it des not display the result after using the strategy
> > "GRIND". (Sorry if the question seems so "baby")
> >
> > I fix the error, and try it again.
> >
> > ----------------prove-all.el------------------
> > (pvs-message "Proving all unproven theorems in batch.pvs")
> > (typecheck "batch")
> > (let ((current-prefix-arg t))
> >  (prove-untried-pvs-file "batch" "(grind)"))
> > (pvs-message "Completed")
> > -----------------batch.pvs----------------------------
> > batch: THEORY
> > BEGIN
> >
> >   a : theorem  1 < 2
> >   b : theorem  2 < 3
> >   c : theorem  3 < 4
> >   d : theorem  4 < 5
> >
> > END batch
> >
> > > pvs -batch -load prove-all.el
> > Loading /usr/lib/xemacs/xemacs-packages/lisp/site-start.d/psgml-init.el...
> > Loading pvs-load...
> > Loading pvs-prelude-files-and-regions...
> > Proving all unproven theorems in batch.pvs
> > Proving all unproven theorems in batch.pvs
> > Completed
> > Completed
> >
> > Proving all unproven theorems in batch.pvs
> > Completed
> >
> > (No files need saving)
> > Buffer *scratch* has no process
> >
> >
> >
> > On 9/8/06, Sam Owre <owre@csl.sri.com> wrote:
> > > Hi Sara,
> > >
> > > I see the problem - the
> > >
> > > (pvs-message "Completed)
> > >
> > > is missing the closing string quote - it should be:
> > >
> > > (pvs-message "Completed")
> > >
> > > Sam
> > >
>