Delivery-Date: 
Sender: info-hol-request@lal.cs.byu.edu
Errors-To: info-hol-request@lal.cs.byu.edu
Precedence: bulk
Message-Id: <199410122106.RAA01450@air52.larc.nasa.gov>
Date: Wed, 12 Oct 1994 17:06:45 -0400
From: "Victor A. Carreno" <vac@air16.larc.nasa.gov>
To: kfisler@cs.indiana.edu
Subject: Re: Single Pulser
In-Reply-To: Mail from '"Kathi Fisler" <kfisler@cs.indiana.edu>' dated: Wed, 12 Oct 1994 11:02:14 -0500 (EST)
Cc: info-hol@cs.uidaho.edu, vac@air16.larc.nasa.gov


>As has already been pointed out, this specification missed the point
>that the output should not be high when the input is low.

>This is not a component that can be realized in physical hardware,
>since we can't predict the drop on the input. 

That is because the specification can not guarantee both:

- that the circuit will produce a pulse for every rising edge

&

- that the output is low when the input is low

*unless you demand instantaneous response*

The specification by Albert Camilleri does not make the output low when the
input is low. Consider the following sequence. (0 = false, 1 = true)

state step   0 1 2 3 4 
inp          0 1 0 1 0 
o            0 0 1 0 1 
rising_edge  0 1 0 1 0 

by: AG (rising_edge -> (!o -> (AX A[!rising_edge U o])))

output 'o' has to be 1 at state step 2 since at step 3 rising_edge is 1.

in fact, Albert's specification can be reduced to: 

SPEC
	  AG (rising_edge -> (AF (o))) &
	  AG (o -> AX (A[!o U rising_edge])) &
  	  AG (rising_edge -> (AX A[!rising_edge U o]))

since output 'o' is always 0 when rising_edge is 1.


Victor.