Home Intro Announce FAQ Docs Download Mail Status Bugs Users Related FM Tools

PVS Bug 654


Synopsis:        Context corruption?
Severity:        serious
Priority:        medium
Responsible:     owre
State:           open
Class:           sw-bug
Arrival-Date:    Wed Jan 16 14:36:36 2002
Originator:      Jerry James
Organization:    eecs.ku.edu
Release:         PVS 2.4
Environment: 
 System:          
 Architecture: 

Description: 
  I am having a perplexing problem with a set theory library that I have
  developed (see <URL:http://www.ittc.ku.edu/~james/research/pvs.html>).
  All attempts at distilling the problem down to something smaller have
  failed so far.  I am using PVS 2.4.1 with XEmacs 21.4.6 on a RedHat
  Linux 7.1 machine.
  
  In the following, when I say "transition to context X", I mean any of
  the following:
    (1) Exit PVS and restart it in the directory for context X.
    (2) M-x change-context and enter the name of the directory containing
        context X.
    (3) M-x save context on the current context, then M-x change-context
        and enter the name of the directory containing context X.
  The problem occurs regardless of which of the three methods of changing
  context is used.
  
  The problem occurs with the number and infinite_sets collections in that
  library.  If you download the library, you will find that the minimum,
  and maximum theories in the number collection have all formulas marked
  "unchecked".  C-c C-p f proves them in each case.  Now transition to the
  infinite_sets collection.  C-c C-f infinite_power; M-x
  status-proof-pvs-file shows that all of the formulas are proved, but 3
  are incomplete; this is due to the "unchecked" theories in number.  M-x
  status-proofchain-importchain shows that this is because the rank theory
  in the number collection is unproved.  Okay, so transition back to the
  number collection, load rank, and C-c C-p f.  It shows that all formulas
  are proved, but incomplete.  This is because the minimum and maximum
  theories in the number collection are once again have all formulas
  marked "unchecked"!  Okay, so we prove them again, and now rank is
  completely proved.  Transition back to the infinite_sets collection and
  check the infinite_power theory again.  It *still* says that three of
  the formulas are proved, but incomplete.  Why?  Because the rank,
  minimum, and maximum theories in the number collection once again have
  all formulas marked "unchecked"!
  
  Around, and around, and around we go...
  
  Random observations that may or may not help:
  
    (1) The same problem occurs with the infinite_sets_ops theory in the
        infinite_sets theory.
  
    (2) This problem used to occur with the bits, minimum, and maximum
        theories.  Sometime during my repeated rounds of proving and
        changing contexts, rank took the place of bits.  I don't know
        why.
  
    (3) Sometimes, PVS reports that it is deleting some .bin files, but
        doesn't say why it is doing so.  I cannot get it to do so every
        time.
  
    (4) Sometimes, PVS generates lots of messages that say something like
        this: "Can't restore [path]", "Can't delete [path]".  In such
        cases, the path is to a file in another collection in the set
        theory library, the file exists, is owned by me, and is both
        readable and writable by me.  I cannot get PVS to reliably
        reproduce this behavior either.
  
    (5) Proving the importchain doesn't help, since it only proves other
        theories in the same context, and this is a cross-context
        problem.  If there is another command that is appropriate for this
        situation, please let me know!
  
    (6) I suspected that the problem might be due to corrupted .pvscontext
        files, so I created new contexts and imported every last file in
        the entire library to the new contexts and proved them, one by
        one.  That didn't help.
  
  Any solutions or workarounds will be very gratefully received, as I need
  this library to support some other work I am doing.
  -- 
  Jerry James
  Assistant Professor
  EECS Department
  University of Kansas
  

How-To-Repeat: 

Fix: 
Home Intro Announce FAQ Docs Download Mail Status Bugs Users Related FM Tools