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

PVS Bug 1055


Synopsis:        error in treatment of pairs
Severity:        serious
Priority:        medium
Responsible:     owre
State:           open
Class:           sw-bug
Arrival-Date:    Thu Jun 10 02:05:00 -0700 2010
Originator:      Hesselink
Release:         PVS 4.2
Organization:    rug.nl
Environment: 
 System:          
 Architecture: 

Description: 
  This is a multi-part message in MIME format.
  --------------000708010109010209070001
  Content-Type: text/plain; charset=ISO-8859-1
  Content-Transfer-Encoding: 7bit
  
  Dear Sam,
  
  The lemma in the attached file generates an error when trying to prove
  it with
  tab G ; tab E.
  
  Best regards,
  Wim
  
  -- 
  Wim H. Hesselink  
  
  Dept. of Computing Science       /   Bernoulliborg, office 374 
     University of Groningen      /    Nijenborgh 9, 9747 AG
                 P.O.Box 407     /     phone +31 50 3633933 (or *3939)
           9700 AK Groningen    /      fax   +31 50 3633800
             The Netherlands   /       http://www.cs.rug.nl/~wim
  
  
  --------------000708010109010209070001
  Content-Type: text/plain;
   name="errordump"
  Content-Transfer-Encoding: 7bit
  Content-Disposition: inline;
   filename="errordump"
  
  
  %% PVS Version 4.2 - Allegro CL Enterprise Edition 8.1 [Linux (x86)] (Jul 22,
  2008 3:35)
  %% 8.1 [Linux (x86)] (Jul 22, 2008 3:35)
  $$$errorPair.pvs
  % W.H. Hesselink, June 2010
  errorPair[N: posnat, R: posnat]: THEORY
  BEGIN
  
  Thread: TYPE = below(N)
  allThreads: finite_set[Thread] = fullset[Thread]
  
  Version: TYPE = below(R)
  
  Pair: TYPE = [Thread, Version]
  
  kk: VAR Pair
  
  state: TYPE = [#
    % shared state
    cc: pred[Thread],
    turn: finite_set[Pair],
    shacnt, nondet: nat,
    predec: [Thread -> setof[Thread]],
    % private state
    turnset, copy: [Thread -> finite_set[Pair]],
    pc, cnt, thr, fupb: [Thread -> nat],
    kk: [Thread -> Pair],
    nx: [Thread -> Version]
  #]
  
  p, q, r: VAR Thread
  x, y: VAR state
  k: VAR Pair
  
  er: LEMMA
    x WITH [`turnset(p)(k):= false]`turnset(p) = remove(k, x`turnset(p))
  
  END errorPair 
  
  -.-.-
  Below I have inserted *pvs* because the dump did not save my proof
  
  Starting pvs-allegro -qq ...
  Allegro CL Enterprise Edition
  8.1 [Linux (x86)] (Jul 22, 2008 3:35)
  Copyright (C) 1985-2007, Franz Inc., Oakland, CA, USA.  All Rights Reserved.
  
  This dynamic runtime copy of Allegro CL was built by:
     [TC8102] SRI International - Lynn Bliss
  
  ;; Optimization settings: safety 1, space 1, speed 3, debug 1.
  ;; For a complete description of all compiler switches given the
  ;; current optimization settings evaluate (explain-compiler-settings).
  ;;---
  ;; Current reader case mode: :case-sensitive-lower
  
  pvs(1): 
  pvs(2): 
  Installing rewrite rule singleton_rew
  
  
  
  
  er :  
  
    |-------
  {1}   FORALL (k: Pair, p: Thread, x: state):
          x WITH [`turnset(p)(k) := FALSE]`turnset(p) =
           remove(k, x`turnset(p))
  
  Rerunning step: (grind)
  Trying repeated skolemization, instantiation, and if-lifting,
  this simplifies to: 
  er :  
  
  {-1}  p!1 < N
    |-------
  {1}   x!1`turnset(p!1) WITH [(k!1) := FALSE] = remove(k!1, x!1`turnset(p!1))
  
  
  
  Rerunning step: (postpone)
  Postponing er.
  
  er :  
  
  {-1}  p!1 < N
    |-------
  {1}   x!1`turnset(p!1) WITH [(k!1) := FALSE] = remove(k!1, x!1`turnset(p!1))
  
  Rule? (apply-extensionality  :hide? t)
  Error: the assertion (compatible? (type lhs) (type rhs)) failed.
    [condition type: simple-error]
  
  Restart actions (select using :continue):
   0: retry assertion.
   1: Return to Top Level (an "abort" restart).
   2: Abort entirely from this (lisp) process.
  [1] pvs(18): :continue 1
  
  
  
  
  Run time  = 0.06 secs.
  Real time = 125.20 secs.
  pvs(23): 
  
  --------------000708010109010209070001--

How-To-Repeat: 

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