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; Tue, 7 Feb 1995 16:45:22 +0000 Received: by leopard.cs.byu.edu (1.38.193.4/16.2) id AA28653; Tue, 7 Feb 1995 09:19:25 -0700 Sender: info-hol-request@lal.cs.byu.edu Errors-To: info-hol-request@lal.cs.byu.edu Precedence: bulk Received: from air52.larc.nasa.gov by leopard.cs.byu.edu with SMTP (1.38.193.4/16.2) id AA28648; Tue, 7 Feb 1995 09:19:21 -0700 Received: by air52.larc.nasa.gov (8.6.9/lanleaf2.4) id LAA13406; Tue, 7 Feb 1995 11:16:36 -0500 Message-Id: <199502071616.LAA13406@air52.larc.nasa.gov> Date: Tue, 7 Feb 1995 11:16:36 -0500 From: "Victor A. Carreno" To: info-hol@leopard.cs.byu.edu Subject: No bug after all (AX !bug) Cc: ratan@facility.cs.utah.edu, vac@air16.larc.nasa.gov Apologies to the group for my last posting and thanks to "ratan" and "schneide". One more point of clarification that ratan answered unknowingly: ratan said: >I cann't explain why the system is printing only one state tho'. But, >when started in state (p=0, q=0), the spec is false: No mater what state the system is started on, the expression (AX q) is false (if not restricted by the state machine) because it is universaly quantified. So the counterexample would have to print all possible next states (4 in this case) to show that the expression does not hold for all possible next states. I guess McMillan decided to omit that. Thanks, Victor.