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

PVS Bug 1070


Synopsis:        Pretty-printer bug
Severity:        serious
Priority:        medium
Responsible:     owre
State:           open
Class:           sw-bug
Arrival-Date:    Sat Oct 02 17:00:01 -0700 2010
Originator:      Erik Martin-Dorel
Release:         PVS 4.2
Organization:    ens-lyon.fr
Environment: 
 System:          
 Architecture: 

Description: 
  This is a multi-part message in MIME format.
  --------------050506010805030402070002
  Content-Type: text/plain; charset=ISO-8859-1; format=flowed
  Content-Transfer-Encoding: 8bit
  
  Hi,
     
  When I do [M-x ppe RET imputations RET] on the (third) theory in the
  attached PVS file, the pretty-printer dies with the following error:
  
  Error: The term
          #!(JUDGEMENT-ELT (JUDGEMENT (JDECLS (JAPPLDECL (NAME (IDOP ((:id sum)
 )) (NOLIB) (NOACTS) (NOMOD) (NOMAP) (NOTGT)) (PDF (ADFORMALS (TYPED-ID (IDOP (
 (:id A))) (TYPE-NAME (NAME (IDOP ((:id finite_set))) (NOLIB) (ACTUALS (TUPLE-E
 XPR (NAME-EXPR (NAME (IDOP ((:id N))) (NOLIB) (NOACTS) (NOMOD) (NOMAP) (NOTGT)
 )))) (NOMOD) (NOMAP) (NOTGT))) (NO-PRED)) (TYPED-ID (IDOP ((:id f))) (FUNTYPE 
 (COMP-TYPE-EXPR-NULL-1) (DOM (EXPR-AS-TYPE (NAME-EXPR (NAME (IDOP ((:id N))) (
 NOLIB) (NOACTS) (NOMOD) (NOMAP) (NOTGT))))) (TYPE-NAME (NAME (IDOP ((:id int))
 ) (NOLIB) (NOACTS) (NOMOD) (NOMAP) (NOTGT)))) (NO-PRED)))))) (HAS-TYPE) (TYPE-
 NAME (NAME (IDOP ((:id int))) (NOLIB) (NOACTS) (NOMOD) (NOMAP) (NOTGT)))) (NOS
 EMIC))
          does not have a 2th argument
  
  Then if I type B-break and enter :bt at the end of the buffer *pvs*,
  it says:
  
  Evaluation stack:
  term-argn <-
     xt-assuming <- mapcan <- xt-module <- xt-adt-or-module <-
     xt-adt-or-modules <- parse <- prettyprint-expanded <- let <- throw <-
     let* <- let <- catch <- eval <- tpl:top-level-read-eval-print-loop <-
     tpl:start-interactive-top-level
  
  Kind regards,
  
  Erik.
  
  My system info :
  ================
  
  PVS Version 4.2 - Allegro CL Enterprise Edition 8.1 [Linux (x86)] (Jul 22, 20
 08 3:35) - Allegro CL Enterprise Edition 8.1 [Linux (x86)] (Jul 22, 2008 3:35)
  
  GNU Emacs 23.2.1 (x86_64-pc-linux-gnu, GTK+ Version 2.20.1) of 2010-08-15 on 
 barber, modified by Debian
  
  Linux localhost 2.6.32-5-amd64 #1 SMP Fri Sep 17 21:50:19 UTC 2010 x86_64 GNU
 /Linux
  
  -- 
  √Črik Martin-Dorel
  PhD student, ENS de Lyon, LIP
  http://perso.ens-lyon.fr/erik.martin-dorel/
  
  --------------050506010805030402070002
  Content-Type: text/plain;
   name="ppe-bug.pvs"
  Content-Transfer-Encoding: 7bit
  Content-Disposition: attachment;
   filename="ppe-bug.pvs"
  
  % Excerpt from lib/TU_Games/
  %---------------------------------------------------------------------
  % A formal theory of cooperative TU-games in PVS 4.2
  % Copyright (C) 2009 Erik Martin-Dorel.
  %---------------------------------------------------------------------
  
  players_set[U: TYPE+]: THEORY
   BEGIN
    elt: U
    players_set: TYPE+ = non_empty_finite_set[U] CONTAINING singleton(elt)
   END players_set
  
  %---------------------------------------------------------------------
  
  coalition_fun[U: TYPE+,       (IMPORTING players_set[U])
                N: players_set]: THEORY
   BEGIN
  
    IMPORTING players_set[U]
  
    powset: TYPE = setof[(N)] % rather than (powerset[U](N))
  
    fullN: powset = fullset[(N)]
  
    v: VAR [powset -> real]
    S: VAR powset
    x, y: VAR [(N) -> real]
    i: VAR (N)
    c: VAR real
    a: VAR nzreal
  
    zero_fun(S): real = 0
    coalition_fun?(v): bool = v(emptyset) = 0
    coalition_fun: TYPE+ = (coalition_fun?) CONTAINING zero_fun
  
    subsets_are_finite: JUDGEMENT setof[(N)] SUBTYPE_OF finite_set[(N)]
  
    IMPORTING %finite_sets@finite_sets_sum[(N),real,0,+],
              finite_sets@finite_sets_sum_real[(N)]
  
    tot(S, x): real = sum(S, x)
  
    tot_S_0: LEMMA tot(S, LAMBDA i: 0) = 0
    tot_distrib: LEMMA tot(S, LAMBDA i: x(i) + y(i)) = tot(S, x) + tot(S, y)
    tot_mult_const:  LEMMA tot(S, LAMBDA i: c * x(i)) = c * tot(S,x)
    tot_distrib_sub: LEMMA tot(S, LAMBDA i: x(i) - y(i)) = tot(S, x) - tot(S, y
 )
    tot_div_const:   LEMMA tot(S, LAMBDA i: x(i) / a) = tot(S,x) / a
  
    set_vect: TYPE = setof[[(N) -> real]]
  
   END coalition_fun
  
  %---------------------------------------------------------------------
  
  imputations[U: TYPE+,     (IMPORTING players_set[U])
              N: players_set, (IMPORTING coalition_fun[U,N])
              v: coalition_fun]: THEORY
   BEGIN
  
    IMPORTING players_set[U],
              coalition_fun[U,N]
  
    % set_vect: TYPE = setof[[(N) -> real]]
  
    x: VAR [(N) -> real]
    i: VAR (N)
    S: VAR powset % = setof[(N)] = [(N) -> bool]
  
    % feasible payoffs
    setFP: set_vect = {x | tot(fullN, x) <= v(fullN)}
  
    % preimputations
    setPI: set_vect = {x | tot(fullN, x) = v(fullN)}
  
    % imputations
    setI: set_vect = {x | member(x, setPI) AND FORALL i: x(i) >= v(singleton(i)
 )}
  
    % core: set_vect = {x: (setPI) | FORALL S: tot(S, x) >= v(S)}
    core: set_vect = {x | member(x, setPI) AND FORALL S: tot(S, x) >= v(S)}
  
    subset_core_I: LEMMA subset?(core, setI)
  
    subset_I_PI:   LEMMA subset?(setI, setPI)
    subset_PI_FP:  LEMMA subset?(setPI, setFP)
  
   END imputations
  
  --------------050506010805030402070002--

How-To-Repeat: 

Fix: 

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