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; Wed, 12 Oct 1994 11:40:03 +0100
Received: by leopard.cs.byu.edu (1.38.193.4/16.2) id AA01338;
          Wed, 12 Oct 1994 04:37:09 -0600
Sender: info-hol-request@lal.cs.byu.edu
Errors-To: info-hol-request@lal.cs.byu.edu
Precedence: bulk
Received: from dworshak.cs.uidaho.edu by leopard.cs.byu.edu 
          with SMTP (1.38.193.4/16.2) id AA01334;
          Wed, 12 Oct 1994 04:37:05 -0600
Received: from oberon.inmos.co.uk (oberon.inmos.co.uk [192.26.234.4]) 
          by dworshak.cs.uidaho.edu (8.6.9/1.0) with ESMTP id DAA18303 
          for <info-hol@cs.uidaho.edu>; Wed, 12 Oct 1994 03:30:26 -0700
Received: from frogland.inmos.co.uk by oberon.inmos.co.uk;
          Wed, 12 Oct 1994 11:14:05 +0100
From: David Shepherd <des@inmos.co.uk>
Message-Id: <8290.9410121009@frogland.inmos.co.uk>
Subject: Re: "Re: Single Pulser/Spec of D. Shepherd"
To: schneide@ira.uka.de (schneide)
Date: Wed, 12 Oct 1994 11:09:23 +0100 (BST)
Cc: info-hol@cs.uidaho.edu
In-Reply-To: <"i80fs2.ira.784:12.10.94.09.49.22"@ira.uka.de> from "schneide" at Oct 12, 94 10:49:15 am
X-Mailer: ELM [version 2.4 PL20]
Content-Type: text
Content-Length: 1730

schneide has said:
> D. Shepherd said:
> 
> |> Then the spec is
> |> 
> |> SPEC
> |>    (AG ((!inp) -> AX(inp -> A [inp U out]))) &
> |>    (AG (out -> AX (A [ !out WU !inp ] )))

hmmm ... I've been thinking too quickly again :-)

> Not exactly. 
> The first part (AG ((!inp) -> AX(inp -> A [inp U out]))) does not
> cover the fact, that  inp is also high when out becomes high.
> This is important, otherwise the impuls of out could follow
> a high-phase of inp.

ok make that 

((!inp) -> AX(inp -> A [inp U (inp & out)])))

? not sure about this but this might have looked better if there
was the "V" operator in SMV.

> The second part (AG (out -> AX (A [ !out WU !inp ] ))) does not
> cover the following:
> After out has gone high, it has to go low at the next point of
> time and then it has to be low until the next rising edge of inp 
> is detected. The above specification only states that out is low 
> until inp goes low. 

This behaviour isn't in the "informal spec" you gave ... no mention
is made on the value of out when inp is low! What you say here is
easily fixed by a 3rd clause

(AG (!inp -> !out))


Having reread you're original message I now see that what you
are doing is translating linear formula in HOL into automata and
then using SMV to perform the check. This is a useful approach to
take as, as I commented, linear formula can be more readable than
CTL ones - however there can be a price to pay in complexity.

--------------------------------------------------------------------------
david shepherd: des@inmos.co.uk                     tel: 0454-616616 x 638
                inmos ltd, 1000 aztec west, almondsbury, bristol, bs12 4sq
		"I  am  not  a  nut      ---      I  am  a  human  being."