Subject: [sv-ac] flaw in Sugar clocked until semantics
From: John Havlicek (john.havlicek@motorola.com)
Date: Tue Oct 22 2002 - 21:49:53 PDT
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".
////
This archive was generated by hypermail 2b28 : Tue Oct 22 2002 - 21:51:11 PDT