Delivery-Date: 
Sender: info-hol-request@lal.cs.byu.edu
Errors-To: info-hol-request@lal.cs.byu.edu
Precedence: list
Message-Id: <199507111856.AA118648974@bobcat.cs.byu.edu>
To: rahard@ee.umanitoba.ca (Budi Rahardjo)
Cc: info-hol@leopard.cs.byu.edu
Subject: Re: [Q] unbounded delay
In-Reply-To: Your message of Tue, 11 Jul 1995 11:50:51 -0500. <9507111650.AA15891@wine>
Date: Tue, 11 Jul 1995 12:56:14 -0600
From: Phil Windley <windley@cs.byu.edu>


On Tue, 11 Jul 1995 11:50:51 -0500 (CDT) Budi Rahardjo writes
+--------------------
| What I really want to say is a combination of the above, i.e.,
| for a 2-input AND gate, if currently one of the inputs is ``F''
| and we change both inputs to ``T''s, EVENTUALLY the output is going
| to be ``T'' (or eventually there is a transition from ``F'' to ``T'').

Here's a go:


define "rise x t = (t = 0) => (x 0)
                            | ~(x (t-1)) /\ (x t)";;

% for use in a subtype %
define "pos n = 0 < n";;

define "below n m = n < m";;

% a two input and gate %
define "and in1 in2 out =
           ! t. ((in1 t) /\ (rise in2 t)) \/
                ((in2 t) /\ (rise in1 t)) \/
                ((rise in1 t) /\ (rise in2 t)) ==>
                ? delay::pos . (rise out (t+delay))";;


% the generalized definition (n inputs) is simpler %
define "andn n inputs out = 
          ! t . ? m::below n . (rise (inputs m) t) /\
                ! m::below n . (inputs m (SUC t)) ==>
                ? delay::pos . (rise out (t+delay))";;
           
I haven't loaded this into HOL, so your mileage may vary.  Note that
"define" is non-standard, I'm too lazy to write the HOL thing out (pun
intended).  

Finally, a few caveats:

1.) My definitions follow your specification, but they are not AND gates.
The specification don't say that the output will stay high as long as all
the inputs are high or that it will drop when one of the inputs drops.
Here's a shot at an AND gate:


define "interval(l,u) x = l < x /\ x < u";;

define "high s t1 t2 = ! t::interval(t1,t2) . (s t)";;

define "andn n inputs out = 
         ? delay::pos . 
         ! t1 .
         ! t2::above t1 . ? m::below n . ~(inputs m t1) /\
                          ? m::below n . ~(inputs m t2) /\
                          ! m::below n . (high (inputs m) t1 t2) ==>
                          (high out (t1+delay) (t2+delay))";;

This says that there is some delay (note this means that the delay for
turning on and turning off is the same) such that for all times t1 and
times t2 greater than t1, if at least one of the inputs is off at time t1
and one of the inputs is off at time t2 and they are all on inbetween then
the output is on for an equal, delayed interval.

2.) Note also, that these may not be the best definitions to use
from the standpoint of verification.  

3.) A fixed delay is much easier to specify:

define "and delay in1 in2 out = 
         ! t. out(t+delay) = (in1 t) /\ (in2 t)

This may be more what you want (unless you really want an indeterminant
delay that can change each time the component is used).  The delay can
still be unspecified, its just a global property that is the same each and
every time an instantiation of the component is used.

--phil--