Delivery-Date: 
Sender: info-hol-request@lal.cs.byu.edu
Errors-To: info-hol-request@lal.cs.byu.edu
Precedence: bulk
From: ratan@facility.cs.utah.edu
Message-Id: <199502070042.RAA27634@lal.cs.utah.edu>
Subject: SMV bug ...
To: info-hol@leopard.cs.byu.edu
Date: Mon, 6 Feb 1995 17:42:58 -0700 (MST)
Mime-Version: 1.0
Content-Type: text/plain; charset=US-ASCII
Content-Transfer-Encoding: 7bit
Content-Length: 3313

[Looks like I sent it to wrong address before.  Please disregard, if it
appears twice in your mailbox].

- ratan

--------------

This is in response to Victor's mail regarding the bug reports sent to
Clarke.

There are no problems with either example1, or example3.  They are
working as expected.

: 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

The behavoir is correct because in the initial state term1 is false
(Explanation follows).  One should remember that the SPEC is what one
refers to as a "state formulae", not path formulae, and that it is
evaluated in the initial state.

Victor Carreno said:

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

That "any value of p and q" is incorrect.  It just means that "p->AX q&.."
doesn't hold in the initial state, in otherwords there is atleast one
initial state where the spec is false.  I guess, the "there are
instances" shows that author was expecting it to be treated as a PATH
FORMULAE instead of as a STATE FORMULAE.

Let us dissect the SPEC:

A formulae like "p -> AX q" when interpreted as a state formulae has the
following interpretation:

(1) If 'p' is true now, then ALL next states satisfy q.  If p is false
    now, then the statement is vacuously true.

On the other hand !p -> AX !q means

(2) If 'p' is false now, then "AX !q" is true, which means that ALL next
    states have q = 0.  If p is true, then the expression is true.

If initially "p" is true, then we can see that (1) is false, because
there is a next state in which "q" is false.  If "p" is false, then (2)
is false.  Which together make the SPEC false.


: 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


Victor also said:

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

I don't think it is consistent with the meaning of next operator.
Atleast, I don't understand how.  (But it does appear to hold in LTL
framework).

I cann't explain why the system is printing only one state tho'.  But,
when started in state (p=0, q=0), the spec is false:

In the spec above:

LHS = (!p -> AX !q) & (p -> AX q)
RHS = (p = AX q)

First "p -> AX q" is true for this state (because p is false).
BUT,  "!p -> AX !q" is false.
So, LHS = true & false = false.

RHS is "p=AX q".
"AX q" is false.  So is p.  So, RHS is equal to "false = false", or
true.

So, RHS is NOT equal to LHS.  So SPEC fails.

thanks
ratan