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 12:43:41 +0100
Received: by leopard.cs.byu.edu (1.38.193.4/16.2) id AA01629;
          Wed, 12 Oct 1994 05:38:03 -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 AA01625;
          Wed, 12 Oct 1994 05:38:00 -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 EAA18330 
          for <info-hol@cs.uidaho.edu>; Wed, 12 Oct 1994 04:31:24 -0700
Received: from frogland.inmos.co.uk by oberon.inmos.co.uk;
          Wed, 12 Oct 1994 12:31:20 +0100
From: David Shepherd <des@inmos.co.uk>
Message-Id: <8680.9410121126@frogland.inmos.co.uk>
Subject: Re: "Re: Single Pulser/Spec of D. Shepherd" (fwd)
To: info-hol@cs.uidaho.edu (info-hol mailing list)
Date: Wed, 12 Oct 1994 12:26:38 +0100 (BST)
X-Mailer: ELM [version 2.4 PL20]
Content-Type: text
Content-Length: 2582

David Shepherd has said:
From des Wed Oct 12 12:26:16 1994
From: David Shepherd <des>
Subject: Re: "Re: Single Pulser/Spec of D. Shepherd"
To: morley@gmd.de (Matthew Morley)
Date: Wed, 12 Oct 1994 12:26:16 +0100 (BST)
Cc: des@inmos.co.uk
In-Reply-To: <199410121109.AA19630@borneo.gmd.de> from "Matthew Morley" at Oct 12, 94 12:09:18 pm
X-Mailer: ELM [version 2.4 PL20]
Content-Type: text
Content-Length: 1879      

Matthew Morley has said:
> I dunno if it's legal CTL (nesting Os, I like stronger logics!) but it
> seems to me that the invariant you & Klaus want is:
> 
> (!inp & O inp) -> O ((inp & !out) U (inp & out & O (!out U !inp)))
> 
> which, if my (also swift) thinking is correct leaves things nicely
> loose around the "what of out when inp is low" area? Note the
> reference point is that before t0.

Its not CTL -- but it is LTL (apart from use of O instead of X).
My mindset seems to be polluted by CTL and I hadn't thought of this formulation
till I saw it - at which point it is obvious!

Also, given LTL's use of U as a "strong" until (p U q means p holds until
q hold *and* q will definitely hold at some point), an extra antecedent

 (G (inp -> F !inp))

is needed to filter out traces where inp remains high for ever.

Using this the formula is proved true.

Now while all these take a trivial time (< 1s) it is instructive to
compare the reachable state space and transition relation size:

1) CTL proof:	
BDD nodes allocated: 14
BDD nodes representing transition relation: 5 + 1
reachable states: 4 (2^2) out of 4 (2^2)

2) HOL linear logic translated to CTL
BDD nodes allocated: 1488
BDD nodes representing transition relation: 279 + 1
reachable states: 44 (2^5.45943) out of 4096 (2^12)

3) LTL translated to CTL
BDD nodes allocated: 704
BDD nodes representing transition relation: 41 + 1
reachable states: 144 (2^7.16993) out of 256 (2^8)

Note that 2) introduces several more variables and has a bigger transition
relation - on larger examples this may be a more serious problem!


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

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