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