Subject: [sv-ac] Re: flaw in Sugar clocked until semantics
From: Cindy Eisner (cindy_eisner@hotmail.com)
Date: Thu Oct 24 2002 - 11:44:30 PDT
john,
you are absolutely right (with a small caveat, see below). thank you
very much for putting so much time into considering the issue - dana
and i were pleasantly surprised to find someone reading so closely!
in addition, by the same reasoning, the semantics of suffix
implications need to be changed in a similar manner. finally, we need
to update the rewrite rules to reflect the new semantics. dana will
send out the new semantics and rewrite rules.
the small caveat is as follows: all semantics in weak context need to
be prefixed with "for all i in [0..|w|) such that
w^{0,i} |= {!c[*];c}". this takes care of the case that there are no
clocks at all, which is the basic difference between strong and weak
operators.
by the way, just to make sure, we intend to verify that equivalence
(and not only duality) is preserved under clocking with the help of
mike gordon (see m.j.c. gordon, using hol to study sugar 2.0
semantics. in proc. 15th intl. confernece on theorem proving in higher
order logics, 2002.)
regards,
cindy.
>From: John Havlicek <john.havlicek@motorola.com>
>Reply-To: john.havlicek@motorola.com
>To: vfv@server.eda.org, sv-ac@server.eda.org
>CC: john.havlicek@mot.com
>Subject: flaw in Sugar clocked until semantics
>Date: Tue, 22 Oct 2002 23:49:53 -0500 (CDT)
>
>Recall that with unclocked semantics, the four Sugar until operators
>form two dual pairs:
>
> until! dual to until_
> until!_ dual to until
>
>In my last mail, I explained why these duality relationships fail
>to hold using the clocked semantics of Sugar 2.0.
>
>I now believe very strongly that the breakdown of the duality
>relationships indicates a fundamental defect in the clocked semantics
>of Sugar 2.0. I believe that numerous untidy subtleties derive from
>the current clocked semantics definitions, some of which are evident in
>the equivalences that I mentioned in my last mail. I predict that these
>subtleties will be no end of trouble for anyone who tries to implement or
>to work with a tool supporting Sugar 2.0.
>
>Fortunately, I do not think it is difficult to repair the Sugar
>clocked semantics for the until operators. This note offers a
>proposal for revised definitions that I believe are superior to the
>existing Sugar 2.0 definitions for several reasons:
>
>1. They restore the duality relationships.
>2. They eliminate the subtleties of the current definitions. They
> have a simple formal symmetry that is lacking in the Sugar 2.0
> definitions.
>3. They preserve the relationships of the derived operators in Subsection
> B.3.2 of the LRM.
>
>The fundamental source of trouble in the Sugar 2.0 clocked semantics
>is the definition of weakly clocked strong until. This definition must
>be changed in order to put things right.
>
>I hope the committees will see the importance of this flaw and will agree
>that now is the time to repair it.
>
>Best regards,
>
>John Havlicek
>
>-------------------------------------------------------------------------------
>
>The first two definitions are Sugar 2.0 definitions.
>
>DEFINITION 1: pi,i |=(c!) f until! g iff i is in dom(pi) and
>there exists k >= i such that both
>a) pi,k |= c and pi,k |=(c!) g
>and
>b) for all j such that i <= j < k, if pi,j |= c then pi,j |=(c!) f.
>////
>
>DEFINITION 2:
>a) "eventually! f" is equivalent to "TRUE until! f".
>b) "always f" is equivalent to "! eventually! !f".
>c) "f until_ g" is equivalent to "f until (f && g)".
>d) "f until!_ g" is equivalent to "f until! (f && g)".
>////
>
>Therefore we have
>
>CLAIM 1: Assume i is in dom(pi).
>a) pi,i |=(c!) eventually! f
> iff
> there exists j >= i such that both pi,j |= c and pi,j |=(c!) f.
>b) pi,i |=(c) always f
> iff
> for all j >= i, if pi,j |= c then pi,j |=(c) f.
>////
>
>
>Now, observe that for i in dom(pi),
>
> pi,i |=(c) !(!f until! !g)
> iff not(pi,i |=(c!) (!f until! !g))
> iff not
> there exists k >= i such that both
> a) pi,k |= c and pi,k |=(c!) !g
> and
> b) for all j such that i <= j < k, if pi,j |= c then pi,j |=(c!) !f
> iff for all k >= i either
> a) if pi,k |= c then not(pi,k |=(c!) !g)
> or
> b) there exists j such that i <= j < k and pi,j |= c and not(pi,j
>|=(c!) !f)
>
> iff
>
> B: for all k >= i either
> a) if pi,k |= c then pi,k |=(c) g
> or
> b) there exists j such that i <= j < k and pi,j |= c and pi,j |=(c)
>f.
>
>CLAIM 2: B holds iff
>
> E: either
> a) there exists k >= i such that both
> i) pi,k |= c and pi,k |=(c) f && g
> and
> ii) for all j such that i <= j < k, if pi,j |= c then pi,j |=(c) g
> or
> b) for all j >= i, if pi,j |= c then pi,j |=(c) g.
>
>PROOF: Assume B. Assume E b) fails, hence
>
>there exists j >= i such that pi,j |= c and not(pi,j |=(c) g).
>
>Then B b) must hold with k = j, so there exists j0 such that i <= j0 < j
>and
>pi,j0 |= c and pi,j0 |=(c) f. Without loss of generality, j0 is the least
>such.
>If not(pi,j0 |=(c) g), then B b) holds with k = j0, and this contradicts
>the
>minimality of j0. Therefore pi,j0 |=(c) f && g. This proves E a) i) with
>k = j0.
>Suppose E a) ii) fails with k = j0. Then there exists j1 such that
>i <= j1 < j0 and pi,j1 |= c and not(pi,j1 |=(c) g). Again, using B b), the
>minimality of j0 is contradicted.
>
>Now assume E. If E b), then B holds by virtue of B a). Suppose now that
>E a) holds with k = k0. Since pi,k0 |= c and pi,k0 |=(c) f, B b) holds for
>all
>k > k0. E a) i) and ii) imply that for all k such that i <= k <= k0, if
>pi,k |= c then pi,k |=(c) g. Therefore, B a) holds for all k such that
>i <= k <= k0.
>
>////
>
>Claim 2 and the desire for duality motivate the following NEW definition:
>
>DEFINITION 3: pi,i |=(c) f until g iff i is in dom(pi) and
>either
>a) there exists k >= i such that both
> i) pi,k |= c and pi,k |=(c) g
> and
> ii) for all j such that i <= j < k, if pi,j |= c then pi,j |=(c) f
>or
>b) for all j >= i, if pi,j |= c then pi,j |=(c) f.
>////
>
>LEMMA 1: pi,i |=(c) f until g iff pi,i |=(c) (f || g) until g.
>PROOF: From Definition 3 it is clear that if pi,i |=(c) f until g,
>then pi,i |=(c) (f || g) until g. Suppose pi,i |=(c) (f || g) until g.
>Then either
>a') there exists k >= i such that both
> i) pi,k |= c and pi,k |=(c) f || g
> and
> ii) for all j such that i <= j < k, if pi,j |= c then pi,j |=(c) f
>or
>b') for all j >= i, if pi,j |= c then pi,j |=(c) f.
>Notice that if condition a) of Definition 3 fails, then from a') it
>follows that b') must hold, hence also condition b) of Definition 3.
>////
>
>PROPOSITION 1:
>a) pi,i |=(c) !(!f until! !g) iff pi,i |=(c) g until_ f.
>b) pi,i |=(c!) !(!f until_ !g) iff pi,i |=(c!) g until! f.
>c) pi,i |=(c) !(!f until!_ !g) iff pi,i |=(c) g until f.
>d) pi,i |=(c!) !(!f until !g) iff pi,i |=(c!) g until!_ f.
>PROOF:
>a) Immediate from Claim 2 and the definitions.
>b) Follows from a) by negations.
>c) Using a) and Lemma 1, note that
>
> pi,i |=(c) !(!f until!_ !g)
> iff pi,i |=(c) !(!f until! (!f && !g))
> iff pi,i |=(c) !(!f until! !(f || g))
> iff pi,i |=(c) (f || g) until_ f
> iff pi,i |=(c) (f || g) until f
> iff pi,i |=(c) g until f.
>
>d) Follows from c) by negations.
>////
>
>Definition 3 and the desire for
>
>(*) pi,i |=(c) f until g iff pi,i |=(c) (f until! g) || (always f)
>
>motivate the following NEW definition:
>
>DEFINITION 4: pi,i |=(c) f until! g iff i is in dom(pi) and
>there exists k >= i such that both
>a) pi,k |= c and pi,k |=(c) g
>and
>b) for all j such that i <= j < k, if pi,j |= c then pi,j |=(c) f.
>////
>
>Notice that with Definition 4, (*) does indeed hold.
>
>PROPOSITION 2: Assume i is in dom(pi).
>a) pi,i |=(c) eventually! f
> iff
> there exists j >= i such that pi,j |= c and pi,j |=(c) f.
>b) pi,i |=(c!) always f
> iff
> for all j >= i, if pi,j |= c then pi,j |=(c!) f.
>////
>
>Definition 1 and the desire for
>
>(**) pi,i |=(c!) f until g iff pi,i |=(c!) (f until! g) || (always f)
>
>motivate the following NEW definition:
>
>DEFINITION 5: pi,i |=(c!) f until g iff i is in dom(pi) and
>either
>a) there exists k >= i such that both
> i) pi,k |= c and pi,k |=(c!) g
> and
> ii) for all j such that i <= j < k, if pi,j |= c then pi,j |=(c!) f
>or
>b) for all j >= i, if pi,j |= c then pi,j |=(c!) f.
>////
>
>Notice that with Definition 5, (**) does indeed hold. (*) and (**)
>provide
>
>PROPOSITION 3: "f until g" is equivalent to "(f until! g) || (always f)".
>////
>
>PROPOSITION 4:
>a) pi,i |=(c!) !(!f until! !g) iff pi,i |=(c!) g until_ f.
>b) pi,i |=(c) !(!f until_ !g) iff pi,i |=(c) g until! f.
>c) pi,i |=(c!) !(!f until!_ !g) iff pi,i |=(c!) g until f.
>d) pi,i |=(c) !(!f until !g) iff pi,i |=(c) g until!_ f.
>PROOF:
>a) pi,i |=(c!) !(!f until! !g)
> iff not(pi,i |=(c) !f until! !g)
> iff not
> there exists k >= i such that both
> i) pi,k |= c and pi,k |=(c) !g
> and
> ii) for all j such that i <= j < k, if pi,j |= c then pi,j |=(c)
>!f
> iff for all k >= i either
> i) if pi,k |= c then not(pi,k |=(c) !g)
> or
> ii) there exists j such that i <= j < k and pi,j |= c and
> not(pi,j |=(c) !f)
> iff for all k >= i either
> i) if pi,k |= c then pi,k |=(c!) g
> or
> ii) there exists j such that i <= j < k and pi,j |= c and pi,j
>|=(c!) f
> Now repeat the argument of Claim 2, using "|=(c!)" in place of "|=(c)"
>to
> see that this last condition holds
> iff either
> a) there exists k >= i such that both
> i) pi,k |= c and pi,k |=(c!) f && g
> and
> ii) for all j such that i <= j < k, if pi,j |= c then pi,j
>|=(c!) g
> or
> b) for all j >= i, if pi,j |= c then pi,j |=(c!) g
> iff pi,i |=(c!) g until_ f.
>b) Follows from a) by negations.
>c) Mimic the proof of Proposition 1 c) with "|=(c!)" in place of "|=(c)".
>d) Follows from c) by negations.
>////
>
>Propositions 1 and 4 provide the following
>
>PROPOSITION 5 (Duality):
>a) "!(!f until! !g)" is equivalent to "g until_ f".
>b) "!(!f until_ !g)" is equivalent to "g until! f".
>c) "!(!f until!_ !g)" is equivalent to "g until f".
>d) "!(!f until !g)" is equivalent to "g until!_ f".
>////
_________________________________________________________________
Unlimited Internet access -- and 2 months free! Try MSN.
http://resourcecenter.msn.com/access/plans/2monthsfree.asp
This archive was generated by hypermail 2b28 : Thu Oct 24 2002 - 11:49:06 PDT