# 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: