Deprecated: The each() function is deprecated. This message will be suppressed on further calls in /home/zhenxiangba/zhenxiangba.com/public_html/phproxy-improved-master/index.php on line 456
A VERSION OF SUGAR WITH SERES AS FORMULAS ========================================= FORMULAS -------- b boolean expression not f negation f1 and f2 conjunction f1 ; f2 concatenation (ITL's chop) f1 : f2 fusion f[*] repetition X! f strong next [f1 U f2] until {f1}(f2) suffix implication {f1} |-> {f2}! strong sufffix implication {f1} |-> {f2} weak sufffix implication f abort b abort f@c! strong clocking N.B. In what follows I use "and", "not", "or" and "-->" for extended Sugar (i.e. object-language) connectives and "And", "Not", "Or" and "==>" for logical (i.e. meta-language) connectives. UNCLOCKED SEMANTICS ------------------- w |= b <==> |w|>0 And w_0 |= b w |= not f <==> Not(w |= f) w |= f1 and f2 <==> w |= f1 And w |= f2 w |= f1 ; f2 <==> Exists w1 w2: w = w1.w2 And w1 |= f1 And w2 |= f2 w |= f1 : f2 <==> Exists w1 w2 s: w = w1.s.w2 And w1.s |= f1 And s.w2 |= f2 w |= f[*] <==> Exists w1 ... wn: All i: 1 <= i <= n ==> wi |= f w |= X! f <==> |w|>1 And w^1 |= f w |= [f1 U f2] <==> Exists k in [0..|w|): w^k |= f2 And All j in (0..k]: w^j |= f1 w |= {f1}(f2) <==> All j in [0..|w|): w^{0,j} |= f1 ==> w^j |= f2 w |= {f1} |-> {f2}! <==> All j in [0..|w|): w^{0,j} |= f1 ==> Exists k in [j..|w|): w^{j,k} |= f2 w |= {f1} |-> {f2} <==> All j in [0..|w|): w^{0,j} |= f1 ==> ((Exists k in [j..|w|): w^{j,k} |= f2) Or (All k in [j..|w|): Exists w': w^{j,k}.w' |= f2)) w |= f abort b <==> w |= f Or w |= b Or Exists j in [1..|w|): Exists w': w^j |= b And w^{0,j-1}.w' |= f Note the w' in the rhs of w |= {f1} |-> {f2} is not restricted to being finite. CLOCKED SEMANTICS ----------------- Define = c and not(X! T) the "and not(X! T)" is to force the path to have length 1, so that the semantics of formula is like the semantics of SERE c, namely w |= <==> |w|=1 and w_0 |= c then define w |=c b <==> |w|>0 And w_0 |= b w |=c not f <==> Not(w |=c f) w |=c f1 and f2 <==> w |=c f1 And w |=c f2 w |=c f1 ; f2 <==> Exists w1 w2: w = w1.w2 And w1 |=c f1 And w2 |=c f2 w |=c f1 : f2 <==> Exists w1 w2 s: w = w1.s.w2 And w1.s |=c f1 And s.w2 |=c f2 w |=c f[*] <==> Exists w1 ... wn: All i: 1 <= i <= n ==> wi |=c f w |=c X! f <==> Exists i in [1..|w|): w^{1,i} |=T {[*]; } And w^i |=c f w |=c [f1 U f2] <==> Exists k in [0..|w|): w^k |=T c And w^k |=c f2 And All j in (0..k]: w^j |=T c ==> w^j |=c f1 w |=c {f1}(f2) <==> All i in [0..|w|): w^{0,i} |=c f1 ==> Exists j in [i..|w|): w^{i,j} |=T {[*]; } And w^j |=c f2 w |=c {f1} |-> {f2}! <==> All i in [0..|w|): w^{0,i} |=c f1 ==> Exists j in [i..|w|): w^{i,j} |=c f2 w |=c {f1} |-> {f2} <==> All i in [0..|w|): w^{0,i} |=c f1 ==> ((Exists j in [i..|w|): w^{i,j} |=c f2) Or (All j in [i..|w|): Exists w': w^{i,j}.w' |=c f2)) w |=c f abort b <==> w |=c f Or w |=c b Or Exists i in [1..|w|): Exists w': w^i |=T (c and b) And w^j |= b And w^{0,i-1}.w' |=c f w |=c f@c1! <==> Exists i in [0..|w|): w^{0,i} |=T {[*]; } And w^i |=c1 f REWRITES -------- T^c(b) = b T^c(not f) = not(T^c(f)) T^c(f1 and f2) = T^c(f1) and T^c(f2) T^c(f1 ; f2) = T^c(f1) ; T^c(f2) T^c(f1 : f2) = T^c(f1) : T^c(f2) T^c(f[*]) = (T^c(f))[*] T^c(X! f) = X![not c U (c and T^c(f)] T^c([f1 U f2]) = [(c --> T^c(f1)) U (c and T^c(f2))] T^c({f1}(f2)) = {T^c(f1)}([not c U (c and T^c(f2)]) T^c({f1} |-> {f2}!) = {T^c(f1)} |-> {T^c(f2)}! T^c({f1} |-> {f2}) = {T^c(f1)} |-> {T^c(f2)} T^c(f abort b) = b Or (T^c(f) abort (c and b)) T^c(f@c1!) = [not c1 U (c1 and T^c1(f)] PROPERTIES ---------- The following properties have been checked (I think!): 1. Clocking with T is equivalent to unclocked semantics ClockFree(f) ==> (w |=T f <==> w |= f) where ClockFree(f) means f contains no clocking constructs. 2. Rewrites match direct semantics: w |=c f <==> w |= T^c(f) 3. Sugar SEREs faithfully encoded as formulas: ClockFree(r) ==> (w |= r <==> w |= S2F(f)) where the translation from SEREs to formulas is: S2F(b) = b and not(X! T) S2F(r1 ; r2 ) = S2F(r1) ; S2F(r2) S2F(r1 : r2 ) = S2F(r1) : S2F(r2) S2F(r1 | r2 ) = S2F(r1) Or S2F(r2) S2F(r1 & r2 ) = S2F(r1) And S2F(r2) S2F(r[*]) = (S2F(r))[*] 4. Sugar formulas faithfully encoded in "SERE-free" formulas ClockFree(f) ==> (w |= f <==> w |= F2F(f)) where the translation from Sugar formulas to SERE-free formulas is: F2F(b) = b F2F(not f) = not(F2F(f)) F2F(f1 and f2) = F2F(f1) and F2F(f2) F2F(X! f) = X!(F2F(f)) F2F([f1 U f2]) = [F2F(f1) U F2F(f2)] F2F({r}(f)) = {S2F(r)}(F2F(f)) F2F({r1} |-> {r2}!) = {S2F(r1)} |-> {S2F(r2)}! F2F({r1} |-> {r2}) = {S2F(r1)} |-> {S2F(r2)} F2F(f abort b) = (F2F(f)) abort b F2F(f@c1) = (F2F(f))@c1