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 09:15:53 +0000 Received: by leopard.cs.byu.edu (1.38.193.4/16.2) id AA17993; Tue, 7 Feb 1995 01:58:09 -0700 Sender: info-hol-request@lal.cs.byu.edu Errors-To: info-hol-request@lal.cs.byu.edu Precedence: bulk Received: from iraun1.ira.uka.de by leopard.cs.byu.edu with SMTP (1.38.193.4/16.2) id AA17989; Tue, 7 Feb 1995 01:57:57 -0700 Received: from i80fs2.ira.uka.de by iraun1.ira.uka.de with SMTP (PP); Tue, 7 Feb 1995 09:56:12 +0100 Received: from ira.uka.de by i80fs2.ira.uka.de id <02677-0@i80fs2.ira.uka.de>; Tue, 7 Feb 1995 09:56:27 +0100 To: info-hol@leopard.cs.byu.edu Subject: Re: Possible problem with SMV Date: Tue, 7 Feb 1995 09:56:26 +0100 From: schneide Message-Id: <"i80fs2.ira.679:07.02.95.08.56.31"@ira.uka.de> I think at least one of the two examples show that CTL can not be used in a way as LTL is used. As I mentioned in the discussion about the single pulser, I have developed a front end for SMV which has been implemented in SML in form of HOL conversions. To see how it works, look at one of the mentioned specs, which I have translated freely into LTL: (--`\t. ( (~p t ==> NEXT (\t.~q t) t) /\ (p t ==> NEXT (\t. q t) t)) = (p t = NEXT q t)`--); My conversion converts this LTL formula into a automata-like formula, which can then be handled with SMV. The resulting theorem is in this case: |- (\t. (~(p t) ==> NEXT (\t. ~(q t)) t) /\ (p t ==> NEXT (\t. q t) t) = p t = NEXT q t) = (\t0. ?pr1 pr0 nx0 q_prop0. ((!t1. (pr1 t0 = F) /\ (pr1 (t1 + t0 + 1) = p (t1 + t0))) /\ (!t1. (pr0 t0 = F) /\ (pr0 (t1 + t0 + 1) = ~(p (t1 + t0)))) /\ (!t1. (nx0 t0 = F) /\ (nx0 (t1 + t0 + 1) = T)) /\ (!t. (q_prop0 t0 = F) /\ (q_prop0 (t + t0 + 1) = nx0 (t + t0)))) /\ (!t. nx0 (t + t0) ==> ((pr0 (t + t0) ==> ~(q (t + t0))) /\ (pr1 (t + t0) ==> q (t + t0)) = pr1 (t + t0) = q (t + t0)) \/ q_prop0 (t + t0))) The right hand side can now be proved by SMV, the used resources are as follows: user time: 0.0666667 s, system time: 0.116667 s BDD nodes allocated: 288 Bytes allocated: 917504 BDD nodes representing transition relation: 54 + 1 The other formula is however not true. My translation into LTL is (--`\t. ~((p t ==> NEXT q t) /\ (~p t ==> NEXT (\t.~q t) t))`--); The generated automata formula is as follows: |- (\t. ~((p t ==> NEXT q t) /\ (~(p t) ==> NEXT (\t. ~(q t)) t))) = (\t0. ?pr0 nx0 q_prop0. ((!t1. (pr0 t0 = F) /\ (pr0 (t1 + t0 + 1) = p (t1 + t0))) /\ (!t1. (nx0 t0 = F) /\ (nx0 (t1 + t0 + 1) = T)) /\ (!t. (q_prop0 t0 = F) /\ (q_prop0 (t + t0 + 1) = nx0 (t + t0)))) /\ (!t. nx0 (t + t0) ==> ~((pr0 (t + t0) ==> q (t + t0)) /\ (~(pr0 (t + t0)) ==> ~(q (t + t0)))) \/ q_prop0 (t + t0))) : thm -- as demonstrated by the following execution sequence state 1.1: p = 0 q = 0 .... resources used: user time: 0.1 s, system time: 0.0666667 s BDD nodes allocated: 524 Bytes allocated: 917504 BDD nodes representing transition relation: 40 + 1 The non-validity of t can be easily seen when it is brought into negation normal form: (\t. p t /\ NEXT (\t. ~(q t)) t \/ ~(p t) /\ NEXT q t) Then there are exactly two models which make the formula true: (1) either p(0)=T and q(1)=F (2) or p(0) = F and q(1) = T However, there are other interpretation and therefore the formula is not valid, e.g. the one given by SMV which evalutates p(0)=F and q(0)=F. Therefore it is sufficient to give just the first state. Klaus.