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; Thu, 13 Oct 1994 18:05:51 +0100 Received: by leopard.cs.byu.edu (1.38.193.4/16.2) id AA21852; Thu, 13 Oct 1994 11:02:41 -0600 Sender: info-hol-request@lal.cs.byu.edu Errors-To: info-hol-request@lal.cs.byu.edu Precedence: bulk Received: from jaguar.cs.byu.edu by leopard.cs.byu.edu with SMTP (1.38.193.4/16.2) id AA21848; Thu, 13 Oct 1994 11:02:40 -0600 Received: from localhost by jaguar.cs.byu.edu (1.38.193.4/CS-Client) id AA14688; Thu, 13 Oct 1994 10:57:21 -0600 Message-Id: <9410131657.AA14688@jaguar.cs.byu.edu> To: info-hol@leopard.cs.byu.edu Subject: Forward of message from Victor A. Carreno (Single Pulser) Date: Thu, 13 Oct 1994 10:57:20 -0600 From: Phil Windley ------- Forwarded Message Date: Thu, 13 Oct 1994 10:55:15 -0400 From: "Victor A. Carreno" To: ac@gslxsrv.rose.hp.com Subject: Re: Single Pulser (reply to Victor) In-Reply-To: Mail from 'Albert Camilleri ' dated: Wed, 12 Oct 94 16:04:11 PDT Cc: info-hol@cs.uidaho.edu, vac@air16.larc.nasa.gov Albert, The following statement (which was posted by kfisler, not by me) >As has already been pointed out, this specification missed the point >that the output should not be high when the input is low. was indeed misinterpreted by me. However, the point is stil valid. What Kathi meant is that the specification should not describe a behaviour where an output pulse is generated when there is not a rising edge. That is, if there is never a rising edge, there should never be an output pulse. The specification: SPEC AG (rising_edge -> (AF (o))) & AG (o -> AX (A[!o U rising_edge])) & AG (rising_edge -> (!o -> (AX A[!rising_edge U o]))) permits a single pulse generated before any rising edge: state step 0 1 2 3 4 5 6 7 8 9 rising_edge 0 0 0 1 0 1 0 1 0 1 ... o 0 1 0 0 1 0 1 0 1 0 ... as demonstrated by: MODULE main VAR o : boolean; d1 : boolean; d2 : boolean; rising_edge : boolean; ASSIGN init(d1) := 0; next(d1) := 1; init(o) := 0; next(o) := case d1 = 0 : 1; rising_edge = 1 : 1; 1 : 0; esac; init(d2) := 0; next(d2) := d1; init(rising_edge) := 0; next(rising_edge) := d2 & !rising_edge; SPEC AG (rising_edge -> (AF (o))) & AG (o -> AX (A[!o U rising_edge])) & AG (rising_edge -> (!o -> (AX A[!rising_edge U o]))) smv -f -r single_pulse.smv - -- specification AG (rising_edge -> AF o) & AG (o -> AX A... is true resources used: user time: 0.0333333 s, system time: 0.0833333 s BDD nodes allocated: 122 Bytes allocated: 917504 BDD nodes representing transition relation: 21 + 1 reachable states: 5 (2^2.32193) out of 16 (2^4) Albert wrote: >No. As far as I am aware, AG (risingEdge -> (AF o)) allows risingEdge and o to >be true at the same time. You are write. At least that is the way defined in temporal logic. I just have a hang-up with reality in which things cannot have instantaneous response. Albert wrote: >Care is required here. Specifications are not intended to guarantee anything. >Specifications are intended to capture intended behaviour and could be anything >we wish them to be. I don't know about you Albert, but I want some guarantee from *my* specifications. :-) Victor. ------- End of Forwarded Message