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

PVS Bug 394


Synopsis:        model checker error
Severity:        serious
Priority:        medium
Responsible:     owre
State:           open
Class:           sw-bug
Arrival-Date:    Wed Dec  8 20:40:01 1999
Originator:      Oleg Sheyner
Organization:    cs.cmu.edu
Release:         PVS 2.3
Environment: 
 System:          
 Architecture: 

Description: 
  
    Hello,
  
  I have tried out the abstract-and-mc strategy and run across the following
  problem.  The abstraction part seems to proceed ok, and produces the followin
 g
  goal:
  
  
  |-------
  {1}   FORALL (abs_s: [# B_1: boolean, B_2: boolean #]):
          (B_2(abs_s)) OR
           NOT mu(LAMBDA (abs_Q: [[# B_1: boolean, B_2: boolean #] -> boolean])
 :
                    LAMBDA (abs_x1: [# B_1: boolean, B_2: boolean #]):
                      (B_2(abs_x1)) OR
                       K_conversion(TRUE)(abs_x1) AND
                        (EXISTS (abs_v: [# B_1: boolean, B_2: boolean #]):
                           abs_Q(abs_v) AND
                            (B_1(abs_v) = B_1(abs_x1) OR
                              (B_2(abs_v) = B_2(abs_x1) AND
                                B_1(abs_v) = B_1(abs_x1))
                               AND
                               NOT (B_2(abs_v)) AND B_1(abs_v) = B_1(abs_x1))))
                 (abs_s)
  
  
  There are only four abstract states, so the model checker should be able to h
 andle
  this.  But the model checker fails with the following output:
  
  [mu_init]: v1.4 Copyright (C) 1992-1997 G. Janssen, Eindhoven University
  Added Relational variable `b857' to Ip.
  Looking up Relational variable: `b857'.
  
  ~(A b855,b856.b856 + ~[mu b857.L b858,b859.b859 + b860 & (E b861,b862.b857(b8
 61,b862) & ((b861 == b858) + (b862 == b859)
  & (b861 == b858) & ~b862 & (b861 == b858)))](b855,b856)) | 1;
   Starting least fixed-point calculation..
  Fixed-point found in 2 steps.
  Formula amounts to 2 BDD nodes.
  
  Failed to Model check:
     could not decode binary encodings of scalars.
  
  
  Does this mean that there are additional restrictions on the mu-calculus form
 ula that the
  model checker can handle?
  
  Sincerely,
  
  Oleg Sheyner
  

How-To-Repeat: 

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