Return-Path: 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 Jul 1995 16:49:06 +0100 Received: by leopard.cs.byu.edu (1.37.109.15/16.2) id AA067106266; Wed, 12 Jul 1995 07:37:46 -0600 Sender: info-hol-request@lal.cs.byu.edu Errors-To: info-hol-request@lal.cs.byu.edu Precedence: list Received: from air52.larc.nasa.gov by leopard.cs.byu.edu with ESMTP (1.37.109.15/16.2) id AA067076259; Wed, 12 Jul 1995 07:37:39 -0600 Received: by air52.larc.nasa.gov (8.6.11/lanleaf2.4) id JAA16289; Wed, 12 Jul 1995 09:39:08 -0400 Message-Id: <199507121339.JAA16289@air52.larc.nasa.gov> Date: Wed, 12 Jul 1995 09:39:08 -0400 From: "Victor A. Carreno" To: info-hol@leopard.cs.byu.edu Subject: Re: [Q] unbounded delay In-Reply-To: Mail from '"Phil Windley" ' dated: Tue, 11 Jul 1995 12:56:14 -0600 Cc: vac@air16.larc.nasa.gov One more caveat on Phil Windley's specification, % 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))";; is that you can have N rising edges in the "and" gate inputs and 1 rising edge in the output. That is, the definition does not specify that there is one rising edge in the output for each condition in the input which should have caused a rising edge. This is somewhat similar to eventualy and eventualy infinitely many times in temporal logic. In a finite sequence, (DIAMOND) p means p should occur at least once before the end of the sequence. (BOX)(DOT_CIRCLE)(DIAMOND) p means that if a new element is added to the end of the sequence, then that element should have the property eventualy p. However, the (BOX)(DOT_CIRCLE)(DIAMOND) p does not give you the one-to-one input output relation either. Victor.