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

PVS Bug 583


Synopsis:        abstract/modelcheck bug
Severity:        serious
Priority:        medium
Responsible:     shankar
State:           open
Class:           sw-bug
Arrival-Date:    Mon Jul 23 20:20:03 2001
Originator:      Oliver Moeller
Organization:    brics.dk
Release:         PVS 2.3
Environment: 
 System:          
 Architecture: 

Description: 
  Hi,
  
  I think I hit a bug in the abstract/model-check part of PVS Version 2.3 Beta
  (patch level 1.2.2.176) - Allegro CL Professional Edition 5.0 [Linux/X86]
  (9/4/99 2:05)  
  
  In the following example, BOTH properties 'reachB' and 'notreachB' were
  provable with the command sequence:
  
  (ABSTRACT
                   ("lambda(z:state):  z`x = 0"
                    "lambda(z:state):  z`y = 0"
                    "lambda(z:state):  z`x <= i"
                    "lambda(z:state):  z`y <= i"
                    "lambda(z:state):  z`x - z`y <= i"))
  (model-check)
  
  The system grow2 mimics a simple timed automaton (here with discrete time).
  If I did not make a mistake, it should always remain in location A.
  
  This example works also, if you replace "i" by - eg. "5".
  
  
  - oli					       http://www.brics.dk/~omoeller
  *com-pu-ter*: device to enhance our capability to err.   <omoeller@brics.dk>
  
  %% %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
  %% Grow2
  %% Version: DISCRETE TIME DELAY
  %% %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
  %% Simple timed automata model with one paramter:
  %%
  %%		     X
  %% Process:	    / \	AA1	        X 
  %%		   /   \	      /  \  AA2
  %%          	  /     \	    / 	   \
  %%	         /       \	  / 	    \
  %%     x <= i   /         \----- /	     \     y <= i
  %%	       / 	  (  A  )  	       \
  %%	      X  	/  --+---\  	       - 
  %%     y := 0  \       /     |     \  	     -/
  %%		\     /      |       \ 	  -/       x := 0
  %%		 \   /       |	      --/
  %%		  \ /	     |
  %%		   X	     |
  %%			    \|/  x>i & y = 0
  %%			   -----
  %%			  (  B  )
  %%			   -----
  %%
  %% clock: x,y
  %% nat:   i
  %% 
  %% Synopsis:
  %%  Abstractions of infinite-discrete-state RT systems
  %% %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
  %% @TABLE OF CONTENTS:		       [TOCD: 07:36 23 Jul 2001]
  %%
  %%  [1] The Model
  %%      [1.1] Preliminaries
  %%      [1.2] Initial State
  %%      [1.3] Discrete Transitions
  %%  [2] The nature of time
  %%  [3] Transition Relation
  %%  [4] Properties
  %% %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
  %% @FILE:    grow2.pvs
  %% @PLACE:   SRI; host:falkner
  %% @FORMAT:  Prototype Verification System (PVS)
  %% @AUTHOR:  M. Oliver M'o'ller     <omoeller@brics.dk>
  %% @BEGUN:   Mon Jul 23 07:35:21 2001
  %% @VERSION: Mon Jul 23 16:33:53 2001
  %% %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
  
  
  grow2: THEORY
  
  BEGIN
  
  %% %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
  %% [1] The Model
  %% %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
  
  %% %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
  %% [1.1] Preliminaries
  %% %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
  
   loc: TYPE = {A, B}
  
   i: nat
  
   state: TYPE = [#
     pc : loc,
     x  : nnreal,
     y  : nnreal
   #]
  
   s, s1: VAR state
  
  
  %% %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
  %% [1.2] Initial State
  %% %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
  
   init(s): bool = 
      s`pc = A
    AND s`x = 0
    AND s`y = 0
  
  
  %% %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
  %% [1.3] Discrete Transitions
  %% %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
  
   nextAA1(s,s1): bool =
      s`pc = A
    AND s`x <= i
    AND s1 = s WITH [`y := 0]
  
   nextAA2(s,s1): bool =
      s`pc = A
    AND s`y <= i
    AND s1 = s WITH [`x := 0 ]
   
   nextAB(s,s1): bool =
      s`pc = A
    AND s`x > i
    AND s`y = 0
    AND s1 = s WITH [`pc := B ]
  
  %% %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
  %% [2] The nature of time
  %% %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
  
  %% == dense =====================================================
  
   delay(s,s1): bool =
      EXISTS (delta: posreal): 
         s1 = s WITH [`x := s`x + delta, 
                      `y := s`y + delta ]
  
  %% == discrete (coarse: step 1) =================================
  
   delay_1(s,s1): bool =
          s1 = s WITH [`x := s`x + 1, 
                       `y := s`y + 1 ]
  
  
  
  %% %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
  %% [3] Transition Relation
  %% %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
  
   next(s,s1): bool =
        nextAA1(s,s1)
     OR nextAA2(s,s1)
     OR nextAB(s,s1)   
     OR delay_1(s,s1)
  
  
  %% %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
  %% [4] Properties
  %% %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
  
  
  %% == proven =============================================================== 
  
    deadlockfree: PROPOSITION
      init(s) => AG(next, LAMBDA s: EX(next, LAMBDA s1: TRUE)(s))(s)
  
    reachB: PROPOSITION
      init(s) => EF(next, LAMBDA s: s`pc = B)(s)
  
    notreachB: PROPOSITION
      init(s) => AG(next, LAMBDA s: s`pc = A)(s)
  
  
  
  %% == unproven =============================================================
  
    response: PROPOSITION
      init(s) => AG(next, LAMBDA s: s`y > 0 => AF(next, LAMBDA s: s`y = 0)(s))(
 s)  
  % leads to:
  % ---------------------
  % [-1]  (B_1(abs_s!1))
  % [-2]  (B_2(abs_s!1))
  % [-3]  abs_s!1`B_3
  %   |-------
  % [1]   B?(abs_s!1`pc)
  % ---------------------
  
  END grow2
  
 
How-To-Repeat: 

 [davesc, 7/23/01]
 In the current reworking of the abstractor, this breaks with
 no method for find-supertype in get-free-state-components.

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