Return-Path: <John.Harrison-request@cl.cam.ac.uk>
Delivery-Date: 
Received: from leopard.cs.byu.edu (no rfc931) by swan.cl.cam.ac.uk 
          with SMTP (PP-6.5) outside ac.uk; Mon, 6 Feb 1995 21:44:56 +0000
Received: by leopard.cs.byu.edu (1.38.193.4/16.2) id AA29872;
          Mon, 6 Feb 1995 14:24:19 -0700
Sender: info-hol-request@lal.cs.byu.edu
Errors-To: info-hol-request@lal.cs.byu.edu
Precedence: bulk
Received: from air52.larc.nasa.gov by leopard.cs.byu.edu 
          with SMTP (1.38.193.4/16.2) id AA29868;
          Mon, 6 Feb 1995 14:24:14 -0700
Received: by air52.larc.nasa.gov (8.6.9/lanleaf2.4) id QAA13118;
          Mon, 6 Feb 1995 16:21:32 -0500
Message-Id: <199502062121.QAA13118@air52.larc.nasa.gov>
Date: Mon, 6 Feb 1995 16:21:32 -0500
From: "Victor A. Carreno" <vac@air16.larc.nasa.gov>
To: info-hol@leopard.cs.byu.edu
Subject: Possible problem with SMV


Last October there was some disscusion by the group about a specification
of a pulser in SMV. This message sent to Clarke at CMU might be of some
interest to some people. 

------- Start of forwarded message -------

There appears to be a bug in the SMV system which results in a
specification being declared "true" when it should be declared false. The
examples are derived from Kathi Fisler controller specification. 

In the first example the specification is declared "true" which means that
"term1" is false for any value of "p" and "q". However, there are instances
for "p" and "q" which will make the term "term1" true resulting in a false
specification as shown in example 2.

The third specification shows a term which from the interpretation of the
next operator should be true but is declared false by the system. Also
note, and this was also pointed out by Kathi Fisler, that the
counterexample only shows state 1. The value of q in state 2 is needed
to evaluate the expression.

Victor Carreno
vac@air16.larc.nasa.gov

Example 1
MODULE main
VAR
   p : boolean;
   q : boolean;
DEFINE term1 := ((p -> (AX q)) & (!p -> (AX !q)));
SPEC term1 -> 0

smv example1.smv
-- specification term1 -> 0 is true

Example 2
MODULE main
VAR
   p : boolean;
   q : boolean;
ASSIGN
   next(q) :=1;
DEFINE term1 := ((p -> (AX q)) & (!p -> (AX !q)));
SPEC term1 -> 0

smv example2.smv
-- specification term1 -> 0 is false
-- as demonstrated by the following execution sequence
state 1.1:
term1 = 1
p = 1
q = 0

state 1.2:term1 = 0
p = 0
q = 1

Example 3

 MODULE main
VAR
   p : boolean;
   q : boolean;

SPEC (((!p -> (AX !q)) & (p -> (AX q))) = (p = (AX q)))

smv example3.smv
-- specification ((!p -> AX (!q)) & (p -> AX q)) = p = (A... is false
-- as demonstrated by the following execution sequence
state 1.1:
p = 0
q = 0